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 centerline{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.