关于哥德尔第二不完全性定理

Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics

We study abstract versions of Gödel's second incompleteness theorem and formulate generalizations of Löb's derivability conditions that work for logics weaker than the classical one. We isolate the role of contraction rule in Gödel's theorem and give a (toy) example of a system based on modal logic without contraction invalidating Gödel's argument.

哥德尔第一不完备定理的一种替代证明

An alternative proof of Godel's first incompleteness theorem

本研究提出哥德尔第一不完备定理的替代证明方法，无需ω一致性且不涉及否定语句编码，从哥德尔常规证明的终点出发完成论证，丰富了该定理的证明路径。

哥德尔不完全性定理的一个蕴涵

An implication of Gödel's incompleteness theorem

给出了哥德尔不完备性定理的一个证明。这个新的证明被认为是哥德尔定理的超限扩展。它表明，如果一个假设的集合论ZFC的Meta水平上，以及在对象水平上，一个矛盾出现。原因是隐藏在哥德尔编号后面的Meta级别和对象级别的隐式识别。这些考虑的影响。

How the Law of Excluded Middle Pertains to the Second Incompleteness Theorem and its Boundary-Case Exceptions

Our earlier publications showed semantic tableau admits partial exceptions to the Second Incompleteness Theorem where a formalism recognizes its self consistency and views multiplication as a 3-way relation (rather than as a total function). We now show these boundary-case evasions will collapse if the Law of the Excluded Middle is treated by tableau as a schema of logical axioms (instead of as derived theorems).

An incompleteness theorem via ordinal analysis

We present an analogue of Gödel's second incompleteness theorem for systems of second-order arithmetic. Whereas Gödel showed that sufficiently strong theories that are $Π^0_1$-sound and $Σ^0_1$-definable do not prove their own $Π^0_1$-soundness, we prove that sufficiently strong theories that are $Π^1_1$-sound and $Σ^1_1$-definable do not prove their own $Π^1_1$-soundness. Our proof does not involve the construction of a self-referential sentence but rather relies on ordinal analysis.

关于哥德尔第二不完备定理的一些推广

On some generalizations of Gödel's second incompleteness theorem

本文从可定义复杂度与可靠性的不可证性、以及语义不完备性两个角度，推广了哥德尔第二不完备定理，并给出了ω-模型和β_n-模型版本的新统一证明。

自指Parases、不完全性和不动点的一种通用方法

A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points

继F. WilliamLawvere，我们证明了许多自指悖论，不完全性定理和不动点定理都来自同一个简单的方案。我们展示了这些相似之处，通过展示这个简单的方案如何包含语义悖论，以及它们如何在逻辑，可计算性理论，复杂性理论和形式语言理论中作为对角线方法和不动点定理出现。

有界可公理化理论的不完备性

Incompleteness of boundedly axiomatizable theories

该研究针对有限语言下量词交替深度有界的一致序列理论，通过归约机制结合塔斯基真不可定义定理证明其不完备性，并拓展得到更多相关不完备性结论。

一个旧的模态不完备性定理的新版本

A new version of an old modal incompleteness theorem

Kripson \cite{Thomason74}证明了一个特定的模态逻辑$\mathbf{L}\subset \mathbf{S4}$相对于Kripke语义是不完全的。后来Gerson \cite{Gerson75}证明了$\mathbf{L}$在邻域语义方面也是不完整的。本文证明了$\mathbf{L}$对于任何一类带算子的完备布尔代数都是不完备的，即它是完全不完备的.

Theorems of Tarski's Undefinability and Godel's Second Incompleteness-Computationally

We present a version of Gödel's Second Incompleteness Theorem for recursively enumerable consistent extensions of a fixed axiomatizable theory, by incorporating some bi-theoretic version of the derivability conditions. We also argue that Tarski's theorem on the Undefinability of Truth is Gödel's First Incompleteness Theorem relativized to definable oracles; a unification of these two theorems is given.

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

Refinements of provability and consistency principles for the second incompleteness theorem

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

关于哥德尔不完备定理不完备性的一则注记

A Note on the Incompleteness of Gödel's Incompleteness Theorems

该研究指出以特定方式递归枚举定理的自动定理证明器（ATPs）会因类似哥德尔不完备定理的机制遗漏部分有效定理，该结论无重大实践理论意义，但具备教学价值。

The incompleteness of an incompleteness argument

Gödel's argument for the First Incompleteness Theorem is, structurally, a proof by contradiction. This article intends to reframe the argument by, first, isolating an additional assumption the argument relies on, and then, second, arguing that the contradiction that emerges at the end should be redirected to refute this initial assumption rather than the completeness of number theory

哥德尔不完备定理与反机械论论证：再探讨

Gödel's incompleteness theorem and the Anti-Mechanist Argument: revisited

本文为纪念Krajewski相关论文的特刊而作，补充阐释其基于哥德尔不完备定理的反机械论论证研究，归类相关误解，结合近期进展深入讨论哥德尔析取论题等三个核心问题。

Incompleteness and Jump Hierarchies

This paper is an investigation of the relationship between Gödel's second incompleteness theorem and the well-foundedness of jump hierarchies. It follows from a classic theorem of Spector's that the relation $\{(A,B) \in \mathbb{R}^2 : \mathcal{O}^A \leq_H B\}$ is well-founded. We provide an alternative proof of this fact that uses Gödel's second incompleteness theorem instead of the theory of admissible ordinals. We then derive a semantic version of the second incompleteness theorem, originally due to Mummert and Simpson, from this result. Finally, we turn to the calculation of the ranks of r…

Godel's Second Incompleteness Theorem for Definable Theories

It is proved that if $T$ is a $Σ_{n+1}$ Definable theory which is $Σ_n$-sound and extends $PA$, then $T$ can not prove the sentence $Σ_n-sound(T)$ that expresses the $Σ_n$-soundness of $T$. Optimality of this result is showed by constructing a $Σ_{n+1}$-definable and $Σ_{n-1}$-sound theory extending $PA$ such that $Σ_n-sound(T)$ is $T$-provable. It is also proved that no R.E. arithmetical theory, evevn very weak theories which are not $Σ_1$-complete, can prove $Σ_1$-soundness of itself.

机械化哥德尔不完备定理与可证性逻辑

Mechanizing Gödel's Incompleteness Theorems and Provability Logic

该研究在Lean 4中形式化验证了哥德尔不完备定理及可证性逻辑GL的Solovay完备性，为数学基础提供机器证明。

Godel-Rosser's Incompleteness Theorems for Non-Recursively Enumerable Theories

Godel's First Incompleteness Theorem is generalized to definable theories, which are not necessarily recursively enumerable, by using a couple of syntactic-semantic notions, one is the consistency of a theory with the set of all true $Π_n$-sentences or equivalently the $Σ_n$-soundness of the theory, and the other is $n$-consistency the restriction of $ω$-consistency to the $Σ_n$-formulas. It is also shown that Rosser's Incompleteness Theorem does not generally hold for definable non-recursively enumerable theories, whence Godel-Rosser's Incompleteness Theorem is optimal in a sense. Though the …

Hilbert's tenth problem, Gödel's incompleteness, Halting problem, a unifying perspective

We formulate a property $P$ on a class of relations on the natural numbers, and formulate a general theorem on $P$, from which we get as corollaries the insolvability of Hilbert's tenth problem, Gödel's incompleteness theorem, and Turing's halting problem. By slightly strengthening the property $P$, we get Tarski's definability theorem, namely that truth is not first order definable. The property $P$ together with a "Cantor's diagonalization" process emphasizes that all the above theorems are a variation on a theme, that of self reference and diagonalization combined. We relate our results to …

A new viewpoint of the Gödel's incompleteness theorem and its applications

A new viewpoint of the Gödel's incompleteness theorem be given in this article which reveals the deep relationship between the logic and computation. Upon the results of these studies, an algorithm be given which shows how to search a proof of statement in first order logic from finite concrete examples, and an approach be proposed to improve searching mathematical proof by neural network.

与$\mathsf{R}$一致的理论的不完全性与不可判定性

Incompleteness and undecidability of theories consistent with $\mathsf{R}$

本文证明了一个同时加强Mostowski定理和Vaught定理的第一不完全性定理版本：对算术R的任意一致扩张的c.e.族，存在一个蕴含R的语句，使所有理论既不能证明它也不能证明其否定。

惊奇检验定理与第二不完全性定理

The Surprise Examination Paradox and the Second Incompleteness Theorem

我们给出了一个新的证明哥德尔的第二不完全性定理，基于柯尔莫哥洛夫复杂性，柴廷的不完全性定理，和一个参数，类似于惊喜检查悖论。然后我们反过来建议第二不完全性定理给出了意外检查悖论的可能解决方案。粗略地说，我们认为，在推导悖论的缺陷是，它包含了一个隐藏的假设，一个可以证明的数学理论的一致性，推导完成;这是不可能的第二个不完全性定理。

无界限的第一不完备性定理

The limitless First Incompleteness Theorem

本文研究第一不完备性定理 G1 的适用界限，通过分析 RE 理论的图灵度与解释度结构，回答既有问题并推广无极小本质不可判定理论的结论。

比较与对照阿罗不可能定理与哥德尔不完备定理

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem

本文引入自指涉系统这一一般数学对象，通过抽象对角化与不动点论证，形式化阿罗不可能定理与哥德尔第一不完备定理之间的对应关系，并揭示两者产生不可能性机制的细微差异。

Gödel incompleteness through Arithmetic Universes after A. Joyal

We give proofs of Gödel's incompleteness theorems after A. Joyal. The proof uses internal category theory in an arithmetic universe, a predicative generalisation of topoi. Applications to Löb's Theorem are discussed.

Hierarchical incompleteness results for arithmetically definable extensions of fragments of arithmetic

There has been a recent interest in hierarchical generalisations of classic incompleteness results. This paper provides evidence that such generalisations are readibly obtainable from suitably hierarchical versions of the principles used in the original proof. By collecting such principles, we prove hierarchical versions of Mostowski's theorem on independent formulae, Kripke's theorem on flexible formulae, and a number of further generalisations thereof. As a corollary, we obtain the expected result that the formula expressing "$T$ is $Σ_n$-ill" is a canonical example of a $Σ_{n+1}$ formula th…

Goedel's Incompleteness Theorem

I present the proof of Goedel's First Incompleteness theorem in an intuitive manner, while covering all technically challenging steps. I present generalizations of Goedel's fixed point lemma to two-sentence and multi-sentence versions, which allow proof of incompleteness through circular versions of the liar's paradox. I discuss the relation of Goedel's First and Second Incompletneness theorems to Goedel's Completeness theorems, and conclude with remarks on implications of these results for mathematics, computation, theory of mind and AI.

数理逻辑导论-问题解决课程

Introduction to mathematical logic - A problem solving course

这是一套288道题，为摩尔式的数理逻辑课程而写。我在一门研究生入门课程中使用过四次这些（或一些变体）。涵盖的主题包括：ZFC的命题逻辑公理以及AC序数和基数算术的等价物一阶逻辑，以及紧致性定理Lowenheim-Skolem定理图灵机，Church的论文完备性定理和第一不完备性定理不可判定理论第二不完备性定理

基于 Turing 范畴的不可判定性定理

Incompleteness theorems via Turing category

本文基于范畴论和直接对角化论证重新表述了哥德尔不可判定性定理，使其适用于不可定义的算术理论，并显式构造了 Gödel 句子。

不完全性语句的分类

A classification of incompleteness statements

本文对不完全性语句进行了分类，探讨了在二阶算术中哪些扩展理论无法证明自身的声性。

复杂性是不完整性的来源吗？

Is Complexity a Source of Incompleteness?

在本文中，我们证明Chaitin的“启发式原理”，{ \it定理的有限指定的理论不能显着更复杂的理论本身}，为一个适当的措施的复杂性。我们证明了该测度在哥德尔数的变化下是不变的。对于这个测度，一个有限指定的、可靠的、相容的理论的定理，强到足以将算术形式化，这是算术上可靠的（如带选择的策梅洛-弗伦克尔集合论或皮亚诺算术），具有有限的复杂性，因此理论的每一个句子，如果比理论复杂得多，都是不可证明的。以前的结果表明，不完全性不是偶然的，而是普遍存在的，在这里得到了概率方面的加强：当$n$趋于无穷大时，长度为$n$的真句子在理论中可证明的概率趋于零，而长度为$n$的句子为真的概率是严格正的。

Godel's Incompleteness Phenomenon - Computationally

We argue that Godel's completeness theorem is equivalent to completability of consistent theories, and Godel's incompleteness theorem is equivalent to the fact that this completion is not constructive, in the sense that there are some consistent and recursively enumerable theories which cannot be extended to any complete and consistent and recursively enumerable theory. Though any consistent and decidable theory can be extended to a complete and consistent and decidable theory. Thus deduction and consistency are not decidable in logic, and an analogue of Rice's Theorem holds for recursively en…

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

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

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

关于Bezboruah与Shepherdson定理的讨论

On a Theorem by Bezboruah & Shepherdson

本文讨论了Bezboruah与Shepherdson定理的不完全性结果，反驳了Kreisel的反对意见，并基于Nielsen和Markov的见解重新证明了该定理。

极限定理的Boolos式证明

Boolos-style proofs of limitative theorems

Boolos的不完备性证明被直接地扩展到产生一些经典逻辑极限定理的简单的“无对角化”证明。

Yablo的Partial和算术不完全性

Yablo's Paradox And Arithmetical Incompleteness

在这篇简短的论文中，我提出了几个定理的句子算术这是有关雅布洛的Paradigas哥德尔的第一个不可判定的句子是有关的骗子悖论。特别是，我认为两个不同的arithemetizations雅布洛的句子：一个类似哥德尔的arithemetizations的骗子，与否定外的可证明性谓词，一个类似杰罗斯洛的不可判定的句子，与否定内。这两种算术化的Yablo句子都是不可判定的，并且与环境形式系统的一致性句子的连接方式大致与哥德尔和杰罗斯洛的句子相同。最后，我考虑一个句子，这是相关的亨金句“我是可证明的”，以同样的方式，前两个算术是相关的哥德尔和杰罗斯洛的句子。我证明了这个句子是可证明的，使用Löb定理，就像Henkin句子的标准证明一样。

About the Chasm Separating the Goals of Hilbert's Consistency Program from the Second Incompletess Theorem

We have published several articles about generalizations and boundary-case exceptions to the Second Incompleteness Theorem during the last 25 years. The current paper will review some of our prior results and also introduce an `enriched' refinement of semantic tableaux deduction. While the Second Incompleteness Theorem is a strong result, we will emphasize its boundary-case exceptions are germane to Global Warming's threat because our systems can own a simultaneous knowledge about their own consistency, together with an understanding of the $Π_1$ implications of Peano Arithmetic.

Incompleteness in the finite domain

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond ${\bf NP\neq co NP}$. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be special cases of such general statements and we want to form…

A Reunion of Godel, Tarski, Carnap, and Rosser

We unify Godel's First Incompleteness Theorem (1931), Tarski's Undefinability Theorem (1933), Godel-Carnap's Diagonal Lemma (1934), and Rosser's (strengthening of Godel's first) Incompleteness Theorem (1936), whose proofs resemble much and use almost the same technique.

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

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

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

Gödel for Goldilocks: A Rigorous, Streamlined Proof of (a variant of) Gödel's First Incompleteness Theorem

Most discussions of Gödel's theorems fall into one of two types: either they emphasize perceived philosophical, cultural "meanings" of the theorems, and perhaps sketch some of the ideas of the proofs, usually relating Gödel's proofs to riddles and paradoxes, but do not attempt to present rigorous, complete proofs; or they do present rigorous proofs, but in the traditional style of mathematical logic, with all of its heavy notation and difficult definitions, and technical issues which reflect Gödel's original approach and broader logical issues. Many non-specialists are frustrated by these two …

可计算性、哥德尔不完全性定理和进化可预测性的内在限制

Computability, Gödel's Incompleteness Theorem, and an inherent limit on the predictability of evolution

进化多样化的过程在潜在结果的巨大基因型空间中展开。在过去的一个世纪里，这种多样化的理论发展取得了显着的进步，该理论的成功部分取决于其适用范围。该理论的大部分内容都集中在潜在基因型空间中相对较小的子集上，这些基因型主要是根据历史或当代模式选择的，然后在这个预定义的集合中预测演化动力学。在何种程度上，这种方法可以被推到一个更广泛的视角，解释进化多样化的潜在开放性？沿着这条路线已经有了一些重要的理论发展，但这种理论能被推多远的问题还没有得到解决。这里证明了一个定理，证明了由于继承的数字性质，使用这种方法可以回答的问题类型存在固有的限制。特别是，即使在极其简单的进化系统中，除非进化是渐进的，否则也不可能有一个完整的理论来解释进化的潜在开放性。该定理与哥德尔不完全性定理和可计算性理论中的停机问题密切相关。

Gödel's Theorem and Direct Self-Reference

In his paper on the incompleteness theorems, Gödel seemed to say that a direct way of constructing a formula that says of itself that it is unprovable might involve a faulty circularity. In this note, it is proved that 'direct' self-reference can actually be used to prove his result.

Incompleteness for stably consistent formal systems

We first partly develop a mathematical notion of stable consistency intended to reflect the actual consistency property of human beings. Then we give a generalization of the first and second Gödel incompleteness theorem to stably $1,2$-consistent formal systems. Our argument in particular re-proves the original incompleteness theorems from first principles, using Turing machine language to (computably) construct our "Gödel sentence" directly, in particular we do not use the diagonal lemma, nor any meta-logic, with the proof naturally formalizable in set theory. In practice such a stably consis…

An Intuitively Complete Analysis of Godel's Incompleteness

A detailed and rigorous analysis of Gödel's proof of his first incompleteness theorem is presented. The purpose of this analysis is two-fold. The first is to reveal what Gödel actually proved to provide a clear and solid foundation upon which to base future research. The second is to construct a coherent explication of Gödel's proof that is not only approachable by the non-specialist, but also brings to light the core principles underlying Gödel's proof.

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

A proof complexity conjecture and the Incompleteness theorem

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

由皮亚诺算术的每一公理和定理引出的丢番图形式的不可判定命题

Undecidable propositions with Diophantine form arisen from every axiom and every theorem of Peano Arithmetic

在MRDP定理的基础上，引入了公式证明方程和Peano算术（PA）的泛证明方程的思想，并结合泛证明方程和哥德尔第二不完全性定理，证明了若PA是相容的，则对PA的每个公理和定理，都可以构造出相应的丢番图形式的不可判定命题.最后，我们提出了一种方法，寻求证明的数学（集合论，数论，代数，几何，拓扑等）命题转化为解决一个丢番图方程。

广义相对论中观测量的不完备性定理

Incompleteness Theorems for Observables in General Relativity

本文运用描述集合论方法证明在广义相对论中丰富的时空集合不存在Borel可定义的完备观测量，揭示该问题与规范自由度相关，并指出理论物理与描述集合论的新联系。

On Constructivity and the Rosser Property: a closer look at some Gödelean proofs

The proofs of Kleene, Chaitin and Boolos for Gödel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Gödel's own proof for his incompleteness theorem does not have the Rosser property, and we show that neither do Kleene's or Boolos' proofs. However, we show that a variant of Chaitin's proof can have the Rosser property. The proofs of…

A mathematical commitment without computational strength

We present a new manifestation of Gödel's second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert's program. Specifically, we consider a proper extension of Peano arithmetic ($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of $Σ^0_2$-sentences. These sentences assert that each computably enumerable ($Σ^0_1$-definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is important for computer science. On a technical level, …

Consequences of a Goedel's misjudgment

The fundamental aim of the paper is to correct an harmful way to interpret a Goedel's erroneous remark at the Congress of Koenigsberg in 1930. Despite the Goedel's fault is rather venial, its misreading has produced and continues to produce dangerous fruits, as to apply the incompleteness Theorems to the full second-order Arithmetic and to deduce the semantic incompleteness of its language by these same Theorems. The first three paragraphs are introductory and serve to define the languages inherently semantic and its properties, to discuss the consequences of the expression order used in a lan…

从哥德尔不完备定理到机器人信念的完备性（扩展摘要）

From Gödel's Incompleteness Theorem to the completeness of bot beliefs (Extended abstract)

本文从哥德尔不完备定理出发，研究理论通过逐步添加公理实现完备化的实用主义逻辑过程，并刻画机器人与自动化学习者可能收敛到的可检验但不可证伪的理论轨迹。

Herbrand Consistency of Some Arithmetical Theories

Gödel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness of a bounded formula logarithmically, but in the presence of Herbrand consistency, for theories ${\rm IΔ_0+Ω_m}$ with $m\geqslant 2$, any witness for any bounded formula can be shortened logarithmicall…

哥德尔、塔斯基、丘奇和骗子

Godel, Tarski, Church, and the Liar

著名的哥德尔不完全性定理和所有逻辑悖论的原型--说谎者悖论--密切相关，这一事实当然不仅是众所周知的，而且是逻辑学家共同体的常识的一部分。事实上，几乎每一个或多或少的定理的正式处理（包括，就此而言，哥德尔的原始论文）都提到了这种联系。鉴于这种联系的存在是司空见惯的事实，更令人惊讶的是，人们对它的确切性质知之甚少。现在，从我们在这篇文章中所做的工作中可以看出，数学的三个中心极限定理，那些关于算术的不完备性和不可判定性以及其中真理的不可定义性的一般思想，可以被看作是解决说谎者悖论的不同方法。事实上，说谎者悖论的一个抽象的形式变体构成了一个一般的概念图式，揭示了它们共同的逻辑根源，将上面提到的定理联系起来，同时表明，在某种意义上，这些是唯一可能的相关限制定理，它们可以被认为是说谎者悖论的不同表现形式。另一方面，正如一个简单的例子所说明的那样，这个悖论的抽象版本开辟了一种可能性，即对真理和可证明性概念以外的概念形成相关的结果。