再论归约性质
The Reduction Property Revisited
摘要:
在本文中,我们将研究一个重要的,但相当技术性的结果,这是所谓的约化性质。这个结果告诉我们两个数论之间有多少算术守恒。这两种理论本质上都是关于反思的基本原则:如果一个句子是可证明的,那么它就是真的。第一个理论是公理化使用反射公理和第二个理论使用反射规则。约化性质告诉我们,第一个理论扩展了第二个理论,但对于一大类公式是保守的。我们在不同的方向上扩展了归约性质。最值得注意的是,我们将看到各种不同类型的反射公理和规则是如何相互关联的。此外,我们扩展的减少属性超限反射原则。由于还没有令人满意的(超)算术解释,因此这种推广应该在纯粹的代数环境中进行。对于专家:经典归约性质的一个推论描述了$Π^0_{n+1}$推论的特征,并告诉我们,对于任何具有正确复杂度的理论$U$和$T$,我们有\[ U + {\sf Con}_{n+1}(T) \equiv_{Π^0_{n+1}} U \cup \{ {\sf Con}_n^k(T)\mid k<ω\}. \]。如果我们对具有$j{\leq}n$的$Π^0_j$公式感兴趣,我们将计算哪些理论可以放在右边。我们回答这个问题也在一个纯粹的代数设置$Π^0_j$ -保守将适当定义。代数转向允许对超限一致性概念的推广。
英文摘要:
In this paper we will study an important but rather technical result which is called The Reduction Property. The result tells us how much arithmetical conservation there is between two arithmetical theories. Both theories essentially speak about the fundamental principle of reflection: if a sentence is provable then it is true. The first theory is axiomatized using reflection axioms and the second theory uses reflection rules. The Reduction Property tells us that the first theory extends the second but in a conservative way for a large class of formulae. We extend the Reduction Property in various directions. Most notably, we shall see how various different kind of reflection axioms and rules can be related to each other. Further, we extend the Reduction Property to transfinite reflection principles. Since there is no satisfactory (hyper) arithmetical interpretation around yet, this generalization shall hence be performed in a purely algebraic setting. For the experts: a consequence of the classical Reduction Property characterizes the $Π^0_{n+1}$ consequences and tells us that for any theories $U$ and $T$ of the right complexity we have \[ U + {\sf Con}_{n+1}(T) \equiv_{Π^0_{n+1}} U \cup \{ {\sf Con}_n^k(T)\mid k<ω\}. \] We will compute which theories can be put at the right-hand side if we are interested in $Π^0_j$ formulas with $j{\leq}n$. We answer the question also in a purely algebraic setting where $Π^0_j$-conservation will be suitably defined. The algebraic turn allows for generalizations to transfinite consistency notions.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。