Incompleteness for stably consistent formal systems

计算过程与不完全性

Computational Processes and Incompleteness

我们介绍了一个正式的定义Wolfram的概念的计算过程的基础上细胞自动机，一个物理学的计算模型。这些过程有一个自然的分类，分为可判定的，中间的和完整的。它表明，在标准的有限损害优先的论点的背景下，不能建立一个中间的计算过程的存在。

从复杂性度量视角看 PAC 可学习理论的哥德尔不完备定理

Gödel Incompleteness Theorem for PAC Learnable Theory from the view of complexity measurement

本文从解释器编译信息的观点定义解释器相关复杂性，并在带函子的形式系统中证明推广的哥德尔不完备定理，揭示 PAC 可学习对象仍可能无最佳解释器，从而限定强 AI 的泛化与可解释性上限。

一个证明复杂性猜想与不完全定理

A proof complexity conjecture and the Incompleteness theorem

该研究通过定义p-时间函数g_T，证明了任何能形式化一阶逻辑语法的理论必不完整，并探讨了命题证明系统、NP集与证明复杂性生成器之间的关系。

解析哥德尔的不完全性神话：代数逻辑的多项式方程和动力系统

Resolving Gödel's Incompleteness Myth: Polynomial Equations and Dynamical Systems for Algebraic Logic

本文介绍了一种新的计算方法，即利用多项式方程和动力系统来计算逻辑命题，并将其应用于哥德尔不完备性定理。逻辑公式服从一组公理的真假值是从相应的多项式方程系统的解计算出来的。一个公式引用其自身的可证明性被证明是一个递归关系，它可以被解释为这样产生一个离散的动力系统，或解释在一个静态的方式来创建一个额外的联立方程。在这个框架中，逻辑公式和其他多项式目标的真假值具有复杂的数据结构：基本值的集合，或者生成这种解值集合的无穷序列的动力系统。除了公式具有确定的基本值这一常规结果外，这些数据结构还编码了几种例外情况：模糊的、不可满足的、不稳定的或偶然的公式。这些例外代表了几种语义上不同类型的不可判定性;没有一个会给数学带来任何基本问题。很容易计算出哥德尔公式，它断言它不能被证明，在特定的方面是例外的：静态地解释，公式定义了一个矛盾方程组（因此它被称为不可满足的）;动态地解释，它定义了一个动力系统，有一个周期轨道，没有不动点（因此它被称为不稳定的）。这些例外并不是逻辑上的灾难性失败;它们是对哥德尔自指结构的精确数学描述。哥德尔的分析并没有揭示任何实质性的不完整性，在正式的推理系统，也没有任何障碍，证明这种系统的一致性，由普通的数学手段。

随机公理有用吗？

Are random axioms useful?

著名的哥德尔不完备性定理说，对于每一个足够丰富的形式理论（包含某种自然意义上的形式算术），都存在真实的不可证明的陈述。这样的陈述很自然地会被添加为公理，但是我们从哪里可以得到它们呢？一个经典的（并且研究得很好的）方法是（给某个理论T）添加一个公理，该公理要求T的相容性。在这篇笔记中，我们讨论另一个（由Chaitin的哥德尔定理激发），并表明它不是真正有用的（在这个意义上，它并没有帮助我们证明新的有趣的定理），至少如果我们不限制证明的复杂性。我们还讨论了一些相关的问题。

验证近似算法

Verified Approximation Algorithms

本文首次形式化验证了六种NP完全优化问题的近似算法，发现现有证明的不完整性并改进了一个近似比，所有证明基于统一不变量方法。

自指 $K$-SAT 与哥德尔不完备定理的有限模拟

Self-Referential $K$-SAT and the Finite Analogue of Gödel's Incompleteness Theorem

通过对数宽度系综 ($K=O(\log N)$) 消除赋值相关性，构造局部不可区分的不可满足/唯一可满足 SAT 对，证明子线性窗口内演绎管道存在信息盲点，导致指数级证明树爆炸，将强指数时间假说 (SETH) 重新解释为哥德尔不完备性在有限计算中的投影。

Comparison of Two Theorem Provers: Isabelle/HOL and Coq

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although, according to Gödel's incompleteness theorems, it is not possible to construct a single formal system which will describe all phenomena in the world, being complete and consistent at the same time, it gave rise to rather practical areas of logic, such as the theory of automated theorem proving. This is a set of techniques used to verify mathematical statements mec…