The completeness theorem of first-order logic

4.7. Countability and Completeness

Countable sets

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

The following are equivalent

A is either finite or countably infinite
A is countable
There exists a total order on A such that all <⃖(x) are finite.

Obviously 1. ⇒ 2. ⇒ 3.
Proof of 3. ⇒ 1.
It is easy to see that f = (A∋x ↦ |<⃖(x)|) is strictly monotone. Thus
∀x∈A, f[<⃖(x)] ⊂ <⃖(f(x)) = V_f(x), and (as f is injective) |f[<⃖(x)]| = |<⃖(x)| = f(x).
Thus by Dedekind-finiteness f[<⃖(x)] = V_f(x).
Finally, Im f ≠ ℕ ⇒ ∃y∈ ℕ\Im f, ∀x∈A, y∉ V_f(x) ∴ f(x) ≤ y hence A is finite.∎
Moreover with finite A, Im f = V_|A| for the same reason as with f[<⃖(x)].

Another way to prove 2. ⇒ 1. is as follows. Let A⊂ℕ, and assume A≠∅ (as ∅ is finite).
Let S_A the successor function (3.12) of A.
As we described the set of all finite subsets of ℕ in 4.6., if A is infinite then A ⊂ Dom S_A, thus |ℕ| ≤ |A|.∎

Any quotient of a countable set is countable. Namely, like already seen with finite sets, any surjection f: ℕ ↠ A has a section given by y↦ min f_•(y).

For the same reason, any product of nonempty subsets of ℕ is nonempty. However, to extend this to products of nonempty countable sets, depends on the existence of a family of choices of injections to ℕ. So, it works if a definition specifying such choices is available; otherwise, it fails since not using the axiom of choice was the point of the question.

Sums of total orders

The sum of a totally ordered family of totally ordered sets ((A_i, ≤_i)_i∈I with a total order on I), is their disjoint union U with the total order defined as follows. Assuming these sets pairwise disjoint to simplify notations as U = ⋃_i∈I A_i, let

≤_U = (⋃_i∈I ≤_i) ∪ (⋃_i<j∈I A_i×A_j)

If I and all A_i are well-ordered then their sum is also well-ordered.
Proof: for any nonempty B⊂U, the least element of B∩A_i for the least i such that B∩A_i ≠ ∅, is the least element of B.∎

However, the property of finiteness of all <⃖(x) is not always preserved. For example it holds in V_n ⊔ ℕ, but not in ℕ ⊔ V_n if n ≠ 0.
For any sequence a∈ℕ^ℕ, the sum U = ∐_n∈ℕ V_{a_n} satisfies

∀(n,x)∈U, |<⃖(n,x)| = x + ∑_k<n a_k

forming a bijection from U to V_{∑_n∈ℕ a_n} if a has finite support, or to ℕ otherwise.
If a is a constant function with value b∈ℕ*, this gives the bijection from ℕ×V_b to ℕ

∀(q,r)∈ℕ×V_b, |<⃖(q,r)| = b⋅q + r

whose inverse is called the Euclidean division by b.

More generally, any set of the form U = ⋃_n∈ℕ A_n where A_n is finite with a specified total order (thus specified injection to V_{|A_n|}) is countable.

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

Proof. The union is a quotient of the disjoint union, which is countable.∎

In particular, ℕ² is countable because it is ⋃_n∈ℕ V_n².
This gives a bijection from ℕ² to ℕ defined by (x,y) ↦ (x < y ? y⋅y + x : x⋅x + x + y).
Another bijection, with a generalization to ℕ^k for any k > 0, will be introduced next.

Lexicographic order

A lexicographically ordered set is a set of functions F ⊂ Y^X where X, Y are totally ordered sets, such that for all f≠g ∈F, the set {x∈X| f(x) ≠ g(x)} has a greatest element m_f,g : this lets a total order on F be defined by f<g ⇔ f(m_f,g) < g(m_f,g).

(Another definition uses the least element, which amounts to reversing the order of X, but that is less useful)

The positional numeral systems, of which the decimal system is a particular case, come depending on a choice of base b > 1, as the use of the lexicographically ordered set V_b^(ℕ).
Indeed

∀g∈V_b^(ℕ),∀x∈ℕ, {f∈V_b^(ℕ)|f<g ∧ m_f,g = x} ≈ V_b^x×V_g(x)

from which comes

|{f∈V_b^(ℕ)|f<g}| = ∑_x∈ℕ b^x ⋅ g(x)

hence V_b^(ℕ) is countably infinite. The particular case V₂^(ℕ) is identifiable with ℘_fin(ℕ),

∀B∈℘_fin(ℕ),|{A∈℘_fin(ℕ)|A<B}| = ∑_x∈B 2^x

and this bijection from ℕ to ℘_fin(ℕ) is a curried form of the BIT predicate.

Now for k > 0 let F_k ⊂ ℕ^k the set of monotone k-tuples of natural numbers. For all g∈F_k and x<k the set {f∈F_k|f<g ∧ m_f,g = x} is in bijection (by restriction) with the set of monotone f:V_x+1 → V_g(x), with cardinal C⁺(g(x),x+1) = C(g(x)+x,x+1). So

|{f∈F_k|f<g}| = ∑_x<k C⁺(g(x),x+1)

hence F_k is countably infinite. Finally, ℕ^k is also countably infinite as h∈ℕ^k bijectively defines f∈F_k by

∀x<k, f(x) = ∑_i≤x h(i).

x\y	0	1	2	3	4
0	0	1	3	6	10
1	2	4	7	11
2	5	8	12
3	9	13

In particular with k=2 we get b₂ : ℕ×ℕ → ℕ defined as b₂(x,y) = T_x+y+x where the triangular numbers are defined by T_n = C⁺(n,2) or equivalently by T₀ = 0 ∧ ∀n∈ℕ, T_n+1 = T_n+n+1.
This gives ℕ² the ground (0,S)-term algebra structure (recursively defining b₂^-1(z))

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

Another way to express b₂^-1 (to infer x and y from b₂(x,y)) first calculates x+y as the only n such that T_n ≤ b₂(x,y) < T_Sn.

The below needs rework

Countable term algebras

Obviously, any ground term algebra whose language L has at least a constant and a non-constant, is Dedekind-infinite. Now, it is more precisely countably infinite if L is countable. Indeed we can define a ground term L-algebra structure on ℕ, which is a bijection from ^Lℕ to ℕ, as follows.
Split L as C∪D where C is the set of constants, and D is the rest of symbols. Then ^Lℕ = C∪(^Dℕ), while C and D are countable, and ^Dℕ is countably infinite (as a sum over D of countably infinite sets, across which a choice of bijections with ℕ can be defined). From there, a bijection from C∪(^Dℕ) to ℕ can be easily found.
In practice, such a bijection from ^Lℕ to ℕ is likely to be already a ground term L-algebra structure provided that its inverse, as a sequence covering C∪(^Dℕ), starts with an element of C.
Indeed, natural cases of such bijections lead to ∀(s,x)∈^Dℕ, ∀i<n_s, x_i<s(x) which would be contradicted by the smallest element outside Min_L ℕ. ∎

Countable choice and dependent choice

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.

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

Existence of ℕ
Existence of a (countable) ground term algebra for any countable algebraic language
Existence of a (countable) model for any consistent first-order theory with a countable language
Existence of an injective {0,S}-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 {0,S}-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, Id_^LU) an injective L-algebra.

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

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

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.

Here is a rather short sketch of proof of the first statement (implicitly suggesting a possible form of a proving system, ignoring efficiency issues) - an even shorter version is contained in that other page.

Reduce T to a single-type theory T₁ simulating the use of types by relevant unary predicate symbols and axioms, but without requiring all objects to belong to some type. Thus, adding the axiom (∃x, 1) to T₁ brings no contradiction (it does not prevent empty types).
This allows to re-write axioms of T₁ in prenex form, that is chains of quantifiers applied to quantifier-free formulas, by equivalences adapted from 2.5 and 2.7, such as

(C ∧ ∃_Ax, R(x)) ⇔ (∃x, C ∧ A(x) ∧ R(x))
(C ∨ ∃_Ax, B(x)) ⇔ (∃x, C ∨ (A(x) ∧ B(x)))
(C ∧ ∀_Ax, B(x)) ⇔ (∀x, C ∧ (A(x) ⇒ B(x)))

Interpret the symbol = in axioms as an ordinary predicate symbol, with the axioms of equality [1.11] (those only using the structures named in the language, which suffice, are already in prenex form and do not use ∃).

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

(The axioms of equality over these are not needed)
Let M be the ground term algebra over the language of operator symbols enriched as just described.
Read the chain of ∀ in each axiom as declaring an axiom schema: one copy of the axiom per possible replacement of its variables by a tuple of elements of M. This 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 sub-terms 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, for example ∀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 these symbols 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₂);"
then 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 bijection from ℕ to ^PM (or anyway a ground functional {0,S}-draft structure on ^PM), 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 a model is formed by quotienting M by the "equality" relation, and removing the elements with no type. ∎

As this construction depends on multiple choices (between equivalent formalizations of a theory, possible bijections from ℕ to ^PM, and variations are possible on the method itself), it can give different models, which may be non-isomorphic and even have different truth values of the theory's undecidable statements.

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

Taking the completeness theorem with Cantor's theorem gives this paradox :
Any consistent set theory has a countable model U, including a set P defined by its term "℘(ℕ)" it sees as uncountable.

P being a part of U is meta-countable, but it is interpreted as uncountable, thus any of its meta-bijections with ℕ "does not exist" (has no representative) as an element of U.

Being meta-countable, P must differ from the meta-interpretation of ℘(ℕ) which is meta-uncountable: P contains all objects in U which play roles of subsets of ℕ, but not all meta-subsets of ℕ are so represented.

Indeed, when the powerset axiom declares the class of subsets of ℕ to be a set ℘(ℕ), it only determines ℘(ℕ) as given by the range of subsets of ℕ which happen to exist (be represented) in the current universe, thus remains relative to this universe.

In the other interpretation of what it means for a class to be a set ("strong" version in "Classes and sets in expanding universes"), this would mean that our universe already contains "really all" subsets of ℕ, forming the supposedly "true" set ℘(ℕ) which will stay fixed in any further expansion of the universe. However, 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