axiom-source 20170501-3 / usr / share / axiom-20170501 / src / algebra / CARD.spad

)abbrev domain CARD CardinalNumber
++ Author: S.M. Watt
++ Date Created: June 1986
++ Date Last Updated: May 1990
++ References:
++   Goedel, "The consistency of the continuum hypothesis",
++   Ann. Math. Studies, Princeton Univ. Press, 1940
++ Description:
++ 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 \spad{x = #X}  and  \spad{y = #Y} then\br
++ \tab{5}\spad{x+y  = #(X+Y)} \tab{5}disjoint union\br
++ \tab{5}\spad{x-y  = #(X-Y)} \tab{5}relative complement\br
++ \tab{5}\spad{x*y  = #(X*Y)} \tab{5}cartesian product\br
++ \tab{5}\spad{x**y = #(X**Y)} \tab{4}\spad{X**Y = g| g:Y->X}
++
++ The non-negative integers have a natural construction as cardinals\br
++ \spad{0 = #\{\}}, \spad{1 = \{0\}}, 
++ \spad{2 = \{0, 1\}}, ..., \spad{n = \{i| 0 <= i < n\}}.
++
++ That \spad{0} acts as a zero for the multiplication of cardinals is
++ equivalent to the axiom of choice.
++
++ The generalized continuum hypothesis asserts \br
++ \spad{2**Aleph i = Aleph(i+1)}
++ and is independent of the axioms of set theory [Goedel 1940].
++
++ Three commonly encountered cardinal numbers are\br
++ \tab{5}\spad{a = #Z} \tab{5}countable infinity\br
++ \tab{5}\spad{c = #R} \tab{5}the continuum\br
++ \tab{5}\spad{f = # g | g:[0,1]->R\}
++
++ In this domain, these values are obtained using\br
++ \tab{5}\spad{a := Aleph 0}, \spad{c := 2**a}, \spad{f := 2**c}.

CardinalNumber() : SIG == CODE where

  SIG ==> Join(OrderedSet, AbelianMonoid, Monoid,
               RetractableTo NonNegativeInteger) with

    commutative "*"
      ++ \spad{commutative("*")} implies a domain has 
      ++ \spad{"*": (D,D) -> D} which is commutative.

    "-" : (%,%) -> Union(%,"failed")
      ++ \spad{x - y} returns an element z such that 
      ++ \spad{z+y=x} or "failed" if no such element exists.
      ++
      ++X c2:=2::CardinalNumber
      ++X c2-c2
      ++X A1:=Aleph 1
      ++X A1-c2

    "**" : (%, %) -> %
      ++ \spad{x**y} returns \spad{#(X**Y)} where \spad{X**Y} is defined
      ++  as \spad{\{g| g:Y->X\}}.
      ++
      ++X c2:=2::CardinalNumber
      ++X c2**c2
      ++X A1:=Aleph 1
      ++X A1**c2
      ++X generalizedContinuumHypothesisAssumed true
      ++X A1**A1

    Aleph : NonNegativeInteger -> %
      ++ Aleph(n) provides the named (infinite) cardinal number.
      ++
      ++X A0:=Aleph 0

    finite? : % -> Boolean
      ++ finite?(\spad{a}) determines whether 
      ++ \spad{a} is a finite cardinal, for example, an integer.
      ++
      ++X c2:=2::CardinalNumber
      ++X finite? c2
      ++X A0:=Aleph 0
      ++X finite? A0

    countable? : % -> Boolean
      ++ countable?(\spad{a}) determines 
      ++ whether \spad{a} is a countable cardinal,
      ++ for example, an integer or \spad{Aleph 0}.
      ++
      ++X c2:=2::CardinalNumber
      ++X countable? c2
      ++X A0:=Aleph 0
      ++X countable? A0
      ++X A1:=Aleph 1
      ++X countable? A1

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

    generalizedContinuumHypothesisAssumed : Boolean -> Boolean
      ++ generalizedContinuumHypothesisAssumed(bool)
      ++ is used to dictate whether the hypothesis is to be assumed.
      ++
      ++X generalizedContinuumHypothesisAssumed true
      ++X a:=Aleph 0
      ++X c:=2**a
      ++X f:=2**c

  CODE ==> add

        NNI ==> NonNegativeInteger
        FINord   ==> -1
        DUMMYval ==> -1
 
        Rep := Record(order: Integer, ival: Integer)
 
        GCHypothesis: Reference(Boolean) := ref false
 
        -- Creation
        0           == [FINord, 0]

        1           == [FINord, 1]

        coerce(n:NonNegativeInteger):% == [FINord, n]

        Aleph n     == [n, DUMMYval]
 
        -- Output
        ALEPHexpr := "Aleph"::OutputForm
 
        coerce(x: %): OutputForm ==
            x.order = FINord => (x.ival)::OutputForm
            prefix(ALEPHexpr, [(x.order)::OutputForm])
 
        -- Manipulation
        x = y ==
            x.order ^= y.order => false
            finite? x          => x.ival = y.ival
            true     -- equal transfinites

        x < y ==
            x.order < y.order => true
            x.order > y.order => false
            finite? x         => x.ival < y.ival
            false    -- equal transfinites

        x:% + y:% ==
            finite? x and finite? y => [FINord, x.ival+y.ival]
            max(x, y)

        x - y ==
            x < y     => "failed"
            finite? x => [FINord, x.ival-y.ival]
            x > y     => x
            "failed" -- equal transfinites

        x:% * y:% ==
            finite? x and finite? y => [FINord, x.ival*y.ival]
            x = 0 or y = 0          => 0
            max(x, y)

        n:NonNegativeInteger * x:% ==
            finite? x => [FINord, n*x.ival]
            n = 0     => 0
            x

        x**y ==
            y = 0 =>
                x ^= 0 => 1
                error "0**0 not defined for cardinal numbers."
            finite? y =>
                not finite? x => x
                [FINord,x.ival**(y.ival):NNI]
            x = 0 => 0
            x = 1 => 1
            GCHypothesis() => [max(x.order-1, y.order) + 1, DUMMYval]
            error "Transfinite exponentiation only implemented under GCH"
 
        finite? x    == x.order = FINord

        countable? x == x.order < 1
 
        retract(x:%):NonNegativeInteger ==
          finite? x => (x.ival)::NNI
          error "Not finite"
 
        retractIfCan(x:%):Union(NonNegativeInteger, "failed") ==
          finite? x => (x.ival)::NNI
          "failed"
 
        -- State manipulation
        generalizedContinuumHypothesisAssumed?() == GCHypothesis()

        generalizedContinuumHypothesisAssumed b == (GCHypothesis() := b)