首页/论文/1902.07404

arXiv 1902.074042019-02math.LO

一致性的可证明性

The Provability of Consistency

Sergei Artemov

备注：: A compact exposition of the main result and a brief foundational discussion

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们提供了一个数学证明的一致性Peano算术PA形式化PA。这个结果与哥德尔的第二不完全性定理是相容的，因为我们的一致性证明不依赖于一致性的表示作为一个特定的算术公式。我们的研究结果表明，形式化理论可以将某些属性的证明形式化，而不会将这些属性的呈现减少到一个公式。我们概述了PA证明方案的理论。

英文摘要：

We offer a mathematical proof of consistency for Peano Arithmetic PA formalizable in PA. This result is compatible with Goedel's Second Incompleteness Theorem since our consistency proof does not rely on the representation of consistency as a specific arithmetical formula. Our findings show that formal theories can finitely formalize proofs of certain properties presented as schemes without reducing the presentation of those properties to a single formula. We outline a theory of proving schemes in PA.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

Peano算术的慢可证性和普通可证性

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-06math.LO

可证明性逻辑：Peano算术中的模型中的模型

Provability Logic: models within models in Peano Arithmetic

在1994年杰希给出了模型理论证明哥德尔的第二不完备定理Zermelo-Fraenkel集合论在以下形式：ZF不证明ZF有一个模型。Kotlarski表明，Jech的证明可以适应皮亚诺算术的作用，模型正在采取的完整一致的扩展。在本说明中，我们采取另一个步骤的方向，取代证明理论的模型理论的论点。我们表明，没有通过算术完备性定理，存在的PA的复杂性模型$Σ^0_2$是独立的PA，其中一个模型是确定的一组公式与参数，在模型中。我们的方法是基于一个新的解释证明逻辑的皮亚诺算术与模态算子解释为真理，在每一个$Σ^0_2$模型。

2022-04-16math.LO

关于Peano算术中的一系列反射原理

On a Hierarchy of Reflection Principles in Peano Arithmetic

我们研究了皮亚诺算术PA的反射原理，这些原理是基于证明和可证明性的。PA中的任何这样的反射原理都等价于$\Box P\!\rightarrow\! P$（$\Box P$代表“$P$是可证明的”）或对于某些$k\geq 0$的$\Box^k u\!\!:\!\!P\!\rightarrow\! P$（$t:P$声明“$t$是$P$的证明”）。反射原则就其演绎强度$$u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box^2 u\!\!:\!\!P\!\rightarrow\! P \ \ \prec\ \ldots\ \prec\ \ \Box P\!\rightarrow\! P.$$而言，构成了一个不可折叠的层次结构

2014-05-11math.LO

算术和超算术蠕虫战

Arithmetical and Hyperarithmetical Worm Battles

Japaridze的可证明性逻辑$GLP$对每个自然数都有一个模态$[n]$，并且已经被Beklemishev用于Peano aritime $(PA)$和相关理论的证明理论分析。除了其他好处之外，这种分析产生了所谓的“每虫都死”$(EWD)$原则，这是一种独立于$PA$的自然组合语句。最近，Beklemishev和Pakhomov研究了$GLP$中超限模态的可证明性概念。我们表明，的确是自然的超限扩展$GLP$是健全的这种解释，并产生独立的组合原则的二阶理论$ACA$的算术理解与充分的感应。我们还提供了与Peano算法的片段$IΣ_n$相关的$EWD$的限制版本。为了证明后者，我们表明，标准的哈代函数优化其变种的基础上树序数。

2022-06-29math.LO

可证性谓词与一致性陈述的模态逻辑方面

Modal logical aspects of provability predicates and consistency statements

Kobe University（神户大学）

本文通过扩展Solovay方法和改进Arai的Rosser可证性谓词构造，建立了逻辑NP、ND、NP4和ND4的算术完全性。

2026-06-12math.LO

公理化可证明$n$ -可证明性

Axiomatizing provable $n$-provability

一个公式$ϕ$在形式算术理论$S$中被称为\emph{$n$-provable}，如果$ϕ$在$S$中连同所有真算术$Π_{n}$ -语句一起被证明为附加公理。虽然一般来说，对于固定的$n>0$，所有$n$可证明公式的集合不是递归可证明的，但是其$n$可证明性在给定的r. e.中是可证明的公式的集合$ϕ$是递归可证明的。元理论$T$是r.e.这个集合是演绎封闭的，并且通常是$S$的扩展。我们证明，这些理论可以自然公理化的迭代局部反射原则的进展。特别地，Peano算术PA的可证1-可证语句集可以用PA上的$\varepsilon_0$倍迭代局部反射模式公理化.我们的特征产生额外的信息，这些理论的证明理论的强度（w.r.t.各种措施），并对他们的axiomatizability。我们还研究了问题的加速证明，并表明，在某些情况下，证明$n$证明的句子可以比它的证明迭代反射原则。

2018-05-01math.LO

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

弗里德曼-自反性：作为consistoids的解释者

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-25math.LO

序列性质、选择子证明与一致性的可证性

Serial Properties, Selector Proofs, and the Provability of Consistency

本文提出选择子证明概念，推广希尔伯特两阶段一致性证明方法，并给出皮亚诺算术 PA 的一致性选择子证明，在 PA 内形式化，从而避开哥德尔第二不完备定理的限制。

2024-03-18math.LO

可证性与一致性原理对第二不完备定理的精化

Refinements of provability and consistency principles for the second incompleteness theorem

本文延续先前研究，证明受非正规模态逻辑启发的弱原理足以推导第二不完备定理的精化形式，并确立了特定原理集合能证明一致性陈述的不可证性及形式化的 $Σ_1$-完备性。

2025-08-11math.LO

明希豪森可证性

Münchhausen provability

由Solovay关于形式可证明性的著名完备性结果可知，可证明性逻辑$\mathrm GL$精确地描述了任何合理且足够强的算术理论的所有可证明的结构性质，并具有可判定的公理化。Japaridze通过考虑$\mathrm GL$的多模态版本$\mathrm GLP$来推广这一结果，其中每个自然数$n$都有模态$[n]$，这是指不断增加的可证明性概念。$\mathrm GLP$的现代处理倾向于将$[n]$可证明性概念解释为“在基础理论$T$中可证明，连同所有真正的$Π^0_n$公式作为神谕”。在本文中，我们将这种解释推广到超限。为了做到这一点，要克服的主要困难是将复杂性$Π^0_n$的甲骨文公式的语法特征推广到超算术层次。本文利用的事实，证明是$Σ^0_1$完成，类似的结果举行更强的证明概念。因此，在$α$层次上定义可证明性的预言语句将被递归地视为在较低层次上的一致性陈述：通过论文名称的可证明性来证明可证明性。本文证明了合理性和完整性的广泛的理论类的建议解释，即任何理论，可以正式的递归上述，并有一些进一步的非常自然的属性。一些评论提供了如何递归可以正式成为二阶算术和降低这些系统的二阶算术的证明理论强度。

2019-08-29math.LO

对Vardanyan定理的一种突破

An Escape from Vardanyan's Theorem

针对Vardanyan定理关于皮亚诺算术量化可证性逻辑不可计算公理化的结论在严格正签名下无法证明的问题，研究推广Kripke可靠性与完全性证明得常域完全性，通过Solovay型构造证明QRC₁系统的算术语义完全性，明确其为QGL严格正片段及QPL(PA)的片段。

2021-08-31math.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-06math.LO

非紧致证明

Non-Compact Proofs

The Graduate Center, the City University of New York（纽约市立大学研究生中心）

本文研究了非紧致证明在PA一致性证明中的作用，指出哥德尔定理禁止紧致证明，但允许非紧致证明在PA内形式化证明PA的一致性。

2025-12-15math.LO

一致性公式在PA中严格强于PA一致性

Consistency formula is strictly stronger in PA than PA-consistency

本文证明PA的一致性公式Con(PA)在PA中严格强于PA一致性，指出Con(PA)不可证并不蕴含PA一致性不可证。

2025-08-28math.LO

算术的一致性

The Consistency of Arithmetic

2010年，弗拉基米尔·沃斯基做了一个关于“如果当前的数学基础不一致怎么办？他说，他非常怀疑有一天可能会发现PA（一阶皮亚诺算术）中的不一致性，大约一年后，爱德华·纳尔逊宣布，他不仅在PA中发现了不一致性，而且在原始递归算术的一小部分中也发现了不一致性。很快，Daniel Tausk和Terence Tao独立发现了一个致命错误，Nelson撤回了他的说法，称PA的一致性是一个“悬而未决的问题”。“许多数学家可能会发现这样的说法令人困惑。PA的一致性真的是一个开放的问题吗？如果是这样的话，PA中不一致的发现会导致所有的数学像纸牌屋一样倒塌吗？本文试图解决这些问题，通过勾勒和讨论现有的证明PA的一致性（包括根岑的证明和弗里德曼的相对兼容性证明，呼吁Bolzano-Weierstrass定理）。由于纳尔逊是一个自称的形式主义者，本文还探讨了形式主义的含义。

2018-07-16math.LO

选择器证明的性质

Properties of Selector Proofs

本文概述选择器证明的数学性质，包括其与普通可证性、ω规则、相对一致性的关系，迭代选择器证明及选择器复杂度，该概念由Artemov引入且与相对一致性密切相关。

2025-09-19math.LO

算术中的统一一致性与哥德尔第二不完全性定理：一个童话

Uniformity of Consistency in Arithmetic and Gödel's Second Incompleteness Theorem: Ein Märchen

University of Vienna（维也纳大学）

本文探讨了足够强的可数理论中一致性的统一验证方法，通过选择器证明实现计算统一性，但无法内部化为哥德尔第二不完全性定理的统一一致性句子。

2026-07-14math.LO

辩证逻辑原理

Dialectica Logical Principles

哥德尔的Dialectica解释旨在获得海廷算术的相对兼容性证明，与双重否定解释一起使用，以获得皮亚诺算术的相容性。近年来，基于哥德尔辩证法解释的证明理论转换（所谓的证明解释）已被系统地用于从证明中提取新内容，因此解释在数学和计算机科学的几个领域中找到了相关的应用。继我们以前的工作哥德尔纤维化，我们提出了一个（超）学说的辩证法，这完全符合解释的逻辑描述的特点。说明我们在范畴论中导出了对蕴涵联结词的解释的可靠性，正如斯佩克特和特罗尔斯特拉所阐明的那样。这就要求有超越直觉主义逻辑、马尔可夫原理（MP）和先验独立性（IP）原则的额外逻辑原则，以及一定的选择。我们展示了这些原则是如何满足的范畴设置，建立一个紧密的（内部语言）之间的对应关系的逻辑系统和范畴框架。这种紧密的对应关系不仅在讨论已经知道的辩证法的应用时应该很方便，比如它用于从（一些）经典定理中提取计算内容（证明挖掘），它用于帮助建模特定的抽象机器等，而且还有助于设计新的应用。

2021-09-16math.CTmath.LO