CardinalNumber¶

card.spad line 1 [edit on github]

Members of the domain CardinalNumber are values indicating the cardinality of sets, both finite and infinite. Arithmetic operations are defined on cardinal numbers as follows. If x = \#X and y = \#Y then x+y = \#(X+Y) disjoint union x-y = \#(X-Y) relative complement x*y = \#(X*Y) cartesian product x^y = \#(X^Y) X^Y = \{g| g: Y->X\} The non-negative integers have a natural construction as cardinals 0 = \#\{\}, 1 = \{0\}, 2 = \{0, 1\}, …, n = \{i| 0 <= i < n\}. That 0 acts as a zero for the multiplication of cardinals is equivalent to the axiom of choice. The generalized continuum hypothesis asserts center{2^Aleph i = Aleph(i+1)} and is independent of the axioms of set theory [Goedel 1940]. 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 using a := Aleph 0, c := 2^a, f := 2^c.

0: %: from AbelianMonoid

1: %: from MagmaWithUnit

*: (%, %) -> %: from Magma
*: (NonNegativeInteger, %) -> %: from AbelianMonoid
*: (PositiveInteger, %) -> %: from AbelianSemiGroup

+: (%, %) -> %: from AbelianSemiGroup

-: (%, %) -> Union(%, failed): x - y returns an element z such that z+y=x or “failed” if no such element exists.

<=: (%, %) -> Boolean: from PartialOrder

<: (%, %) -> Boolean: from PartialOrder

=: (%, %) -> Boolean: from BasicType

>=: (%, %) -> Boolean: from PartialOrder

>: (%, %) -> Boolean: from PartialOrder

^: (%, %) -> %: x^y returns \#(X^Y) where X^Y is defined as \{g| g: Y->X\}.
^: (%, NonNegativeInteger) -> %: from MagmaWithUnit
^: (%, PositiveInteger) -> %: from Magma

~=: (%, %) -> Boolean: from BasicType

Aleph: NonNegativeInteger -> %: Aleph(n) provides the named (infinite) cardinal number.

coerce: % -> OutputForm: from CoercibleTo OutputForm
coerce: NonNegativeInteger -> %: from CoercibleFrom NonNegativeInteger

countable?: % -> Boolean: countable?(a) determines whether a is a countable cardinal, i.e. an integer or Aleph 0.

finite?: % -> Boolean: finite?(a) determines whether a is a finite cardinal, i.e. an integer.

generalizedContinuumHypothesisAssumed?: () -> Boolean: generalizedContinuumHypothesisAssumed?() tests if the hypothesis is currently assumed.

generalizedContinuumHypothesisAssumed: Boolean -> Boolean: generalizedContinuumHypothesisAssumed(bool) is used to dictate whether the hypothesis is to be assumed.