----------------------------------------------------------------------------
-- |
-- Module : LargeCardinalHierarchy
-- Copyright : (c) Stephen E. A. Britton 2010
-- License : BSD-style (see LICENSE)
--
-- Maintainer : Stephen E. A. Britton (sbritton (at) cbu (dot) edu)
-- Stability : unstable
-- Portability : OS independent
--
-- The /LargeCardinalHierarchy/ module defines a recursively enumerable,
-- countably infinite subclass of the logically
-- (consistent) maximal transfinite set-theoretic universe
-- ZFC+Con(LargeCardinals) (Zermelo-Frankel Set Theory + Axiom of Choice
-- + All known large cardinals consistent with ZFC) via data constructors
-- for each large cardinal within the hierarchy and functions over them.
-- The algebraic data type 'Card' is a Haskell implementation
-- of the set theoretic proper class of all cardinals, /Card/.
-- 'Card' has value constructors for a countably infinite (aleph-null sized)
-- subset of every cardinal type of all known large cardinals consistent
-- with ZFC (Zermelo-Frankel Set Theory + Axiom of Choice) or,
-- equivalently, ZF+GCH (Zermelo-Frankel Set Theory + Generalized Continuum Hypothesis).
--
-----------------------------------------------------------------------------
module LargeCardinalHierarchy where
import Control.Monad
data Card = Card Integer
| Aleph Card
| WeaklyInaccessible Card
| StronglyInaccessible Card
| AlphaInaccessible Card
| HyperInaccessible Card
| Hyper2Inaccessible Card
| WeaklyMahlo Card
| StronglyMahlo Card
| AlphaMahlo Card
| HyperMahlo Card
| Reflecting Card
| PiIndescribable (Int, Int) Card
| TotallyIndescribable Card
| NuIndescribable Card
| LambdaUnfoldable Card
| Unfoldable Card
| LambdaShrewd Card
| Shrewd Card
| Ethereal Card
| Subtle Card
| AlmostIneffable Card
| Ineffable Card
| NIneffable Card
| TotallyIneffable Card
| Remarkable Card
| AlphaErdos Card
| GammaErdos Card
| AlmostRamsey Card
| Jonsson Card
| Rowbottom Card
| Ramsey Card
| IneffablyRamsey Card
| Measurable Card
| ZeroDagger Card
| LambdaStrong Card
| Strong Card
| Woodin Card
| WeaklyHyperWoodin Card
| Shelah Card
| HyperWoodin Card
| Superstrong Card
| Subcompact Card
| StronglyCompact Card
| Supercompact Card
| EtaExtendible Card
| Extendible Card
| Vopenka Card
| NSuperstrong Card
| NAlmostHuge Card
| NSuperAlmostHuge Card
| NHuge Card
| NSuperHuge Card
| RankIntoRank Card
| Reinhardt Card
| TAV -- the supremum of Card, class of all cardinals
| AbsoluteInfinity
deriving (Eq, Ord, Show)
{-|
'apply' is a binary higher-order function
that takes a function /f/ and a list of type /x/ values, [x],
and returns a new list of values derived from the application of /f/ to
each of the /x/ values within [x].
-}
apply f [x] = [f x]
apply f (x:xs) = [f x] ++ apply f xs
{-|
'zero' is /the/ unique nullary function within the
/LargeCardinalHierarchy/ module that returns the additive identity element
(and multiplicative absorbing element within the class of all cardinals),
cardinal 0, via the 'Card' constructor.
-}
zero :: Card
zero = Card 0
{-|
'one' is /the/ unique nullary function within the
/LargeCardinalHierarchy/ module that returns the multiplicative identity element
within the class of all cardinals, cardinal 1, via the 'Card' constructor.
-}
one :: Card
one = Card 1
{-|
'absolute' is a /type synonym/ (nullary function) for /AbsoluteInfinity/; the
supremum of the class of all cardinals, 'Card'.
-}
absolute :: Card
absolute = AbsoluteInfinity
{-|
'zeros' is a nullary function that returns a countably-infinite (aleph-null sized)
sequence (a /stream/) of cardinal zeros.
-}
zeros :: [Card]
zeros = repeat zero
{-|
'ones' is a nullary function that returns a countably-infinite (aleph-null sized)
sequence (a /stream/) of cardinal ones.
-}
ones :: [Card]
ones = repeat one
{-|
'alefz' is a unary function that takes an 'Int' /n/ and
returns an /n/-element list of the first /n/ aleph numbers enumerating from
aleph-null.
-}
alefz :: Int -> [Card]
alefz n = take n (order 1 Aleph)
{-|
'tavs' is a nullary function that returns a countably-infinite (aleph-null sized)
sequence (a /stream/) of 'TAV's; 'TAV' being the symbol for the absolutely infinite
supremum of the class of all cardinals, 'Card'.
-}
tavs :: [Card]
tavs = repeat TAV
{-|
'absolutes' is a nullary function that returns a countably-infinite (aleph-null sized)
sequence (a /stream/) of 'AbsoluteInfinity's; 'AbsoluteInfinity' being the
/cardinality/ the class of all cardinals, 'Card'.
-}
absolutes :: [Card]
absolutes = repeat absolute
{-|
'absoluteInfinities' is a /type synonym/ (nullary function) for 'absolutes'.
-}
absoluteInfinities :: [Card]
absoluteInfinities = absolutes
{-|
'(#)' is binary function from ('Card', 'Card') to 'Card'.
'(#)' takes two cardinal numbers and returns their binary sum.
Category-theoretically speaking, '(#)' is a /coproduct/ in the class of
all cardinals, 'Card'.
-}
(#) :: Card -> Card -> Card
(#) (Card m) (Card n) = Card (m + n)
(#) m n = max m n
{-|
'(#.)' is a unary (or, multiary) function from ['Card'] to 'Card'.
'(#.)' takes a list of cardinal numbers and returns their multiary sum.
Category-theoretically speaking, '(#.)' is a /coproduct/ in the class of
all cardinals, 'Card'.
-}
(#.) :: [Card] -> Card
(#.) xs = foldl (#) (Card 0) xs
{-|
'(*.)' is a binary function from ('Card', 'Card') to 'Card'.
'(*.)' takes two cardinal numbers and returns their binary product.
-}
(*.) :: Card -> Card -> Card
(*.) (Card m) (Card n) = Card (m * n)
(*.) m (Card 0) = Card 0
(*.) (Card 0) n = Card 0
(*.) m n = max m n
{-|
'x' is a unary (or, multiary) function from ['Card'] to 'Card'.
'x' takes a list of cardinal numbers and returns their multiary product.
-}
x :: [Card] -> Card
x xs = foldl (*.) (Card 1) xs
{-|
'(^.)' is a binary function from ('Card','Card') to 'Card'.
'(^.)' take two cardinal numbers and returns the power of the
zeroth cardinal number exponentiated to the first cardinal number.
-}
(^.) :: Card -> Card -> Card
(^.) (Card m) (Card n) = Card (m ^ n)
(^.) (Card m) (Aleph (Card n)) = if m == 0 || m == 1
then Card m
else Aleph (Card (n + 1))
(^.) (Aleph (Card m)) (Card n) = if n == 0
then Card 1
else Aleph (Card m)
(^.) (Aleph (Card m)) (Aleph (Card n)) = if m > n
then Aleph (Card m)
else Aleph (Card (n + 1))
(^.) (Card m) TAV = if m == 0 || m == 1
then Card m
else TAV
(^.) TAV (Card n) = if n == 0
then Card 1
else TAV
{-|
'cp' is a binary function from [a] & [b] to [(a, b)].
'cp' takes two /lists/ of elements and returns the
list of all ordered pairs of elements between the two lists.
'cp' is the /Cartesian product/ operator.
-}
cp :: [a] -> [b] -> [(a, b)]
cp as bs = [(a, b) | a <- as, b <- bs]
{-|
'cartesianProduct' is a binary function from [a] & [b] to [(a, b)].
'cartesianProduct' takes two lists of elements and returns the
list of all ordered pairs of elements between the two lists
'cartesianProduct' is the /Cartesian product/ operator.
-}
cartesianProduct :: [a] -> [b] -> [(a, b)]
cartesianProduct = cp
{-|
'powerList' is a unary function from [a] -> [[a]].
'powerList' takes a list of elements and returns the list of all sublists
of that list. 'powerList' is a /canonical/ example of Haskell's facilitation
in expressing functions elegantly.
-}
powerList :: [a] -> [[a]]
powerList = filterM (const [True,False])
{-|
'ascend' is a unary function from 'Integer' to ['Card'].
'ascend' takes a natural number /n/ and returns a list of aleph cardinals from
aleph 0 to aleph n.
-}
ascend :: Integer -> [Card]
ascend 0 = [Aleph (Card 0)]
ascend n = ascend (n - 1) ++ [Aleph (Card n)]
{-|
'descend' is a unary function from 'Integer' to ['Card'].
'descend' takes a natural number /n/ and returns a list of aleph cardinals from
aleph n to aleph 0.
-}
descend :: Integer -> [Card]
descend 0 = [Aleph (Card 0)]
descend n = [Aleph (Card n)] ++ descend (n - 1)
{-|
'level' is a ternary function from ('Int', 'Card', 'Integer') to 'Card'.
'level' takes an 'Int' /n/, a 'Card' value constructor /cons/, and an 'Integer' /m/
and returns a 'Card' equal to /cons/ '$' /cons/ '$' /cons/ '$' ... '$' 'Card' /m/.
-}
level :: Int -> (Card -> Card) -> Integer -> Card
level 0 cons m = Card m
level n cons m = cons $ level (n - 1) cons m
{-|
'ascent' is a quaternary function from ('Int', 'Card', 'Integer', 'Integer') to
['Card']. 'ascent' takes an 'Int' /x/, a 'Card' value constructor /cons/, and
two 'Integer's /y/ and /z/ and returns a list of 'level' /x/ type
/cons/ 'Card' values from /y/ to /z/, where /y/ <= /z/.
'ascent' is a generalization of 'ascend'
over all data constructors in 'Card'.
-}
ascent :: Int -> (Card -> Card) -> Integer -> Integer -> [Card]
ascent x cons y z = apply (level x cons) [y .. z]
{-|
'descent' is a quaternary function from ('Int', 'Card', 'Integer', 'Integer') to
['Card']. 'descent' takes an 'Int' /x/, a 'Card' value constructor /cons/, and
two 'Integer's /y/ and /z/ and returns a list of 'level' /x/ type
/cons/ 'Card' values from /y/ to /z/, where /y/ >= /z/.
'descent' is a generalization of 'descend'
over all data constructors in 'Card'.
-}
descent :: Int -> (Card -> Card) -> Integer -> Integer -> [Card]
descent x cons y z = apply (level x cons) [y, y - 1 .. z]
{-|
'c' is a unary function that takes an 'Integer' /n/ and
returns a finite cardinal number, 'Card' /n/.
-}
c :: Integer -> Card
c n = Card n
{-|
'alef' is a unary function that takes an 'Integer' /n/ and
returns a tranfinite aleph number subscripted by cardinal /n/, 'Aleph' /n/.
-}
alef :: Integer -> Card
alef n = aleph 1 n
{-|
'aleph' is a binary function from ('Int', 'Integer') to 'Card'.
'aleph' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'Aleph' whose deepest subscript is /n/.
-}
aleph :: Int -> Integer -> Card
aleph m n = level m Aleph n
{-|
'beth' is a binary function from ('Int', 'Integer') to 'Card'.
'beth' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'Aleph' whose deepest subscript is /n/.
-}
beth :: Int -> Integer -> Card
beth m n = aleph m n
{-|
'wInac' is a binary function from ('Int', 'Integer') to 'Card'.
'wInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'WeaklyInaccessible' whose deepest subscript is /n/.
-}
wInac :: Int -> Integer -> Card
wInac m n = level m WeaklyInaccessible n
-- | 'weaklyInaccessible' is a /function synonym/ for 'wInac'.
weaklyInaccessible :: Int -> Integer -> Card
weaklyInaccessible = wInac
{-|
'sInac' is a binary function from ('Int', 'Integer') to 'Card'.
'sInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'StronglyInaccessible' whose deepest subscript is /n/.
-}
sInac :: Int -> Integer -> Card
sInac m n = level m StronglyInaccessible n
-- | 'stronglyInaccessible' is a /function synonym/ for 'sInac'.
stronglyInaccessible :: Int -> Integer -> Card
stronglyInaccessible = sInac
{-|
'theta' is a binary function from ('Int', 'Integer') to 'Card'.
'theta' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'StronglyInaccessible' cardinal whose deepest subscript is /n/.
'theta' is a /function synonym/ for 'sInac'.
-}
theta :: Int -> Integer -> Card
theta = sInac
{-|
'aInac' is a binary function from ('Int', 'Integer') to 'Card'.
'aInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'AlphaInaccessible' whose deepest subscript is /n/.
-}
aInac :: Int -> Integer -> Card
aInac m n = level m AlphaInaccessible n
{-|
'alphaInaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
'alphaInaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'AlphaInaccessible' whose deepest subscript is /n/.
'alphaInaccessible' is a /function synonym/ for 'aInac'.
-}
alphaInaccessible :: Int -> Integer -> Card
alphaInaccessible = aInac
{-|
'hInac' is a binary function from ('Int', 'Integer') to 'Card'.
'hInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
-}
hInac :: Int -> Integer -> Card
hInac m n = level m HyperInaccessible n
{-|
'hyperInaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
'hyperInaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
'hyperInaccessible' is a /function synonym/ for 'hInac'.
-}
hyperInaccessible :: Int -> Integer -> Card
hyperInaccessible = hInac
{-|
'nu' is a binary function from ('Int', 'Integer') to 'Card'.
'nu' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
'nu' is a /function synonym/ for 'hInac'.
-}
nu :: Int -> Integer -> Card
nu = hInac
{-|
'h2Inac' is a binary function from ('Int', 'Integer') to 'Card'.
'h2Inac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
-}
h2Inac :: Int -> Integer -> Card
h2Inac m n = level m Hyper2Inaccessible n
{-|
'hyper2Inaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
'hyper2Inaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
'hyper2Inaccessible' is a /function synonym/ for 'h2Inac'.
-}
hyper2Inaccessible :: Int -> Integer -> Card
hyper2Inaccessible = h2Inac
{-|
'mu' is a binary function from ('Int', 'Integer') to 'Card'.
'mu' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
'mu' is a /function synonym/ for 'h2Inac'.
-}
mu :: Int -> Integer -> Card
mu = h2Inac
{-|
'wMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'wMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'WeaklyMahlo' whose deepest subscript is /n/.
-}
wMahlo :: Int -> Integer -> Card
wMahlo m n = level m WeaklyMahlo n
{-|
'weaklyMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'weaklyMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'WeaklyMahlo' whose deepest subscript is /n/.
'weaklyMahlo' is a /function synonym/ for 'wMahlo'.
-}
weaklyMahlo :: Int -> Integer -> Card
weaklyMahlo = wMahlo
{-|
'sMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'sMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'StronglyMahlo' whose deepest subscript is /n/.
-}
sMahlo :: Int -> Integer -> Card
sMahlo m n = level m StronglyMahlo n
{-|
'stronglyMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'stronglyMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'StronglyMahlo' whose deepest subscript is /n/.
'stronglyMahlo' is a /function synonym/ for 'sMahlo'.
-}
stronglyMahlo :: Int -> Integer -> Card
stronglyMahlo = sMahlo
{-|
'rho' is a binary function from ('Int', 'Integer') to 'Card'.
'rho' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
'm' 'level' 'StronglyMahlo' cardinal whose deepest subscript is /n/.
-}
rho :: Int -> Integer -> Card
rho m n = level m StronglyMahlo n
{-|
'aMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'aMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'AlphaMahlo' whose deepest subscript is /n/.
-}
aMahlo :: Int -> Integer -> Card
aMahlo m n = level m AlphaMahlo n
{-|
'alphaMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'alphaMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'AlphaMahlo' whose deepest subscript is /n/.
'alphaMahlo' is a /function synonym/ for 'aMahlo'.
-}
alphaMahlo :: Int -> Integer -> Card
alphaMahlo = aMahlo
{-|
'hMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'hMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'HyperMahlo' whose deepest subscript is /n/.
-}
hMahlo :: Int -> Integer -> Card
hMahlo m n = level m HyperMahlo n
{-|
'hyperMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
'hyperMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
/m/ 'level' 'HyperMahlo' whose deepest subscript is /n/.
-}
hyperMahlo :: Int -> Integer -> Card
hyperMahlo = hMahlo
{-|
Binary function from (Int, Integer) to Card
reflect takes an Int m and an Integer n and returns an
m level reflecting cardinal whose deepest subscript is n
-}
reflect :: Int -> Integer -> Card
reflect m n = level m Reflecting n
reflecting :: Int -> Integer -> Card
reflecting = reflect
{-|
Binary function from (Int, Int, Int, Integer) to Card
pii takes an Int x, an Int y, an Int m, and an Integer n
and returns the m level pi-(x, y)-indescribable cardinal
whose deepest subscript is n
-}
pii :: Int -> Int -> Int -> Integer -> Card
pii x y m n = level m (PiIndescribable (x, y)) n
piIndesc :: Int -> Int -> Int -> Integer -> Card
piIndesc = pii
piIndescribable :: Int -> Int -> Int -> Integer -> Card
piIndescribable = pii
ti :: Int -> Integer -> Card
ti m n = level m TotallyIndescribable n
totalIndesc :: Int -> Integer -> Card
totalIndesc = ti
totallyIndescribable :: Int -> Integer -> Card
totallyIndescribable = ti
ni :: Int -> Integer -> Card
ni m n = level m NuIndescribable n
nuIndesc :: Int -> Integer -> Card
nuIndesc = ni
nuIndescribable :: Int -> Integer -> Card
nuIndescribable = ni
lambdaUnfold :: Int -> Integer -> Card
lambdaUnfold m n = level m LambdaUnfoldable n
lambdaUnfoldable :: Int -> Integer -> Card
lambdaUnfoldable = lambdaUnfold
unfold :: Int -> Integer -> Card
unfold m n = level m Unfoldable n
unfoldable :: Int -> Integer -> Card
unfoldable = unfold
lambdaShrewd :: Int -> Integer -> Card
lambdaShrewd m n = level m LambdaShrewd n
shrewd :: Int -> Integer -> Card
shrewd m n = level m Shrewd n
{-|
Binary function from (Int, Integer) to Card
ether takes an Int m and an Integer n and returns an
m level ethereal cardinal whose deepest subscript is n
-}
ether :: Int -> Integer -> Card
ether m n = level m Ethereal n
ethereal :: Int -> Integer -> Card
ethereal = ether
{-|
Binary function from (Int, Integer) to Card
subtle takes an Int m and an Integer n and returns an
m level subtle cardinal whose deepest subscript is n
-}
subtle :: Int -> Integer -> Card
subtle m n = level m Subtle n
almostIneff :: Int -> Integer -> Card
almostIneff m n = level m AlmostIneffable n
almostIneffable :: Int -> Integer -> Card
almostIneffable = almostIneff
ineff :: Int -> Integer -> Card
ineff m n = level m Ineffable n
ineffable :: Int -> Integer -> Card
ineffable = ineff
nIneff :: Int -> Integer -> Card
nIneff m n = level m NIneffable n
nIneffable :: Int -> Integer -> Card
nIneffable = nIneff
totalIneff :: Int -> Integer -> Card
totalIneff m n = level m TotallyIneffable n
totallyIneffable :: Int -> Integer -> Card
totallyIneffable = totalIneff
remark :: Int -> Integer -> Card
remark m n = level m Remarkable n
remarkable :: Int -> Integer -> Card
remarkable = remark
aErdos :: Int -> Integer -> Card
aErdos m n = level m AlphaErdos n
alphaErdos :: Int -> Integer -> Card
alphaErdos = aErdos
gamma :: Int -> Integer -> Card
gamma m n = level m GammaErdos n
gErdos :: Int -> Integer -> Card
gErdos = gamma
gammaErdos :: Int -> Integer -> Card
gammaErdos = gamma
aRamsey :: Int -> Integer -> Card
aRamsey m n = level m AlmostRamsey n
almostRamsey :: Int -> Integer -> Card
almostRamsey = aRamsey
jonsson :: Int -> Integer -> Card
jonsson m n = level m Jonsson n
rowbottom :: Int -> Integer -> Card
rowbottom m n = level m Rowbottom n
ramsey :: Int -> Integer -> Card
ramsey m n = level m Ramsey n
iRamsey :: Int -> Integer -> Card
iRamsey m n = level m IneffablyRamsey n
ineffablyRamsey :: Int -> Integer -> Card
ineffablyRamsey = iRamsey
measure :: Int -> Integer -> Card
measure m n = level m Measurable n
measurable :: Int -> Integer -> Card
measurable = measure
{-|
Binary function from (Int, Integer) to Card
kappa takes an Int m and an Integer n and returns an
m level measurable cardinal whose deepest subscript is n
-}
kappa :: Int -> Integer -> Card
kappa = measure
zeroDag :: Int -> Integer -> Card
zeroDag m n = level m ZeroDagger n
zeroDagger :: Int -> Integer -> Card
zeroDagger = zeroDag
lambdaStrong :: Int -> Integer -> Card
lambdaStrong m n = level m LambdaStrong n
strong :: Int -> Integer -> Card
strong m n = level m Strong n
woodin :: Int -> Integer -> Card
woodin m n = level m Woodin n
whWoodin :: Int -> Integer -> Card
whWoodin m n = level m WeaklyHyperWoodin n
weaklyHyperWoodin :: Int -> Integer -> Card
weaklyHyperWoodin = whWoodin
shelah :: Int -> Integer -> Card
shelah m n = level m Shelah n
hWoodin :: Int -> Integer -> Card
hWoodin m n = level m HyperWoodin n
hyperWoodin :: Int -> Integer -> Card
hyperWoodin = hWoodin
ss :: Int -> Integer -> Card
ss m n = level m Superstrong n
supStrong :: Int -> Integer -> Card
supStrong = ss
superstrong :: Int -> Integer -> Card
superstrong = ss
superStrong :: Int -> Integer -> Card
superStrong = ss
subcompact :: Int -> Integer -> Card
subcompact m n = level m Subcompact n
stronglyCompact :: Int -> Integer -> Card
stronglyCompact m n = level m StronglyCompact n
supCompact :: Int -> Integer -> Card
supCompact m n = level m Supercompact n
superCompact :: Int -> Integer -> Card
superCompact = supCompact
eta :: Int -> Integer -> Card
eta m n = level m EtaExtendible n
etaExtend :: Int -> Integer -> Card
etaExtend = eta
etaExtendible :: Int -> Integer -> Card
etaExtendible = eta
ex :: Int -> Integer -> Card
ex m n = level m Extendible n
extend :: Int -> Integer -> Card
extend = ex
extendible :: Int -> Integer -> Card
extendible = ex
vopenka :: Int -> Integer -> Card
vopenka m n = level m Vopenka n
nss :: Int -> Integer -> Card
nss m n = level m NSuperstrong n
nSuperstrong :: Int -> Integer -> Card
nSuperstrong = nss
nah :: Int -> Integer -> Card
nah m n = level m NAlmostHuge n
nAlmostHuge :: Int -> Integer -> Card
nAlmostHuge = nah
nsah :: Int -> Integer -> Card
nsah m n = level m NSuperAlmostHuge n
nSuperAlmostHuge :: Int -> Integer -> Card
nSuperAlmostHuge = nsah
nh :: Int -> Integer -> Card
nh m n = level m NHuge n
nHuge :: Int -> Integer -> Card
nHuge = nh
nsh :: Int -> Integer -> Card
nsh m n = level m NSuperHuge n
nSuperHuge :: Int -> Integer -> Card
nSuperHuge = nsh
rank :: Int -> Integer -> Card
rank m n = level m RankIntoRank n
{-|
Binary function from (Int, Integer) to Card
lambda takes an Int m and an Integer n and returns an
m level rank-into-rank cardinal whose deepest subscript is n
-}
lambda :: Int -> Integer -> Card
lambda = rank
rankIntoRank :: Int -> Integer -> Card
rankIntoRank = rank
reinhardt :: Int -> Integer -> Card
reinhardt m n = level m Reinhardt n
{-|
Binary function from 'Int' x 'Card' to Card
order takes an Int m and a Card card and returns the
countably infinite list of level m card(s) indexed over
the natural numbers [0..]. That is, order returns
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
order increases 'linearly' over its second argument
keeping its first argument constant. order indexes in a
zero order manner over the natural numbers.
order m card =
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
fixedpoints increases 'hierarchly' over its first argument
keeping its second argument constant. fixedpoints indexes
in a higher order manner over its own arguments.
fixedpoints m card =
[(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]
-}
order :: Int -> (Card -> Card) -> [Card]
order m card = apply (level m card) [0..]
{-|
Binary function from Int x Card to Card
zeroOrder takes an Int m and a Card card and returns the
countably infinite list of level m card(s) indexed over
the natural numbers [0..]. That is, zeroOrder returns
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
zeroOrder increases 'linearly' over its second argument
keeping its first argument constant. zeroOrder indexes in a
zero order manner over the natural numbers.
zeroOrder m card =
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
zeroOrder 1 Aleph =
[Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]
higherOrder increases 'hierarchly' over its first argument
keeping its second argument constant. higherOrder indexes
in a higher order manner over its own arguments.
higherOrder m card =
[(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]
higherOrder 1 Aleph =
[(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]
-}
zeroOrder :: Int -> (Card -> Card) -> [Card]
zeroOrder = order
{-|
Binary function from Int x Card to Card
orderClass takes an Int m and a Card card and returns the
countably infinite list of level m card(s) indexed over
the natural numbers [0..]. That is, orderClass returns
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
orderClass is identical to order
-}
orderClass :: Int -> (Card -> Card) -> [Card]
orderClass = order
{-|
Unary function from Card to Card
club takes a Card value constructor card and returns
the countably infinite list of type card Card fixed points
indexed over the natural numbers [0..]. That is, club returns
[(card 1 0), (card 2 0), (card 3 0), . . .]
club is an implementation of the normal function f: Ordinals -> Ordinals
that defines a closed and unbounded (club) class of ordinal
fixed points according to the "Fixed point lemma for normal functions"
-}
club :: (Card -> Card) -> [Card]
club card = iterate card (Card 0)
{-|
Binary function from Int x Card to Card
fixedpoints takes an Int m and a Card value constructor card and returns
the countably infinite list of type card Card fixed points
indexed over the natural number m. That is, fixedpoints returns
[(card 1 m), (card 2 m), (card 3 m), . . .]
fixedpoints is an implementation of the normal function
f: Ordinals -> Ordinals
that defines a closed and unbounded (club) class of ordinal
fixed points according to the "Fixed point lemma for normal functions"
fixedpoints increases 'hierarchly' over its first argument
keeping its second argument constant. fixedpoints indexes
in a higher order manner over its own arguments.
fixedpoints m card =
[(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]
order increases 'linearly' over its second argument
keeping its first argument constant. order indexes in a
zero order manner over the natural numbers.
order m card =
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
-}
fixedpoints :: Integer -> (Card -> Card) -> [Card]
fixedpoints m card = iterate card (Card m)
{-|
Binary function from Int x Card to Card
higherOrder takes an Int m and a Card value constructor card and returns
the countably infinite list of type card Card fixed points
indexed over the natural number m. That is, higherOrder returns
[(card 1 m), (card 2 m), (card 3 m), . . .]
higherOrder is an implementation of the normal function
f: Ordinals -> Ordinals
that defines a closed and unbounded (club) class of ordinal
fixed points according to the "Fixed point lemma for normal functions"
higherOrder increases 'hierarchly' over its first argument
keeping its second argument constant. higherOrder indexes
in a higher order manner over its own arguments.
higherOrder m card =
[(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]
higherOrder 1 Aleph =
[(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]
zeroOrder increases 'linearly' over its second argument
keeping its first argument constant. zeroOrder indexes in a
zero order manner over the natural numbers.
zeroOrder m card =
[(card m 0), (card m 1), (card m 2), (card m 3), . . .]
zeroOrder 1 Aleph =
[Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]
-}
higherOrder :: Integer -> (Card -> Card) -> [Card]
higherOrder = fixedpoints
{-|
Quaternary function from Int x Card x Int x Int to [Card]
fromTo takes an Int ord, a Card value constructor cons, an Int m,
and an Int n and returns the list of type cons Card(s) of order
ord indexed from m to n. That is, fromTo returns
[(cons ord m), . . . , (cons ord n)]
fromTo ord cons m n = descent ord cons m n
-}
fromTo :: Int -> (Card -> Card) -> Int -> Int -> [Card]
fromTo ord cons m n = drop m (take (n + 1) (order ord cons))
alephs :: Int -> [Card]
alephs n = order n Aleph
alefs :: Integer -> [Card]
alefs n = fixedpoints n Aleph
wInacs :: Int -> [Card]
wInacs n = order n WeaklyInaccessible
weaklyInaccessibles :: Int -> [Card]
weaklyInaccessibles = wInacs
wInacz :: Integer -> [Card]
wInacz n = fixedpoints n WeaklyInaccessible
weaklyInaccessiblez :: Integer -> [Card]
weaklyInaccessiblez = wInacz
sInacs :: Int -> [Card]
sInacs n = order n StronglyInaccessible
stronglyInaccessibles :: Int -> [Card]
stronglyInaccessibles = sInacs
sInacz :: Integer -> [Card]
sInacz n = fixedpoints n StronglyInaccessible
stronglyInaccessiblez :: Integer -> [Card]
stronglyInaccessiblez = sInacz
aInacs :: Int -> [Card]
aInacs n = order n AlphaInaccessible
alphaInaccessibles :: Int -> [Card]
alphaInaccessibles = aInacs
aInacz :: Integer -> [Card]
aInacz n = fixedpoints n AlphaInaccessible
alphaInaccessiblez :: Integer -> [Card]
alphaInaccessiblez = aInacz
hInacs :: Int -> [Card]
hInacs n = order n HyperInaccessible
hyperInaccessibles :: Int -> [Card]
hyperInaccessibles = hInacs
hInacz :: Integer -> [Card]
hInacz n = fixedpoints n HyperInaccessible
hyperInaccessiblez :: Integer -> [Card]
hyperInaccessiblez = hInacz
h2Inacs :: Int -> [Card]
h2Inacs n = order n Hyper2Inaccessible
hyper2Inaccessibles :: Int -> [Card]
hyper2Inaccessibles = h2Inacs
h2Inacz :: Integer -> [Card]
h2Inacz n = fixedpoints n Hyper2Inaccessible
hyper2Inaccessiblez :: Integer -> [Card]
hyper2Inaccessiblez = h2Inacz
wMahlos :: Int -> [Card]
wMahlos n = order n WeaklyMahlo
weaklyMahlos :: Int -> [Card]
weaklyMahlos = wMahlos
wMahloz :: Integer -> [Card]
wMahloz n = fixedpoints n WeaklyMahlo
weaklyMahloz :: Integer -> [Card]
weaklyMahloz = wMahloz
sMahlos :: Int -> [Card]
sMahlos n = order n StronglyMahlo
stronglyMahlos :: Int -> [Card]
stronglyMahlos = sMahlos
sMahloz :: Integer -> [Card]
sMahloz n = fixedpoints n StronglyMahlo
stronglyMahloz :: Integer -> [Card]
stronglyMahloz = sMahloz
aMahlos :: Int -> [Card]
aMahlos n = order n AlphaMahlo
alphaMahlos :: Int -> [Card]
alphaMahlos = aMahlos
aMahloz :: Integer -> [Card]
aMahloz n = fixedpoints n AlphaMahlo
alphaMahloz :: Integer -> [Card]
alphaMahloz = aMahloz
hMahlos :: Int -> [Card]
hMahlos n = order n HyperMahlo
hyperMahlos :: Int -> [Card]
hyperMahlos = hMahlos
hMahloz :: Integer -> [Card]
hMahloz n = fixedpoints n HyperMahlo
hyperMahloz :: Integer -> [Card]
hyperMahloz = hMahloz
reflections :: Int -> [Card]
reflections n = order n Reflecting
reflexions :: Integer -> [Card]
reflexions n = fixedpoints n Reflecting
piis :: Int -> Int -> Int -> [Card]
piis super sub order = apply (pii super sub order) [0..]
piIndescribables :: Int -> Int -> Int -> [Card]
piIndescribables = piis
piiz :: Int -> Int -> Integer -> [Card]
piiz super sub index = iterate (PiIndescribable (super, sub)) (Card index)
piIndescribablez :: Int -> Int -> Integer -> [Card]
piIndescribablez = piiz
tis :: Int -> [Card]
tis n = order n TotallyIndescribable
totallyIndescribables :: Int -> [Card]
totallyIndescribables = tis
tiz :: Integer -> [Card]
tiz n = fixedpoints n TotallyIndescribable
totallyIndescribablez :: Integer -> [Card]
totallyIndescribablez = tiz
nis :: Int -> [Card]
nis n = order n NuIndescribable
nuIndescribables :: Int -> [Card]
nuIndescribables = nis
niz :: Integer -> [Card]
niz n = fixedpoints n NuIndescribable
nuIndescribablez :: Integer -> [Card]
nuIndescribablez = niz
lambdaUnfolds :: Int -> [Card]
lambdaUnfolds n = order n LambdaUnfoldable
lambdaUnfoldables :: Int -> [Card]
lambdaUnfoldables = lambdaUnfolds
lambdaUnfoldz :: Integer -> [Card]
lambdaUnfoldz n = fixedpoints n LambdaUnfoldable
lambdaUnfoldablez :: Integer -> [Card]
lambdaUnfoldablez = lambdaUnfoldz
unfolds :: Int -> [Card]
unfolds n = order n Unfoldable
unfoldables :: Int -> [Card]
unfoldables = unfolds
unfoldz :: Integer -> [Card]
unfoldz n = fixedpoints n Unfoldable
unfoldablez :: Integer -> [Card]
unfoldablez = unfoldz
lambdaShrewds :: Int -> [Card]
lambdaShrewds n = order n LambdaShrewd
lambdaShrewdz :: Integer -> [Card]
lambdaShrewdz n = fixedpoints n LambdaShrewd
shrewds :: Int -> [Card]
shrewds n = order n Shrewd
shrewdz :: Integer -> [Card]
shrewdz n = fixedpoints n Shrewd
ethers :: Int -> [Card]
ethers n = order n Ethereal
ethereals :: Int -> [Card]
ethereals = ethers
etherz :: Integer -> [Card]
etherz n = fixedpoints n Ethereal
etherealz :: Integer -> [Card]
etherealz = etherz
subtles :: Int -> [Card]
subtles n = order n Subtle
subtlez :: Integer -> [Card]
subtlez n = fixedpoints n Subtle
almostIneffs :: Int -> [Card]
almostIneffs n = order n AlmostIneffable
almostIneffables :: Int -> [Card]
almostIneffables = almostIneffs
almostIneffz :: Integer -> [Card]
almostIneffz n = fixedpoints n AlmostIneffable
almostIneffablez :: Integer -> [Card]
almostIneffablez = almostIneffz
ineffs :: Int -> [Card]
ineffs n = order n Ineffable
ineffables :: Int -> [Card]
ineffables = ineffs
ineffz :: Integer -> [Card]
ineffz n = fixedpoints n Ineffable
ineffablez :: Integer -> [Card]
ineffablez = ineffz
nIneffs :: Int -> [Card]
nIneffs n = order n NIneffable
nIneffables :: Int -> [Card]
nIneffables = nIneffs
nIneffz :: Integer -> [Card]
nIneffz n = fixedpoints n NIneffable
nIneffablez :: Integer -> [Card]
nIneffablez = nIneffz
totalIneffs :: Int -> [Card]
totalIneffs n = order n TotallyIneffable
totallyIneffables :: Int -> [Card]
totallyIneffables = totalIneffs
totalIneffz :: Integer -> [Card]
totalIneffz n = fixedpoints n TotallyIneffable
totallyIneffablez :: Integer -> [Card]
totallyIneffablez = totalIneffz
remarkables :: Int -> [Card]
remarkables n = order n Remarkable
remarkablez :: Integer -> [Card]
remarkablez n = fixedpoints n Remarkable
aErdoss :: Int -> [Card]
aErdoss n = order n AlphaErdos
alphaErdoss :: Int -> [Card]
alphaErdoss = aErdoss
aErdosz :: Integer -> [Card]
aErdosz n = fixedpoints n AlphaErdos
alphaErdosz :: Integer -> [Card]
alphaErdosz = aErdosz
gErdoss :: Int -> [Card]
gErdoss n = order n GammaErdos
gammaErdoss :: Int -> [Card]
gammaErdoss = gErdoss
gErdosz :: Integer -> [Card]
gErdosz n = fixedpoints n GammaErdos
gammaErdosz :: Integer -> [Card]
gammaErdosz = gErdosz
aRamseys :: Int -> [Card]
aRamseys n = order n AlmostRamsey
almostRamseys :: Int -> [Card]
almostRamseys = aRamseys
aRamseyz :: Integer -> [Card]
aRamseyz n = fixedpoints n AlmostRamsey
almostRamseyz :: Integer -> [Card]
almostRamseyz = aRamseyz
jonssons :: Int -> [Card]
jonssons n = order n Jonsson
jonssonz :: Integer -> [Card]
jonssonz n = fixedpoints n Jonsson
rowbottoms :: Int -> [Card]
rowbottoms n = order n Rowbottom
rowbottomz :: Integer -> [Card]
rowbottomz n = fixedpoints n Rowbottom
ramseys :: Int -> [Card]
ramseys n = order n Ramsey
ramseyz :: Integer -> [Card]
ramseyz n = fixedpoints n Ramsey
iRamseys :: Int -> [Card]
iRamseys n = order n IneffablyRamsey
ineffablyRamseys :: Int -> [Card]
ineffablyRamseys = iRamseys
iRamseyz :: Integer -> [Card]
iRamseyz n = fixedpoints n IneffablyRamsey
ineffablyRamseyz :: Integer -> [Card]
ineffablyRamseyz = iRamseyz
measures :: Int -> [Card]
measures n = order n Measurable
measurables :: Int -> [Card]
measurables = measures
measurez :: Integer -> [Card]
measurez n = fixedpoints n Measurable
measurablez :: Integer -> [Card]
measurablez = measurez
zeroDags :: Int -> [Card]
zeroDags n = order n ZeroDagger
zeroDaggers :: Int -> [Card]
zeroDaggers = zeroDags
zeroDagz :: Integer -> [Card]
zeroDagz n = fixedpoints n ZeroDagger
zeroDaggerz :: Integer -> [Card]
zeroDaggerz = zeroDagz
lambdaStrongs :: Int -> [Card]
lambdaStrongs n = order n LambdaStrong
lambdaStrongz :: Integer -> [Card]
lambdaStrongz n = fixedpoints n LambdaStrong
strongs :: Int -> [Card]
strongs n = order n Strong
strongz :: Integer -> [Card]
strongz n = fixedpoints n Strong
woodins :: Int -> [Card]
woodins n = order n Woodin
woodinz :: Integer -> [Card]
woodinz n = fixedpoints n Woodin
whWoodins :: Int -> [Card]
whWoodins n = order n WeaklyHyperWoodin
weaklyHyperWoodins :: Int -> [Card]
weaklyHyperWoodins = whWoodins
whWoodinz :: Integer -> [Card]
whWoodinz n = fixedpoints n WeaklyHyperWoodin
weaklyHyperWoodinz :: Integer -> [Card]
weaklyHyperWoodinz = whWoodinz
shelahs :: Int -> [Card]
shelahs n = order n Shelah
shelahz :: Integer -> [Card]
shelahz n = fixedpoints n Shelah
hWoodins :: Int -> [Card]
hWoodins n = order n HyperWoodin
hyperWoodins :: Int -> [Card]
hyperWoodins = hWoodins
hWoodinz :: Integer -> [Card]
hWoodinz n = fixedpoints n HyperWoodin
hyperWoodinz :: Integer -> [Card]
hyperWoodinz = hWoodinz
sss :: Int -> [Card]
sss n = order n Superstrong
superstrongs :: Int -> [Card]
superstrongs = sss
ssz :: Integer -> [Card]
ssz n = fixedpoints n Superstrong
superstrongz :: Integer -> [Card]
superstrongz = ssz
scs :: Int -> [Card]
scs n = order n Subcompact
subcompacts :: Int -> [Card]
subcompacts = scs
scz :: Integer -> [Card]
scz n = fixedpoints n Subcompact
subcompactz :: Integer -> [Card]
subcompactz = scz
stronglycompacts :: Int -> [Card]
stronglycompacts n = order n StronglyCompact
stronglycompactz :: Integer -> [Card]
stronglycompactz n = fixedpoints n StronglyCompact
supercompacts :: Int -> [Card]
supercompacts n = order n Supercompact
supercompactz :: Integer -> [Card]
supercompactz n = fixedpoints n Supercompact
etas :: Int -> [Card]
etas n = order n EtaExtendible
etaExtendibles :: Int -> [Card]
etaExtendibles = etas
etaz :: Integer -> [Card]
etaz n = fixedpoints n EtaExtendible
etaExtendiblez :: Integer -> [Card]
etaExtendiblez = etaz
extends :: Int -> [Card]
extends n = order n Extendible
extendibles :: Int -> [Card]
extendibles = extends
extendz :: Integer -> [Card]
extendz n = fixedpoints n Extendible
extendiblez :: Integer -> [Card]
extendiblez = extendz
vopenkas :: Int -> [Card]
vopenkas n = order n Vopenka
vopenkaz :: Integer -> [Card]
vopenkaz n = fixedpoints n Vopenka
nsss :: Int -> [Card]
nsss n = order n NSuperstrong
nSuperstrongs :: Int -> [Card]
nSuperstrongs = nsss
nssz :: Integer -> [Card]
nssz n = fixedpoints n NSuperstrong
nSuperstrongz :: Integer -> [Card]
nSuperstrongz = nssz
nahs :: Int -> [Card]
nahs n = order n NAlmostHuge
nAlmostHuges :: Int -> [Card]
nAlmostHuges = nahs
nahz :: Integer -> [Card]
nahz n = fixedpoints n NAlmostHuge
nAlmostHugez :: Integer -> [Card]
nAlmostHugez = nahz
nsahs :: Int -> [Card]
nsahs n = order n NSuperAlmostHuge
nSuperAlmostHuges :: Int -> [Card]
nSuperAlmostHuges = nsahs
nsahz :: Integer -> [Card]
nsahz n = fixedpoints n NSuperAlmostHuge
nSuperAlmostHugez :: Integer -> [Card]
nSuperAlmostHugez = nsahz
nHuges :: Int -> [Card]
nHuges n = order n NHuge
nHugez :: Integer -> [Card]
nHugez n = fixedpoints n NHuge
nshs :: Int -> [Card]
nshs n = order n NSuperHuge
nSuperHuges :: Int -> [Card]
nSuperHuges = nshs
nshz :: Integer -> [Card]
nshz n = fixedpoints n NSuperHuge
nSuperHugez :: Integer -> [Card]
nSuperHugez = nshz
ranks :: Int -> [Card]
ranks n = order n RankIntoRank
rankIntoRanks :: Int -> [Card]
rankIntoRanks = ranks
rankz :: Integer -> [Card]
rankz n = fixedpoints n RankIntoRank
rankIntoRankz :: Integer -> [Card]
rankIntoRankz = rankz
reinhardts :: Int -> [Card]
reinhardts n = order n Reinhardt
reinhardtz :: Integer -> [Card]
reinhardtz n = fixedpoints n Reinhardt