4.2. 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 CD 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 bns 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<ns, xi<s(x) which would be contradicted by the smallest element outside MinL ℕ. ∎

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 hvET of a term T in an algebra E for every interpretation v of its set V of variables, the family (hv)vEV is re-curried into a function from T to EEV. So, a first-order formula interpreted in a system E can be understood as a term interpreted in an algebra whose base set is the set OpE ∪ RelE of all operations and all relations in E where

OpE = ⋃n∈ℕ OpE(n) and RelE = ⋃n∈ℕ ℘(En).

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 proof system (a proof theory, expressible by a verification 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. The completeness of first-order logic was originally Gödel's thesis. Once proven for a specific formal proving system, it gives a perfect meaning to the concept of provability in first-order logic (independent of the choice of formalism with the same quality), eliminating any disagreement between realism and formalism for first-order theories.

Theorem. First-order logic has a proving system both sound and complete in the following equivalent senses 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): 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} is inconsistent
T ∪ {¬A} has no model
A is true in all models of T.  ∎
So, the provability function giving the set of theorems from each set of axioms, is the closure of the Galois connection defined by the truth relation RX×Y between However, as already announced in truth in mathematics and will be shown by the incompleteness theorem, unclarities remain about provability and existence of models:

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. 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. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. Infinity and the axiom of choice
4.5. How theories develop
4.6. The Incompleteness Theorem