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