(the
Completeness theorem is on another page)

Previous section : Non-standard
models of Arithmetic

[see definitions of «meta»
in 1.3., «predicate» and «invariant» in 1.4, and «closed» in 1.6,
so here "invariant" will mean "definable"; and *T*⊢*
F *means that

The idea is that, in any theory able to describe formulas, any
formula will also have the ability to take, as argument, a
quotation of itself (this quotation included).

**Theorem. ***Let T a theory able to describe
itself, in the sense that it defines in (every one of) its
model M an *

*Each expression**F*in the language of*T*, can be quoted, i.e. we can write*a closed term**t*_{F}of*T**in the same language, whose value is the copy*of F in*[**F*]*T*′,*It can describe the quotation process in**T*′,*by a unary term**J*of*T*, taking argument in some class of expressions of T', and values in the class of closed terms of T ' : for any expression F we have⊢*T*(*J*)=[*t*_{F}].*t*_{F}*It can operate formal substitutions (compositions) in T ' : given a variable A in a class of expressions of*with a distinguished free variable, and*T '*the class of closed terms of*u in**T ', the operation*:*(**A*So, for any unary formula F and closed term K of T we have*u*) gives the expression in T ' obtained by replacing the variable of A by u.*T*⊢(*t*:_{F}*t*) =_{K}*t*_{F}_{(}_{K}_{)}.

Proof.

LetH(A) be the expressionF(A:J(A)) with variableAranging over the class of expressions of T' with the same type (in T') asF(in T), and thus asH(without specifying the range of their distinguished variable).

Then letXbe the term (t_{H}:J(t_{H})). ThusG, that isF(t_{H}:J(t_{H})), can also be abbreviated asH(t_{H}). ThusT⊢ (:t_{H}(J) ) =t_{H}t∎_{G}

Proof : by the self-quotation theorem, taking for

Intuitively, if we read

**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. Of course it will keep its unique true interpretation as long as the set of natural numbers remains standard. From this we deduce that any model of a founding theory (arithmetic or set theory) obtained by such a construction, necessarily contains non-standard numbers, that modify the first-order properties of the set of natural numbers (with addition and multiplications).

Finally, any construction of a model should be understood as implicitly depending on some (arbitrary) preexisting universe, with its set of natural numbers whose character of "being standard" cannot be defined in the absolute.

**Theorem. ***If T ′ is
built like T which can express the provability p
in T ′, and F is a
closed formula, *⊢

1) (T

2) (

3) (

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 for 1): 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