1.B. Introduction to incompleteness

Truth undefinability

The incompleteness phenomenon (time order of interpretations) appears for the case of the interpretation of statements, in the form of the Truth Undefinability Theorem. Let us introduce some details about it (but sketches of full proofs will only be given in 5.7, still skipping some tedious steps). Any theory 1TT able to describe a theory (beyond the most trivial ones), can also be developed to describe any well-describable theory. Namely we can start with an 1TT with a general notion of "expression" (in any language) then define there the class of expressions only using some specific language; then provability from given axioms is simply definable from logical validity.

Now let T be any theory which contains 1TT, or which can be developed to produce it. For example it can be some set theory (even without the axiom of infinity, replaced by some tools to work with classes instead of sets...).

Then such a T is able to describe itself just if it is well-describable. But for now we only need general notions of expression and statements which will contain images of those of T. The possibility to specifically describe T will only be used later, for the Incompleteness Theorems.

Let S be the meta-set of statements of T, and S the class defined in T to play the role of S in any model M of T. From any statement FS we can form a ground term of T we shall denote as its quotation "F", which aims to designate the object playing the role of that statement : M⊨"F"∈S.
Let S1 be the meta-set of all formulas of T with only one free variable (with type S but this type detail may be ignored), meant to define invariant sub-classes of S (candidate classes of "true statements").

Truth Undefinability Theorem (weak version). For any model M of T, the meta-class {AS | MA} of statements true in M, cannot agree with any invariant class of objects "statements" in M:

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 in explicit (finitistic) though complex ways. So it gives the "pure" information of a "known unknown" : a necessary error on an explicit A "simply" made of ¬C, with just the more complex argument providing the quote "A" by an explicit (finitistic) process of self-reference, tricky to form and understand.

But a different proof of the weak version is possible (strangely unknown in the literature), from the Berry paradox (technical details, involving subtleties in the foundations of arithmetic, were moved to Part 4) : from a definition of the truth of statements one can define 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 not only somewhat simpler and more obvious to accept, it also provides a different information: it shows the pervasiveness of the "unknown unknown" giving a 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").

Let us draw a first direct consequence. Consider some "almost complete" foundational theory T, i.e. a first-order theory containing TT and, for instance, approaching by second-order universal elimination a second-order theory which is complete, i.e. fully defining its intended standard model M. Even then, no invariant predicate defined by T in M (such as "truth" predicates mentioned in 1.A) can ever be the "right" truth predicate over the class of "statements of T", i.e. giving to all statements of T the values they take in the same M. Therefore, any model of T defined by T in M and matching a T-invariant "truth" predicate (such models must exist thanks to consistency) will necessarily be non-standard, differing from M in its interpretations of statements.

The hierarchy of formulas : existence and provability

To decipher the facts of truth undefinability and incompleteness, formulas can be analyzed by syntax to specify the sources of possible undecidability or other kind of indefiniteness. So to speak, binders are the main source of indefiniteness. Thus, 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 given class) are less definite than bounded quantifiers (∃x∈ and ∀x∈ ) and other binders whose range is a set. For FST, the condition for a class to be a set is to be finite (skipping more technical details). 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 ≤.
Let us qualify a statement as existential if it is made of an open ∃ as root, followed by a formula without open quantifier. Existential statements of FST or equivalent theories (TT and Z1), are essentially the same as halting conditions of algorithms (processed by an abstract "computer" with unlimited available time and resources): They are also crucially linked to the concept of provability in both following ways.

Incompleteness theorems

The famous two incompleteness theorems by Gödel, are respectively deducible from the weak and strong versions of the truth undefinability theorem. The hardest step is to show that Z1 suffices to develop TT, so that incompleteness properties of TT also affects Z1. This difficulty can be skipped by ignoring arithmetic and simply expressing incompleteness as affecting TT and thus FST (admitting the development of TT from FST which is easier).
The first theorem says that no algorithm can produce exactly all truths of arithmetic. The deduction is very simple : for any algorithm, the class of objects it can produce is invariant. Therefore it cannot coincide with the class of true statements of a theory to which the weak truth undefinability theorem applies, namely the theory 1TT and any other theory containing it. To also apply it to arithmetic requires to use Godel's work of developing 1TT from arithmetic. Without it we can still deduce the incompleteness of second-order logic (its lack of complete proof algorithm) by a formalization of 1TT in second-order logic which completely determines its truths. (to be completed)
The size (complexity) of a proof, reflects the number of elements that need to be described in an attempted construction of a counter-example to a given theorem, to observe the necessary failure of this construction (while the choice of formalization only affects the size of proofs in more moderate proportions); this is not a priori predictable from, say, the size of the statement, for reasons which will be developed later.

As will be shown by the incompleteness theorem, unclarities remain about provability and existence of models: For any two well-defined theories (in an algorithmic sense) T, T' which encompass arithmetic (such as set theories), no suffice to make these formulas decidable for every value of s, as soon as they aim to encode provability in a theory which also contains arithmetic.


But any axiomatic formalization of arithmetic in first-order logic is incomplete, in both following senses of the question: This incompleteness affects the provability predicate itself, though only on one side, as follows.
On the one hand, if the formula p(A) of provability of a formula A, is true, then it is provable: a proof of p(A) can in principle be produced by the following method in 2 steps:
  1. Find a proof of A (as it is assumed to exist);
  2. Process it by some automatic converter able to formally convert any proof of A into a proof that a proof of A exists.

On the other hand, it is not always refutable when false : no matter the time spent seeking in vain a proof of a given unprovable formula, we might still never be able to formally refute the possibility to finally find a proof by searching longer, because of the risk for a formula to be only provable by unreasonably long proofs.

The time of proving

Among the possible formalizations of proofs, are formulas V(p,s) of meaning that the number p encodes a valid proof of a statement encoded by the number s, depending on unary predicate symbols t,l,a which encode the classes of components of T (its types, symbols and axioms ; the induction axioms of arithmetic would need to admit the use of symbols t,l,a if these symbols were not definable, while they usually are since we only consider definable theories). The resulting provability formula (∃p, V(p,s)) is independent of the chosen sound and complete way to define V, in the sense that all such provability formulas are provably equivalent to each other in first-order arithmetic. More formally, for any two such arithmetical formulas V, V' encoding proof verification in the same theory,

(Arithmetic + symbols and axioms for t,l,a) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

However to complete the definition of provability, once written as a formula of this kind, remains the issue of interpreting the ∃p realistically, in the standard model of arithmetic ℕ, intuitively described as the system of only all actually finite natural numbers, as will be clarified in Part 4. This use of the standard ℕ can be intuitively understood as the use of actual infinity, needed by lack of predictable limits on the needed (minimal) sizes of proofs for given statements. Indeed as will be explained in 1.A, incompleteness theorems will undermine this definiteness in both ways : establishing both the unpredictability of the size of needed proofs, and the irreducible undecidability of some provability predicates in any algorithmic formalization of arithmetic (while the realistic view sees them all as definite).

If no proof of a statement could be found within given limited resources, it may still be a theorem whose proofs could not be found as they may be any longer. This is often unpredictable, for deep theoretical reasons which will appear from the study of the incompleteness theorem and related ones such as Gödel's speed-up 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
Time in model theory
Introduction to incompleteness
Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : Temps en théorie des modèles