Editing Gödel's incompleteness theorems (section)

== Proof sketch for the first theorem ==
{{Main|Proof sketch for Gödel's first incompleteness theorem}}

The [[proof by contradiction]] has three essential parts. To begin, choose a formal system that meets the proposed criteria:

# Statements in the system can be represented by natural numbers (known as Gödel numbers). The significance of this is that properties of statements—such as their truth and falsehood—will be equivalent to determining whether their Gödel numbers have certain properties, and that properties of the statements can therefore be demonstrated by examining their Gödel numbers. This part culminates in the construction of a formula expressing the idea that ''"statement {{mvar|S}} is provable in the system"'' (which can be applied to any statement "{{mvar|S}}" in the system).
# In the formal system it is possible to construct a number whose matching statement, when interpreted, is [[self reference|self-referential]] and essentially says that it (i.e. the statement itself) is unprovable. This is done using a technique called "[[diagonal lemma|diagonalization]]" (so-called because of its origins as [[Cantor's diagonal argument]]).
# Within the formal system this statement permits a demonstration that it is neither provable nor disprovable in the system, and therefore the system cannot in fact be ω-consistent. Hence the original assumption that the proposed system met the criteria is false.

=== Arithmetization of syntax ===

The main problem in fleshing out the proof described above is that it seems at first that to construct a statement {{mvar|p}} that is equivalent to "{{mvar|p}} cannot be proved", {{mvar|p}} would somehow have to contain a reference to {{mvar|p}}, which could easily give rise to an infinite regress. Gödel's technique is to show that statements can be matched with numbers (often called the arithmetization of [[syntax]]) in such a way that ''"proving a statement"'' can be replaced with ''"testing whether a number has a given property"''. This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by [[Alan Turing]] in his work on the ''[[Entscheidungsproblem]]''.

In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its [[Gödel number]], in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers.  The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is how English can be stored as a [[Character encoding|sequence of numbers for each letter]] and then combined into a single larger number:
:* The word '''<code>hello</code>''' is encoded as 104-101-108-108-111 in [[ASCII]], which can be converted into the number 104101108108111.
:* The logical statement '''<code>x=y => y=x</code>''' is encoded as 120-061-121-032-061-062-032-121-061-120 in [[ASCII]], which can be converted into the number 120061121032061062032121061120.

In principle, proving a statement true or false can be shown to be equivalent to proving that the number matching the statement does or does not have a given property. Because the formal system is strong enough to support reasoning about ''numbers in general'', it can support reasoning about ''numbers that represent formulae and statements'' as well. Crucially, because the system can support reasoning about ''properties of numbers'', the results are equivalent to reasoning about ''provability of their equivalent statements''.

=== Construction of a statement about "provability" ===
Having shown that in principle the system can indirectly make statements about provability, by analyzing properties of those numbers representing statements it is now possible to show how to create a statement that actually does this.

A formula {{math|''F''(''x'')}} that contains exactly one free variable {{mvar|x}} is called a ''statement form'' or ''class-sign''. As soon as {{mvar|x}} is replaced by a specific number, the statement form turns into a ''[[bona fide]]'' statement, and it is then either provable in the system, or not. For certain formulas one can show that for every natural number {{mvar|n}}, {{tmath|F(n)}} is true if and only if it can be proved (the precise requirement in the original proof is weaker, but for the proof sketch this will suffice). In particular, this is true for every specific arithmetic operation between a finite number of natural numbers, such as "2{{resx}}3 = 6".

Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form {{math|''F''(''x'')}} can be assigned a Gödel number denoted by {{math|'''G'''(''F'')}}. The choice of the free variable used in the form {{mvar|F}}({{mvar|x}}) is not relevant to the assignment of the Gödel number {{math|'''G'''(''F'')}}.

{{anchor|Bew}}The notion of provability itself can also be encoded by Gödel numbers, in the following way: since a proof is a list of statements which obey certain rules, the Gödel number of a proof can be defined. Now, for every statement {{mvar|p}}, one may ask whether a number {{mvar|x}} is the Gödel number of its proof. The relation between the Gödel number of {{mvar|p}} and {{mvar|x}}, the potential Gödel number of its proof, is an arithmetical relation between two numbers.  Therefore, there is a statement form {{math|''Bew''(''y'')}} that uses this arithmetical relation to state that a Gödel number of a proof of {{mvar|y}} exists:
:{{math|1=''Bew''(''y'') = ∃ ''x''}} ({{mvar|y}} is the Gödel number of a formula and {{mvar|x}} is the Gödel number of a proof of the formula encoded by {{mvar|y}}).

The name '''Bew''' is short for ''beweisbar'', the German word for "provable"; this name was originally used by Gödel to denote the provability formula just described.  Note that "{{math|''Bew''(''y'')}}" is merely an abbreviation that represents a particular, very long, formula in the original language of {{mvar|T}}; the string "{{math|Bew}}" itself is not claimed to be part of this language.

An important feature of the formula {{math|''Bew''(''y'')}} is that if a statement {{mvar|p}} is provable in the system then {{math|''Bew''('''G'''(''p''))}} is also provable. This is because any proof of {{mvar|p}} would have a corresponding Gödel number, the existence of which causes {{math|Bew('''G'''(''p''))}} to be satisfied.

=== Diagonalization ===

The next step in the proof is to obtain a statement which, indirectly, asserts its own unprovability. Although Gödel constructed this statement directly, the existence of at least one such statement follows from the [[diagonal lemma]], which says that for any sufficiently strong formal system and any statement form {{mvar|F}} there is a statement {{mvar|p}} such that the system proves
:{{math|''p'' ↔ ''F''('''G'''(''p''))}}.
By letting {{mvar|F}} be the negation of {{math|''Bew''(''x'')}}, we obtain the theorem
:{{math|''p'' ↔ ~''Bew''('''G'''(''p''))}}
and the {{mvar|p}} defined by this roughly states that its own Gödel number is the Gödel number of an unprovable formula.

The statement {{mvar|p}} is not literally equal to {{math|~''Bew''('''G'''(''p''))}}; rather, {{mvar|p}} states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement. But when this calculation is performed, the resulting Gödel number turns out to be the Gödel number of {{mvar|p}} itself. This is similar to the following sentence in English:
:", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable.
This sentence does not directly refer to itself, but when the stated transformation is made the original sentence is obtained as a result, and thus this sentence indirectly asserts its own unprovability. The proof of the diagonal lemma employs a similar method.

Now, assume that the axiomatic system is [[omega-consistent|ω-consistent]], and let {{mvar|p}} be the statement obtained in the previous section.

If {{mvar|p}} were provable, then {{math|''Bew''('''G'''(''p''))}} would be provable, as argued above. But {{mvar|p}} asserts the negation of {{math|''Bew''('''G'''(''p''))}}. Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that {{mvar|p}} cannot be provable.

If the negation of {{mvar|p}} were provable, then {{math|''Bew''('''G'''(''p''))}} would be provable (because {{mvar|p}} was constructed to be equivalent to the negation of {{math|''Bew''('''G'''(''p''))}}). However, for each specific number {{mvar|x}}, {{mvar|x}} cannot be the Gödel number of the proof of {{mvar|p}}, because {{mvar|p}} is not provable (from the previous paragraph). Thus on one hand the system proves there is a number with a certain property (that it is the Gödel number of the proof of {{mvar|p}}), but on the other hand, for every specific number {{mvar|x}}, we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of {{mvar|p}} is not provable.

Thus the statement {{mvar|p}} is undecidable in our axiomatic system: it can neither be proved nor disproved within the system.

In fact, to show that {{mvar|p}} is not provable only requires the assumption that the system is consistent. The stronger assumption of ω-consistency is required to show that the negation of {{mvar|p}} is not provable. Thus, if {{mvar|p}} is constructed for a particular system:
*If the system is ω-consistent, it can prove neither {{mvar|p}} nor its negation, and so {{mvar|p}} is undecidable.
*If the system is consistent, it may have the same situation, or it may prove the negation of {{mvar|p}}. In the later case, we have a statement ("not {{mvar|p}}") which is false but provable, and the system is not ω-consistent.

If one tries to "add the missing axioms" to avoid the incompleteness of the system, then one has to add either {{mvar|p}} or "not {{mvar|p}}" as axioms. But then the definition of "being a Gödel number of a proof" of a statement changes. which means that the formula {{math|''Bew''(''x'')}} is now different. Thus when we apply the diagonal lemma to this new Bew, we obtain a new statement {{mvar|p}}, different from the previous one, which will be undecidable in the new system if it is ω-consistent.

=== Proof via Berry's paradox ===
{{harvtxt|Boolos|1989}} sketches an alternative proof of the first incompleteness theorem that uses [[Berry's paradox]] rather than the [[liar paradox]] to construct a true but unprovable formula. A similar proof method was independently discovered by [[Saul Kripke]].{{sfn|Boolos|1998|p=383}} Boolos's proof proceeds by constructing, for any [[computably enumerable]] set {{mvar|S}} of true sentences of arithmetic, another sentence which is true but not contained in {{mvar|S}}. This gives the first incompleteness theorem as a corollary. According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic.{{sfn|Boolos|1998|p=388}}

=== Computer verified proofs ===
{{See also|Automated theorem proving}}

The incompleteness theorems are among a relatively small number of nontrivial theorems that have been transformed into formalized theorems that can be completely verified by [[proof assistant]] software. Gödel's original proofs of the incompleteness theorems, like most mathematical proofs, were written in [[natural language]] intended for human readers.

Computer-verified proofs of versions of the first incompleteness theorem were announced by [[Natarajan Shankar]] in 1986 using [[Nqthm]] {{harv|Shankar|1994}}, by Russell O'Connor in 2003 using [[Rocq (software)|Rocq]] (previously known as ''Coq'') {{harv|O'Connor|2005}} and by John Harrison in 2009 using [[HOL Light]] {{harv|Harrison|2009}}. A computer-verified proof of both incompleteness theorems was announced by [[Lawrence Paulson]] in 2013 using [[Isabelle theorem prover|Isabelle]] {{harv|Paulson|2014}}.