% Copyright The Numerical Algorithms Group Limited 1992-94. All rights reserved.
% !! DO NOT MODIFY THIS FILE BY HAND !! Created by ht.awk.
\newcommand{\CardinalNumberXmpTitle}{CardinalNumber}
\newcommand{\CardinalNumberXmpNumber}{9.6}
%
% =====================================================================
\begin{page}{CardinalNumberXmpPage}{9.6 CardinalNumber}
% =====================================================================
\beginscroll

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

The non-negative integers have a natural construction as cardinals
\begin{verbatim}
0 = #{ }, 1 = {0}, 2 = {0, 1}, ..., n = {i | 0 <= i < n}.
\end{verbatim}
The fact that \spad{0} acts as a zero for the multiplication of cardinals is
equivalent to the axiom of choice.

\xtc{
Cardinal numbers can be created by conversion from non-negative integers.
}{
\spadpaste{c0 := 0 :: CardinalNumber \bound{c0}}
}
\xtc{
}{
\spadpaste{c1 := 1 :: CardinalNumber \bound{c1}}
}
\xtc{
}{
\spadpaste{c2 := 2 :: CardinalNumber \bound{c2}}
}
\xtc{
}{
\spadpaste{c3 := 3 :: CardinalNumber \bound{c3}}
}
\xtc{
They can also be obtained as the named cardinal \spad{Aleph(n)}.
}{
\spadpaste{A0 := Aleph 0 \bound{A0}}
}
\xtc{
}{
\spadpaste{A1 := Aleph 1 \bound{A1}}
}
\xtc{
The \spadfunFrom{finite?}{CardinalNumber} operation tests whether a value is a
finite cardinal, that is, a non-negative integer.
}{
\spadpaste{finite? c2 \free{c2}}
}
\xtc{
}{
\spadpaste{finite? A0 \free{A0}}
}
\xtc{
Similarly, the \spadfunFrom{countable?}{CardinalNumber}
operation determines whether a value is
a countable cardinal, that is, finite or \spad{Aleph(0)}.
}{
\spadpaste{countable? c2 \free{c2}}
}
\xtc{
}{
\spadpaste{countable? A0 \free{A0}}
}
\xtc{
}{
\spadpaste{countable? A1 \free{A1}}
}
Arithmetic operations are defined on cardinal numbers as follows:
If \spad{x = \#X}  and  \spad{y = \#Y} then

\indent{0}
\spad{x+y  = \#(X+Y)} \tab{20} cardinality of the disjoint union \newline
\spad{x-y  = \#(X-Y)} \tab{20} cardinality of the relative complement \newline
\spad{x*y  = \#(X*Y)} \tab{20} cardinality of the Cartesian product \newline
\spad{x**y = \#(X**Y)}\tab{20} cardinality of the set of maps from \spad{Y} to \spad{X} \newline

\xtc{
Here are some arithmetic examples.
}{
\spadpaste{[c2 + c2, c2 + A1] \free{c2 A1}}
}
\xtc{
}{
\spadpaste{[c0*c2, c1*c2, c2*c2, c0*A1, c1*A1, c2*A1, A0*A1] \free{c0,c1,c2,A0,A1}}
}
\xtc{
}{
\spadpaste{[c2**c0, c2**c1, c2**c2, A1**c0, A1**c1, A1**c2] \free{c0,c1,c2,A1}}
}
\xtc{
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.
}{
\spadpaste{[c2-c1, c2-c2, c2-c3, A1-c2, A1-A0, A1-A1] \free{c1,c2,c3,A0,A1}}
}
%-% \HDindex{generalized continuum hypothesis}{CardinalNumberXmpPage}{9.6}{CardinalNumber}
The generalized continuum hypothesis asserts that
\begin{verbatim}
2**Aleph i = Aleph(i+1)
\end{verbatim}
and is independent of the axioms of set theory.\footnote{Goedel,
{\it The consistency of the continuum hypothesis,}
Ann. Math. Studies, Princeton Univ. Press, 1940.}
\xtc{
The \spadtype{CardinalNumber} domain provides an operation to assert
whether the hypothesis is to be assumed.
}{
\spadpaste{generalizedContinuumHypothesisAssumed true \bound{GCH}}
}
\xtc{
When the generalized continuum hypothesis
is assumed, exponentiation to a transfinite power is allowed.
}{
\spadpaste{[c0**A0, c1**A0, c2**A0, A0**A0, A0**A1, A1**A0, A1**A1] \free{c0,c1,c2,A0,A1,GCH}}
}

Three commonly encountered cardinal numbers are

\indent{0}
\spad{a = \#}{\bf Z} \tab{20}       countable infinity \newline
\spad{c = \#}{\bf R} \tab{20}      the continuum       \newline
\spad{f = \#\{g| g: [0,1] -> {\bf R}\}}                \newline

\xtc{
In this domain, these values are obtained under the
generalized continuum hypothesis in this way.
}{
\spadpaste{a := Aleph 0 \free{GCH}\bound{a}}
}
\xtc{
}{
\spadpaste{c := 2**a    \free{a}  \bound{c}}
}
\xtc{
}{
\spadpaste{f := 2**c    \free{c}  \bound{f}}
}
\endscroll
\autobuttons
\end{page}
%