1.C. Introduction to incompleteness

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.

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, A needs no more quantifier of any kind than C, in this sense : This 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 interprets connectives over instances of C, then ∃BS, C(⌜B⌝) ⇎ C(⌜C(⌜B⌝)⌝), i.e. C differs from truth on C(⌜B⌝).

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.

Existential classes and provability

Let us qualify a formula as existential if written ∃x, A(x), with an open ∃ as root (or several, which can be re-expressed as one) followed by a bounded formula A. In this section this will be meant in FOTs only. Existential statements amount to halting conditions of algorithms processed by abstract "computers" with unlimited resources: Similarly, an existential class of a FOT, i.e. defined by an existential formula ∃y, A(y,x), can be equivalently qualified as algorithmically defined, i.e. the range of all outputs given on the way by an endlessly running algorithm; it defines truth over the existential statements obtained from it by replacing x by any quote. This is linked to provability as follows. Usual existential classes of "theorems" among first-order statements with a given language, are formed in 2 steps:
  1. Give a first-order theory with an existential class of axioms (usual ones, including all theories from our list, even have bounded definitions);
  2. Apply there the concept of proof of first-order logic.
The provability formula (∃p, V(p,s)) from the second step is independent of the chosen definition for a sound and complete concept of proof in first-order logic, in the sense that any two of these leading to FOT-formulas V, V' encoding proof verification for the same theory (defined by symbols τ, L, X), they give the same theorems :

FOT (+ symbols τ, L, X with axioms) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

As the first step defines τ, L, X in FOT, it simplifies the above as FOT ⊢ ...

Conversely, if C is an existential class of "theorems" among first-order statements of a theory, and contains the first-order logical consequences of any conjunction of its elements (intuitively, the proving framework contains the power of first-order logic), then C is the class of T-provable statements by first-order logic from some algorithmically defined first-order theory T : at least trivially, the theory which takes C as its class of axioms.

First incompleteness theorem

Let C be a class of "T-provable" FOT-statements for an algorithmically defined theory T able to express these (i.e. C is an existential class of FOT-statements containing the first-order logical consequences of any conjunction of its elements). Further assume T stronger than FOT (i.e. C contains all axioms of FOT, and thus its theorems). Then for all existential A,

A ⇒ (A is FOT-provable) ⇒ C(⌜A⌝)

while the FOT-soundness of T means the converse (C(⌜A⌝) ⇒ A for all A).
By weak truth undefinability, C being existential must differ from truth. If moreover T is FOT-sound, then each case of difference is a case of T-undecidability, so that T is incomplete (it leaves some statements undecidable). Hence the incompleteness of second-order logic (1.11). This approaches, yet does not give, the famous

First incompleteness theorem. Any algorithmically defined and consistent theory stronger than FOT is incomplete.

Now by the proof by the Berry paradox, if T is FOT-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 A must make C(A) undecidable. As C is existential, all its True values (1) are provable, thus some False value (0) must be unprovable. So some FOT-statement A must exist letting C(A) false but T-irrefutable; in other words, A is T-unprovable but this unprovability is itself T-unprovable.

Second incompleteness theorem

The second incompleteness theorem (whose proof uses the strong version of truth undefinability) says C(A) is T-irrefutable for all statements A just if T is consistent :

¬C(⌜0⌝) ⇒ ∀AS, ¬C(⌜¬C⌝:A)

where the colon ( : ) means substitution between described expressions so that (⌜B⌝:⌜a⌝) = ⌜B(a)⌝. This is summed up by the case A=0, namely C(⌜¬C(⌜0⌝)⌝) ⇒ C(⌜0⌝) i.e. the consistency of T, if true, is T-unprovable.
Rephrasing this by completeness, if T has no standard contradiction then it has a model containing a non-standard contradiction (and thus no verifiable model).

Also equivalently, T cannot prove the existence of any truth predicate over a notion it describes as the set of its own statements. This is somehow explained, though not directly implied, by weak truth undefinability, which prevents using the current model as an example, since the truth over all standard statements there cannot be T-defined as any invariant predicate (not even speculatively i.e. only working in some models).

Proving times

So, any amount of resources spent seeking T-proofs of a statement A in vain, remains unable to T-refute the T-provability of A, i.e. T keeps "seeing a chance" for A to be T-provable by longer proofs. A theory T' strictly stronger than T can refute the T-provability of some A (namely by using a T-refutation of A) but remains indecisive on others (such as A = the inconsistency of T').
Any FOT-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.

More concepts of strength

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 FOT-sound one, adding the statement of its consistency as axiom gives a "better" one, i.e. stronger and still FOT-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.

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 : Introduction aux théorèmes d'incomplétude