1.B. Truth undefinability
Continuing our introduction to the big picture of the foundations of mathematics, let us sketch
a particular aspect of the time
ordering of interpretations : the inability of self-describing theories to define (predict)
the values of their own statements. This will show the strictness of the strength hierarchy of
theories, and will be a key step in the proof of the incompleteness of arithmetic
(and thus second-order logic).
Standard objects and quotes
Objects in standard models of a
FOT will themselves
be called standard, which intuitively means "truly finite" : they can in principle be
mathematically quoted, i.e. for each such object x we can form a ground term,
here abbreviated by the notation ⌜x⌝, which designates x in the standard model.
So, the standard model of arithmetic ℕ is made of standard numbers,
values n of quotes ⌜n⌝ looking like 1+...+1 (actual details will be
studied in Part 4).
References to the truth of statements and the meaning of classes
of FOTs will be implicitly meant as their standard interpretations unless otherwise stated.
Non-standard models can be understood as extensions of the standard one:
they still contain all standard objects, i.e. copies of objects of the standard model,
defined as values of their mathematical quotes; but differ by having more objects
beyond these, called non-standard objects (not quotable).
Non-standard numbers will also be called pseudo-finite : they are
seen by the theory as «finite» but with the schema of properties of being
«absolutely indescribably large» : larger than any
standard number, thus actually infinite.
In expressions of statements or classes of foundational theories, it usually makes no difference
to allow finite-valued parameters (= whose type belongs to a FOT part of the theory)
insofar as they are more precisely meant to only take standard values, and can thus be replaced
by their quotes.
In a non-standard model of FST, standard sets are the truly finite sets with only standard
elements. But this does not define standardness, which cannot either be defined using
quotes (which are infinitely many meta-objects). As will be clear in Part 4, the axiom
schema makes standardness undefinable by any formula of FOTs: the meta-set of standard
objects in a non-standard model is not a class, and thus (for FST) not a set.
Truth Undefinability theorems
Any well-describable theory T stronger than TT (i.e. able to express TT)
can also describe itself : the definitions of the τ, L, X composing T
form the development from TT (and thus from T) of the version of 1TT
describing T. But this will only be fully used for incompleteness theorems (1.C).
First, truth undefinability will need TT (with general notions of expressions) but
not X (distinguishing axioms among statements; usual τ and L being
finite raise no issues).
(As a bare version of 1TT with undefined τ, L or X would not be a
proper development from TT, its working would require to add the use of τ, L, X
in the axiom schema : of induction for Z1, or of specification for FST...).
Let S be the meta-class of statements of T, and S the class defined in 1TT
and thus in T to play the role of S in any model M of T.
For any statement F∈S, its quote ⌜F⌝
designates in M the element of S playing the role of that statement :
1TT⊢ (⌜F⌝∈S).
Let S1 be the meta-class of formulas of T with only one free variable
(with range S but this detail may be ignored), meant to define invariant unary predicates
over S. Now none of these can match the truth of statements in the same model:
Truth Undefinability Theorem (weak version). For any model M
of T, the meta-class {A∈S | M⊨A} of statements true
in M, differs from any invariant class, in M, of objects "statements":
∀C∈S1, ∀M⊨T, ∃A∈S,
M⊨ (A ⇎ C(⌜A⌝))
Truth Undefinability Theorem (strong version). ∀C∈S1,
∃A∈S, T ⊢ (A ⇎ C(⌜A⌝)).
The tradition focuses on proving the strong version (details in Part 5) :
the proof using the liar paradox provides an explicit A, defined as
¬C(⌜A⌝) where the quote ⌜A⌝ is obtained by an explicit (finitistic)
but complex self-reference technique. So it gives the "pure" information of a
"known unknown" : the necessary failure of C to interpret an
explicit A "simply" made of ¬C over a complex ground term.
But the weak version can be proven another way, from the Berry paradox (details involving subtleties in
the foundations of arithmetic were moved to Part 4) : from a definition of the truth of
statements one can define the predicate between formulas and numbers telling which
formula defines which number, and thus define a number in the style of "the smallest
number not definable in less than twenty words" which would lead to contradiction.
This proof is both more intuitive (as it skips the difficulties of self-reference), and provides
a different information: it shows the pervasiveness of the "unknown unknown" giving a finite
range of statements A which are "less pure" in their kind but less complex in size,
among which an "error" must exist, without specifying where
(it depends on which number would be so "defined").
The hierarchy of formulas
The facts of truth undefinability, undecidability or other indefiniteness of formulas can
be understood by analysing their syntax, as mainly coming from their use of binders:
the most definite formulas are those without binder ; then, intuitively, the definiteness
of a given binder is a matter of how set-like its range is. In set theories,
open quantifiers
(ranging over the universe or a class) are less definite than bounded quantifiers
and other binders whose range is a set.
For FST, the essential condition for a class to be a set is finiteness. Similarly
in arithmetic, quantifiers can be bounded using the order : (∃x<k, )
and (∀x<k, ) respectively abbreviate (∃x,
x<k ∧ ) and (∀x, x<k ⇒ ) and the same for ≤.
The values of bounded statements of FOTs, are independent of the model as their
interpretation only involves standard objects.
Any standard object of a FOT has all the same bounded properties (= expressed by
bounded formulas with no other free variable) in any model.
Refined versions
The proofs of the truth undefinability theorems, explicitly giving some A on which
any C differs from truth, prove more than their mere conclusions: they somehow
specify the extent of this difference. Namely :
- the strong version just lets A be ¬C with
argument replaced by an explicit ground term (without binder but quite complex);
-
the Berry paradox
shows the existence of some A among statements which are TT-provably equivalent to big
connectives over instances of C applied to diverse such terms (but simpler).
This latter equivalence is done by developing some FOT-bounded quantifiers, thus with finite
ranges ; its proof only uses axioms of TT, though C can use a broader language.
Therefore if C is definite on the whole class of statements of T, is constant along
TT-provably equivalent statements and faithfully processes connectives over instances of
C, then C differs from truth on some C(⌜B⌝), i.e.∃B∈S, C(⌜B⌝) ⇎ C(⌜C(⌜B⌝)⌝)
For either case (weak or strong), in some sense, A needs no more quantifier
of any kind than C. So any bounded C differs from truth on some
bounded A. In FOTs this is quite a bad difference, but not surprising by lack of
bounded candidate truth-approaching C to think of.
Truth predicates
Let us call truth predicate of a theory T described by another theory T',
any predicate C (defined by T' with
possible parameters) over the class S of statements of T, such that
- ∀A∈X, C(A) i.e. it contains all axioms of T
- ∀A∈S, C(A)∨C(¬A)
- C is consistent.
Equivalently, 2. and 3. can be replaced by
- ∀A∈S, C(A) ⇎ C(¬A)
- C contains all logical consequences of any conjunction of its own elements.
The existence of a truth predicate of T obviously implies its consistency.
But the converse is also provable in TT, making these equivalent:
If T is consistent then a truth predicate of T can be
(TT-provably) TT-defined from it in this way: - Take all statements in an arbitrary order;
- Add each to axioms if consistent with previously accepted axioms.
Such a definition is not algorithmic (the condition "if consistent" cannot be checked in
finite time), but it involves no other parameter than T and an order on its language.
Properties of models
The (first-order) properties of a model M of T, are the statements of
T true in M.
The class of properties of any model of T is a truth
predicate of T. However this does not always make sense, due to truth undefinability :
TT lacks general definitions for the classes of properties of infinite systems with unlimited
numbers of quantifiers.
Systematic meaningfulness only comes in strictly stronger frameworks such as MT,
able to hold as sets some infinite classes (such as classes of finite objects)
serving as types (classes of objects) in M.
Yet the Completeness theorem, while simply expressed in set theories with Infinity, also
appears in TT as a schema of theorems, which for any definition of a consistent
theory, conceives a model as a class of objects with TT-defined structures. Our
simple construction
(4.7) ensures the truth of axioms and ignores other statements. By
following it, all statements become interpreted as special cases of TT-statements
(with parameters τ, L, X composing
T, to be replaced by their definitions). The truth predicate so obtained on that class
may not be TT-invariant, but is anyway MT-invariant provided that
T was (as MT can define truth over the class of TT-statements).
But applying the Completeness theorem to a given truth predicate (which can be TT-defined),
proves in TT the existence of a model whose properties conform to it, though its
interpreted notions are not sets. This presents in 2 steps how to construct a model
with TT-invariant properties, while the same goal is also achieved by the single but
harder construction of the traditional proof (by Henkin) of the completeness theorem.
Other languages:
FR : 1.B. Indéfinissabilité de la vérité