====================================================================
CardinalNumber examples
====================================================================

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.

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

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:
o )show CardinalNumber

