4.7. Countability and Completeness

Countable sets

A set A is called countable if |A| ≤ |ℕ|, and countably infinite if |A| = |ℕ|.

Proposition. Any countable set is either finite or countably infinite (the converse is obvious).

Proof. Let A⊂ℕ, and assume A≠∅ (as ∅ is finite).
Let S' the successor function (3.12) of A.
If ∃x∈ℕ, A ⊂ <⃖(x) then |A| ≤ x thus A is finite.
Otherwise, A ⊂ Dom S' (as A is well-ordered), thus |ℕ| ≤ |A|.∎

Actually, in the infinite case, the bijection with ℕ is obtained without use of the Cantor-Bernstein theorem, for the following reason.
Let B = 〈{min A}〉S'. Then B=A.
Indeed otherwise x∈A\B implies B ⊂ <⃖(x) (from the definitions of S' and B), leading to the contradicting consequences that B is finite (|B| ≤ x), and B ⊂ Dom S'.∎

The definition of countability can be rephrased without the axiom of infinity, to mean either finite or countably infinite, the latter meaning the existence of a ground Σ-term algebra structure; thus, countability can be defined as the existence of a ground functional Σ-draft structure.

Without using AC, if there is a surjection f: ℕ ↠ A (or more generally a surjection from any countable set) then A is countable.
Indeed a section of f is given by y↦ min f•(y).

More statements of the axiom of infinity

Let us extend our list of equivalent statements of the axiom of infinity with the below 2. and 3. where
  1. Existence of ℕ
  2. Existence of a (countable) ground term algebra for any countable algebraic language
  3. Existence of a (countable) model for any consistent first-order theory with a countable language
  4. Existence of an injective Σ-algebra.
Obviously, 2. ⇒ 4. ⇒ 1.
3. ⇒ 4. depends on the claim of consistency of arithmetic, at least its very poor excerpt expressing the concept of injective Σ-algebra. A rigorous interpretation of the question is whether this consistency is provable in Finite Set Theory, which I do not know, but it does not seem very interesting anyway.

Let us refer instead to the intuitive obviousness of this consistency : we can interpret and accept the point philosophically, by a switch of perspective.
Namely, we are implicitly assuming the consistency of our set theory, fancied as describing a universe U (which just does not form "a set" from the same viewpoint). The excerpt of set theory which describes tuples forms a theory describing U as an injective algebra with language made of the tuples definers. Then 3. ⇒ 2. follows by noting, for any language L of algebraic symbols which belong to U, that U is an injective L-algebra. If U is standard, this takes the simplified conventional form LU ⊂ U, making (U, IdLU) an injective L-algebra.

We shall focus on proving 1. ⇒ 2. ⇒ 3. below.

y\x 01234
0 0 1 4 9 16
1 2 3 5 10 17
2 6 7 8 11 18
3 12 13 14 15 19

Countability of ℕ2

A natural bijection between ℕ×ℕ and ℕ is defined by (x,y) ↦ (y < x ? x⋅x + y : y⋅y + x + y).

y\x 0 1 2 3 4
0 0 1 3 6 10
1 2 4 7 11
2 5 8 12
3 9 13
Another bijection b2 : ℕ×ℕ → ℕ is defined as b2(x,y) = Tx+y+y from the sequence (Tn) of triangular numbers defined by 2⋅Tn = n⋅(n+1) (see properties of parity) or equivalently by T0=0 ∧ ∀n∈ℕ, Tn+1=Tn+n+1. This makes ℕ×ℕ a ground term (0,S)-algebra where

0ℕ×ℕ=(0,0)
S(0,y)=(Sy,0)
S(Sx,y)=(x,Sy)

which recursively defines b2-1(z), where x+y is the only n such that Tn≤z<TSn.

It would follow that any countable sum of countable sets is countable if we accept the axiom of countable choice ACℕ to justify the existence of a sequence of injections to ℕ from each set. Otherwise the result still holds for finite sums (by the finite choice theorem), and when a rule can be given to pick a specific choice in a systematic way.

It will be left to the reader to define more natural bijections with ℕ for specific cases such as sums A⊔B when either one or both of the countable sets A and B is infinite.

Countability of ℕn

There are multiple ways of defining a bijection between ℕn and ℕ for any n>2, without the ones appearing much more natural than the others.
Some come by taking inspiration from each of both above bijections between ℕ2 and ℕ, to generalize it from n=2 to other n.
More ways are obtained by picking a bijection b2 : ℕ2 ↔ ℕ, and defining the next ones recursively, using either of

ℕSn ≈ ℕn×ℕ ≈ ℕ×ℕ ≈ ℕ
ℕSn ≈ ℕ×ℕn ≈ ℕ×ℕ ≈ ℕ

for each n>0, which for n=1 gives back the chosen b2 in either case.
Formally, the first way recusively defines this sequence of bijections bn:ℕn ↔ ℕ for n>0 by

b1=Idℕ
∀n>0,∀u∈ℕSn, bSn(u) = b2(bn(u|Vn),un)

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 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 provided that the chosen sequence covering C∪(Dℕ) starts with an element of C, 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 hv∈ET of a term T in an algebra E for every interpretation v of its set V of variables, the family (hv)v∈EV 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 with maybe two base types : the sets OpE and RelE of all operations and all relations in E; or split as two sequences of types, OpE(n) and RelE(n). 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

Let us finally prove the Completeness theorem previously commented in 1.1, 1.9, 1.10, 1.B and 1.C.

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 a possible form of a proving system, but ignoring efficiency issues; the axiom of choice is not used and is anyway out of topic):

Reduce T to a single-type theory T1 simulating the use of types by relevant unary predicate symbols and axioms, but without requiring all objects to belong to some type. Thus, the axiom (∃x, 1) can be added to T1 without harm (it still allows types to be empty).
Then re-write axioms of T1 in prenex form, that is chains of quantifiers applied to quantifier-free formulas (using equivalences from 2.5 and 2.6 simplified for a nonempty model).
Interpret the symbol = in axioms as an ordinary predicate symbol, with the axioms of equality [1.11].

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 T2 (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 T2 is still consistent, as any contradiction in T2 (= finite set of axioms not satisfied by any tuple of Boolean values of their variables) would provide a contradiction in T1, as follows:
From all subterms occurring in used axioms of T2, 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 T1, into the axiom ∀x,z, A(x,K(x),z, S(x,z)) in T2. Successively replace them all by variables in T1: for terms S(t0,t1) and S(t0,t2) (where t0, t1, t2 ∈ M), the reasoning in T1 will say
"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 use the contradiction in T2 where y replaces K(t0), u1 replaces S(t0,t1) and u2 replaces S(t0,t2).
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.  ∎

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
3. Algebra 1
4. Arithmetic and first-order foundations
4.1. Algebraic terms
4.2. Quotient systems
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness
4.7. Countability and Completeness
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions
4.A. The Berry paradox
5. Second-order foundations
6. Foundations of Geometry