We give a survey of current research on Gödel's incompleteness theorems from the following three aspects: classifications of different proofs of Gödel's incompleteness theorems, the limit of the applicability of Gödel's first incompleteness theorem, and the limit of the applicability of Gödel's second incompleteness theorem.
Gödel's first and second incompleteness theorems are corner stones of modern mathematics. In this article we present a new proof of these theorems for ZFC and theories containing ZFC, using Chaitin's incompleteness theorem and a very basic numbers extension. As opposed to the usual proofs, these proofs don't use any fixed-point theorem and rely solely on sets structure. Unlike in the original proof, the statements which can be shown to be unprovable by our technique exceed by far one specific statement constructed from the axiom set. Our goal is to draw attention to the technique of number ext…
In this paper, we provide a fairly general self-reference-free proof of the Second Incompleteness Theorem from Tarski's Theorem of the Undefinability of Truth.
This paper is a continuation of Arai's paper on derivability conditions for Rosser provability predicates. We investigate the limitations of the second incompleteness theorem by constructing three different Rosser provability predicates satisfying several derivability conditions.
In this paper, we use Gödel's incompleteness theorem as a case study for investigating mathematical depth. We take for granted the widespread judgment by mathematical logicians that Gödel's incompleteness theorem is deep, and focus on the philosophical question of what its depth consists in. We focus on the methodological study of the depth of Gödel's incompleteness theorem, and propose three criteria to account for its depth: influence, fruitfulness, and unity. Finally, we give some explanations for our account of the depth of Gödel's incompleteness theorem.
A formalisation of Gödel's incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows {Ś}wierczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of this theory is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.
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).
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.
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.
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
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…
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 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.
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.
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…
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.
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.
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.
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.
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…
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.
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…
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, …
