弱算术子系统的层次

Arithmetic, Infinite Trees, and Second-order Subsystems: Notes and Observations

Work in progress concerning alternative formalizations of arithmetic.

构造性多型理论与二阶算术子系统的比较

Comparison of constructive multi-typed theory with subsystems of second order arithmetic

本文描述了构造性数学的一个公理化理论BT。BT有一个谓词性的概括公理，适用于可数个集合类型和通常的组合运算。BT具有直觉主义逻辑，与经典逻辑一致，具有与形式丘奇命题一致、存在性与析取性等构造性特征。BT可以与所谓的算术真值理论PATr和包含无穷多种自然数集合的二阶算术SA相互解释。我们比较BT与一些标准的二阶算法，并调查证明理论的BT，PATr和SA片段的强度。

论泛谓词的层次

On hierarchies of universal predicates

我们调查了一个层次的算术结构所获得的超限除了一个典型的通用谓词，其中的典型通用谓词M被定义为M的最小通用谓词的可定义性。我们确定了层次的上界，并给出了层次中可定义集合的一个刻画。

二阶算术子系统中的Lebesgue数与Atsuji空间

Lebesgue numbers and Atsuji spaces in subsystems of second order arithmetic

在二阶算术子系统的框架下研究完备可分度量空间的性质。特别是我们认为勒贝格和Atsuji空间。前者是使得每个开覆盖U都有一个勒贝格数，即一个正数q，使得对于空间的每个点x，都存在一个U的元素，它包含中心为x、半径为q的球;后者是使得每个连续函数到另一个完全可分度量空间是一致连续的。主要结果是：“每个紧空间是Lebesgue空间”等价于WKL_0，“每个完备Lebesgue空间是紧空间”和“每个完备Atsuji空间是紧空间”等价于ACA_0，“每个Lebesgue空间是Atsuji空间”在RCA_0中可证;“每个Atsuji空间都是Lebesgue”这一命题在ACA_0中是可证明的，但我们不知道它是否等价于ACA_0。证明了“到闭集的距离是一个连续函数“等价于Pi^1_1-CA_0;证明了“存在一个完备的可分度量空间，它是完备的，Heine-Borel紧的”等价于Pi^1_1-CA_0。Lebesgue，Atsuji）”都等价于WKL_0。

高阶算术中确定性的界限

The Limits of Determinacy in Higher-Order Arithmetic

本文在超算术层级中逐级界定有限差分的确定性强度，推广Montalbán-Shore定理至所有Borel层级，并证明反射原理与量化确定性公理等价，解答了Pacheco和Yokoyama的两个问题。

Solovay's Relative Consistency Proof for FIM and BI

In 2002 Robert Solovay proved that a subsystem BI of classical second order arithmetic, with bar induction and arithmetical countable choice, can be negatively interpreted in the neutral subsystem BSK of Kleene's intuitionistic analysis FIM using Markov's Principle MP. Combining this result with Kleene's formalized recursive realizability, he established (in primitive recursive arithmetic PRA) that FIM + MP and BI have the same consistency strength. This historical note includes Solovay's original proof, with his permission, and the additional observation that Markov's Principle can be weakene…