(the
Completeness theorem is on another page)

Previous section : Non-standard
models of Arithmetic

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"]

*«a theory»**T*′ where each nullary or unary expression*F*of*T*meta-invariantly translates as [*F*] in*T*′,*a unary predicate**v*to apply to the image [*F*] of each closed formula*F*of*T*,

Proof.

Assume the image [

In

Let

Let

Then [

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

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.

**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*]).
∎

No converse: a proof in

Next : Comments on the powerset axiom

or directly : Introduction to the foundations of geometry

Back to homepage : Set Theory and Foundations of Mathematics