arXiv 2112.080052021-12-15math.LO

迭代$Π^1_1$ -理解的良序原则

Well ordering principles for iterated $Π^1_1$-comprehension

Anton Freund, Michael Rathjen

摘要：

我们介绍序数崩溃的原则，灵感来自证明论，但有一套理论的味道。这些原则被证明是等价的迭代$Π^1_1$ -理解和存在的容许集，弱基理论。我们的工作扩展了以前的结果的非迭代的情况下，这已经在Montalbán的“开放问题在反向数学”（公牛。Log. 17（3）2011）。这个先前的结果已经被应用于组合和集合论原理的逆向数学。本文件是一个重要的贡献，连接这些领域的一般方法。

英文摘要：

We introduce ordinal collapsing principles that are inspired by proof theory but have a set theoretic flavor. These principles are shown to be equivalent to iterated $Π^1_1$-comprehension and the existence of admissible sets, over weak base theories. Our work extends a previous result on the non-iterated case, which had been conjectured in Montalbán's "Open questions in reverse mathematics" (Bull. Symb. Log. 17(3)2011). This previous result has already been applied to the reverse mathematics of combinatorial and set theoretic principles. The present paper is a significant contribution to a general approach that connects these fields.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

$Π^1_1$ -作为良序原则的理解

$Π^1_1$-Comprehension as a Well-Ordering Principle

扩张器是保持良好基础的线性阶的特别均匀的变换$X\mapsto T_X$。如果存在几乎保序的塌缩函数$\vartheta:T_X\rightarrow X$（精确定义如下），则称$X$是$T$的Bachmann-Howard不动点.在本文中，我们证明了$Π^1_1$ -理解等价于断言，每个扩张有一个良好的Bachmann-Howard不动点。这证明了M. Rathjen和A.蒙塔尔班

2019-08-19math.LO

Fraïssé猜想、部分非直谓性与良序原理（第一部分）

Fraïssé's conjecture, partial impredicativity and well-ordering principles, part I

本研究在反推数学框架下，于Suzuki与Yokoyama拓展的部分非直谓性层级中，找到Fraïssé猜想的更优上界，证明伪Π¹₁-概括原理蕴含该猜想，还提出Δ⁰₂-Ramsey定理余有穷版本并关联相关反射原理，为后续给出组合上界奠基。

2024-06-19math.LO

证明论与逆向数学中的良序原理

Well-Ordering Principles in Proof Theory and Reverse Mathematics

关于逆数学中的一些常见理论与某些良序原理的等价性的几个定理已经用递归理论和组合方法得到了证明（Friedman，Marcone，Montalban et al.）并通过证明理论技术（Afshari，Freund，Girard，Rathjen，Thomson，Valencia Vizcano，Weiermann等人）取得了深远的成果，在后一种情况下，采用演绎搜索树和无穷逻辑中的序界割消定理。在第一级，良序原则的形式是（*）"如果X是良序的，那么f（X）是良序的"，其中f是从序数到序数的标准证明论函数（这样的f总是扩张子）。本文的一个目的是提出一个支持这些结果的一般方法，使人们能够从（*）构建特定理论的omega模型，甚至从（*）的类型2版本构建beta模型。由于（*）具有复杂性Pi-1 - 2，这样的原理不能在Pi-1 - 1-理解的水平上表征更强的理解。这需要一个高阶版本的（*），它采用了序数表示系统的思想，并在非断言证明理论中使用了折叠函数。最简单的是Bachmann结构。将后一种构造与任何扩张器f相对化，并断言这总是产生良序，结果等价于Pi-1 - 1-comprehension。这个结果已经被证实，大约10年前就有了一个证明策略，但证明只是在最近几年才完成的。

2020-10-23math.LO

反射代数与迭代真值理论的守恒性结果

Reflection algebras and conservation results for theories of iterated truth

我们考虑扩展的语言皮亚诺算术transmittiterated真理定义满足一致塔斯基双条件。如果没有进一步的公理，这些理论被认为是原始算术系统的保守扩展。然而，更强的系统可以通过在它们之上添加归纳公理或反射公理来获得。这类理论可以解释一些著名的二阶算术的谓词可约片段，如迭代算术理解。我们得到尖锐的结果，这些系统的证明理论的强度，使用可证明性逻辑的方法。反射原理自然地定义了作用于我们的迭代真值基本理论的可公理化扩展的半格上的一元算子。这个代数的顶元素所产生的子结构为被研究的理论类提供了一个规范的序数记号系统。使用这些符号，我们获得了对应于超算术层次的不同逻辑复杂性水平的迭代反射原理的保守性关系，即，Schmerl公式的类似物。这些关系，反过来，提供了我们的系统和一些相关的谓词可还原理论的证明理论分析。特别是，我们统一计算的序数特征的标准措施，他们的证明理论的强度，如可证明的良序，类可证明递归函数，和$Π_1^0$ -序数。

2019-10-30math.LO

将$ω$ -模型反射约化为迭代句法反射

Reducing $ω$-model reflection to iterated syntactic reflection

在数理逻辑中，有两种看似不同的原则，称为“反射原则”。语义反射原理断言，如果一个公式在整个宇宙中成立，那么它在一个集合大小的模型中成立。句法反射原则断言，来自某个复杂性类的每个可证明句子都是真的。本文在二阶算术的背景下研究这两种反射原理之间的联系。我们证明，对于一个大的理论，$ω$模型反射是等价的索赔，均匀$Π^1_1$反射沿可数良序的任意迭代是$Π^1_1$ -声音。这个结果产生了强度在$\mathsf{ACA}_0$和$\mathsf{ATR}$之间的理论的一致序分析。我们分析的主要技术新颖性是引入了理论$T$的证明论扩张器的概念，它是可数序数上的算子，将$\prec$的序类型映射到$T+\mathsf{WO}(\prec)$的证明论序数。我们得到精确的结果证明理论扩张器的增长作为可证明的$ω$模型反射的函数。这种方法使我们能够同时获得不仅$Π^0_1$，$Π^0_2$，和$Π^1_1$序数，但也逆数学定理的良序原则。

2022-06-14math.LO

高阶Bachmann-Howard原理

A Higher Bachmann-Howard Principle

我们提出了一个更高的良序原则，这是等价的（超过辛普森集理论版本的$\text{ATR}_0$）的存在性传递模型的Kripke-Platek集合论，从而$Π^1_1$ -理解。这是Montalbán和Rathjen的一个猜想的部分解：部分解的意义在于我们的良序原则比猜想中所要求的建设性要小。

2018-09-19math.LO

更多相关论文收起更多论文

类对策的开放决定性

Open determinacy for class games

类博弈的开放决定性原理-具有长度为$ω$的完全信息的两人博弈，其中移动是从可能的适当类中选择的，例如序数上的博弈-在Zermelo-Fraenkel集合论ZFC或Gödel-Bernays集合论GBC中是不可证明的，如果这些理论是一致的，因为可以证明在ZFC中有一个可定义的开真类博弈，没有可定义的获胜策略。事实上，类博弈的开放决定性原则，甚至仅仅是封闭决定性原则，就意味着Con（ZFC）和迭代实例Con（Con（ZFC））以及更多，因为它意味着一阶真理存在一个满足类，而对于迭代的关于真理的真理，相对于任何类参数，确实存在一个真理谓词的超限塔。根据塔斯基的真的递归定义，这也许可以用一个更一般的事实来解释，即在GBC上的闭根决定性原理完全等价于在良基类关系上的初等超限递归ETR原理。同时，类对策的开放决定性原理在Kelley-Morse集合论KM的一个适当片段GBC+ $Π^1_1$ -综合理论中是可证明的.

2016-07-07math.LO