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 FS, 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 {AS | MA} of statements true in M, differs from any invariant class, in M, of objects "statements":

CS1, ∀MT, ∃AS, M⊨ (AC(⌜A⌝))

Truth Undefinability Theorem (strong version).CS1, ∃AS, T ⊢ (AC(⌜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 : 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.

BS, 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
  1. AX, C(A) i.e. it contains all axioms of T
  2. AS, C(A)∨CA)
  3. C is consistent.
Equivalently, 2. and 3. can be replaced by
  1. AS, C(A) ⇎ CA)
  2. 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:
  1. Take all statements in an arbitrary order;
  2. 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.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions,..., meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Axioms and proofs
1.10. Quantifiers
1.11. Second-order quantifiers
Philosophical aspects
1.A. Time in model theory
1.B. Truth undefinability
1.C. Introduction to incompleteness
1.D. Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 1.B. Indéfinissabilité de la vérité