1.C. Introduction to incompleteness

Existential classes and provability

Let us qualify a formula as existential if it is made of an open ∃ as root, followed by a bounded formula. This section will implicitly only qualify as such those of FST or equivalent theories. Existential statements are essentially the same as halting conditions of algorithms (processed by an abstract "computer" with unlimited available time and resources): Similarly, an existential class of FST, defined by an existential formula ∃y, A(y,x) without parameter, is the range of all outputs x from a given algorithm (which may run endlessly while giving outputs on the way, ignoring the order); it can also be seen as a copy of the truth predicate over a specific range of existential statements. This is linked to provability in both ways. Usual concepts of proof, leading to an existential class of theorems, are formed in 2 steps:
  1. Give a first-order theory whose class of axioms is defined in TT without parameter nor open quantifier, as is the case for all theories from our list (but an existential class of axioms would fit too ; each axiom may of course use open quantifiers);
  2. Apply the concept of proof of first-order logic to this theory.
While the exact expression of this provability formula (∃p, V(p,s)) involves a formal definition of proof in first-order logic, it is independent of the chosen sound and complete way to define it, in the sense that all such formulas V, V' encoding (in FST or equivalent) the verification of proofs for the same (other) theory (defined by symbols t,l,a), are provably equivalent to each other:

FST (+ symbols t,l,a with axioms) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

First incompleteness theorem

Any existential class C of statements of FST including the axioms of FST and stable by logical deduction, can be seen as a class of theorems of some theory T containing FST and describable by it (a T-provability predicate) : at least the theory T defined as FST but with C as its class of axioms, fits.
Let us call such a T FST-sound if all its theorems among statements of FST are true in its standard model (this is traditionally called arithmetical soundness). In this case T-provability is equivalent to truth for all existential statements (truth ⇒ FST-provability ⇒ T-provability ⇒ truth).

Gödel's first incompleteness theorem comes by applying the weak truth undefinability theorem for FST (and thus the equivalent theory Z1), to these existential classes C : while remarkably approaching truth, they still cannot coincide with it. Hence the incompleteness of second-order logic announced in 1.11.

Now by the proof by the Berry paradox, if T is FST-sound then there exists a connective over instances of C with diverse arguments, whose value is T-unprovable. The value of a connective being deducible from the known values of its arguments, some X must make C(X) undecidable. Since all its True (1) values are provable, some False (0) value must be unprovable. So there must exist a statement X of FST such that C(X) is false but T-irrefutable; in other words, X is T-unprovable but this unprovability is itself T-unprovable.

Second incompleteness theorem

Using the strong truth undefinability theorem, the second incompleteness theorem will extend the above result to all statements X of FST :

¬C(0) ⇒ ∀XS, ¬C("¬C":X)

where : interprets substitution ("A":"x" = "A(x)"), i.e. if T is consistent then every C(X) is T-irrefutable, may it be true or false. This is summed up by the case X=0, namely C("¬C(0)") ⇒ C(0) i.e. the consistency of T, if true, is T-unprovable. By completeness, if T has no standard contradiction then it has a non-standard model containing a non-standard contradiction (and thus not containing any model).

This can be compared to truth undefinability as follows. For any theory describing a notion representing that of its own statements, truth undefinability says it cannot (even speculatively i.e. only working in some models) define without parameter the truth predicate of interpretation in the current model; second incompleteness means that it cannot prove the existence of any (consistent) truth predicate (while this existence is provably equivalent to the consistency of the theory).

In the resulting perspective on the foundations of mathematics, 2 other concepts of strength order between foundational theories may be considered (their properties remain to be specified...) : There can be no ultimate well-described foundational theory : for any FST-sound one, adding the statement of its consistency as axiom gives a "better" one, i.e. stronger and still FST-sound (and much more efficient ways to strengthen a theory with respect to complexity are possible). The justifications to accept any theory (version of set theory) as a valid (sound) foundation of mathematics must remain somewhat philosophical as they cannot be completely formalized as a proof.

The time of proving

So, any amount of resources spent seeking T-proofs of a statement X in vain, remains unable to T-refute the T-provability of X, i.e. T keeps "seeing a chance" for X to be T-provable by longer proofs. A theory T' strictly stronger than T can refute the T-provability of some X (namely by using a T-refutation of X) but remains indecisive on others (such as X = the inconsistency of T').
Any FST-sound foundational theory (as a knowledge criterion) will always leave some existential statements practically undecidable, may they be actually true or false, the search for proof or refutation appearing vain within any given limits of available computing resources : As another aspect of the same fact, provability predicates cannot be equivalent to any bounded formula (due to truth undefinability, as they are equivalent to truth in the class of bounded statements).
Intuitively speaking, to interpret (see as definite) any provability predicate (equivalently, the truth predicate over existential statements) requires a realistic view : a use of the actual infinity of ℕ specifically meant as its standard interpretation (which cannot be completely axiomatized).

In a kind of paradox, while the completeness theorem is proven by an abstract construction taking the fact of absence of proof and using actual infinity to produce a counter example (model), there is no "inverse construction" which from the fact about infinities that no system exists with given properties, would produce any finite witness that is its proof (which must nevertheless exist).
Instead, analyzing the proof of the completeness theorem, it appears that the minimal size (complexity) of proofs of any theorem, roughly reflects the number of well-chosen elements that need to be described in an attempted construction of a counter-example, to discover the necessary failure of such a construction ; the chosen formalization of proof theory can only affect the size of proofs in more moderate (describable) proportions.

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 : Temps en théorie des modèles