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.
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.
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.
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.
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.
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…
Relativization is one of the central topics in the study of algebras of relations. Some relativized relation algebras behave much nicer than the original relation algebras. In this paper, we study the atomicity of the finitely generated free algebras of these nice classes of relativized relation algebras. In particular, we give an answer for the open problem, posed by I. Nemeti in 1985, which asks whether the finitely generated free algebras of the class of the weak associative relation algebras WA are atomic or not.
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.
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.
The founding of the theory of cylindric algebras, by Alfred Tarski, was a conscious effort to create algebras out of first order predicate calculus. Let $n\inω$. The classes of non-commutative cylindric algebras ($NCA_n$) and weakened cylindric algebras ($WCA_n$) were shown, by István Németi, to be examples of decidable versions of first order logic with $n$ variables. In this article, we give new proofs for the decidability of the equational theories of these classes. We also give an answer to the open problem, posed by Németi in 1985, addressing the atomicity of the finitely generated free a…
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 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 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.
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 …
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…
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 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.
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…
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 …
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.
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…
Godelian sentences of a sufficiently strong and recursively enumerable theory, constructed in Godel's 1931 groundbreaking paper on the incompleteness theorems, are unprovable if the theory is consistent; however, they could be refutable. These sentences are independent when the theory is so-called omega-consistent; a notion introduced by Godel, which is stronger than (simple) consistency, but ``much weaker'' than soundness. Godel goes to great lengths to show in detail that omega-consistency is stronger than consistency, but never shows, or seems to forget to say, why it is much weaker than so…
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…
We prove that the class of all ordinals Ord is not weakly compact with respect to definable classes. Specifically, in any model of ZFC, the definable tree property fails for Ord, in that there is a definable Ord tree with no definable cofinal branch; the definable partition property fails, in that there is a definable 2-coloring of pairs from a certain definable proper class, with no definable homogeneous proper class; and the definable compactness property fails for $\mathcal{L}_{\infty,ω}$, in that there is a definable theory in this logic all of whose set-sized subtheories are satisfiable, …
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, …
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…
In this article I investigate the phenomenon of minimum models of second-order set theories, focusing on Kelley--Morse set theory $\mathsf{KM}$, Gödel--Bernays set theory $\mathsf{GB}$, and $\mathsf{GB}$ augmented with the principle of Elementary Transfinite Recursion. The main results are the following. (1) A countable model of $\mathsf{ZFC}$ has a minimum $\mathsf{GBC}$-realization if and only if it admits a parametrically definable global well-order. (2) Countable models of $\mathsf{GBC}$ admit minimal extensions with the same sets. (3) There is no minimum transitive model of $\mathsf{KM}$.…
The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper from 2011 revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by ${\textbf{IL}}({\rm All})$. In this paper we present a new principle $\sf R$ in ${\textbf{IL}}({\rm All})$. We show that $\sf R$ does not follow from the logic ${\textbf{IL}}{\sf P_0W^*}$ that contain…
The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of multiplication and order (x,<) behaves differently in the above mentioned domains of numbers. By a theorem of Robinson, addition is definable by multiplication and order in the domain of natural numbers…
