The completeness theorem of first-order logic

4.7. Countability and Completeness

Numbers of injections

For any finite sets X, Y, the set Inj(X,Y) of injections from X to Y is finite (subset of the finite set Y^X), and its cardinal only depends on those of X and Y. Let us denote

P(|Y|,|X|) = |Inj(X,Y)|

Then obviously ∀n∈ℕ,

P(n,0) = 1
P(n,1) = n
∀k∈ℕ, n<k ⇒ P(n,k) = 0

Now let A ⊂ X, B = X\A and π_A : Inj(X,Y) → Inj(A,Y) defined by f ↦ f_|A. Then

∀g∈ Inj(A,Y), π_A•(g) ≈ Inj(B, Y\Im g)

by the bijection f ↦ f_|B. Hence with |A|=i=|Im g|, |B|= k and |Y|= n+i,

∀n,k,i ∈ℕ, P(n+i, k+i) = P(n,k)⋅P(n+i, i)

In particular,

P(n+1, k+1) = P(n,k)⋅(n+1)
P(n+i, i+1) = n⋅P(n+i, i)

The last one can also be written

∀n,k ∈ℕ, P(n,k+1) = (n−k)⋅P(n,k)

by extension to n<k ⇒ P(n,k+1)= 0 = P(n,k).
Either formula, together with P(n,0) = 1 and the 0 value for n<k, forms a recursive definition of P(n,k). Either way, this implies coincidence with the definition of the falling factorial (among other possible notations and names) on a larger domain

∀n∈ℤ,∀k∈ℕ, P(n,k) = ∏_i<k (n−i)

where i<k abbreviates i∈V_k.

The above formulas keep validity for negative n except that P(n,k) ≠ 0. Namely, it is conveniently expressed there by the rising factorial

∀n∈ℤ,∀k∈ℕ, P⁺(n,k) = ∏_i<k (n+i) = P(n+k−1,k)
P(-n,k) = P⁺(n,k)⋅(-1)^k

The factorial comes as a particular case :

∀n∈ℕ, n! = |𝔖_n| = P(n,n) = P⁺(1,n) >0

The falling and rising factorials can be expressed from it : ∀n,k ∈ℕ,

n!⋅P⁺(n+1, k) = n!⋅P(n+k,k) = (n+k)!

Numbers of combinations

For any set X and any k∈ℕ, a k-combination of X is a subset A⊂X such that |A| = k. The number of k-combinations of V_n (and thus of any set of n elements) is denoted C(n,k). This easily implies by Inj(V_k,V_n)∋f ↦ Im f, the following formula which we extend as a definition of C on a larger domain:

∀n∈ℤ,∀k∈ℕ, k!⋅C(n,k) = P(n,k)

Indeed P(n,k) is still a multiple of k! for negative n, as it repeats its values from positive n for the same k. Namely, let us similarly define ∀n∈ℤ,∀k∈ℕ,

C⁺(n,k) = C(n+k−1,k)
C(-n,k) = C⁺(n,k)⋅(-1)^k

including C⁺(0,0) = C(0,0) = 1 from the latter formula.

As 0! = 1! = 1 we generally have C(n,0) = C⁺(n,0) = 1 and C(n,1) = C⁺(n,1) = n.
As A ↦ ∁_X A defines a bijective correspondence between k-combinations and n-combinations of V_n+k,

∀n,k∈ℕ, C(n+k,k) = C(n+k,n) = C⁺(n+1,k) = C⁺(k+1,n)

The first equality is more usually written k≤n ⇒ C(n,k) = C(n,n−k).

Given n=|X| and k,l∈ℕ, the number of possible data of disjoint A,B ⊂X with |A| = k and |B| = l, can be expressed in 3 ways according to which of A, B or A∪B is chosen first. This gives the following double equality (its validity for all n∈ℤ follows either by relating cases of negative n to those of positive n, or by deducing the general formula from numerical definitions after multiplication by k!⋅l!) :

∀n∈ℤ,∀k,l∈ℕ, C(n−k,l)⋅C(n,k) = C(n−l,k)⋅C(n,l) = C(k+l,l)⋅C(n,k+l)

In particular when l = 1

∀n∈ℤ,∀k∈ℕ, (n−k)⋅C(n,k) = n⋅C(n−1,k) = (k+1)⋅C(n,k+1)

From there follows

∀n∈ℤ,∀k∈ℕ*, C(n,k) = C(n−1,k−1) + C(n−1,k)

The simple proof for n,k∈ℕ*, is that a k-combination of V_n is either a k-combination of V_n−1, or ({n−1} ∪ a k−1-combination of V_n−1).
General proof :
k⋅C(n−1,k) = (n−k)⋅C(n−1,k−1) = k⋅(C(n,k) − C(n−1,k−1)) ∎
This proof has 2 variants, each failing to cover some cases due to multiplication by zero:

n⋅C(n−1,k) = (n−k)⋅C(n,k) = n⋅(C(n,k) − C(n−1,k−1))
(n−k)⋅C(n−1,k) = n⋅C(n−1,k) − k⋅C(n−1,k) = (n−k)⋅(C(n,k) − C(n−1,k−1))

The form of these versions together suggest an idea of possible failure on n=k=0 for an extension of C(n,k) to negative k. Two natural extensions may be considered. The one giving 0 for all negative k, preserves C(n,k) = C(n−1,k−1) + C(n−1,k) but breaks C(n,k) = C(n,n−k). Another, preserves the latter but breaks the former and switches the sign of the link between C(n+k−1,k) and C(-n,k) for negative k. We shall not use either.

The number of strictly monotone g:V_k → V_n is C(n,k).
Proof : g bijectively matches the k-combination Im g of V_n. ∎

The number of monotone f:V_k → V_n is C⁺(n,k).
Proof : f bijectively matches strictly monotone g:V_k → V_n+k−1 by g(x) = f(x) + x. ∎

Monotone f:V_k → V_n+1, monotone g:V_n → V_k+1, and k-combinations A of V_n+k, are so bijectively related by

∀x<k, ∀y<n, f(x) ≤ y ⇔ x < g(y) ⇔ x < |A∩V_x+y+1|

The number of h:V_n → ℕ such that ∑h = k is C⁺(n,k).
Proof : h bijectively matches monotone f:V_k → V_n by ∀x<n, h(x) = |f_•(x)|. ∎

The number of h:V_n → ℕ such that ∑h ≤ k is C⁺(n+1,k).
Proof : they are bijectively h = h'_{|V_n} for h':V_n+1 → ℕ such that ∑h' = k. ∎

The number of h:V_k → ℕ such that ∑h < n is C⁺(n,k).
Proof : h bijectively matches monotone f:V_k → V_n by ∀x<k, f(x) = ∑_i≤x h(i). ∎

Related wikipedia pages:

Binomial coefficient

Combination

Multiset

Countable sets

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

Not all sets are countable, as in particular ℘(ℕ) is not countable.

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 each A_n is finite, is countable under either additional assumption

The axiom of countable choice AC_ℕ
Or, each A_n has an invariant (specifiable) total order (thus specified injection to V_{|A_n|}).

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

Under the axiom of countable choice, any infinite set E is Dedekind-infinite.

Proof. ∀n∈ℕ, ∃j: V_n↪E. Hence the existence of a function from the countable set ∐_n∈ℕ V_n to E whose restriction to each component V_n is injective. Its image is both countable and infinite, thus |ℕ| ≤ |E|.∎

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

ℕ² 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).
Hence the countability of any U = ⋃_n∈ℕ A_n where each A_n is countable, either with an invariant injection to ℕ (which together define a surjection from a subset of ℕ² to U), or under countable choice.

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.

Countable term algebras

Constructing ground term algebras over any language, suffices to also give term algebras with any set of variables, by treating those variables as more constants in the language. This construction remains to be specified for any language L₀∪L₁ where the set L₀ of constants and the set L₁ of other symbols (with nonzero arity), are both non-empty (beyond the one-one case for which it gave ℕ).
Obviously, such ground term algebras are also Dedekind-infinite. We shall prove their existence, starting with cases of countable L, for which they are also countably infinite.
Indeed we can define a ground term L₀∪L₁-algebra structure on ℕ as follows.
^L₀∪L₁ℕ = L₀∪ ^L₁ℕ, while L₀ is countable, and since L₁ is countable,

^L₁ℕ = ∐_s∈L₁ ℕ^n_s ≈ L₁×ℕ ≈ ℕ

By such a bijection of a natural kind as above defined, any (s,u) ∈ ^L₁ℕ matches an n ∈ ℕ such that Im u ⊂ V_n+1.
But, after composing this with a natural bijection of L₀∪ ℕ with ℕ starting with a constant (from L₀), to give ℕ a bijective L₀∪L₁-structure, any (s,u) ∈ ^L₁ℕ finally matches there an n ∈ ℕ such that Im u ⊂ V_n.
In other words, the relation R from 4.1 is included in the strict order of ℕ and is thus well-founded. This gives ℕ a role of ground L₀∪L₁-term algebra. ∎

Generally, one may form a ground term L-algebra out of any injective L-algebra, by taking its minimal subalgebra.

Aside this construction of countable term algebras based on the axiom of infinity, another idea to form injective algebras starts by assuming the existence of a model U of a very simple kind of set theory. Namely, the excerpt of set theory which describes tuples, makes U an injective algebra over the language made of the tuples definers. From this, term algebras come as subalgebras generated by sets whose elements are not tuples. Beyond the mere tuples definers, for any language L of algebraic symbols which belong to U, the set U is an injective L-algebra. If U is standard, this takes the simple form ^LU ⊂ U, making (U, Id_^LU) an injective L-algebra.

Proof of 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 statement A true in all countable models of T is deducible from its axioms.

The equivalence is easy : 1. is the particular case of 2. where A is 0 (false); conversely, it implies all of 2. by

There can be different ways to prove 1. (or even directly 2.) depending on the precise chosen formal system of rules of proof with this quality. But, we shall skip here such details (those of propositional calculus, whose interest is rather technical and specialized), or somehow keep them implicit, to focus on the other side of the proof : the construction of a model of any consistent theory. Yet I have two such constructions to offer (which may be both original, as usual proofs given elsewhere look much more complex).

The below method, first transforms T by somehow sorting its components by kinds, then successively applies a different construction for each kind. Its advantage is that each separate construction is more "pure" forming a distinct concept.
Another method in another page, keeps the theory with its mixture of components, to apply one global construction encompassing all kinds. It is somewhat simpler and more intuitive.

As T may admit multiple types, it is first reduced to a single-type theory T₁ simulating the use of types by unary relation symbols and axioms (as in 1.7 and 1.10), but not requiring all objects to belong to some type. Adding the axiom (∃x, 1) in T₁ (if not a theorem of T) is harmless, not contradicting a possible emptiness of each type.
Axioms of T₁ are then expressed 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)))

Then turn T₁ into a theory T₂ by 2 more changes

Remove ∃ from axioms, by replacing each occurrence of ∃ 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 role of = gets played by an ordinary relation symbol with the axioms of equality 1. to 5. where axiom schemas 2. and 5. range over the symbols from T₁.

(Axiom 5. of equality over additional operation symbols is neither needed nor harmful).

Form a propositional theory T₃, made of

The set ^PM of Boolean variables where P is the set of relation symbols from T₂ and M is the ground term algebra with operation symbols from T₂.
Axioms (composed of logical connectives over Boolean variables), come from those of T₂ seen as shemas (one copy of an axiom per possible replacement of its variables under ∀ by a tuple of elements of M)

If T₃ had a contradiction, namely if a finite set of its axioms was not satisfiable by any tuple of Boolean values of their variables, it would lead to a contradiction in T₁ as follows:

Take the finite list (without repetition) of all terms whose root is an additional symbol S of T₂ (not from T), and which occur as sub-terms among the axioms of T₃ involved in the contradiction. Then list all axioms of T₂ which use these terms. For example an axiom of T₁,

∀x,∃y,∀z,∃u, A(x,y,z,u)

gave the axiom of T₂

∀x,z, A(x,K(x),z, S(x,z))

Successively replace any such terms in used axioms of T₂ by variables in T₁, as follows : if we have for example terms S(t₀,t₁) and S(t₀,t₂) (where t₀, t₁, t₂ ∈ M), the reasoning in T₁ will first do such replacements in t₀,t₁ and t₂ where applicable (starting with their smallest sub-terms), then say of the so modified t₀,t₁ and t₂
"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 so on, to finally apply the contradiction from T₃ where y replaces K(t₀), u₁ replaces S(t₀,t₁) and u₂ replaces S(t₀,t₂).

Now in absence of contradiction, the set ^PM of Boolean variables gets interpreted this way : recursively by a chosen bijection from ℕ to ^PM, add one by one to the axioms, each of these Boolean variables if not refutable from previously accepted axioms. So, 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.

Skolem's Paradox

Comparing the completeness theorem with Cantor's theorem gives this paradox :
Any consistent set theory has a countable model U, including a set P playing the role named as "℘(ℕ)", which it qualifies as "uncountable".

This discrepancy can be analyzed in two ways:

As a discrepancy of interpretation of ℘(ℕ): P is the set of all elements of U playing roles of subsets of ℕ, but, as a countable set, this role-playing cannot be bijective to "the true" uncountable ℘(ℕ). This means not all (meta-)subsets of ℕ appear as sets in U.
While there exist bijections between P and ℕ, this claim is seen as false when interpreting set theory taking U as universe. This means any such bijection "does not exist" (has no representative) as an element of U. This discrepancy is similar to the previous one, affecting set exponentiation instead of powerset.

Actually, even the interpretation of ℕ is likely to differ, as we shall explain with non-standard models of arithmetic ; but this does not invalidate the above observations (and there also exist countable universes whose interpretations of arithmetic are standard, as will be seen with the Lowenheim-Skolem theorem).

Anyway so, 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 the current 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