算术、无限树与二阶子系统：注释与观察
Arithmetic, Infinite Trees, and Second-order Subsystems: Notes and Observations
摘要：
正在进行的关于算术的其他形式化的工作。
英文摘要：
Work in progress concerning alternative formalizations of arithmetic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
相关论文
弱算术子系统的层次
Hierarchies of Subsystems of Weak Arithmetic
我们完整地刻画了弱算术的各个子系统的逻辑层次，即：ZR，ZR + N，ZR + GCD，ZR + Bez，OI + N，OI + GCD，OI + Bez.
math.LO
构造性多型理论与二阶算术子系统的比较
Comparison of constructive multi-typed theory with subsystems of second order arithmetic
本文描述了构造性数学的一个公理化理论BT。BT有一个谓词性的概括公理，适用于可数个集合类型和通常的组合运算。BT具有直觉主义逻辑，与经典逻辑一致，具有与形式丘奇命题一致、存在性与析取性等构造性特征。BT可以与所谓的算术真值理论PATr和包含无穷多种自然数集合的二阶算术SA相互解释。我们比较BT与一些标准的二阶算法，并调查证明理论的BT，PATr和SA片段的强度。
math.LO
二阶算术子系统中的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。
math.LO
休谟原理、第五基本定律与皮亚诺算术的比较
Comparing Hume's Principle, Basic Law V and Peano Arithmetic
本文提出了休谟原理和基本定律V的模型的新结构与有限的理解量。在这些结构中使用的技术是从超算术理论和领域的模型论中提取的，并且在二阶皮亚诺算术的各个子系统中形式化这些技术允许人们对这些理论的可解释性强度设置上限和下界，从而将这些理论与二阶算术的规范子系统进行比较。本文的主要结果是：（i）基本定律V的超算术部分有一个相容的推广，它解释了二阶皮亚诺算术的超算术部分;（ii）休谟原理的超算术部分不能解释二阶皮亚诺算术的超算术部分，因此在这个特殊意义上不存在弗雷格定理的谓词版本。
math.LO
关于$\mathbb{Z}$是弱算术系统的非标准模型的直和项的注记
A note on $\mathbb{Z}$ as a direct summand of nonstandard models of weak systems of arithmetic
有正常开归纳的非标准模型（$NOI$），其中$\mathbb{Z}$是它们的加性群的直接和项。我们表明，这是不可能的非标准模型的$IE_2$。
math.LO
关于有限型算术的一个注记
A note on arithmetic in finite types
我们提出了一个版本的算术在所有有限型，它允许一个定义的平等在更高的类型，所有的同余是可推导的，其中的合理性的辩证法解释是证明内部的系统本身，这允许内涵和外延的模型和演绎定理。
math.LO
更多相关论文收起更多论文
算术片段与循环证明
Fragments of arithmetic and cyclic proofs
本文提出一种更简单且适合证明分析与自动化归纳证明搜索的皮亚诺算术循环证明系统，并展示传统归纳受限子系统可表示为其片段。
math.LO
紧可数次可数空间的逆数学
Reverse mathematics of compact countable second-countable spaces
我们研究可数次可数拓扑空间理论的逆数学，重点是紧性。我们表明，这种空间的一般理论的工作原理，如预期的子系统$\mathsf{ACA}_0$的二阶算术，但我们发现，许多意想不到的病理可能发生在较弱的子系统。特别地，我们证明了$\mathsf{RCA}_0$不能证明每个紧的离散可数的第二可数空间是有限的，并且$\mathsf{RCA}_0$不能证明两个紧的可列的第二可数空间的乘积是紧的.为了规避这些病态，我们引入了加强形式的紧凑性，离散性和Hausdorff更好地表现在子系统的二阶算术弱于$\mathsf{ACA}_0$。
math.LO
高阶算术中确定性的界限
The Limits of Determinacy in Higher-Order Arithmetic
本文在超算术层级中逐级界定有限差分的确定性强度，推广Montalbán-Shore定理至所有Borel层级，并证明反射原理与量化确定性公理等价，解答了Pacheco和Yokoyama的两个问题。
math.LO
关于二阶算术中一致反射分片的一个注记
A note on fragments of uniform reflection in second order arithmetic
我们认为片段的一致反映的公式在层次分析理论的二阶算术。主要结果是：对于任何二阶算术理论$T_0$，扩展了${\sf RCA}_0$并可由$Π^1_{k+2}$语句公理化;对于任何$n\geq k+1$，\[ T_0+ \mathrm{RFN}_{\varPi^1_{n+2}}(T) \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}(\varepsilon_0), \] \[ T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}}(T) \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-}, \]，其中$T$是用全归纳扩充的$T_0$，而$\mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-}$表示无参数$\varPi^1_n$公式的超限归纳直到$\varepsilon_0$的模式.
math.LO
关于组合真值谓词的有界归纳的注记
Notes on bounded induction for the compositional truth predicate
我们证明了算术语言的可拓组合真值谓词理论在真值谓词的$Δ_0$ -归纳方案和完全算术归纳方案下对Peano算术是不保守的。此外，我们表明，一个稍微修改的理论的真理实际上证明了全球反射原则的基础理论。
math.LO
C-系统的子系统与正则子系统
Subsystems and regular quotients of C-systems
C系统是由J. Cartmell以“上下文范畴”的名义引入的。本文研究了C-系统的子对象和从属对象。在子对象的情况下，我们考虑所有的子对象，而在从属对象的情况下，只有{ \em正则}从属对象，特别是具有相应的投影态射在对象和态射上都是满射的性质。这是一个简短的文件的基础上的材料的“说明类型系统”由同一作者。这个版本基本上是相同的版本出版的当代数学n.658。
math.LO
关于极弱一元二元算术系统的注记
Notes on Systems of Very Weak Unary Dyadic Arithmetic
University of Southern California（南加州大学）
本文引入几种极弱的一阶一元二元字符串串联理论，证明它们与已知的极弱理论（如二叉树理论WT、二元串联理论WD和Robinson算术R）相互可解释，从而确立其本质不可判定性。
math.LO
Skolem算术中的可定义集
Definable sets in Skolem arithmetic
本文研究Skolem算术中的可定义集问题，提出全新的可定义集刻画方法，采用不同组合工具证明该理论的可判定性，旨在给出比现有证明更简洁的可判定性证明。
math.LO
FIM和BI的Solovay相对兼容性证明
Solovay's Relative Consistency Proof for FIM and BI
在2002年，Robert Solovay证明了经典二阶算术的子系统BI，具有条归纳和算术可数选择，可以在Kleene直觉分析的中性子系统BSK中使用马尔可夫原理MP进行否定解释。结合这个结果与Kleene的形式化递归可实现性，他（在原始的递归算术PRA中）建立了B1 + MP和BI具有相同的一致性强度。这个历史笔记包括索洛维的原始证明，在他的许可下，以及额外的观察，即马尔可夫原理可以被削弱为与布劳威尔创造的主题反例一致的双重否定移位公理。
math.HOmath.LO
关于非经典非标准算术的一点注记
A note on non-classical Nonstandard Arithmetic
近年来，提出了一系列限制于有限型语言（即非标准算术）的非标准分析的形式系统。我们挑出一个特殊的系统由Dinis-Gaspar，这是分类的作者作为一部分的直觉非标准算术。他们的系统确实与非标准分析的转移公理不一致，后者的公理本质上是经典的，因为它意味着（高阶）理解。在本文中，我们回答了以下问题：（Q1）在逆向数学的精神，什么是转移的最小片段是不符合Dinis-Gaspar系统？(Q2)还有哪些公理与Dinis-Gaspar系统不一致？也许令人惊讶的是，第二个问题的答案表明，Dinis-Gaspar系统与一些（非经典）连续性定理不一致，在我们看来，这些连续性定理可以归类为直觉主义。最后，我们表明，Dinis-Gaspar系统涉及到一个标准的部分地图，这表明该系统还推动了什么仍然算作“非标准分析”或“内部集合论”的边界。
math.LO
关于$Π^0_{n+1}$ - LEM、$Σ^0_{n+1}$ - LEM和$Σ^0_{n+1}$ - DNE的说明
Note on $Π^0_{n+1}$-LEM, $Σ^0_{n+1}$-LEM and $Σ^0_{n+1}$-DNE
我们表明，Akama，Berardi，Hayashi和Kohlenbach的结果，对直觉算术HA的某些算术原理的相对独立性，也保持在Kleene和Vesley的直觉分析，它扩展了HA的系统，与经典算术一致，但不与经典分析。还考虑了这些原则的通用闭包的双重否定，并表明HA和FIM的表现有所不同。各种基本问题仍然悬而未决。
math.LO
Howard-Bachmann-谱系的序理论刻画
An order-theoretic characterization of the Howard-Bachmann-hierarchy
在这篇文章中，我们提供了一个内在的特征，著名的霍华德-Bachmann序数的一个自然的良好的偏序，通过证明这个序数可以实现为一个极大序模型的一类广义树关于同胚嵌入关系。我们利用我们的计算得出了一些关于二阶算术的相应子系统的结论。所有这些子系统都处理光-面$Π^1_1$ -理解的版本
math.LO
二阶算术中的框架可定义性
Frame definability in second-order arithmetic
Mathematical Institute, Tohoku University（东北大学数学研究所）
该文研究模态逻辑框架可定义性的反数学强度，证明估值扩张引理等相关原则与二阶算术子系统$\text{ACA}^{+}_0}$等价，还考察了CTL、LTL对应原则的强度。
math.LO
关于窄系统的一个注记
A Note on Narrow Systems
本文研究树与窄系统的关系，证明高度为κ的树若有窄子系统则含良剪子树，并推广至双基数树。
math.LO
关于直觉算术上反射的迭代
Iterating reflection over intuitionistic arithmetic
University of Leeds（利兹大学）
本文研究了直觉算术上反射的迭代，提出了统一反射的新证明方法，并扩展了Feferman完备性定理的应用。
math.LO
关于一阶算术证明论的两点注记
Two remarks on proof theory of first-order arithmetic
在这个说明中，让我们给两个意见证明理论PA。首先，在PA中引入可导关系，使可证$Σ_{1}$ -公式的有界证明集成立。第二，Paris-Harrington的证明，他们的独立性的结果是重新制定显示的“一致性”证明PA的组合原则的基础上。
math.LO
类理论与二阶算术中的非紧致性
Non-tightness in class theory and second-order arithmetic
本文证明限制Z2和KM的概括公理模式会产生非紧致理论，GB和ACA0及其添加Sigma^1_k-概括的扩张均承认不同的可双解释扩张，表明紧致性以最小方式刻画Z2和KM。
math.LO
原始递归算术等式版本的循环证明
Cyclic proofs in the equational version of Primitive recursive arithmetic
针对原始递归算术的等式版本提出循环证明系统，并利用结构证明论工具证明其等价性，无需自动机方法。
math.LO
逆向数学与超图的着色
Reverse mathematics and colorings of hypergraphs
工作在子系统的二阶算术，我们制定了超图的几种表示。然后证明了各种顶点着色定理与${\sf WKL}_0$，${\sf ACA}_0$和$Π^1_ 1$ - ${\sf CA}_0$的等价性.
math.LO
关于标准系统和超滤子的注记
A note on standard systems and ultrafilters
设$(M,\scott X) \models \ACA$使得$P_\scott X$，即$\scott X$中所有无界集的集合，允许一个可定义的完全超滤子，并设$T$是在$\scott X$中编码的一阶算术的理论扩展，使得$M$认为$T$是相容的。证明了$M$存在一个末端扩展$N \models T$，使得$M$在$N$中的子集与在$\scott X$中的子集完全相同.作为特殊情况，我们得到了任何具有可定义的超滤子的Scott集编码相容理论$T$扩展一阶算术是$T$递归饱和模型的标准系统.
math.LO
