The completeness theorem of first-order logic

4.6. The Completeness Theorem

Existence of countable term algebras

For any countable algebraic language L with at least a constant and a non-constant, finding a countable ground term L-algebra (necessarily infinite) amonts to defining a ground term L-algebra structure on ℕ, which is a bijection from ^Lℕ to ℕ.
Splitting L as C∪D where C is the set of constants, and D is the rest of symbols, we have ^Lℕ = C∪(^Dℕ). But C and D are countable (either finite or infinite), and ^Dℕ is a union over D of disjoint sets with explicitly definable bijections with ℕ (such as the b_{n_s} we saw). In any case, a bijection between C∪(^Dℕ) and ℕ can be found without problem.
In practice, such bijections from ^Lℕ to ℕ happen to be ground term L-algebra structures because ∀(s,x)∈^Dℕ, ∀i<n_s, x_i<s(x) which would be contradicted by the smallest element outside Min_L ℕ. ∎

Interpretation of first-order formulas

Trying to extend the formal construction of the interpretation of terms in algebras, to the case of formulas interpreted in systems, the difficulty is to cope with the interpretation of quantifiers (or generally binders, if we wish to still generalize).
A possibility, is to switch to a view over all variables as bound throughout the formula: from the concept of interpretation h_v∈E^T of a term T in an algebra E for every interpretation v of its set V of variables, the family (h_v)_v∈E^V is re-curried into a function from T to E^{E^V}. So, a first-order formula interpreted in a system E can be understood as a term interpreted in an algebra with maybe two base types : the sets Op_E and Rel_E of all operations and all relations in E; or split as two sequences of types, Op_E⁽ⁿ⁾ and Rel_E⁽ⁿ⁾. We might not need the full sets of these, but at least, an algebra of these (a subset stable by all needed logical operations).
We took unions over ℕ for the case we would need to see "all possible formulas" as terms interpreted in one same algebra.

The Completeness Theorem

Any good formal proving system (a theory describing proof syntax, verifiable by an algorithm) needs of course to be sound, which means only "proving" what is always true (the provability of a formula implies its truth in every model). More remarkable is the converse property, that is completeness :

Theorem. First-order logic has a proving system both sound and complete in the following equivalent senses

Any consistent first-order theory T with countable language has a countable model.
Any formula true in all countable models of such a theory is deducible from its axioms.

This quality of perfection, established for a certain formal proving system for first-order logic, ensures that any other formal proving system with the same quality will be necessarily equivalent : any formal proof according to one is automatically convertible into a proof according to any other.

Sketch of proof of the first statement (implicitly suggesting how such a proving system can be made; not using the axiom of choice, anyway out of topic):
Express axioms in prenex form, that is chains of quantifiers applied to quantifier-free formulas (using equivalences from 2.1 and 2.3 simplified for a nonempty model).
Interpret the symbol = in axioms as an ordinary predicate symbol, with the axioms of equality [1.6].
Replace each occurrence of ∃ in an axiom by the use of an additional operator symbol K, for example

(∀x,x', ∃y, ∀z, A(x,x',y,z)) ⇢ (∀x,x',∀z, A(x,x',K(x,x'), z)).

Let M be the ground term algebra over the language of operator symbols enriched as just described. Reinterpreting all ∀ in axioms as the use of axiom schemas (one axiom for each replacement of variables by a tuple of elements of M), gives a propositional theory T' (its axioms are composed of logical connectives over Boolean variables), whose set of Boolean variables is ^PM where P is the set of predicate symbols in the theory plus the "equality" symbol.
Observe that T' is still consistent, as any contradiction in T' (= finite set of axioms not satisfied by any tuple of Boolean values of their variables) would provide a contradiction in T, as follows:

From all subterms occurring in used axioms of T', list without repetition all those whose root is a symbol S which was added to the language when converting some axiom ∀x,∃y,∀z,∃u, A(x,y,z,u) of T, into the axiom ∀x,z, A(x,K(x),z, S(x,z)) in T'. Successively replace them all by variables in T: for terms S(t₀,t₁) and S(t₀,t₂) (where t₀, t₁, t₂ ∈ M), the reasoning in T will say
"Let y such that ∀z,∃u, A(t₀,y,z,u);
let u₁ such that A(t₀,y,t₁,u₁);
let u₂ such that A(t₀,y,t₂,u₂);"
and use the contradiction in T' where y replaces K(t₀), u₁ replaces S(t₀,t₁) and u₂ replaces S(t₀,t₂).

Recursively by a chosen enumeration of ^PM as a countable set, add one by one to the axioms, each of these Boolean variables if it is consistent with previously accepted axioms, so that all get values without contradiction.
Then the quotient of M by the equivalence relation of "equality", forms a model (with the "true equality"). ∎

As this construction depends on an arbitrary order between formulas, different choices give different models, which may be non-isomorphic and even have different properties reflecting the undecidability of the theory's formulas.

Deduction of the second statement from the first :

T⊢ A
⇔ T ∪ {¬A} is inconsistent
⇔ T ∪ {¬A} has no countable model
⇔ A is true in all countable models of T. ∎

However, as already announced in truth in mathematics and will be shown by the incompleteness theorem, unclarities remain about provability and existence of models:

The proven equivalence between consistency and existence of a model, does not inform whether these are both true, or both false:
- Provability, if true, can stay practically unknowable: if a proof exists, nothing says how to find it; it may be too big to be ever given.
- The consistency of a theory may be true but unprovable: completeness only ensures that, in this case (and it may be undecidable whether it is the case or not), there also exists universes in which, equivalently, this theory is inconsistent and it has no models.
Such constructions of models as provided by the above proof, are not really effective, as they are not algorithmic: they require an infinity of steps, each of which involves an infinite knowledge (knowing if a formula remains consistent with previously accepted ones, which is the answer to a halting problem of search for contradiction). Actually, most foundational theories such as set theories, do not have any algorithmically definable model.

Skolem's Paradox

Comparing the results of the completeness theorem with Cantor's theorem gives this paradox :
If set theory is consistent then it has countable models, though it sees some sets there, such as ℘(ℕ), as uncountable.

A countable model U interprets the powerset "℘(E)" of an infinite "set" E∈U as the "set" P of all objects in U which play the role of subsets of E (but may differ from these when U is non-standard); as P is meta-countable, it cannot exhaust the uncountable meta-powerset of "all" subsets of E.
As P is meta-countable, it externally has a bijection with ℕ or U; but such bijections "do not exist" (have no representatives) as objects in U.

Rigorously speaking, when the powerset axiom says that the class of subsets of E is a set written ℘(E), it can only determine the interpretation of the functor ℘ relatively to (depending on) the universe where its open quantifiers are interpreted: «all subsets of E existing in this universe are in ℘(E)». In the other interpretation of what it means for a class to be a set, this would mean that the universe already contains "really all" subsets of E, forming the supposedly "true" set ℘(E) which will stay fixed in any further expansion of the universe. However, for the powerset of an infinite set, this wish cannot be expressed in first-order logic nor any other conceivable mathematical formalism: there is no way to talk about meta-sets that "cannot be found" in this universe but would «exist elsewhere» (in any mysterious bigger universe) to exclude them from there. (Only one aspect of this idea can be formalized as the axiom schema of specification).

Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and first-order foundations

4.1. Algebraic terms
4.2. Term algebras
4.3. Integers and recursion
4.4. Presburger Arithmetic
4.5. Finiteness and countability
4.6. The Completeness Theorem
4.7. Non-standard models of Arithmetic
4.8. Developing theories : definitions
4.9. Constructions

5. Second-order foundations
6. Foundations of Geometry