Separating Bounded Arithmetics by Herbrand Consistency
研究了$Π_1-$分离有界算术族的问题。它表明，Herbrand一致性的概念，在其充分的一般性，不能$Π_1-$分离的理论${\rm IΔ_0+\bigwedge_jΩ_j}$从${\rm IΔ_0}$ ;虽然它可以$Π_1-$分离${\rm IΔ_0+Exp}$从${\rm IΔ_0}$。这推广了L. A. Kokiodziejczyk（2006），通过证明在${\rm IΔ_0+\bigwedge_jΩ_j}$理论中${\rm IΔ_0}$的Herbrand一致性的不可证明性。
2016-12-10 cs.LO math.LO
Short Proofs for Slow Consistency
令$\operatorname{Con}(\mathbf T)\!\restriction\!x$表示有限一致性语句“在具有$\leq x$符号的$\mathbf T$中没有矛盾证明”。Pudlák已经证明，对于一大类自然理论$\mathbf T$，理论$\mathbf T$中的$\operatorname{Con}(\mathbf T)\!\restriction\!n$的最短证明的长度是由$n$中的多项式限定的。同时，他承认$\mathbf T$没有有限一致性语句$\operatorname{Con}(\mathbf T+\operatorname{Con}(\mathbf T))\!\restriction\!n$的多项式证明。相反，我们证明了Peano算法（$\mathbf{PA}$）具有$\operatorname{Con}(\mathbf{PA}+\operatorname{Con}^*(\mathbf{PA}))\!\restriction\!n$的多项式证明，其中$\operatorname{Con}^*(\mathbf{PA})$是Peano算法的慢一致性声明，由S. D. Friedman，Rathjen and Weiermann.我们还得到了一个新的证明结果，通常的一致性声明$\operatorname{Con}(\mathbf{PA})$是等价的$\var…
2020-03-06 math.LO
Dense ideals and cardinal arithmetic
从大基数，我们证明了正常的，罚款，$κ$ -完全$λ$ -稠密理想$\mathcal{P}_κ(λ)$的继任者$κ$的一致性。我们探讨了稠密的理想，基数算术和广场之间的相互作用，回答了一些开放的问题福尔曼。
2023-03-24 math.LO
Uniformity of Consistency in Arithmetic and Gödel's Second Incompleteness Theorem: Ein Märchen
University of Vienna（维也纳大学）
本文探讨了足够强的可数理论中一致性的统一验证方法，通过选择器证明实现计算统一性，但无法内部化为哥德尔第二不完全性定理的统一一致性句子。
2026-07-14 math.LO
Consistency proof of a fragment of PV with substitution in bounded arithmetic
本文提出的证据表明，巴斯的$S^2_2$可以证明库克和厄克特的$\mathrm{PV}$的诱导已被删除，但取代已被保留的片段的一致性。这一结果改进了Beckmann的结果，证明了在有界算术$S^1_2$中这样一个系统的无替换相容性.我们的证明依赖于$\mathrm{PV}$的“计算”的概念。在我们的工作中，我们首先证明，在所考虑的系统中，如果证明了一个方程并且计算了它的左侧或右侧，那么分别对其右侧或左侧进行相应的计算。通过仔细计算计算的大小的界限，这个定理的证明在一个有界的算术，从系统的相容性很容易证明。这一结果显然暗示了有界算术的分离，因为巴斯和贾贾托维奇指出，在巴斯的$S^1_2$中，如果没有归纳法，但有替换，就不可能证明$\mathrm{PV}$的一个片段的一致性。然而，他们的证明实际上表明，不可能证明系统的一致性，这是通过向我们这样的系统添加命题逻辑和其他公理来获得的。另一方面，我们所考虑的系统是严格等式的，这是我们的证明所依赖的一个性质。
2018-12-24 cs.LO math.LO
Iterating reflection over intuitionistic arithmetic
University of Leeds（利兹大学）
本文研究了直觉算术上反射的迭代，提出了统一反射的新证明方法，并扩展了Feferman完备性定理的应用。
2025-10-22 math.LO
Two remarks on proof theory of first-order arithmetic
在这个说明中，让我们给两个意见证明理论PA。首先，在PA中引入可导关系，使可证$Σ_{1}$ -公式的有界证明集成立。第二，Paris-Harrington的证明，他们的独立性的结果是重新制定显示的“一致性”证明PA的组合原则的基础上。
2020-12-31 math.LO
Slow and Ordinary Provability for Peano Arithmetic
Peano算术的慢可证性（$\mathsf{PA}$）是由S. D.弗里德曼，M。Rathjen和A.魏尔曼他们研究了慢一致性声明$\mathrm{Con}_{\mathsf{s}}$，该声明断言矛盾在$\mathsf{PA}$中不是慢可证明的。他们表明，$\mathsf{PA}+\mathrm{Con}_{\mathsf{s}}$的逻辑强度严格介于$\mathsf{PA}$和$\mathsf{PA}$之间，以及它的普通一致性：$\mathsf{PA}\subsetneq \mathsf{PA}+\mathrm{Con}_{\mathsf{s}}\subsetneq \mathsf{PA}+\mathrm{Con}$。本文进一步研究了$\mathsf{PA}$中的慢可证明性及其与普通可证明性之间的关系。我们研究了慢可证性的三种变体。每一个的相关一致性陈述产生一个理论，该理论在逻辑强度方面严格介于$\mathsf{PA}$和$\mathsf{PA}+\mathrm{Con}$之间。我们研究图灵-费弗曼级数的基础上，这些变种的慢证明。我们表明，对于我们的三个概念，图灵-费弗曼级数达到$\mathsf{PA}+\mathrm{Con}$在不同的步骤，即$\varepsilon_0$，$ω$，和$2$。对于三个慢可证明性谓词中的每一个，我们还确定其与普通$\mathsf{PA}$ -可证明…
2016-06-06 math.LO
Solovay's Relative Consistency Proof for FIM and BI
在2002年，Robert Solovay证明了经典二阶算术的子系统BI，具有条归纳和算术可数选择，可以在Kleene直觉分析的中性子系统BSK中使用马尔可夫原理MP进行否定解释。结合这个结果与Kleene的形式化递归可实现性，他（在原始的递归算术PRA中）建立了B1 + MP和BI具有相同的一致性强度。这个历史笔记包括索洛维的原始证明，在他的许可下，以及额外的观察，即马尔可夫原理可以被削弱为与布劳威尔创造的主题反例一致的双重否定移位公理。
2021-01-14 math.HO math.LO
Bounded arithmetic AID for Frege system
本文介绍一个有界算术系统AID（Alogtime Inductive Definitions）. AID的主要特征是允许一种形式的归纳定义，这是从Buss对Frege系统F的命题一致性证明中提取出来的。我们证明了AID证明了F的可靠性，反之，AID中的任何一个B^b_0-定理都会产生布尔语句，而F具有多重证明。进一步，我们定义了AID + Δ b^_0 - CA与P. Clote方程系统ALV的量化理论QALV之间的Δ b_1-忠实解释.因此ALV也证明了F.
1998-09-30 math.LO
Epsilon Substitution for $ID_1$ via Cut-Elimination
$ε$ -替换方法是一种为算术理论提供一致性证明的技术。我们使用这种技术来证明的一致性的impredicative理论$ID_1$使用一个变种的削减消除形式主义介绍了薄荷糖。
2015-09-01 math.LO
Non-Compact Proofs
The Graduate Center, the City University of New York（纽约市立大学研究生中心）
本文研究了非紧致证明在PA一致性证明中的作用，指出哥德尔定理禁止紧致证明，但允许非紧致证明在PA内形式化证明PA的一致性。
2025-12-15 math.LO
Consistency of circuit evaluation, extended resolution and total NP search problems
我们认为集$Γ(n,s,k)$的狭窄条款表示，没有定义的大小$s$电路与$n$的输入是可反驳的$k$步骤中的分辨率R。我们表明，每一个CNF短期内可反驳的扩展R，ER，可以很容易地减少到一个实例的$Γ(0,s,k)$（与$s,k$取决于ER-反驳的大小），特别是，$Γ(0,s,k)$解释为一个相对化的NP搜索问题是完整的所有这些问题证明总有界算术理论$V^1_1$。我们使用的思想，隐式证明定义从$Γ(0,s,k)$一个非相对化NP搜索问题$iΓ$，我们表明，它是完整的所有这些问题证明在有界算术理论$V^1_2$。可在$S^1_2$中定义减少。我们指出如何类似的结果可以证明其他一些命题证明系统和有界算术理论，以及如何建设可以用来定义特定的随机不可满足的公式，我们制定了两个开放的问题。
2015-09-10 cs.LO math.LO
Friedman-reflexivity: interpreters as consistoids
哈维弗里德曼表明，在皮亚诺算术，一致性声明的一个公理化的理论$A$可以表征为最弱的声明$C$皮亚诺算术，使${\sf PA}+C$解释$A$。我们研究的基础理论$U$的属性，任何的公理化$A$，有一个最弱的$C$，使$U+C$解释$A$。我们称这种理论为弗里德曼自反性理论。我们表明，一个非常弱的理论，Peano Corto，是弗里德曼自反的。我们在这里没有得到通常的一致性陈述，而是有界的、无割的或Herbrand一致性陈述。我们证明了弗里德曼自反序列理论的特征定理。我们提供了一个例子，弗里德曼自反序列理论，实质上不同于皮亚诺算术和皮亚诺科尔托的范例情况下。由弗里德曼自反基$U$提供的类似一致性的语句可以用于为通过$A$中的$U$的解释$K$来解释$U$的公理化的$A$定义类似可证明性的概念。我们把基于这种思想的模态逻辑称为\emph{interpreter logics}。这些逻辑满足Löb条件。我们提供了这些逻辑扩展{ \sf S}4、{ \sf K}45和Löb逻辑的条件。我们表明，如果$U$或$A$是顺序的，那么扩展Löb的逻辑的条件得到满足。此外，如果我们的基本理论$U$是连续的，如果，此外，它的解释者可以有效地找到，我们证明Solovay定理。即使类可证性算子不一定能用哥德尔数的谓词表示，这也成立。在文章的最后，我们简要地讨论了如何成功的坐标自由的方法。
2022-01-25 math.LO
Separation of bounded arithmetic using a consistency statement
本文证明了Buss的有界算术族$S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$不完全坍缩.更准确地说，我们证明，对于一定的$D$，$S^1_2 \subsetneq S^{2D+5}_2$持有。此外，我们可以允许$S^1_2, S^2_2, \ldots$的BASIC公理的真量词自由公式的任何有限集。根据Takeuti的论点，这意味着$\mathrm{P} \neq \mathrm{NP}$。设$\mathbf{Ax}$是BASIC公理的一个特定公式。我们证明$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$足够大的$D$，而$S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的系统$\mathrm{PV}^-_1(D)$，系统$\mathrm{PV}^-_1$的一个片段，诱导免费的库克的$\mathrm{PV}$，其中证明只包含公式小于$D$连接词的一阶扩展。$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的证明是通过直接改编的$\mathrm{…
2019-10-30 cs.LO math.LO
Serial Properties, Selector Proofs, and the Provability of Consistency
本文提出选择子证明概念，推广希尔伯特两阶段一致性证明方法，并给出皮亚诺算术 PA 的一致性选择子证明，在 PA 内形式化，从而避开哥德尔第二不完备定理的限制。
2024-03-18 math.LO
Hilbert's "Verunglueckter Beweis," the first epsilon theorem, and consistency proofs
在20世纪20年代，阿克曼和冯诺依曼，在追求希尔伯特的纲领，工作的一致性证明算术系统。一种提出的方法给出这样的证明是希尔伯特的ε替代方法。然而，还有第二种方法，这在20世纪20年代的希尔伯特学派的出版物中没有反映出来，它是希尔伯特第一定理的直接先驱，也是伯奈斯的某种“一般一致性结果”。对这种所谓的“失败证明”的形式的分析进一步阐明了希尔伯特纲领作为一种工具主义事业的解释，其目的是表明，只要一个“真实”命题可以用“理想”手段证明，它也可以用“真实”的有限手段证明。
2003-07-05 math.HO math.LO
The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program
在1917-1920年短暂地与逻辑主义调情之后，大卫·希尔伯特在1920年提出了他自己的数学基础计划，并在整个20世纪20年代与保罗·伯奈斯和威廉·阿克曼等合作者一起发展了它。该项目的两个技术支柱是为更强大和更全面的数学领域开发公理系统，并证明这些系统的一致性。这些领域的早期进展是由希尔伯特（和伯奈斯）在1917年至1923年期间在哥廷根大学的一系列讲座课程中取得的，特别是阿克曼1924年的论文。主要的创新是希尔伯特公理系统所基于的ε演算的发明，以及作为一致性证明基础的ε替换方法的发展。本文追溯了“逻辑与数学同时发展”的发展过程，并分析了阿克曼对原始递归算术和第一个综合数学系统的一致性证明，后者使用了替换法。令人惊讶的是，这些证明使用的超穷归纳法与根岑后来的一致性证明以及非原始递归定义中使用的方法没有什么不同，并且这些方法在当时被认为是有限的。
2001-02-24 math.HO math.LO
Dialectica Logical Principles
哥德尔的Dialectica解释旨在获得海廷算术的相对兼容性证明，与双重否定解释一起使用，以获得皮亚诺算术的相容性。近年来，基于哥德尔辩证法解释的证明理论转换（所谓的证明解释）已被系统地用于从证明中提取新内容，因此解释在数学和计算机科学的几个领域中找到了相关的应用。继我们以前的工作哥德尔纤维化，我们提出了一个（超）学说的辩证法，这完全符合解释的逻辑描述的特点。说明我们在范畴论中导出了对蕴涵联结词的解释的可靠性，正如斯佩克特和特罗尔斯特拉所阐明的那样。这就要求有超越直觉主义逻辑、马尔可夫原理（MP）和先验独立性（IP）原则的额外逻辑原则，以及一定的选择。我们展示了这些原则是如何满足的范畴设置，建立一个紧密的（内部语言）之间的对应关系的逻辑系统和范畴框架。这种紧密的对应关系不仅在讨论已经知道的辩证法的应用时应该很方便，比如它用于从（一些）经典定理中提取计算内容（证明挖掘），它用于帮助建模特定的抽象机器等，而且还有助于设计新的应用。
2021-09-16 math.CT math.LO
On the logical complexity of cyclic arithmetic
本文研究循环算术证明的逻辑复杂性，证明其与皮亚诺算术的片段在定理证明上等价，并给出证明大小和一致性的元数学结果。
2020-01-03 cs.LO math.LO
Toward a Characterization of Simulation Between Arithmetic Theories
研究何时一个具有多项式时间可决定公理的算术理论能高效证明关于真句子ϕ的有界一致性陈述，探讨算术理论间模拟的条件与限制。
2026-10-02 cs.CC math.LO
