The wholeness axiom and Laver sequences (Q1591376)

The ``Wholeness Axiom'' WA discussed in the paper is formalized in the language \(\{\in,{\mathbf j}\}\) where \({\mathbf j}\) is a unary function symbol. It consists of the followng axioms: (1) \(\exists x({\mathbf j}(x)\neq x)\), (2) For every formula \(\varphi(x_1,\dots, x_m)\) in the language \(\{\in\}\), \[ \forall x_1,\dots, x_m(\varphi(x_1,\dots, x_m)\leftrightarrow \varphi({\mathbf j}(x_1),\dots,{\mathbf j}(x_m))), \] (3) Each instance of the usual Separation scheme involving a formula \(\psi\) in the language \(\{\in,{\mathbf j}\}\). These axioms assert that \({\mathbf j}\) is a nontrivial elementary embedding from the universe into itself and that Separation holds for formulas with occurrences of \({\mathbf j}\). It is shown that \(\text{ZFC}+ \text{WA}\) has consistency strength strictly between \(I_3\) and the existence of a cardinal that is super-\(n\) huge for every \(n\). (By a result of \textit{K. Kunen} [J. Symb. Log. 36, 407-413 (1971; Zbl 0272.02087)], the stronger theory obtained by asking that Replacement holds for formulas with occurrences of \({\mathbf j}\) is inconsistent.) \(\text{ZFC}+ \text{WA}\) is used as a starting point for studying generalizations of Laver sequences (a Laver sequence at an infinite cardinal \(\kappa\) is a function \(f:\kappa\to V_\kappa\) with the property that for every set \(x\) an every \(\lambda\geq \max(\kappa,|\text{TC}(x)|)\) there is a normal ultrafilter \(U\) on \(P_\kappa(\lambda)\) such that \(x= i_U(f)(\kappa)\), where \(i_U\) is the canonical embedding determined by \(U\)). For example, it is shown that if WA holds and \(\kappa\) is the critical point of the WA-embedding \(j: V\to V\), then there is a Laver sequence \(f\) at \(\kappa\) with the following property: there exist \(\lambda\), \(U\) such that \(\lambda>\kappa\) and \(U\) is a normal ultrafilter on \(P_\kappa(\lambda)\), \(|\text{TC}(i_U(f)(\kappa))|\leq \lambda\) and if \(D\) is the normal ultrafilter on \(\kappa\) derived from \(i_U\), then, for each \(g:\kappa\to \kappa\) definable in \(V_\kappa\) (with parameters), the function \(\alpha\mapsto|f(\alpha)|\) dominates \(g\) on a set in \(D\). The existence of such a sequence is consistency-wise much stronger than supercompactness (it implies that there is a model of set theory with a proper class of extendibles). More generally, the paper is concerned with the problem of determining which large cardinals admit their own brand of Laver sequences and under what large cardinal assumptions these sequences can be built.