Cardinal number and Ordinal number are two concepts derived from human abilities on judging and comparing quantities, the two intuitive roots of number sense.
For ordinal number we have axioms as below:
- O1: trichotomy, for any elements x and y, exactly one of these statements is true:
- x < y
- y < x
- x = y
- O2: transitivity, for any elements x, y, z, if x < y and y < z, then x < z.
- O3: well-ordered, every nonempty subset has a least element, that is, it has an element x such that there is no other element y in the subset where y < x.
On the other hand, the definition of Cardinal number is a little bit complex. So let's just back to the Peano numbers.
- P1: 0 is a natural number.
- P2: axioms on equality
- P2.1: for every natural number x, x = x. That is, equality is reflexive.
- P2.2: for all natural numbers x and y, if x = y, then y = x. That is, equality is symmetric.
- P2.3: for all natural numbers x, y and z, if x = y and y = z, then x = z. That is, equality is transitive.
- P2.4: for all a and b, if b is a natural number and a = b, then a is also a natural number. That is, the natural numbers are closed under equality.
- P3: axioms on successor
- P3.1: for every natural number n, S(n) is a natural number. That is, the natural numbers are closed under S.
- P3.2: for all natural numbers m and n, m = n if and only if S(m) = S(n). That is, S is an injection.
- P3.3: for every natural number n, S(n) = 0 is false. That is, there is no natural number whose successor is 0.
- P4: if K is a set such that: 0 is in K, and for every natural number n, n being in K implies that S(n) is in K; then K contains every natural number.
We had noticed that axiom O3 and P4 are all related with a kind of well foundedness, both can help us to setup the structure by induction. So let us define new structure Eq for equality
- Eq1: equality is reflexive, similar with P2.1
- Eq2: equality is symmetric, similar as P2.2
- Eq3: equality is transitive, similar as P2.3
- Eq4: Eq is closed under equality, similar as P2.4
and new structure Ind for inducible which are satisfied a serial of axioms
- Ind0: R is well-founded
- Ind1: we can construct Ind recursively by using R
Could we then define Cardinal number as Eq + Ind?
Thanks for comment from @coffeemath, I made revision to clarify inducible