Gödel's incompleteness theorems

Gödel's incompleteness theorems represent fundamental propositions within mathematical logic, addressing the inherent limitations of provability within formal axiomatic systems. Kurt Gödel's publication of these findings in 1931 marked a pivotal moment for both mathematical logic and the philosophy of mathematics. These theorems are widely understood to demonstrate the impossibility of Hilbert's program, which sought to establish a comprehensive and consistent axiomatic foundation for all of mathematics.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in philosophy of mathematics. The theorems are interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

The first incompleteness theorem asserts that any consistent axiomatic system, whose theorems are recursively enumerable (i.e., can be generated by an algorithm), cannot encompass all true statements concerning the arithmetic of natural numbers. Consequently, within any such consistent formal framework, certain true propositions about natural numbers will inevitably remain unprovable. Conversely, there will also exist statements about natural numbers that are false, yet whose falsehood cannot be formally demonstrated within that same system.

The second incompleteness theorem, which builds upon the first, demonstrates that no such formal system can prove its own consistency.

Utilizing a diagonal argument, Gödel's incompleteness theorems initiated a series of interconnected findings concerning the inherent limitations of formal systems. Subsequent developments included Tarski's undefinability theorem, which addresses the formal undefinability of truth; Church's demonstration that Hilbert's Entscheidungsproblem is undecidable; and Turing's theorem, establishing the absence of an algorithm capable of solving the halting problem.

Formal Systems: Completeness, Consistency, and Effective Axiomatization

Gödel's incompleteness theorems are applicable to formal systems possessing sufficient complexity to articulate the fundamental arithmetic of natural numbers, provided these systems are both consistent and effectively axiomatized. Within the domain of first-order logic, formal systems are frequently referred to as formal theories. Broadly defined, a formal system constitutes a deductive framework comprising a specific set of axioms and rules for symbolic manipulation (or inference rules), which enable the derivation of new theorems from the initial axioms. First-order Peano arithmetic exemplifies such a system, where all variables are designated to represent natural numbers. Conversely, in systems like set theory, only a subset of the formal system's sentences articulate propositions concerning natural numbers. Crucially, the incompleteness theorems pertain to formal provability within these defined systems, distinguishing it from informal notions of provability.

Formal systems can exhibit various properties, notably completeness, consistency, and the presence of an effective axiomatization. However, the incompleteness theorems demonstrate that systems incorporating a sufficient degree of arithmetic cannot simultaneously satisfy all three of these criteria.

Effective Axiomatization

A formal system is designated as effectively axiomatized (or alternatively, effectively generated) if its collection of theorems is recursively enumerable. This condition implies the theoretical existence of a computational algorithm capable of listing every theorem within the system, without including any non-theorems. Illustrative examples of effectively generated theories encompass Peano arithmetic and Zermelo–Fraenkel set theory (ZFC).

True arithmetic, a theoretical construct, comprises all veridical statements concerning standard integers, expressed within the language of Peano arithmetic. While this theory exhibits both consistency and completeness, and incorporates a sufficient scope of arithmetic, it crucially lacks a recursively enumerable set of axioms, thereby failing to meet the preconditions for the incompleteness theorems.

Completeness

An axiomatic set is considered syntactically (or negation-) complete if, for every statement formulated within its language, either the statement itself or its negation can be formally derived from the axioms. This specific definition of completeness is pertinent to Gödel's first incompleteness theorem. It should not be conflated with semantic completeness, which signifies that the axiomatic set can prove all semantic tautologies inherent to the specified language. In his distinct completeness theorem (which should not be confused with the incompleteness theorems discussed herein), Gödel demonstrated that first-order logic possesses semantic completeness. However, it lacks syntactic completeness, as certain sentences expressible within the language of first-order logic can neither be proven nor disproven solely from its foundational axioms.

Hilbert and other mathematicians posited that, within a mathematical system, an axiomatization would eventually be discovered that would enable the proof or disproof (through the demonstration of its negation) of every mathematical formula.

A formal system can be syntactically incomplete either by design, as is common in various logics, or due to the omission or undiscovered nature of essential axioms. For instance, Euclidean geometry, when lacking the parallel postulate, remains incomplete because certain statements within its linguistic framework, including the parallel postulate itself, cannot be derived from the existing axioms. Analogously, the theory of dense linear orders is incomplete but achieves completeness upon the inclusion of an additional axiom asserting the absence of endpoints in the order. The continuum hypothesis, a statement formulated within the language of ZFC, is not provable within ZFC, thereby rendering ZFC incomplete. In this particular scenario, no evident candidate for a new axiom exists to resolve this incompleteness.

First-order Peano arithmetic appears to be consistent. Assuming its consistency, it possesses an infinite yet recursively enumerable set of axioms and is capable of encoding sufficient arithmetic to satisfy the hypotheses of the incompleteness theorem. Consequently, according to the first incompleteness theorem, Peano Arithmetic is incomplete. This theorem provides a concrete instance of an arithmetic statement that is neither provable nor disprovable within Peano's arithmetic. Furthermore, this statement holds true in the standard model. Additionally, no effectively axiomatized, consistent extension of Peano arithmetic can achieve completeness.

Consistency

A set of axioms is deemed consistent if no statement and its negation can both be derived from these axioms; conversely, it is considered inconsistent. In essence, a consistent axiomatic system is characterized by its freedom from contradiction.

Peano arithmetic's consistency can be demonstrated from ZFC, though not internally. Analogously, ZFC itself cannot internally prove its own consistency. However, the system ZFC augmented with the axiom "there exists an inaccessible cardinal" establishes ZFC's consistency, because if κ represents the smallest such cardinal, then V_κ within the von Neumann universe constitutes a model of ZFC, and a theory is consistent if and only if it possesses a model.

Should all statements within the language of Peano arithmetic be adopted as axioms, the resulting theory would be complete, possess a recursively enumerable set of axioms, and be capable of describing both addition and multiplication. Nevertheless, such a theory would lack consistency.

Further instances of inconsistent theories emerge from the paradoxes that manifest when the axiom schema of unrestricted comprehension is posited within set theory.

Systems Incorporating Arithmetic

The incompleteness theorems are exclusively applicable to formal systems capable of demonstrating a sufficient body of facts concerning natural numbers. A prime example of such a sufficient collection is the set of theorems within Robinson arithmetic Q. While certain systems, like Peano arithmetic, can directly articulate statements about natural numbers, others, such as ZFC set theory, possess the capacity to interpret natural number statements within their own linguistic framework. Both approaches are suitable for the application of the incompleteness theorems.

The theory of algebraically closed fields with a specified characteristic is complete, consistent, and characterized by an infinite yet recursively enumerable set of axioms. Nevertheless, it is not feasible to encode integers within this theory, nor can the theory describe integer arithmetic. A comparable illustration is the theory of real closed fields, which fundamentally corresponds to Tarski's axioms for Euclidean geometry. Consequently, Euclidean geometry itself, as formulated by Tarski, exemplifies a complete, consistent, and effectively axiomatized theory.

Presburger arithmetic comprises a set of axioms for natural numbers that exclusively includes the addition operation, deliberately omitting multiplication. This system is complete, consistent, and recursively enumerable, capable of encoding addition but not the multiplication of natural numbers. This demonstrates that for Gödel's theorems to apply, a theory must be able to encode both addition and multiplication, not merely addition.

Dan Willard (2001) investigated certain weak arithmetic systems that possess sufficient arithmetic relations to formalize Gödel numbering but lack the functional capacity for multiplication, consequently failing to demonstrate the second incompleteness theorem; specifically, these systems are consistent and capable of proving their own consistency.

Conflicting Goals

The selection of an axiom set typically aims to maximize the derivation of correct results while precluding the proof of any erroneous statements. For instance, one might conceptualize a set of true axioms capable of demonstrating every true arithmetical assertion concerning natural numbers (Smith 2007, p. 2). Within the standard framework of first-order logic, an inconsistent axiom set inherently proves every statement expressible in its language, a phenomenon sometimes termed the principle of explosion, thereby rendering it automatically complete. Conversely, an axiom set that achieves both completeness and consistency establishes a maximal collection of non-contradictory theorems.

The pattern observed in prior discussions concerning Peano arithmetic, ZFC, and ZFC + "there exists an inaccessible cardinal" is generally immutable. Specifically, the system ZFC + "there exists an inaccessible cardinal" cannot internally establish its own consistency. Furthermore, it lacks completeness, as exemplified by the continuum hypothesis, which remains undecidable within ZFC + "there exists an inaccessible cardinal".

The first incompleteness theorem demonstrates that, within formal systems capable of expressing elementary arithmetic, a finite, complete, and consistent list of axioms is unattainable. Each consistent axiomatic addition invariably leaves other true statements unprovable, even with the newly incorporated axiom. Should an axiom be introduced that renders the system complete, this completeness is achieved at the expense of inconsistency. Moreover, even an infinite list of axioms cannot simultaneously be complete, consistent, and effectively axiomatized.

First Incompleteness Theorem

Gödel's first incompleteness theorem was initially presented as "Theorem VI" within Gödel's 1931 publication "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I". The theorem's hypotheses were subsequently refined by J. Barkley Rosser (1936) through the application of Rosser's trick. The resultant theorem, incorporating Rosser's refinement, can be articulated in English as follows, assuming that a "formal system" implies effective generation.

First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e. there are statements of the language of F which can neither be proved nor disproved in F." (Raatikainen 2020)

The unprovable statement G_F identified by the theorem is commonly termed "the Gödel sentence" pertaining to the system F. The demonstration involves the construction of a specific Gödel sentence for the system F; however, an infinite multitude of statements within the system's language exhibit identical properties, including, for instance, the conjunction of the Gödel sentence with any logically valid sentence.

Every effectively generated system possesses a unique Gödel sentence. One can construct an expanded system F' encompassing the entirety of F, augmented by G_F as an additional axiom. This augmentation will not yield a complete system, as Gödel's theorem remains applicable to F', thereby precluding the completeness of F'. Consequently, G_F is indeed a theorem within F', by virtue of its axiomatic status. Since G_F merely asserts its unprovability in F, its provability within F' introduces no contradiction. Nevertheless, as the incompleteness theorem extends to F', a novel Gödel statement, G_F ', will emerge for F', demonstrating its continued incompleteness. The statement G_F ' will diverge from G_F by referring to F' instead of F.

Syntactic Form of the Gödel Sentence

The Gödel sentence is formulated to exhibit indirect self-reference. It posits that a sentence constructed through a specific procedural sequence will lack provability within F. Nevertheless, this construction sequence is precisely designed such that the resulting sentence is, in fact, G_F itself. Consequently, the Gödel sentence G_F implicitly asserts its own unprovability within the formal system F.

In establishing the first incompleteness theorem, Gödel demonstrated that the concept of provability within a formal system can be entirely articulated using arithmetical functions operating on the Gödel numbers assigned to the system's sentences. Thus, a system capable of proving numerical facts can also, indirectly, establish facts concerning its own statements, contingent upon its effective generation. Inquiries into the provability of statements within such a system are thereby transformed into questions regarding the arithmetical properties of numbers themselves, which the system would be able to decide if it were complete.

Consequently, while the Gödel sentence indirectly references statements within the system F, its interpretation as an arithmetical assertion reveals a direct reference solely to natural numbers. It posits that no natural number possesses a specific property, which is defined by a primitive recursive relation (Smith 2007, p. 141). Accordingly, the Gödel sentence can be formulated within the language of arithmetic using a straightforward syntactic structure. Specifically, it can be articulated as an arithmetical formula comprising a series of leading universal quantifiers followed by a quantifier-free body (these formulas reside at level Π<!-- Π --> §1314§ §1718§ {\displaystyle \Pi _{1}^{0}} of the arithmetical hierarchy). Furthermore, through the application of the MRDP theorem, the Gödel sentence can be re-expressed as a declaration that a specific polynomial with multiple variables and integer coefficients never evaluates to zero when integers are substituted for its variables (Franzén 2005, p. 71).

Truth of the Gödel Sentence

The first incompleteness theorem establishes that the Gödel sentence G_F, formulated within an appropriate formal theory F, is unprovable within F. Given that, when construed as an arithmetical statement, this unprovability precisely corresponds to what the sentence indirectly asserts, the Gödel sentence is, in actuality, true (Smoryński 1977, p. 825; 28–33). Consequently, the sentence G_F is frequently characterized as "true but unprovable" (Raatikainen 2020). Nevertheless, as the Gödel sentence cannot formally define its own intended interpretation, its truth, specifically for G_F, must be ascertained through a meta-analysis conducted externally to the system. Typically, this meta-analysis can be performed within the weak formal system known as primitive recursive arithmetic, which demonstrates the implication Con(F)→G_F, where Con(F) represents a canonical statement affirming the consistency of F (Smoryński 1977, p. 840; Kikuchi & Tanaka 1994, p. 403).

While the Gödel sentence of a consistent theory is true when considered as a statement about the intended interpretation of arithmetic, it will be false in certain nonstandard models of arithmetic, a consequence of Gödel's completeness theorem (Franzén 2005, p. 135). This theorem establishes that if a sentence is independent of a theory, the theory will possess models in which the sentence is true and other models in which it is false. As previously noted, the Gödel sentence for a system F is an arithmetical assertion claiming the non-existence of any number with a specific property. The incompleteness theorem demonstrates that this assertion remains independent of the system F, and the truth of the Gödel sentence arises from the fact that no standard natural number exhibits the property in question. Any model where the Gödel sentence is false must, therefore, contain an element that satisfies this property within that model. Such a model is necessarily "nonstandard," implying it includes elements that do not correspond to any standard natural number (Raatikainen 2020, Franzén 2005, p. 135).

Relationship with the Liar Paradox

In the introductory section of "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I," Gödel explicitly identifies Richard's paradox and the liar paradox as semantic parallels to his syntactical incompleteness findings. The liar paradox is famously articulated as the statement, "This sentence is false." An analysis of this sentence reveals its inherent contradiction: if it were true, it would, by its own assertion, be false; conversely, if it were false, it would then be true. A Gödel sentence, denoted G, for a system F, presents an analogous assertion to the liar sentence, but replaces the concept of truth with that of provability. Specifically, G declares, "G is not provable in the system F." The subsequent examination of the truth and provability of G constitutes a formalized version of the logical analysis applied to the truth condition of the liar sentence.

It is not feasible to substitute "not provable" with "false" in a Gödel sentence, because the predicate "Q is the Gödel number of a false formula" cannot be represented as an arithmetical formula. This principle, known as Tarski's undefinability theorem, was discovered independently by Gödel, during his work on the incompleteness theorem's proof, and by Alfred Tarski, the theorem's namesake.

Extensions of Gödel's Original Result

Compared to the theorems articulated in Gödel's 1931 paper, many contemporary formulations of the incompleteness theorems exhibit greater generality in two primary aspects. These generalized statements are designed to apply to a broader class of systems and to incorporate weaker assumptions regarding consistency.

While Gödel demonstrated the incompleteness of the Principia Mathematica system, a specific arithmetical framework, he noted that a parallel demonstration could be provided for any effective system possessing a certain level of expressiveness. Gödel commented on this broader applicability in his paper's introduction but confined his proof to a single system for the sake of concreteness. In modern statements of the theorem, it is customary to articulate the conditions of effectiveness and expressiveness as foundational hypotheses for the incompleteness theorem, thereby extending its scope beyond any particular formal system. The precise terminology used to state these conditions had not yet been developed when Gödel published his results in 1931.

The initial formulation and demonstration of Gödel's incompleteness theorem necessitated the premise that the formal system in question was not merely consistent, but specifically ω-consistent. A system is defined as ω-consistent if it avoids being ω-inconsistent. Conversely, a system exhibits ω-inconsistency if it contains a predicate P for which, despite proving ~P(m) for every specific natural number m, it simultaneously proves the existence of a natural number n satisfying P(n). This implies that the system asserts the existence of a number possessing property P, yet concurrently refutes that any particular number instantiates this property. While ω-consistency inherently entails consistency, the converse is not true; consistency does not guarantee ω-consistency. In 1936, J. Barkley Rosser enhanced the incompleteness theorem by introducing a modified proof, known as Rosser's trick, which solely required the system to be consistent, thereby removing the stricter condition of ω-consistency. This refinement primarily holds technical significance, given that all veridical formal theories of arithmetic—those whose axioms are universally true statements concerning natural numbers—are inherently ω-consistent, rendering Gödel's original theorem applicable to them. The more robust iteration of the incompleteness theorem, which postulates only consistency instead of ω-consistency, is now widely recognized as Gödel's incompleteness theorem or the Gödel–Rosser theorem.

The Second Incompleteness Theorem

Within any formal system F that incorporates fundamental arithmetic, a formula, denoted Cons(F), can be canonically constructed to represent the consistency of F. This formula articulates the property that no natural number exists which encodes a formal derivation within system F culminating in a syntactic contradiction. Frequently, the syntactic contradiction is instantiated as "0=1", leading Cons(F) to assert that no natural number encodes a derivation of "0=1" from the axioms of F.

Gödel's second incompleteness theorem demonstrates that, given general assumptions, this canonically defined consistency statement, Cons(F), cannot be formally proven within F itself. This theorem was initially presented as "Theorem XI" in Gödel's seminal 1931 publication, "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I." For the subsequent exposition, the designation "formalized system" implicitly incorporates the assumption that F is effectively axiomatized. The theorem asserts that for any consistent system F capable of expressing a sufficient degree of elementary arithmetic, the consistency of F cannot be established through proof within F itself. This theorem surpasses the first incompleteness theorem in strength, primarily because the statement formulated in the first theorem does not explicitly articulate the system's consistency. The demonstration of the second incompleteness theorem is achieved by formalizing the proof of the first incompleteness theorem directly within the system F.

Formalizing Consistency

A significant technical nuance exists within the second incompleteness theorem concerning the methodology for representing the consistency of F as a formula within the language of F. Multiple approaches exist for articulating a system's consistency, and these various formalizations do not invariably yield equivalent outcomes. The specific formula Cons(F), as referenced in the second incompleteness theorem, constitutes one particular formalization of consistency.

Alternative formalizations asserting the consistency of F might prove to be inequivalent within F, with some even being provable. For instance, first-order Peano arithmetic (PA) is capable of demonstrating the consistency of "the largest consistent subset of PA." However, given that PA itself is consistent, its largest consistent subset is, by definition, PA itself; thus, in this specific interpretation, PA "proves its own consistency." Crucially, PA does not prove that its largest consistent subset is, in actuality, the entirety of PA. (Here, "largest consistent subset of PA" refers to the maximal consistent initial segment of PA's axioms, as determined by a specific effective enumeration.)

The Hilbert–Bernays Provability Conditions

The conventional demonstration of the second incompleteness theorem posits that the provability predicate Prov_A(P) adheres to the Hilbert–Bernays provability conditions. With #(P) denoting the Gödel number corresponding to a formula P, these provability conditions stipulate the following:

1. Should F establish a proof for P, it then follows that F proves Prov_A(#(P)).
2. F establishes the first Hilbert-Bernays condition, specifically demonstrating that F proves Prov_A(#(P)) → Prov_A(#(Prov_A(#(P)))).
3. F also proves the second Hilbert-Bernays condition, which is an analogue of modus ponens: Prov_A(#(P → Q)) ∧ Prov_A(#(P)) → Prov_A(#(Q)).

Certain systems, such as Robinson arithmetic, are sufficiently robust to satisfy the premises of the first incompleteness theorem but do not establish the Hilbert–Bernays conditions. Conversely, Peano arithmetic is robust enough to confirm these conditions, a characteristic shared by all theories exceeding Peano arithmetic in strength.

Implications for Consistency Proofs

Gödel's second incompleteness theorem further establishes that a system F§34§, provided it meets the previously delineated technical conditions, cannot prove the consistency of any system F§910§ that itself proves the consistency of F§1516§. The rationale for this is that such a system F§2122§ can demonstrate that if F§2728§ proves the consistency of F§3334§, then F§3940§ is demonstrably consistent. The assertion that F§4546§ is consistent is formally expressed as "for all numbers n, n possesses the decidable property of not being a code for a proof of contradiction in F§5556§." If F§6162§ were actually inconsistent, then F§6768§ would establish, for a specific n, that n represents the code of a contradiction within F§7778§. However, if F§8384§ were also to prove the consistency of F§8990§ (i.e., the non-existence of such an n), then F§8384§ would inherently be inconsistent. This line of reasoning can be formally articulated in F§9798§ to show that if F§103104§ is consistent, then F§109110§ is consistent. Since, by the second incompleteness theorem, F§115116§ does not establish its own consistency, it is similarly unable to establish the consistency of F§121122§.

This corollary of the second incompleteness theorem demonstrates the impossibility of establishing the consistency of Peano arithmetic, for instance, through any finitistic methods formalizable within a system whose consistency is demonstrable within Peano arithmetic (PA). For example, the system of primitive recursive arithmetic (PRA), broadly recognized as a precise formalization of finitistic mathematics, can be demonstrably proven consistent within PA. Consequently, PRA is incapable of establishing the consistency of PA. This observation is widely interpreted as implying that Hilbert's program, which sought to validate the application of "ideal" (infinitistic) mathematical principles in the derivation of "real" (finitistic) mathematical statements by providing a finitistic proof of the consistency of these ideal principles, is ultimately unattainable.

The corollary also underscores the epistemological significance of the second incompleteness theorem. Such a demonstration would yield no substantive insight if a system F proved its own consistency. This is attributable to the fact that inconsistent theories are capable of proving all statements, including their own consistency. Thus, a consistency proof of F within F would offer no indication regarding the consistency of F; no uncertainties about the consistency of F would be alleviated by such a consistency proof. The primary value of consistency proofs resides in the potential to establish the consistency of a system F within a system F' that is, in some respect, less questionable than F itself, for instance, a system demonstrably weaker than F. For many commonly encountered theories F and F', such as F = Zermelo–Fraenkel set theory and F' = primitive recursive arithmetic, the consistency of F' is demonstrable within F. Consequently, F' cannot establish the consistency of F, as dictated by the aforementioned corollary of the second incompleteness theorem.

The second incompleteness theorem does not entirely preclude the possibility of proving the consistency of a different system with alternative axioms. For example, Gerhard Gentzen established the consistency of Peano arithmetic within an alternative system incorporating an axiom that posits the well-foundedness of the ordinal designated as ε§34§. Gentzen's theorem catalyzed the advancement of ordinal analysis in proof theory.

Examples of Undecidable Statements

The term 'undecidable' possesses two distinct interpretations within the fields of mathematics and computer science. The first, a proof-theoretic sense, is employed in the context of Gödel's theorems, denoting a statement that is neither provable nor refutable within a specified deductive system. The second interpretation, which will not be elaborated upon here, relates to computability theory. This latter sense applies not to statements but to decision problems, which are defined as countably infinite collections of questions, each requiring a binary (yes or no) answer. A problem is classified as undecidable if no computable function can correctly resolve every question within its designated set.

Given the dual interpretations of the term 'undecidable,' the descriptor 'independent' is occasionally employed as an alternative, specifically to denote the 'neither provable nor refutable' sense.

The undecidability of a statement within a specific deductive system does not inherently address whether the statement's truth value is well-defined or ascertainable through alternative means. Rather, undecidability solely signifies that the particular deductive system under consideration cannot establish the truth or falsity of the statement. The existence of so-called 'absolutely undecidable' statements, whose truth value can never be ascertained or is ill-specified, remains a contentious issue within the philosophy of mathematics.

The collaborative research of Gödel and Paul Cohen has yielded two concrete examples of undecidable statements, interpreted in the first sense of the term. Specifically, the continuum hypothesis is neither provable nor refutable within ZFC, the standard axiomatization of set theory. Concurrently, the axiom of choice is neither provable nor refutable within ZF, which encompasses all ZFC axioms except the axiom of choice. These particular results do not rely on the incompleteness theorem. Gödel demonstrated in 1940 that neither of these statements could be disproved within ZF or ZFC set theory. Subsequently, in the 1960s, Cohen proved that neither statement is provable from ZF, and furthermore, the continuum hypothesis cannot be proved from ZFC.

Shelah (1974) established that the Whitehead problem, a concept within group theory, is undecidable—in the first sense of the term—within the framework of standard set theory.

Gregory Chaitin formulated undecidable statements within algorithmic information theory and, in this domain, proved an additional incompleteness theorem. Chaitin's incompleteness theorem asserts that for any system capable of representing a sufficient amount of arithmetic, an upper bound c exists, such that no specific number can be proven within that system to possess a Kolmogorov complexity exceeding c. While Gödel's theorem is associated with the liar paradox, Chaitin's result is connected to Berry's paradox.

Undecidable Statements Provable in More Comprehensive Systems

These statements serve as natural mathematical equivalents to Gödel's 'true but undecidable' sentence. While they can be proven within a more extensive system, generally accepted as a valid form of reasoning, they remain undecidable in a more limited system, such as Peano Arithmetic.

In 1977, Paris and Harrington demonstrated that the Paris–Harrington principle, a variant of the infinite Ramsey theorem, is undecidable within (first-order) Peano arithmetic, yet is provable in the more robust system of second-order arithmetic. Subsequently, Kirby and Paris showed that Goodstein's theorem, a statement concerning sequences of natural numbers that is somewhat simpler than the Paris–Harrington principle, is also undecidable in Peano arithmetic.

Kruskal's tree theorem, which possesses applications in computer science, is also undecidable from Peano arithmetic but provable within set theory. In fact, Kruskal's tree theorem (or its finite form) is undecidable even in the considerably stronger system ATR₀, which codifies principles deemed acceptable under the philosophy of mathematics known as predicativism. The related, but more generalized, graph minor theorem (2003) has significant consequences for computational complexity theory.

Relationship to Computability

The incompleteness theorem is intimately connected to several findings regarding undecidable sets within recursion theory.

Kleene (1943) demonstrated a proof of Gödel's incompleteness theorem, leveraging fundamental principles from computability theory. A key finding in this domain establishes the undecidability of the halting problem, meaning no computational algorithm can accurately ascertain whether a given program P will ultimately terminate when executed with a specific input. Kleene's argument posited that if a complete and effective arithmetical system possessing specific consistency attributes were to exist, it would necessitate the halting problem being decidable, which is a logical inconsistency. This particular proof methodology has also been articulated by Shoenfield (1967), Charlesworth (1981), and Hopcroft & Ullman (1979).

Franzén (2005) elucidates how Matiyasevich's resolution of Hilbert's 10th problem can be employed to construct a proof for Gödel's first incompleteness theorem. Matiyasevich established that no algorithm exists which, when provided with a multivariate polynomial p(x§56§, x§910§,...,x_k) having integer coefficients, can ascertain the existence of an integer solution to the equation p = 0. Given that integer-coefficient polynomials and integers are directly representable within the language of arithmetic, any sufficiently robust arithmetical system T would prove the existence of a solution if a multivariate integer polynomial equation p = 0 indeed possesses one in the integers. Furthermore, assuming the system T exhibits ω-consistency, it would never assert that a specific polynomial equation has a solution when no integer solution exists. Consequently, if T were both complete and ω-consistent, one could algorithmically determine whether a polynomial equation has a solution by simply enumerating the proofs within T until either "p has a solution" or "p has no solution" is discovered, which directly contradicts Matiyasevich's theorem. Therefore, it is deduced that T cannot simultaneously be ω-consistent and complete. Additionally, for every consistent, effectively generated system T, it is feasible to effectively construct a multivariate polynomial p over the integers such that the equation p = 0 has no integer solutions, yet this absence of solutions cannot be demonstrated within T.

Smoryński (1977) illustrates how the presence of recursively inseparable sets can be utilized to establish the first incompleteness theorem. This demonstration is frequently expanded to reveal that systems like Peano arithmetic are fundamentally undecidable.

Chaitin's incompleteness theorem offers an alternative approach for generating independent statements, grounded in Kolmogorov complexity. Similar to Kleene's previously discussed proof, Chaitin's theorem is exclusively pertinent to theories characterized by the additional condition that all their axioms hold true within the standard model of natural numbers. Gödel's incompleteness theorem, however, is notable for its applicability to consistent theories that may still contain false assertions in the standard model; such theories are termed ω-inconsistent.

Outline of the Proof for the First Theorem

The proof, structured as a reductio ad absurdum, comprises three fundamental components. Initially, a formal system must be selected that satisfies the stipulated criteria:

1. Within the system, statements are representable by natural numbers, referred to as Gödel numbers. This representation is crucial because the attributes of statements, including their veracity or falsity, become equivalent to ascertaining specific properties of their corresponding Gödel numbers. Consequently, statement properties can be elucidated through an analysis of their Gödel numbers. This stage culminates in the formulation of an expression that conveys the concept that "statement S is provable within the system", a concept applicable to any statement "S" within that system.
2. Within the formal system, it is feasible to construct a number whose corresponding statement, upon interpretation, exhibits self-referentiality, fundamentally asserting its own unprovability. This is achieved through a method known as "diagonalization," a term derived from its conceptual roots in Cantor's diagonal argument.
3. This statement, when situated within the formal system, allows for a demonstration that it is neither provable nor disprovable within that system, thereby indicating that the system cannot, in actuality, be ω-consistent. Consequently, the initial premise that the proposed system fulfilled the specified criteria is invalidated.

Arithmetization of Syntax

The primary challenge in elaborating the aforementioned proof lies in the initial appearance that constructing a statement p, which asserts "p cannot be proved," would necessitate p to incorporate a self-reference to p, potentially leading to an infinite regress. Gödel's methodology resolves this by demonstrating that statements can be correlated with numbers—a process termed the arithmetization of syntax—thereby enabling the substitution of "proving a statement" with "testing whether a number possesses a specified property". This approach facilitates the construction of a self-referential formula without incurring an infinite regress of definitions. Alan Turing subsequently employed this identical technique in his research concerning the Entscheidungsproblem.

A mechanism can be established wherein each formula or statement expressible within the system is assigned a unique Gödel number, allowing for a mechanical bidirectional conversion between formulas and their corresponding Gödel numbers. Although these numbers may possess considerable length in terms of digits, this characteristic does not impede the process; the crucial aspect is their constructibility. An illustrative example involves the representation of English text as a numerical sequence for each letter, subsequently consolidated into a singular, larger number:

The term

• "hello" is encoded as 104-101-108-108-111 using ASCII, which can then be transformed into the composite number 104101108108111.
• The logical proposition x=y => y=x is represented in ASCII as 120-061-121-032-061-062-032-121-061-120, which can be subsequently converted into the numerical value 120061121032061062032121061120.

Fundamentally, demonstrating the truth or falsity of a statement can be shown to be analogous to proving whether its corresponding Gödel number possesses or lacks a specific property. Given that the formal system is sufficiently robust to facilitate reasoning concerning numbers in general, it is also capable of reasoning about numbers that symbolize formulae and statements. Critically, since the system can accommodate reasoning about properties of numbers, the derived conclusions are equivalent to inferences regarding the provability of their corresponding statements.

Developing a Statement Pertaining to "Provability"

Following the demonstration that the system can, in essence, indirectly articulate statements concerning provability, an analysis of the properties of numbers representing these statements enables the construction of a statement that directly achieves this function.

A formula F(x), characterized by the presence of precisely one free variable x, is designated as a statement form or class-sign. Upon the substitution of x with a specific numerical value, the statement form transforms into a bona fide statement, which is then either provable or unprovable within the system. For particular formulas, it can be demonstrated that for every natural number n, the expression ⁠${\displaystyle F(n)}$⁠ holds true if and only if it is provable (the exact condition in the original proof is less stringent, but this simplification is adequate for a proof sketch). This principle applies specifically to any arithmetic operation involving a finite set of natural numbers, such as "2 × 3 = 6".

Statement forms, by their nature, are not propositions and consequently cannot be subjected to proof or disproof. Nevertheless, each statement form F(x) can be allocated a Gödel number, symbolized as G(F). The specific selection of the free variable within the form F(x) does not influence the assignment of its Gödel number G(F).

The concept of provability itself can similarly be encoded using Gödel numbers through the following mechanism: given that a proof constitutes an ordered sequence of statements adhering to specific rules, a Gödel number for a proof can be established. Subsequently, for any given statement p, one can inquire whether a number x represents the Gödel number of its proof. The relationship between the Gödel number of p and x (the potential Gödel number of its proof) constitutes an arithmetical relation between these two numerical values. Consequently, a statement form Bew(y) exists, which leverages this arithmetical relation to assert the existence of a Gödel number corresponding to a proof of y.

The formula Bew(y) is defined as existing x such that y represents the Gödel number of a formula, and x represents the Gödel number of a proof for the formula encoded by y.

The designation Bew is an abbreviation for beweisbar, the German term for "provable," which Gödel initially employed to signify the aforementioned provability formula. It is crucial to note that "Bew(y)" functions solely as a shorthand for a specific, extensive formula within the original language of T; the literal string "Bew" is not asserted to be an element of this language.

A significant characteristic of the formula Bew(y) is that the provability of a statement p within the system implies the provability of Bew(G(p)). This implication arises because any proof of p possesses a unique Gödel number, and the existence of this number satisfies the condition for Bew(G(p)).

Diagonalization

The subsequent phase of the proof involves deriving a statement that implicitly declares its own unprovability. While Gödel directly formulated this statement, the existence of at least one such assertion is a consequence of the diagonal lemma. This lemma posits that for any sufficiently robust formal system and any statement form F, there exists a statement p for which the system demonstrates

p ↔ F(G(p)).

By defining F as the negation of Bew(x), the following theorem is derived:

p ↔ ~Bew(G(p))

The statement p, as defined by this equivalence, approximately asserts that its own Gödel number corresponds to the Gödel number of an unprovable formula.

The statement p is not directly equivalent to ~Bew(G(p)). Instead, p posits that executing a specific calculation will yield a Gödel number corresponding to an unprovable statement. However, upon performing this calculation, the resultant Gödel number is revealed to be that of p itself. This phenomenon parallels the following English sentence:

", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable.

This sentence does not explicitly refer to itself; however, when the specified transformation is applied, the original sentence is produced, thereby causing it to indirectly assert its own unprovability. The demonstration of the diagonal lemma utilizes an analogous methodology.

Subsequently, assuming the axiomatic system is ω-consistent, let p represent the statement derived in the preceding section.

If p were provable, then Bew(G(p)) would also be provable, as previously established. However, p asserts the negation of Bew(G(p)). Consequently, the system would exhibit inconsistency by proving both a statement and its negation. This inherent contradiction demonstrates that p cannot be provable.

If the negation of p were provable, then Bew(G(p)) would also be provable, given that p was constructed to be equivalent to the negation of Bew(G(p)). Nevertheless, for any specific number x, x cannot represent the Gödel number of the proof for p, as p is not provable, as established in the preceding paragraph. Consequently, the system would simultaneously prove the existence of a number possessing a particular property (being the Gödel number of the proof of p) while also proving, for every specific number x, that it lacks this property. Such a contradiction is impossible within an ω-consistent system. Therefore, the negation of p is not provable.

Consequently, the statement p is undecidable within the axiomatic system, meaning it can neither be formally proven nor disproven internally.

Demonstrating that p is not provable merely necessitates the assumption of system consistency. The more stringent assumption of ω-consistency is essential to establish the unprovability of the negation of p. Therefore, if p is formulated for a specific system:

• Should the system be ω-consistent, it is incapable of proving either p or its negation, rendering p undecidable.
• If the system is merely consistent, it might exhibit the same scenario, or it could potentially prove the negation of p. In the latter instance, a statement ("not p") would be both false and provable, indicating that the system is not ω-consistent.

If attempts are made to supplement a system with "missing axioms" to address its incompleteness, either p or "not p" must be incorporated as axioms. This modification, however, alters the definition of "being a Gödel number of a proof" for a given statement, consequently changing the formula Bew(x). Applying the diagonal lemma to this revised `Bew` then yields a new statement, p, distinct from its predecessor, which will remain undecidable within the augmented system, provided it maintains ω-consistency.

Demonstration Utilizing Berry's Paradox

Boolos (1989) outlined an alternative demonstration of the first incompleteness theorem, employing Berry's paradox instead of the liar paradox to formulate a statement that is true yet unprovable. Saul Kripke independently developed a comparable proof methodology. Boolos's approach involves constructing, for any computably enumerable set S of true arithmetic sentences, an additional sentence that is true but not a member of S. This construction yields the first incompleteness theorem as a direct consequence. Boolos posited that this proof holds significance due to its presentation of a "different sort of reason" for the inherent incompleteness observed in effective, consistent theories of arithmetic.

Computationally Verified Proofs

The incompleteness theorems represent a select group of non-trivial mathematical propositions that have been successfully formalized, enabling their complete verification through proof assistant software. Gödel's initial demonstrations of these theorems, consistent with the majority of mathematical proofs, were articulated in natural language for human comprehension.

Computationally verified proofs for various iterations of the first incompleteness theorem have been reported: Natarajan Shankar in 1986 utilizing Nqthm (Shankar 1994), Russell O'Connor in 2003 employing Rocq (formerly designated as Coq) (O'Connor 2005), and John Harrison in 2009 with HOL Light (Harrison 2009). Furthermore, Lawrence Paulson announced a computer-verified proof encompassing both incompleteness theorems in 2013, using Isabelle (Paulson 2014).

Outline of the Second Theorem's Proof

The primary challenge in demonstrating the second incompleteness theorem lies in establishing that the various principles of provability, integral to the first incompleteness theorem's proof, can be formally expressed within a system S through a formal predicate P representing provability. Upon achieving this formalization, the second incompleteness theorem is derived by formalizing the entirety of the first incompleteness theorem's proof within the system S itself.

Let p denote the previously constructed undecidable sentence. For the purpose of deriving a contradiction, assume that the consistency of system S is demonstrable from within system S itself. This assumption is equivalent to proving the assertion "System S is consistent." Subsequently, consider the statement c, defined as c = "If system S is consistent, then p is not provable." The demonstration of sentence c can be formalized within system S, thereby allowing the statement c, "p is not provable" (or equivalently, "not P(p)"), to be proven within system S.

It follows that if the consistency of system S can be established (i.e., the statement within the hypothesis of c), then p is demonstrated to be unprovable. However, this leads to a contradiction, as the First Incompleteness Theorem dictates that this very sentence (specifically, what is implied by c, ""p" is not provable") is precisely what is constructed to be unprovable. This necessity underscores the requirement for formalizing the First Incompleteness Theorem within S: to prove the Second Incompleteness Theorem, a contradiction with the First Incompleteness Theorem is required, achievable only by demonstrating its validity within S. Consequently, the consistency of system S cannot be proven, from which the assertion of the Second Incompleteness Theorem directly ensues.

Analysis and Ramifications

The findings regarding incompleteness significantly influence the philosophy of mathematics, especially formalist perspectives that rely on a singular system of formal logic to delineate their foundational principles.

Implications for Logicism and Hilbert's Second Problem

Gödel's incompleteness theorems are occasionally considered to pose significant challenges to the logicist program, advanced by Gottlob Frege and Bertrand Russell, which sought to establish natural numbers through logical principles. However, Bob Hale and Crispin Wright contend that these theorems do not undermine logicism, given their applicability to both first-order logic and arithmetic. They assert that this issue primarily concerns individuals who posit that natural numbers must be defined exclusively within first-order logic.

Numerous logicians maintain that Gödel's incompleteness theorems delivered a decisive setback to David Hilbert's second problem, which sought a finitary consistency proof for mathematics. Specifically, the second incompleteness theorem is frequently interpreted as rendering this problem intractable. Nevertheless, this interpretation is not universally accepted among mathematicians, and the definitive status of Hilbert's second problem remains unresolved.

Minds and Machines

Scholars, including philosopher J. R. Lucas and physicist Roger Penrose, have extensively discussed the potential implications of Gödel's incompleteness theorems for human intelligence. A central aspect of this discourse revolves around whether the human mind can be considered equivalent to a Turing machine, or, by extension of the Church–Turing thesis, any finite computational device. Should this equivalence hold, and assuming the machine's consistency, Gödel's incompleteness theorems would then be applicable.

Putnam (1960) proposed that although Gödel's theorems are inapplicable to individual humans due to their fallibility and inherent inconsistency, they might be relevant to the broader human capacity for science or mathematics. Under the assumption of its consistency, either its consistency remains unprovable, or it cannot be adequately represented by a Turing machine.

Wigderson (2010) has advanced the proposition that the notion of mathematical "knowability" ought to be grounded in computational complexity rather than solely on logical decidability. He asserts that "when knowability is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us."

In his works Gödel, Escher, Bach and I Am a Strange Loop, Douglas Hofstadter references Gödel's theorems as an illustration of what he terms a strange loop—a hierarchical, self-referential construct inherent within an axiomatic formal system. He posits that this structural characteristic is analogous to that which engenders consciousness, specifically the subjective sense of "I," within the human psyche. Whereas the self-reference in Gödel's theorem originates from the Gödel sentence asserting its own unprovability within the formal system of Principia Mathematica, the self-reference in the human mind arises from the brain's process of abstracting and categorizing stimuli into "symbols"—or neuronal groups responsive to concepts—within what functions as a formal system, ultimately generating symbols that model the perceiving entity itself. Hofstadter further contends that a strange loop within a sufficiently intricate formal system can produce "downward" or "upside-down" causality, a scenario where the conventional hierarchy of cause-and-effect is inverted. Regarding Gödel's theorem, this phenomenon is concisely exemplified as follows:

Merely from knowing the formula's meaning, one can infer its truth or falsity without any effort to derive it in the old-fashioned way, which requires one to trudge methodically "upwards" from the axioms. This is not just peculiar; it is astonishing. Normally, one cannot merely look at what a mathematical conjecture says and simply appeal to the content of that statement on its own to deduce whether the statement is true or false.

For the mind, which constitutes a significantly more intricate formal system, this "downward causality" is perceived by Hofstadter as the ineffable human intuition that mental causation resides at the higher level of desires, concepts, personalities, thoughts, and ideas, rather than at the lower level of neuronal interactions or even fundamental particles, despite physics attributing causal power to the latter.

There is thus a curious upside-downness to our normal human way of perceiving the world: we are built to perceive “big stuff” rather than “small stuff”, even though the domain of the tiny seems to be where the actual motors driving reality reside.

Paraconsistent Logic

While Gödel's theorems are typically examined within the framework of classical logic, they also contribute to the investigation of paraconsistent logic and intrinsically contradictory propositions, known as dialetheia. Priest (1984, 2006) contends that substituting the concept of formal proof in Gödel's theorem with the conventional understanding of informal proof can demonstrate the inconsistency of naive mathematics, thereby supporting dialetheism. This inconsistency arises from incorporating a truth predicate for a system directly into the system's own language. Shapiro (2002) offers a more nuanced evaluation of Gödel's theorems' relevance to dialetheism.

Extramathematical Applications of the Incompleteness Theorems

The incompleteness theorems are occasionally invoked through appeals and analogies to substantiate arguments extending beyond the domains of mathematics and logic. However, numerous scholars, including Franzén (2005), Raatikainen (2005), Sokal & Bricmont (1999), and Stangroom & Benson (2006), have critically assessed such broad applications and interpretations. For instance, Sokal & Bricmont (1999) and Stangroom & Benson (2006) cite Rebecca Goldstein's observations regarding the discrepancy between Gödel's explicit Platonism and the anti-realist appropriations of his concepts. Sokal & Bricmont (1999) specifically critique Régis Debray's application of the theorem within a sociological framework, a usage Debray has subsequently defended as metaphorical (ibid.).

Historical Context

Following the publication of his doctoral thesis in 1929, which presented the proof of the completeness theorem, Gödel subsequently addressed a distinct problem for his habilitation. His initial objective was to achieve an affirmative resolution to Hilbert's second problem. During that era, theoretical frameworks encompassing natural and real numbers, akin to second-order arithmetic, were designated as "analysis," whereas theories exclusively concerning natural numbers were termed "arithmetic."

Gödel was not the sole researcher engaged with the consistency problem. In 1925, Ackermann had presented a flawed consistency proof for analysis, endeavoring to employ Hilbert's original method of ε-substitution. Later that same year, von Neumann successfully rectified this proof for an arithmetic system devoid of induction axioms. By 1928, Ackermann had conveyed a revised proof to Bernays, prompting Hilbert to declare in 1929 his conviction that arithmetic's consistency had been established and that a consistent proof for analysis would soon emerge. However, subsequent to the publication of the incompleteness theorems, which revealed the inherent error in Ackermann's revised proof, von Neumann furnished a specific instance demonstrating the fundamental unsoundness of its primary technique.

During his investigations, Gödel ascertained that while a statement asserting its own falsehood results in a paradox, a statement affirming its unprovability does not. Specifically, Gödel was cognizant of the finding subsequently termed Tarski's indefinability theorem, despite never formally publishing it. On August 26, 1930, Gödel disclosed his first incompleteness theorem to Carnap, Feigel, and Waismann; all four individuals were scheduled to participate in the Second Conference on the Epistemology of the Exact Sciences, a significant gathering held in Königsberg the subsequent week.

Formal Presentation

The Königsberg conference of 1930 constituted a collaborative assembly of three academic societies, attracting many prominent logicians of that era. Carnap, Heyting, and von Neumann each presented one-hour lectures on the mathematical philosophies of logicism, intuitionism, and formalism, respectively. The conference program also featured Hilbert's valedictory address, delivered upon his departure from the University of Göttingen. In his speech, Hilbert articulated his conviction that all mathematical problems are amenable to solution, concluding his address with the statement:

For the mathematician there is no Ignorabimus, and, in my opinion, not at all for natural science either. ... The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is no unsolvable problem. In contrast to the foolish Ignorabimus, our credo avers: We must know. We shall know!

This address rapidly gained recognition as a concise encapsulation of Hilbert's philosophical stance on mathematics; its concluding six words, "Wir müssen wissen. Wir werden wissen!," were later inscribed as his epitaph in 1943. Despite Gödel's probable presence at Hilbert's address, the two scholars never had a personal encounter.

Gödel presented his initial incompleteness theorem during a roundtable discussion on the conference's third day. This revelation garnered minimal attention, except from von Neumann, who engaged Gödel in a private discussion. Subsequently, in the same year, von Neumann independently derived a proof for the second incompleteness theorem, building upon his understanding of the first. He communicated this discovery to Gödel via a letter dated November 20, 1930. Concurrently, Gödel had independently established the second incompleteness theorem and incorporated it into his manuscript, which was submitted to Monatshefte für Mathematik on November 17, 1930.

Gödel's seminal paper, titled "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" (translated as "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I"), was published in Monatshefte in 1931. The title suggests Gödel's initial intention to release a second installment of the paper in a subsequent volume of the Monatshefte; however, the rapid acceptance of the first publication prompted a revision of his original plans.

Generalization and Acceptance

Between 1933 and 1934, Gödel delivered a series of lectures on his theorems at Princeton, attended by notable figures such as Church, Kleene, and Rosser. During this period, Gödel recognized that a crucial prerequisite for his theorems was the system's effectiveness, then referred to as "general recursive." In 1936, Rosser demonstrated that the ω-consistency hypothesis, a fundamental component of Gödel's initial proof, could be substituted with simple consistency, provided the Gödel sentence was suitably modified. These advancements refined the incompleteness theorems into their contemporary formulation.

Gentzen presented his consistency proof for first-order arithmetic in 1936. Hilbert deemed this proof "finitary," despite the fact that, as Gödel's theorem had previously established, it cannot be formally expressed within the arithmetic system it aims to prove consistent.

The profound implications of the incompleteness theorems for Hilbert's program were rapidly acknowledged. In 1939, Bernays incorporated a comprehensive proof of the incompleteness theorems into the second volume of Grundlagen der Mathematik. This volume also featured Ackermann's supplementary findings on the ε-substitution method and Gentzen's consistency proof for arithmetic, marking the inaugural complete published demonstration of the second incompleteness theorem.

Criticisms

Finsler

In 1926, Finsler employed a variant of Richard's paradox to formulate an expression that was demonstrably false yet unprovable within a specific, informal framework he had devised. Gödel was not cognizant of this publication when he established his incompleteness theorems (Collected Works Vol. IV., p. 9). In 1931, Finsler corresponded with Gödel to apprise him of this paper, asserting its priority regarding an incompleteness theorem. Finsler's methodology, however, did not depend on formalized provability and bore only a superficial resemblance to Gödel's contributions. Gödel reviewed the paper but identified significant deficiencies, articulating his concerns about the absence of formalization in his reply to Finsler. Throughout his subsequent career, Finsler persistently advocated for his philosophy of mathematics, which deliberately avoided formalization.

Zermelo

In September 1931, Ernst Zermelo communicated with Gödel, identifying what he termed an "essential gap" in Gödel's reasoning. Gödel responded in October with a ten-page letter, clarifying that Zermelo's premise—that the concept of truth within a system is definable by that same system—was erroneous, a point generally refuted by Tarski's undefinability theorem. Nevertheless, Zermelo persisted, publishing his critiques, which included "a rather scathing paragraph on his young competitor." Gödel, with Carnap's concurrence, concluded that further engagement on the matter would be unproductive. A significant portion of Zermelo's later research focused on logics more robust than first-order logic, through which he aimed to demonstrate both the consistency and categoricity of mathematical theories.

Wittgenstein

Ludwig Wittgenstein's posthumously published 1953 work, Remarks on the Foundations of Mathematics, contains several passages discussing the incompleteness theorems. One particular section, often referred to as the "notorious paragraph," suggests a potential conflation of "true" and "provable" within Russell's system. Gödel was associated with the Vienna Circle when Wittgenstein's early philosophy, particularly *Tractatus Logico-Philosophicus*, significantly influenced the group's intellectual discourse. Debate has arisen regarding whether Wittgenstein genuinely misunderstood the incompleteness theorem or merely articulated his thoughts ambiguously. Gödel's posthumous papers indicate his belief that Wittgenstein misinterpreted his concepts.

Numerous commentators have interpreted Wittgenstein as having misunderstood Gödel's work. However, alternative readings by Floyd & Putnam (2000) and Priest (2004) contend that much of this commentary misinterprets Wittgenstein's actual position. Upon their initial publication, Bernays, Dummett, and Kreisel each authored highly critical reviews of Wittgenstein's remarks. The unanimous negative reception ensured that Wittgenstein's observations on the incompleteness theorems had minimal impact within the logic community. In 1972, Gödel explicitly stated, "Has Wittgenstein lost his mind? Does he mean it seriously? He intentionally utters trivially nonsensical statements," and communicated to Karl Menger that Wittgenstein's comments demonstrated a fundamental misunderstanding of the incompleteness theorems.

It is clear from the passages you cite that Wittgenstein did not understand [the first incompleteness theorem] (or pretended not to understand it). He interpreted it as a kind of logical paradox, while in fact is just the opposite, namely a mathematical theorem within an absolutely uncontroversial part of mathematics (finitary number theory or combinatorics).

The publication of Wittgenstein's Nachlass in 2000 initiated a series of philosophical papers evaluating the justification of the initial criticisms leveled against his remarks. Floyd & Putnam (2000) argue that Wittgenstein possessed a more comprehensive grasp of the incompleteness theorem than previously acknowledged. Their analysis particularly focuses on the interpretation of a Gödel sentence for an ω-inconsistent system as stating "I am not provable," given that such a system lacks models where the provability predicate accurately reflects actual provability. Conversely, Rodych (2003) asserts that their interpretation of Wittgenstein lacks historical substantiation. Berto (2009) investigates the connections between Wittgenstein's writings and theories of paraconsistent logic.

References

Articles by Gödel

• Kurt Gödel, 1931, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I", *Monatshefte für Mathematik und Physik*, v. 38 n. 1, pp. 173–198. doi:10.1007/BF01700692
• —, 1931, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I", in Solomon Feferman, ed., 1986. Kurt Gödel Collected Works, Vol. I. Oxford University Press, pp. 144–195. ISBN 978-0195147209. This volume presents the original German text with a facing English translation, preceded by an introductory note from Stephen Cole Kleene.
• —, 1951, "Some Basic Theorems on the Foundations of Mathematics and Their Implications", in Solomon Feferman, ed., 1995. Kurt Gödel Collected Works, Vol. III, Oxford University Press, pp. 304–323. ISBN 978-0195147223.

Translations, during his lifetime, of Gödel's paper into English

The subsequent translations exhibit discrepancies in both wording and typographical presentation. Typographical accuracy is crucial, as Gödel explicitly intended to highlight "those metamathematical notions that had been defined in their usual sense before . . ." (van Heijenoort 1967, p. 595). Three distinct translations are available. Regarding the initial translation, John Dawson noted its significant deficiencies and the "devastating review" it received in the Journal of Symbolic Logic. Furthermore, Gödel himself expressed dissatisfaction with Braithwaite's accompanying commentary (Dawson 1997, p. 216). This Meltzer translation was subsequently superseded by an improved version, prepared by Elliott Mendelson for Martin Davis's anthology, The Undecidable. Although Mendelson considered this translation "not quite so good" as anticipated, he consented to its publication due to time constraints (ibid). Dawson's footnote indicates that Mendelson later regretted this decision, as the published volume was compromised by poor typography and numerous errors (ibid). Dawson further confirms that Gödel preferred the translation produced by Jean van Heijenoort (ibid). An additional version, valuable for advanced students, comprises lecture notes transcribed by Stephen Kleene and J. B. Rosser. These notes document lectures delivered by Gödel at the Institute for Advanced Study in the spring of 1934 (cf. commentary by Davis 1965, p. 39 and beginning on p. 41). This particular rendition is titled "On Undecidable Propositions of Formal Mathematical Systems." The following are listed in chronological order of publication:

• Meltzer, B. (Translator) and Braithwaite, R. B. (Introduction). (1962). On Formally Undecidable Propositions of Principia Mathematica and Related Systems. Dover Publications, New York (Dover edition, 1992). ISBN 0-486-66980-7 (paperback). This edition includes a helpful translation of Gödel's German abbreviations on pages 33–34. However, as previously indicated, the typography, translation, and commentary in this volume are considered unreliable. Regrettably, this translation, including its questionable content, was subsequently reprinted by:

Hawking, S. (Editor). (2005). God Created the Integers: The Mathematical Breakthroughs That Changed History. Running Press, Philadelphia. ISBN 0-7624-1922-9. Gödel's paper commences on page 1097, preceded by Hawking's commentary beginning on page 1089.

• Davis, M. (Editor). (1965). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions. Raven Press, New York. (No ISBN). Gödel's paper starts on page 5, following a single page of editorial commentary.
• van Heijenoort, J. (Editor). (1967). (3rd edition). From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, Cambridge, Massachusetts. ISBN 0-674-32449-8 (paperback). Van Heijenoort was responsible for the translation. He noted that "Professor Gödel approved the translation, which in many places was accommodated to his wishes" (p. 595). Gödel's paper commences on page 595, with van Heijenoort's commentary preceding it on page 592.
• Davis, M. (Editor). (1965). (Ibid). "On Undecidable Propositions of Formal Mathematical Systems." This edition presents a version incorporating Gödel's errata corrections and additional notes, commencing on page 41, following two pages of commentary by Davis. Prior to its inclusion in Davis's volume, this lecture was only available as mimeographed notes.

Scholarly Articles by Other Authors

• Boolos, G. (1989). "A New Proof of the Gödel Incompleteness Theorem." Notices of the American Mathematical Society, 36, 388–390, 676. Reprinted in Boolos (1998, pp. 383–388).
• Buldt, B. (2014). "The Scope of Gödel's First Incompleteness Theorem." Logica Universalis, 8, 499–552. doi:10.1007/s11787-014-0107-3.
• Charlesworth, A. (1981). "A Proof of Gödel's Theorem in Terms of Computer Programs." Mathematics Magazine, 54(3), 109–121. doi:10.2307/2689794. JSTOR 2689794..
• Davis, M. (2006). "The Incompleteness Theorem." (PDF). Notices of the AMS, 53(4), 414.Finsler, Paul (1926). "Formale Beweise und die Entscheidbarkeit". Mathematische Zeitschrift, 25, 676–682. doi:10.1007/bf01283861. S2CID 121054124.Grattan-Guinness, Ivor, ed. (2005). Landmark Writings in Western Mathematics 1640-1940. Elsevier. ISBN 9780444508713.van Heijenoort, Jean (1967). "Gödel's Theorem". In Edwards, Paul (ed.), Encyclopedia of Philosophy, Vol. 3, Macmillan, pp. 348–357.Hellman, Geoffrey (1981). "How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism". Noûs, 15 (4 - Special Issue on Philosophy of Mathematics), 451–468. doi:10.2307/2214847. ISSN 0029-4624. JSTOR 2214847.
• Hirzel, Martin (2000). "On formally undecidable propositions of Principia Mathematica and related systems I." This publication provides an English translation of Gödel's original paper, archived on September 16, 2004.
• Kikuchi, Makoto; Tanaka, Kazuyuki (July 1994). "On Formalization of Model-Theoretic Proofs of Gödel's Theorems". Notre Dame Journal of Formal Logic, 35 (3), 403–412. doi:10.1305/ndjfl/1040511346. MR 1326122.Kleene, S. C. (1943). "Recursive predicates and quantifiers". Transactions of the American Mathematical Society, 53 (1), 41–73. doi:10.1090/S0002-9947-1943-0007371-8.Raatikainen, Panu (2020). "Gödel's Incompleteness Theorems". Stanford Encyclopedia of Philosophy. Retrieved November 7, 2022.Raatikainen, Panu (2005). "On the philosophical relevance of Gödel's incompleteness theorems". Revue Internationale de Philosophie, 59 (4), 513–534. doi:10.3917/rip.234.0513. S2CID 52083793.Journal of Symbolic Logic, vol. 1 (1936), pp. 87–91. Reprinted in Martin Davis (1965), The Undecidable (loc. cit.), pp. 230–235.
• Rosser, John Barkley (1939). "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem". Originally published in the Journal of Symbolic Logic, vol. 4 (1939), pp. 53–60. Reprinted in Martin Davis (1965), The Undecidable (loc. cit.), pp. 223–230.
• Smoryński, C. (1977). "The incompleteness theorems". In Jon Barwise (ed.), Handbook of Mathematical Logic. Amsterdam: North-Holland Publishing Co., pp. 821–866. ISBN 978-0-444-86388-1.Willard, Dan E. (2001). "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles". Journal of Symbolic Logic, 66 (2), 536–596. doi:10.2307/2695030. JSTOR 2695030.Zach, Richard (2003). "The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program" (PDF). Synthese, 137 (1), Springer Science and Business Media LLC, 211–259. arXiv:math/0102189. doi:10.1023/a:1026247421383. ISSN 0039-7857. S2CID 16657040.Zach, Richard (2005). "Kurt Gödel, paper on the incompleteness theorems (1931)". In Grattan-Guinness, Ivor (ed.), Landmark Writings in Western Mathematics 1640-1940. Elsevier, pp. 917–925. doi:10.1016/b978-044450871-3/50152-2. ISBN 9780444508713.Books Pertaining to the Theorems
  • Berto, Francesco (2010). There's Something about Gödel: The Complete Guide to the Incompleteness Theorem. John Wiley and Sons.
  • Domeisen, Norbert (1990). Logik der Antinomien. Bern: Peter Lang. 142 pages. ISBN 3-261-04214-1. Zbl 0724.03003.
  • Franzén, Torkel (2005). Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. Wellesley, MA: A K Peters. ISBN 1-56881-238-8. MR 2146326.Smith, Peter (2007). An Introduction to Gödel's Theorems. Cambridge, U.K.: Cambridge University Press. ISBN 978-0-521-67453-9. MR 2384958.
  • Shankar, N. (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge Tracts in Theoretical Computer Science, vol. 38. Cambridge: Cambridge University Press. ISBN 0-521-58533-3.
  • Smullyan, Raymond. 1987. Forever Undecided. ISBN 0192801414. This work presents puzzles based on undecidability in formal systems.
  • Smullyan, Raymond. 1992. Gödel's Incompleteness Theorems. Oxford University Press. ISBN 0195046722.
  • Smullyan, Raymond. 1994. Diagonalization and Self-Reference. Oxford University Press. MR 1318913. ISBN 0198534507.
  • Smullyan, Raymond. 2013. The Gödelian Puzzle Book: Puzzles, Paradoxes and Proofs. Courier Corporation. ISBN 978-0-486-49705-1.
  • Wang, Hao (1996). A Logical Journey: From Gödel to Philosophy. MIT Press. ISBN 0-262-23189-1. MR 1433803.

  Miscellaneous References

  • Berto, Francesco (2009). "The Gödel Paradox and Wittgenstein's Reasons." Philosophia Mathematica, series III, no. 17.
  • Dawson, John W. Jr. (1996). Logical Dilemmas: The Life and Work of Kurt Gödel. Taylor & Francis. ISBN 978-1-56881-025-6.
  • Dawson, John W. Jr. (1997). Logical Dilemmas: The Life and Work of Kurt Gödel. Wellesley, Massachusetts: A. K. Peters. ISBN 978-1-56881-256-4. OCLC 36104240.
  • Goldstein, Rebecca. 2005. Incompleteness: The Proof and Paradox of Kurt Gödel. W. W. Norton & Company. ISBN 0-393-05169-2.
  • Floyd, Juliet, and Hilary Putnam (2000). "A Note on Wittgenstein's 'Notorious Paragraph' about the Gödel Theorem." The Journal of Philosophy, 97 (11): 624–632. doi:10.2307/2678455. ISSN 0022-362X. JSTOR 2678455.
  • Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge: Cambridge University Press. ISBN 978-0521899574.
  • Hilbert, David, and Paul Bernays. Grundlagen der Mathematik. Springer-Verlag.
  • Hopcroft, John E., and Jeffrey Ullman (1979). Introduction to Automata Theory, Languages, and Computation. Reading, Massachusetts: Addison-Wesley. ISBN 0-201-02988-X.
  • Hofstadter, Douglas R. (2007) [originally 2003]. "Chapter 12. On Downward Causality." In I Am a Strange Loop. Basic Books. ISBN 978-0-465-03078-1.
  • Jones, James P. (1980). "Undecidable Diophantine Equations." Bulletin of the American Mathematical Society, §56§ (2): 859–862. doi:10.1090/S0273-0979-1980-14832-6.
  • Kleene, Stephen Cole (1967). "Mathematical Logic." Nature, 216 (5111): 201. Bibcode:1967Natur.216..201G. doi:10.1038/216201b0. Reprinted by Dover, 2002. ISBN 0-486-42533-9.
  • O'Connor, Russell (2005). "Essential Incompleteness of Arithmetic Verified by Coq." In Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 3603, pp. 245–260. arXiv:cs/0505034. doi:10.1007/11541868_16. ISBN 978-3-540-28372-0. S2CID 15610367.
  • Paulson, Lawrence (2014). "A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets." Review of Symbolic Logic, 7 (3): 484–498. arXiv:2104.14260. doi:10.1017/S1755020314000112. S2CID 13913592.
  • Priest, Graham (1984). "Logic of Paradox Revisited." Journal of Philosophical Logic, 13 (2): 153–179. doi:10.1007/BF00453020.
  • Priest, Graham. (2004). "Wittgenstein's Remarks on Gödel's Theorem." In M. Kölbel (Ed.), Wittgenstein's Lasting Significance (pp. 207–227). Psychology Press. ISBN 978-1-134-40617-3.
  • Putnam, Hilary. (1960). "Minds and Machines." In S. Hook (Ed.), Dimensions of Mind: A Symposium. New York University Press.Dialectica, 57(3), 279–313. doi:10.1111/j.1746-8361.2003.tb00272.x.Israel Journal of Mathematics, 18(3), 243–256. doi:10.1007/BF02757281. MR 0357114.Mind, 111(444), 817–32. doi:10.1093/mind/111.444.817.
  • Shoenfield, Joseph R. (1967). Mathematical Logic. Association for Symbolic Logic (published 2001), Natick, MA. ISBN 978-1-56881-135-2.
  • Tourlakis, George. (2003). Lectures in Logic and Set Theory, Volume 1, Mathematical Logic. Cambridge University Press. ISBN 978-0-521-75373-9.
  • Wigderson, Avi. (2010). "The Gödel Phenomena in Mathematics: A Modern View" (PDF). In Kurt Gödel and the Foundations of Mathematics: Horizons of Truth. Cambridge University Press.Philosophy of Logic (Vol. 5 of Handbook of the Philosophy of Science, pp. 411–447). Elsevier, Amsterdam. arXiv:math/0508572. doi:10.1016/b978-044451541-4/50014-2. ISBN 978-0-444-51541-4. OCLC 162131413. S2CID 291599.
    • Godel's Incompleteness Theorems on In Our Time at the BBC
    • Paraconsistent Logic § Arithmetic and Gödel's Theorem entry in the Stanford Encyclopedia of Philosophy.
    • World's shortest explanation of Gödel's theorem using a printing machine as an example.
    • "Gödel incompleteness theorem", Encyclopedia of Mathematics, EMS Press, 2001 [1994]Source: TORIma Academy Archive