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

Let

If ∃

Otherwise,

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

- 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 Σ-algebra.

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 * ^{L}U* ⊂

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

y\x |
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 |

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 |

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

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.

Some come by taking inspiration from each of both above bijections between ℕ

More ways are obtained by picking a bijection

ℕ^{Sn} ≈ ℕ^{n}×ℕ ≈ ℕ×ℕ ≈ ℕ

ℕ^{Sn} ≈ ℕ×ℕ^{n} ≈ ℕ×ℕ ≈ ℕ

Formally, the first way recusively defines this sequence of bijections

*b*_{1}=Id_{ℕ}

∀*n*∈ℕ*,∀*u*∈ℕ^{Sn}, *b _{Sn}*(

Split

In practice, such a bijection from

Indeed, natural cases of such bijections lead to ∀(

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

Reduce *T* to a single-type theory *T*_{1} 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*_{1} brings no contradiction (it does not prevent
empty types).

This allows to re-write axioms of *T*_{1} 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* ∧ ∃_{A}*x*, *R*(*x*))
⇔ (∃*x*, *C* ∧ *A*(*x*) ∧ *R*(*x*))

(*C* ∨ ∃_{A}*x*, *B*(*x*)) ⇔
(∃*x*, *C* ∨ (*A*(*x*) ∧ *B*(*x*)))

(*C* ∧ ∀_{A}*x*, *B*(*x*)) ⇔ (∀*x*, *C* ∧ (*A*(*x*) ⇒ *B*(*x*)))

(∀*x*,*x'*, ∃*y*, ∀*z*,
*A*(*x*,*x'*,*y*,*z*))
⇢ (∀*x*,*x'*,∀*z*,
*A*(*x*,*x'*,*K*(*x*,*x'*), *z*)).

Let

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

Observe that

From all sub-terms occurring in used axioms of T_{2}, 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_{1}, into the axiom ∀x,z, A(x,K(x),z,
S(x,z)) in T_{2}. Successively replace these symbols by variables in T_{1}: for terms
S(t_{0},t_{1})
and S(t_{0},t_{2})
(where t_{0}, t_{1}, t_{2}
∈ MT_{1} will say"Let y such that ∀z,∃u,
A(t_{0},y,z,u); let u_{1} such that
A(t_{0},y,t_{1},u_{1});let u_{2} such that
A(t_{0},y,t_{2},u_{2});"then use the contradiction in T_{2} where y replaces
K(t_{0}), u_{1} replaces
S(t_{0},t_{1}) and u_{2}
replaces S(t_{0},t_{2}). |

Then a model is formed by quotienting

As this construction depends on multiple choices (between equivalent formalizations
of a theory, possible bijections from ℕ to ^{P}*M*, 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.

T⊢A

⇔T∪ {¬A} is inconsistent

⇔T∪ {¬A} has no countable model

⇔Ais true in all countable models ofT. ∎

*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.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 4.2. Quotient systems

4.3. Term algebras

4.4. Integers and recursion

4.5. Presburger Arithmetic

4.6. Finiteness

4.7.

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

6. Foundations of Geometry