1====================================================================
2CardinalNumber examples
3====================================================================
4
5The CardinalNumber domain can be used for values indicating the
6cardinality of sets, both finite and infinite.  For example, the
7dimension operation in the category VectorSpace returns a cardinal
8number.
9
10The non-negative integers have a natural construction as cardinals
11
12  0 = #{ }, 1 = {0}, 2 = {0, 1}, ..., n = {i | 0 <= i < n}.
13
14The fact that 0 acts as a zero for the multiplication of cardinals is
15equivalent to the axiom of choice.
16
17Cardinal numbers can be created by conversion from non-negative integers.
18
19  c0 := 0 :: CardinalNumber
20   0
21                      Type: CardinalNumber
22
23  c1 := 1 :: CardinalNumber
24   1
25                      Type: CardinalNumber
26
27  c2 := 2 :: CardinalNumber
28   2
29                      Type: CardinalNumber
30
31  c3 := 3 :: CardinalNumber
32   3
33                      Type: CardinalNumber
34
35They can also be obtained as the named cardinal Aleph(n).
36
37  A0 := Aleph 0
38   Aleph(0)
39                      Type: CardinalNumber
40
41  A1 := Aleph 1
42   Aleph(1)
43                      Type: CardinalNumber
44
45The finite? operation tests whether a value is a finite cardinal, that
46is, a non-negative integer.
47
48  finite? c2
49   true
50                      Type: Boolean
51
52  finite? A0
53   false
54                      Type: Boolean
55
56Similarly, the countable?  operation determines whether a value is a
57countable cardinal, that is, finite or Aleph(0).
58
59  countable? c2
60   true
61                      Type: Boolean
62
63  countable? A0
64   true
65                      Type: Boolean
66
67  countable? A1
68   false
69                      Type: Boolean
70
71Arithmetic operations are defined on cardinal numbers as follows:
72If x = #X  and y = #Y then
73
74  x+y  = #(X+Y) cardinality of the disjoint union
75  x-y  = #(X-Y) cardinality of the relative complement
76  x*y  = #(X*Y) cardinality of the Cartesian product
77  x**y = #(X**Y) cardinality of the set of maps from Y to X
78
79Here are some arithmetic examples.
80
81  [c2 + c2, c2 + A1]
82   [4, Aleph(1)]
83                      Type: List CardinalNumber
84
85  [c0*c2, c1*c2, c2*c2, c0*A1, c1*A1, c2*A1, A0*A1]
86   [0, 2, 4, 0, Aleph(1), Aleph(1), Aleph(1)]
87                      Type: List CardinalNumber
88
89  [c2**c0, c2**c1, c2**c2, A1**c0, A1**c1, A1**c2]
90   [1, 2, 4, 1, Aleph(1), Aleph(1)]
91                      Type: List CardinalNumber
92
93Subtraction is a partial operation: it is not defined when subtracting
94a larger cardinal from a smaller one, nor when subtracting two equal
95infinite cardinals.
96
97  [c2-c1, c2-c2, c2-c3, A1-c2, A1-A0, A1-A1]
98   [1, 0, "failed", Aleph(1), Aleph(1), "failed"]
99                      Type: List Union(CardinalNumber,"failed")
100
101The generalized continuum hypothesis asserts that
102
103  2**Aleph i = Aleph(i+1)
104
105and is independent of the axioms of set theory.
106
107(reference: Goedel, The consistency of the continuum hypothesis,
108Ann. Math. Studies, Princeton Univ. Press, 1940.)
109
110The CardinalNumber domain provides an operation to assert whether the
111hypothesis is to be assumed.
112
113  generalizedContinuumHypothesisAssumed true
114   true
115                      Type: Boolean
116
117When the generalized continuum hypothesis is assumed, exponentiation
118to a transfinite power is allowed.
119
120  [c0**A0, c1**A0, c2**A0, A0**A0, A0**A1, A1**A0, A1**A1]
121   [0, 1, Aleph(1), Aleph(1), Aleph(2), Aleph(1), Aleph(2)]
122                      Type: List CardinalNumber
123
124Three commonly encountered cardinal numbers are
125
126  a = #Z countable infinity
127  c = #R the continuum
128  f = #{g| g: [0,1] -> R}
129
130In this domain, these values are obtained under the generalized
131continuum hypothesis in this way.
132
133  a := Aleph 0
134   Aleph(0)
135                      Type: CardinalNumber
136
137  c := 2**a
138   Aleph(1)
139                      Type: CardinalNumber
140
141  f := 2**c
142   Aleph(2)
143                      Type: CardinalNumber
144
145See Also:
146o )show CardinalNumber
147
148