4.6. Finiteness

To review equivalent forms of the axiom of infinity, we need to work without assuming it.

Equinumerosity and cardinals

The equivalence predicate ≈ of equinumerosity between sets, is defined by the existence of a bijection :

AB ⇔ ∃fBA, f : AB

Equinumerous sets are said to "have the same cardinal". For our needs, the cardinal |A| of any set A, intuitively meant as the equivalence class of A by ≈ in the class of all sets, can be formalized as A itself, where any direct or indirect use of "equality" between cardinals (never mixed with other elements) actually refers to the use of ≈.
For example, a "set of cardinals" can be thought of as a set of sets, and an inclusion between two of them, XY, can be read as abbreviating (∀AX, ∃BY, AB). More specifically, this can even be directly seen as inclusion if both X and Y are seen as unions of equinumerosity classes inside the powerset of an arbitrary fixed large enough set, such as the union of all the sets which are considered in a given context. This practice is a particular case of development of a theory (here, set theory), as will be detailed in 4.11.

Some binary predicates on the class of sets

Cardinals are naturally ordered by : |A| ≤ |B| if there exists an injection from A to B. Indeed it is obviously a preorder (as injections form the morphisms of a category on the class of sets), while its antisymmetry is given by the Cantor-Bernstein theorem.
Let us define the binary predicates ≺ and S by

|A| ≺ |B| ⇔ ∃f:AB, Im fB
ASB ⇔ ∃xB, A = B\{x}.


ASB ⇒ |A| ≺ |B| ⇒ |A| ≤ |B| ⇔ (|A| ≺ |B| ∨ AB).
|A| ≺ ℘(A)

Indeed Ax↦{x} : A↪℘(A) and ∅∈℘(A) is not a singleton; moreover by Cantor's theorem (2.7), |A| ≠ ℘(A).
For any sets A,B,C,
  1. ASB ⇒ (|A| ≺ |C| ⇔ |B| ≤ |C|)
  2. ASB ⇒ (|C| ≺ |B| ⇔ |C| ≤ |A|)
Proving 1. is easy. Then 2. can be deduced by noting that if (ASBf:CB ∧ Im fB) then

Im fA ∨ (D = fA ⇒ (DSCf|D:DA ∧ Im f|DA)) ∎

Then for any sets A,B,C,D,


This can deduced (simpler than done elsewhere) from the above, either by Cantor-Bernstein, or by noting that the constructed injections are bijective here.
Namely, for BDAC, which uses 2., denoting ∁BA = {x}, ∁DC = {y} and f : BD, it can be written

(f(x) y)Df|A = (Az ↦ (f(z) = y ? f(x) : f(z))) : AC

because f -1(y) ∈ Af(x) ≠ yf(x)∈ C.

Structures relating cardinals

Any meta-structure first defined on the class of set, defines by restriction a structure on the powerset ℘(E) of any set E, and then by quotient, on the set KE = ℘(E)/≈ of cardinals of subsets of E. From definitions with abusive notations, |A| ≤ |E| ⇔ |A| ∈ KE.

In KE, the relation S is both functional and injective thanks to the above result. Let us complete this into a structure with language Σ = {0,S} first introduced to define ℕ, by interpreting 0 as {∅}. Then as a Σ-system, KE is functional, surjective and injective, and Dom SKE ∪ {|E|} = KE.

If FE then the natural injection from KF to KE is a Σ-embedding (like any injective morphism from a surjective system to an injective one). As each KE plays the role of a set of cardinals (namely those less than |E|), such natural injections can be conventionally seen as inclusions (KFKE).

On the "class" of cardinals, operators of addition, multiplication and exponentiation are naturally defined from the relevant operations between sets,

|A| + |B| = |AB|
|A| ⋅ |B| = |A×B|
|A||B| = |AB|
1 = |{•}|

with their famous equality properties deducible from the existences of canonical bijections (2.8).


Without assuming them to form a set ℕ, natural numbers can be conceived as synonymity classes of Σ-terms.

A subset AE will be called finite if, equivalently,

  1. A ∈ MinΣ ℘(E), i.e. ∅⌈SEA
  2. |A| ∈ MinΣ KE
  3. AVn for some natural number n
  4. There is a B ⊂ ℘(E) that is a Σ-term with root A.
Moreover this does not depend on E, and a finite A determines the number n=|A| in 2., 3. and 4..

Proof. 4.⇒1.⇒2. is obvious.
2.⇒3. : in the Σ-draft D = MinΣ KE, S is injective and its transitive closure T is irreflexive (by well-foundedness), thus

T ∈ MorΣ(D,℘(D))

Denoting Vn = T(n), the function n↦|Vn| forms a Σ-morphism from D to KED.
Thus ∀nD, |Vn|=n in the convention that DKED.

3.⇒4. : T defines a Σ-embedding from the term with root n into ℘(Vn) which is isomorphic to ℘(A) when AVn.
Remaining details are left to the reader.∎

Some properties of cardinal ordering

Proposition. If a set E is finite then KE is the ground Σ-term with root |E| (so, all subsets of finite sets are finite, and the order between finite cardinals is the one generated by S) and for any set F, |E| ≤ |F| ∨ |F| ≤ |E|.

To prove it comes down to proving that any cardinal |F| outside the ground Σ-term X with root |E| is greater than |E|, which can be conveniently done in two possible ways.

One way involves a distinction of cases.
If F is infinite, from Dom SKF ∪ {|F|} = KF we deduce MinΣ KF ⊂ Dom SKF, thus MinΣ KF is a ground term Σ-algebra, i.e. a copy of ℕ, thus contains all finite cardinals: any finite cardinal is lower than any infinite one.
If F is finite then |E|, |F| both belong to MinΣ KEF. There, any two elements are comparable by ⌈S⌉ because, by the proof from 4.5, any nonempty subset of MinΣ KEF has a least element for ⌈S⌉. Then they are also comparable by ≤ as ⌈S⌉ ⊂ ≤.

The other way uses 0 ≤ |F| and

∀(x,y)∈SX, |F| ≠ x ≤ |F| ⇒ x ≺ |F| ⇒ y ≤ |F| ∎

Proposition. For any set E, |E| ≺ |E| ⇔ |ℕ| ≤ |E| which implies that E is infinite.

Proof. If f:EE and x ∈ ∁E Im f then 〈{x}〉f ≈ ℕ (as a unary {f}-term algebra), and |E| ≤ |∁E {x}| which, by antisymmetry, contradicts the irreflexivity of S among cardinals of finite sets.
Conversely, if ℕ ⊂ E then the extension of S by IdE\ℕ is an injective, non-surjective transformation of E.∎
(The missing converse, that |ℕ| ≤ |E| for any infinite E, cannot be proven without the axiom of choice, as will be discussed in 5.5)

Equivalent expressions of the axiom of infinity

Let us review equivalent statements of the axiom of infinity in set theory with the powerset. (Our first two expressions directly involve the powerset anyway, though the next ones might do without it.)

The first two are the statements of existence of

Indeed by the above, ℕ is infinite, while from any infinite E we can define ℕ = MinΣ KE.
Other equivalent statements are those of existence of Indeed Σ is such a language ; conversely, such an injective algebra can easily be seen as an injective Σ-algebra by picking a constant symbol and defining an injective S out of a non-constant symbol.

More equivalent statements will be reviewed in the next section.

More results

When an operator between cardinals (an operator between sets where the cardinal of the result only depends on those of the arguments) can be expressed as recursive with respect to a given argument, this usually allows to deduce by induction the finiteness of the result when arguments take finite values. Then the restriction to ℕ of such operators form arithmetical operations thus defined by set theoretical tools, bypassing the difficulties to justify the meaningfulness of recursive definitions in first-order arithmetic.

In particular, if A and B are finite then AB, A×B and AB are finite. Indeed these can be successively deduced by induction as follows: for a given finite A, the fininess holds for B = ∅, and if BSB' then the finiteness of the result from (A,B) implies that from (A,B'), because, respectively,


So, the class of finite cardinals (which is a set ℕ if not all sets are finite), is stable by the algebraic structures of addition, multiplication and exponentiation, and is thus a model of arithmetic.

A union AB of finite sets is also finite. This can be seen as ABA⊔(B\A), where B\A is finite because B is. From this, follows by induction that any finite union of finite sets is finite. Then, any term is finite (the set of roots of infinite sub-terms of a draft is empty thanks to well-foundedness, when all symbols have finite arities).

As V2B ⥬ ℘(B), the finiteness of B implies that of ℘(B), and both are equivalent since |B| < ℘(B).

If there is a surjection f : AB and A is finite then B is finite, |B| ≤ |A|, and (|B| = |A| ⇔ Inj f).
There are two main ways to prove it:

Any left cancellative element of a finite monoid (M, e, •) is invertible. Thus, any finite cancellative monoid is a group.

Proof: for any xM, the transformation •(x) is injective in a finite set, thus also surjective. Being both left invertible and right cancellative (a monic retraction), x is invertible.∎

Finite composition in commutative monoids

Let uMX where X is a finite set and (M, e, •) is a monoid. Totally ordering X turns u into a string, element of some free monoid F, such as the one with basis Im u (generally, if u = vw then a total order on X gives w the role of element of the free monoid F with basis Dom v), which is then interpreted in M by the unique morphism of monoids from F to M which extends IdIm u (or v).
Now if M is commutative then this value of u in M is independent of the chosen order on X; we shall call it the composite of u and write it [u]. This may later be called the sum or product of u depending on the name of the composition operation in given monoids which will be taken in the role of M, such as the addition or the multiplication in ℕ or another numbers system.
This pushes further the removal of structures from ground {e,•}-terms to be interpreted in monoids: the commutativity axiom now removes the total order from the domain X of the string, after the axioms of associativity and identity removed the parenthesis and occurrences of the identity element from terms (turning them into strings).

Let us prove this by induction on the cardinal of X. The composite in M of the empty function is the identity element e of M, obviously independently of a total order on the empty X.
Any total order on a nonempty X has a last element xX. Then denoting A = X\{x}, the value in M of the string it gives is au(x) where aM is the composite of u|A (common value for all its total orders). What needs to be checked is that for all x,yX, denoting a, bM the respective composites of u|A and u|B where A = X\{x} and B = X\{y}, we have au(x) = bu(y).
If x=y we are done. Otherwise, denoting c = •[u|X\{x,y}] ∈ M (or the value it takes for any chosen order on X\{x,y}), we have

au(x) = c•(u(y)•u(x)) = c•(u(x)•u(y)) = bu(y). ∎

Obviously for any AX we have

[u] = [u|A] • [u|X\A] = [u|X\A] • [u|A].

Our proof from which this result is inferred, only used commutativity between elements of Im u. So, this implicitly contains or repeats the proof from 3.5 that a monoid generated by a commutative subset is also commutative.

(to be completed)

Back to homepage : 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