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 strong version just lets
*A*be ¬*C*with argument replaced by an explicit ground term (without binder but quite complex); -
the Berry paradox shows
the existence of some
*A*among formulas which are TT-provably equivalent to big connectives over instances of*C*applied to diverse such terms (but simpler).

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.

- Any such ∃
*x*,*A*(*x*) is equivalent to the halting of an algorithm that enumerates all*x*, interprets*A*on each, and stops when it finds*A*true there; - The halting condition of any algorithm is an existential statement
∃
*t*,*A*(*t*) where*A*(*t*) says it halts at time*t*(details are of course much more complex).

- The truth of an existential statement (∃
*x*,*A*(*x*)) implies its FOT-provability (by existential introduction over the quote of*x*), so both are equivalent; - Any effective concept of theorem (class of provable statements
*s*) of any theory in any framework, must be an existential class(∃ for some*p*,*V*(*p*,*s*))*V*(*p*,*s*) meaning that*p*is a valid proof of*s*.

- Give a first-order theory with an existential class of axioms (usual ones, including all theories from our list, even have bounded definitions);
- Apply there the concept of proof of first-order logic.

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

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.

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

By weak truth undefinability,

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

¬*C*(⌜0⌝) ⇒ ∀*A*∈*S*, ¬*C*(⌜¬*C*⌝:*A*)

Rephrasing this by completeness, if

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).

Any FOT-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.

- 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 FOT (this is related to the issue of proof of FOT-soundness, but to express the FOT-soundness of a theory requires a stronger framework such as MT due to truth undefinability).

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.

FR : Introduction aux théorèmes d'incomplétude