Cardinal Number

The CardinalNumber domain can be used for values indicating the cardinality of sets, both finite and infinite. For example, the dimension operation in the category VectorSpace returns a cardinal number.

The non-negative integers have a natural construction as cardinals

0 = #{ }, 1 = {0}, 2 = {0, 1}, ..., n = {i | 0 <= i < n}.

The fact that 0 acts as a zero for the multiplication of cardinals is equivalent to the axiom of choice.

Cardinal numbers can be created by conversion from non-negative integers.

c0 := 0 :: CardinalNumber
 0
                    Type: CardinalNumber

c1 := 1 :: CardinalNumber
 1
                    Type: CardinalNumber

c2 := 2 :: CardinalNumber
 2
                    Type: CardinalNumber

c3 := 3 :: CardinalNumber
 3
                    Type: CardinalNumber

They can also be obtained as the named cardinal Aleph(n).

A0 := Aleph 0
 Aleph(0)
                    Type: CardinalNumber

A1 := Aleph 1
 Aleph(1)
                    Type: CardinalNumber

The finite? operation tests whether a value is a finite cardinal, that is, a non-negative integer.

finite? c2
 true
                    Type: Boolean

finite? A0
 false
                    Type: Boolean

Similarly, the countable? operation determines whether a value is a countable cardinal, that is, finite or Aleph(0).

countable? c2
 true
                    Type: Boolean

countable? A0
 true
                    Type: Boolean

countable? A1
 false
                    Type: Boolean

Arithmetic operations are defined on cardinal numbers as follows: If x = #X and y = #Y then

x+y  = #(X+Y) cardinality of the disjoint union
x-y  = #(X-Y) cardinality of the relative complement
x*y  = #(X*Y) cardinality of the Cartesian product
x**y = #(X**Y) cardinality of the set of maps from Y to X

Here are some arithmetic examples.

[c2 + c2, c2 + A1]
 [4, Aleph(1)]
                    Type: List CardinalNumber

[c0*c2, c1*c2, c2*c2, c0*A1, c1*A1, c2*A1, A0*A1]
 [0, 2, 4, 0, Aleph(1), Aleph(1), Aleph(1)]
                    Type: List CardinalNumber

[c2**c0, c2**c1, c2**c2, A1**c0, A1**c1, A1**c2]
 [1, 2, 4, 1, Aleph(1), Aleph(1)]
                    Type: List CardinalNumber

Subtraction is a partial operation: it is not defined when subtracting a larger cardinal from a smaller one, nor when subtracting two equal infinite cardinals.

[c2-c1, c2-c2, c2-c3, A1-c2, A1-A0, A1-A1]
 [1, 0, "failed", Aleph(1), Aleph(1), "failed"]
                    Type: List Union(CardinalNumber,"failed")

The generalized continuum hypothesis asserts that

2**Aleph i = Aleph(i+1)

and is independent of the axioms of set theory [Goedel].

The CardinalNumber domain provides an operation to assert whether the hypothesis is to be assumed.

generalizedContinuumHypothesisAssumed true
 true
                    Type: Boolean

When the generalized continuum hypothesis is assumed, exponentiation to a transfinite power is allowed.

[c0**A0, c1**A0, c2**A0, A0**A0, A0**A1, A1**A0, A1**A1]
 [0, 1, Aleph(1), Aleph(1), Aleph(2), Aleph(1), Aleph(2)]
                    Type: List CardinalNumber

Three commonly encountered cardinal numbers are

a = #Z countable infinity
c = #R the continuum
f = #{g| g: [0,1] -> R}

In this domain, these values are obtained under the generalized continuum hypothesis in this way.

a := Aleph 0
 Aleph(0)
                    Type: CardinalNumber

c := 2**a
 Aleph(1)
                    Type: CardinalNumber

f := 2**c
 Aleph(2)
                    Type: CardinalNumber

See Also:

• )show CardinalNumber

[Goedel]

The consistency of the continuum hypothesis, Ann. Math. Studies, Princeton Univ. Press, 1940.)