Editing Gödel's incompleteness theorems (section)

=== 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.