- Any existential statement ∃
*x*,*A*(*x*) is the halting condition of an algorithm that enumerates every*x*, interprets*A*over each, and stops when it finds*A*true somewhere; - The halting condition of any algorithm is expressible as an existential statement
∃
*t*,*A*(*t*) where, roughly speaking (details are of course more complex),*A*claims that this algorithm will halt at time*t*.

- The truth of an existential statement (∃
*x*,*A*(*x*)), implies its FST-provability, by existential introduction over the quote of*x*, and thus also implies its truth in non-standard models; while the converse holds (FST-provability ⇒ truth). - Any effective concept of theorem, i.e. class of provable statements
*s*by any specified theory with its logical framework, must be an existential class (∃*p*,*V*(*p*,*s*)) where the bounded formula*V*expresses (in a possibly encoded way) that*p*is a valid proof of*s*.

- 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);
- Apply the concept of proof of first-order logic to this theory.

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

Let us call such a

Gödel's first incompleteness theorem comes by applying the weak truth undefinability
theorem for FST (and thus the equivalent theory Z_{1}), 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.

¬*C*(0) ⇒ ∀*X*∈*S*, ¬*C*("¬*C*":*X*)

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...) :- The deducibility (provable implication) between consistency statements:
*T'*is stronger than*T*if the consistency of*T*is deducible from the consistency of*T'*; then*T'*is called strictly stronger than*T*if the consistency of*T*is a theorem of*T'*; - The inclusion order between classes of theorems among statements of FST (this is related to the issue of proof of FST-soundness, but to express the FST-soundness of a theory requires a stronger framework such as MT due to truth undefinability).

Any FST-sound foundational theory (as a knowledge criterion) will always leave some existential statements

- No systematic prediction of a limit to the expectable size of the smallest proof(s) of any statement can be expressed as directly measurable from its form (such as its size) : such proofs may be too big to be stored in our galaxy, or even indescribably big. (An example of statement expected to require a very big proof is given as object of Gödel's speed-up theorem).
- Undecidable (thus false) existential statements (∃
*x*,*A*(*x*)) only have non-standard examples of*x*such that*A*(*x*); but these look very similar to the true case, as non-standard objects are precisely those appearing "indescribably big" in the non-standard model containing them (just extending the range of meant "describable sizes" to all standard ones).

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.

FR : Temps en théorie des modèles