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 definitions of terms interpreted in algebras, to formalize the general concept of formula interpreted in systems, the difficulty is to cope with the interpretation of quantifiers (or generally binders, if we wish to still generalize). A possible solution, is to treat all variables as bound throughout the formula.
Binding all variables modifies the view on the above concept of interpretation of a term T with set of variables V in an algebra E by re-currying the family (hv) of functions from T to E where v runs over EV, 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 ℕ 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 needs of course to be sane, which means never proving anything wrong (so that the provability of a formula ensures its truth in every model). More remarkable is the converse property, that is completeness. Without trying to completely formalize the concept of proof, the below will implicitly suggest its possibility for first-order logic.

Theorem. First-order logic has a proving system (a proof theory, expressible by an algorithm of proof verification), not only sane but also complete in the following equivalent senses
This theorem was originally Gödel's thesis; below is a simplified version. It gives model theory its strength, establishing the equivalence between realism and formalism for first-order theories. 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.
Sketch of proof of the first statement (not using the axiom of choice, anyway out of topic here):
  1. Rewrite through equivalences in 2.1 and 2.3 (simplified by assuming a nonempty model) each axiom into a chain of quantifiers applied to a quantifier-free formula (prenex form).
  2. Replace each occurrence of ∃ in an axiom by a new operator symbol K added to the language of the theory, in the natural way where for example
    (∀x,x', ∃y, ∀z, A(x,x',y,z)) ⇢ (∀x,x',∀z, A(x,x',K(x,x'), z)).
  3. Replace the predicate = in axioms, by an ordinary predicate symbol to play the role of equality, together with the axioms of equality [1.6].
  4. Let M be the ground term algebra over the language of operator symbols enriched as described in 2. Reinterpreting each ∀ in axioms into axiom schemas replacing their variables with all possible tuples 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.
  5. 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) can be converted into a contradiction in the initial theory T, as follows:
    List without repetition all (ground) terms occurring as a subterm of some used axiom of T ', and whose root is some symbol S that was added by converting some axiom of T such as "∀x,∃y,∀z,∃u, A(x,y,z,u)" into the axiom "∀x,z, A(x,K(x),z, S(x,z))" in T '. For example if we have terms S(t0,t1) and S(t0,t2) (where t0, t1, t2M), the reasoning in T can start by
    "Let y such that ∀z,∃u, A(t0,y,z,u);
    let u1 such that A(t0,y,t1,u1);
    let u2 such that A(t0,y,t2,u2);"
    and continue using the contradiction in T ' where y replaces K(t0), u1 replaces S(t0,t1) and u2 replaces S(t0,t2).
  6. 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.
  7. Then the quotient of M by the equivalence relation of "equality", forms a model (with the "true equality"). ∎
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.  ∎
In other words, taking the Galois connection as in the fundamental example RX×Y where the lesson of the completeness theorem is that provability, which maps any given set of axioms to the set of resulting theorems, coincides with the closure of this connection.

However, this still does not make everything clear about provability and existence of models, as announced in the section on truth in mathematics, and will be established by the incompleteness theorem:

Skolem's Paradox

The powerset axiom says that the class of subsets of E is a set written ℘(E). In the other interpretation of what it means for a class to be a set, this would mean that we have a universe big enough to contain "really all" subsets of E, forming the supposedly "true" set ℘(E) which will stay fixed in any further expansion of the universe. However this expectation cannot be formalized in first-order logic for the powerset of an infinite set (it would transcend any possible formalization as a mathematical theory): «For all subsets of E...» can only mean «For all subsets of E that can be found in this universe...». Indeed, mathematical theories can only describe objects that "are here" (in the given model), but objects that "cannot be found" might still «exist elsewhere», and there is no way to talk about them to express their non-existence: no formalism can exclude the possible meta-existence of subsets of an infinite E, that would only exist in a bigger universe beyond our universe with its ℘(E). (Only one aspect of this idea can be formalized as the axiom schema of specification).
Finally, as the powerset axiom implicity takes the actual form of a relation between ℘(E) and the universe where its open quantifiers are interpreted, it only determines ℘(E) as depending on the universe: a bigger universe may interpret the functor ℘ with another value on the same E. This relativity of meaning of the powerset, which brings as formally bounded formulas on given objects, some undecidabilities that would otherwise merely concern unbounded formulas (with open quantifiers, subject to indeterminations on the size of the universe) is the key to many paradoxes in the foundations of mathematics.

First comes Skolem's paradox:
If set theory is consistent then it has countable models, despite Cantor's theorem by which some sets there, such as ℘(ℕ), are uncountable.

This fact has two aspects: But since ℘(ℕ) is involved in the description of ℕ itself, there is no more necessity for models to correctly interpret ℕ either: as will be explained in the next sections, the interpretation N of ℕ in any countable model constructed in such ways is actually a non-standard model of arithmetic, having a bijection but no isomorphism with ℕ. The paradox still holds as the countable set P plays the role of ℘(N), but it must differ from the "true" ℘(N) which is also uncountable (bijections between sets N and ℕ induce bijections between their powersets, which preserve uncountability).
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. Infinity and the axiom of choice
4.4. Non-standard models of Arithmetic
4.5. How theories develop
4.6. The Incompleteness Theorem