The Incompleteness Theorem

(the Completeness theorem is on another page)
Previous section : Non-standard models of Arithmetic

The Truth Undefinability Theorem

This theorem by Tarski (see wikipedia article) expresses the impossibility for a single formula v of a founding theory (such as a set theory) to correctly specify all the truths of the same theory, giving as v(x) for every object x representing every closed formula X, the same Boolean value as the formula X would directly give in that theory (in other words, such that v(x) ⇔ X) - or the values it can invariantly specify, even if they are consistent, only fit with models not resembling the one currently used.

The proof of this theorem roughly consists in showing that such a formula v would give means to express another formula G claiming its own falsity, which would be a contradiction :
[see definitions of «meta» in 1.3., «predicate» and «invariant» in 1.4, and «closed» in 1.6, so here "invariant" will mean "definable"]

Theorem. Let T a theory defining in each of its possible models M the invariant data of : Then there exists a closed formula G of T, such that T⊢ (G ⇎ v[G]).

Proof.
Assume the image [F] in T ′ of each unary formula F of T is named by a closed term tF of T, whose construction can be formalized by a unary term J of T: J([F])=[tF].
In T ′, replacing the variable of a unary formula A by a closed term u, forms a closed formula (A:u). So in T, for any unary formula F and closed term K we have ([F]:[K]) =[F(K)].
Let H(A) be the formula ¬v(A:J(A)), with variable A in the class of unary formulas of T ′.
Let G be the formula H(tH).
Then [G]=([H]:J([H])), thus the conclusion. ∎

Corollary. If M is explicitly built (meta-invariant) determining values of closed formulas F of T (or if M is any model agreeing with specific invariant determinations of these values), then the computation v[F] in M of these values by the same rules (if possible) is incorrect.

Proof. G and v[G] are computed by the same rules but respectively interpreted outside and inside M. As G ⇎ v[G], if the outside computation is correct, then the one in M is not. ∎

In particular, the construction in the proof of the completeness theorem necessarily makes a «wrong choice» at some step. Namely, it is the provability predicate (whether each formula is refutable from previous axioms) used in each step of its construction, that is the weakly defined concept: it is a non-algorithmic operation, differently interpreted between models. Finally, it can be understood as implicitly depending on some (arbitrary) preexisting universe.

The Incompleteness Theorem

Continuing with the assumptions of the Truth Undefinability Theorem, let us present Gödel's incompleteness theorem, according to which whenever T is consistent (which we admitted in this study, since a model of T is used and thus exists) and T ′ is supposed to have the same format (having the image of each axiom of T among its own axioms or at least theorems), then the consistency of T ′ is not provable inside the formalism of T.  To make things simple let us express it and sketch its proof in the context of proof theory (assuming the concept of "proof" to be already available):

Theorem. If T ′ is built like T which can express the provability p in T ′, and F is a closed formula,
1) (T⊢ F) ⇒ (T⊢ p[F])
2) (T⊢ ¬p[0]) ⇔ (T⊢ 0) (Gödel's second incompleteness theorem : no consistent theory can prove its own consistency)
3) (T⊢ p[F] ⇒ F) ⇔ (T⊢ F) (Löb's theorem, from which «This claim is provable» is deduced)

Proofs:
1) The proof of F in T can be copied into T ′, or converted to a proof of existence of a proof.
2) Let T⊢ (G ⇎ p[G]). The proof (T⊢ G) ⇔ (T⊢ G∧p[G]) ⇔ (T⊢ 0) formalized in T gives T⊢(p[G]⇔p[0]). Thus (T⊢ ¬p[0]) ⇔ (T⊢ ¬p[G]) ⇔ (T⊢ G) ⇔ (T⊢ 0).
3) from 2) applied to the theory (T+¬F). Finally take F=«F is provable», ie T⊢ (F ⇔ p[F]). ∎

Contrapositive viewpoint if T can describe models: every model of some T ′ is a model of T.
No converse: a proof in T ′, model of proof theory that is «finite» according to T, may actually be infinite and thus no real proof. If a formula F only has infinite «proofs», its provability is undecidable and false: the unfound proofs of F seem to not have been seeked long enough, and models where F is false cannot be reliably built, so «do not always exist». Wherever models of T can be found, some of them cannot find any one of them anymore.


Next :  Comments on the powerset axiom
or directly : Introduction to the foundations of geometry

 Back to homepage : Set Theory and Foundations of Mathematics