Bew - Proof Sketch For The First Theorem - Proof of Independence

Proof of Independence

Now assume that the formal system is ω-consistent. Let p be the statement obtained in the previous section.

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

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

Thus the statement p is undecidable: it can neither be proved nor disproved within the chosen system. So the chosen system is either inconsistent or incomplete. This logic can be applied to any formal system meeting the criteria. The conclusion is that all formal systems meeting the criteria are either inconsistent or incomplete. It should be noted that p is not provable (and thus true) in every consistent system. The assumption of ω-consistency is only required for the negation of p to be not provable. So:

• In an ω-consistent formal system, neither p nor its negation can be proved, and so p is undecidable.
• In a consistent formal system either the same situation occurs, or the negation of p can be proved; In the later case, a statement ("not p") is false but provable.

Note that if one tries to fix this by "adding the missing axioms" to avoid the undecidability of the system, then one has to add either p or "not p" as axioms. But this then creates a new formal system₂ (old system + p), to which exactly the same process can be applied, creating a new statement form Bew₂(x) for this new system. When the diagonal lemma is applied to this new form Bew₂, a new statement p₂ is obtained; this statement will be different from the previous one, and this new statement will be undecidable in the new system if it is ω-consistent, thus showing that system₂ is equally inconsistent. So adding extra axioms cannot fix the problem.