A transfinite cardinal arithmetic library including all known large cardinals
|Latest on Hackage:||0.0.1|
This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.
All rights reserved.
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).