Bew - Second Incompleteness Theorem

Second Incompleteness Theorem

Gödel's second incompleteness theorem first appeared as "Theorem XI" in Gödel's 1931 paper On Formally Undecidable Propositions in Principia Mathematica and Related Systems I.

The formal theorem is written in highly technical language. The broadly accepted natural language statement of the theorem is:

For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.

This strengthens the first incompleteness theorem, because the statement constructed in the first incompleteness theorem does not directly express the consistency of the theory. The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the theory itself.

A technical subtlety in the second incompleteness theorem is how to express the consistency of T as a formula in the language of T. There are many ways to do this, and not all of them lead to the same result. In particular, different formalizations of the claim that T is consistent may be inequivalent in T, and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that the largest consistent subset of PA is consistent. But since PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it is consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term "largest consistent subset of PA" is technically ambiguous, but what is meant here is the largest consistent initial segment of the axioms of PA ordered according to specific criteria; i.e., by "Gödel numbers", the numbers encoding the axioms as per the scheme used by Gödel mentioned above).

For Peano arithmetic, or any familiar explicitly axiomatized theory T, it is possible to canonically define a formula Con(T) expressing the consistency of T; this formula expresses the property that "there does not exist a natural number coding a sequence of formulas, such that each formula is either of the axioms of T, a logical axiom, or an immediate consequence of preceding formulas according to the rules of inference of first-order logic, and such that the last formula is a contradiction".

The formalization of Con(T) depends on two factors: formalizing the notion of a sentence being derivable from a set of sentences and formalizing the notion of being an axiom of T. Formalizing derivability can be done in canonical fashion: given an arithmetical formula A(x) defining a set of axioms, one can canonically form a predicate Prov_A(P) which expresses that P is provable from the set of axioms defined by A(x).

In addition, the standard proof of the second incompleteness theorem assumes that Prov_A(P) satisfies that Hilbert–Bernays provability conditions. Letting #(P) represent the Gödel number of a formula P, the derivability conditions say:

1. If T proves P, then T proves Prov_A(#(P)).
2. T proves 1.; that is, T proves that if T proves P, then T proves Prov_A(#(P)). In other words, T proves that Prov_A(#(P)) implies Prov_A(#(Prov_A(#(P)))).
3. T proves that if T proves that (P → Q) and T proves P then T proves Q. In other words, T proves that Prov_A(#(P → Q)) and Prov_A(#(P)) imply Prov_A(#(Q)).