The wholeness axiom and Laver sequences Original Research Article

In this paper we introduce the Wholeness Axiom (WA), which asserts that there is a nontrivial elementary embedding from V to itself. We formalize the axiom in the language View the MathML source, adding to the usual axioms of ZFC all instances of Separation, but no instance of Replacement, for View the MathML source-formulas, as well as axioms that ensure that View the MathML source is a nontrivial elementary embedding from the universe to itself. We show that WA has consistency strength strictly between View the MathML source and the existence of a cardinal that is super-n-huge for every n. View the MathML source is used as a background theory for studying generalizations of Laver sequences. We define the notion of Laver sequence for general classes View the MathML source consisting of elementary embeddings of the form View the MathML source, where M is transitive, and use five globally defined large cardinal notions – strong, supercompact, extendible, super-almost-huge, superhuge – for examples and special cases of the main results. Assuming WA at the beginning, and eventually refining the hypothesis as far as possible, we prove the existence of a strong form of Laver sequence (called special Laver sequences) for a broad range of classes View the MathML source that include the five large cardinal types mentioned. We show that if κ is globally superstrong, if View the MathML source is Laver-closed at beth fixed points, and if there are superstrong embeddings i with critical point κ and arbitrarily large targets such that View the MathML source is weakly compatible with i, then our standard constructions are View the MathML source-Laver at κ. (In particular, if κ is super-almost-huge (superhuge, super-2-huge), there is an extendible (super-almost-huge, superhuge) Laver sequence at κ.) In addition, in most cases our Laver sequences can be made special if View the MathML source is upward λ-closed for sufficiently many λ.