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