Large Cardinals, Measures, and Elementary Embeddings

We first justify the small-union estimate used here. For every infinite cardinal theta, $\mathrm{\mid }\theta \times \theta \mathrm{\mid }=\theta$: by induction on infinite cardinals order pairs by their maximum coordinate, then lexicographically. An initial segment ending at coordinates below $\gamma +1<\theta$ has size at most $\mathrm{\mid }(\gamma +1)\times (\gamma +1)\mathrm{\mid }<\theta$, by the induction hypothesis at $\mathrm{\mid }\gamma +1\mathrm{\mid }$ (or by finite counting). This well-order has type at most theta, since otherwise its first theta elements would be a proper initial segment of size theta. The reverse bound uses the injection $\xi \mapsto (\xi ,0)$. Consequently for fewer than kappa sets of size below kappa, regularity bounds the set of their cardinalities and the index cardinal below a common infinite cardinal $\eta <\kappa$. Such an eta exists because a strong-limit cardinal is a limit cardinal: if kappa were the successor of eta, Cantor diagonalization would give $2^{\eta }\ge \kappa$. AC selects injections of the sets into eta, embedding their disjoint union into $\eta \times \eta$. Its size is therefore below kappa.

Induct on $\alpha <\kappa$. The empty V_0 is small. At a successor, $\mathrm{\mid }{V}_{\alpha +1}\mathrm{\mid }=2^{\mathrm{\mid }{V}_{\alpha }\mathrm{\mid }}<\kappa$ by strong limit. At a nonzero limit alpha there are fewer than kappa earlier levels, so step 1.1 bounds their union below kappa. If $x\in V_{\kappa }$, it is a subset of some earlier V level, hence has size below kappa.

If $Y\subseteq V_{\kappa }$ and $\mathrm{\mid }Y\mathrm{\mid }<\kappa$, Replacement collects the ranks of its members; regularity bounds their supremum plus one below kappa. Thus the supremum of their ranks plus one, namely rank(Y), is below kappa, so $Y\in V_{\kappa }$. For empty Y the rank is zero.

For $\mu ,\nu <\kappa$, graphs inject the set of functions $\nu \to \mu$ into $\mathcal{P}(\nu \times \mu )$. Step 1.1 bounds the product size by some infinite $\eta <\kappa$, so ${\mu }^{\nu }\le 2^{\eta }<\kappa$. This also covers finite cardinals; more explicitly ${\mu }^0=1$, $0^{\nu }=0$ for positive nu and $1^{\nu }=1$.

Let C be the set of infinite strong-limit cardinals below kappa. It is unbounded: above a given bound start with an infinite cardinal ${\theta }_0<\kappa$ larger than it, put ${\theta }_{n+1}=2^{{\theta }_n}$ and $\delta ={\sup }_n{\theta }_n<\kappa$ by regularity. Cantor diagonalization makes the sequence strictly increasing. Its supremum is a cardinal: a bijection of delta with a smaller ordinal would inject a larger theta_n into a smaller cardinal. For every cardinal $\mu <\delta$ some theta_n exceeds mu, hence $2^{\mu }\le {\theta }_{n+1}<\delta$. Thus delta is in C. If delta<kappa is a nonzero limit accumulation point of C, it is similarly a cardinal, and for every cardinal mu<delta there is $\rho \in C\cap \delta$ above mu, giving $2^{\mu }<\rho <\delta$. Thus delta is in C, proving closure. No enumeration choices are needed in this last uniquely defined iteration.

Transitivity transfers Extensionality and Foundation: every actual member of a set in V_kappa lies there, including an ambient Foundation witness. Empty and omega belong to V_kappa, since kappa is uncountable. Pairs, unions and full power sets of sets of rank below kappa again have rank below kappa: each requires only finitely many ordinal successor steps, and kappa is a limit ordinal. These actual operations verify Empty Set, Pairing, Union, Power Set and Infinity internally.

For Separation, ambient Separation using the fixed V_kappa-relativized formula gives a subset of a, hence an element of its full power set in V_kappa. For Replacement, ambient Replacement with that fixed relativized functional formula gives an image Y of $a\in V_{\kappa }$. It is a subset of V_kappa of size at most |a| (AC well-orders a and assigns each image its least preimage). F1 gives |a|<kappa and then Y in V_kappa. F3 identifies these with every internal schema instance.

For a family a of nonempty sets in V_kappa, ambient AC gives a choice function g on a. Each ordered pair in its graph uses only sets in a and their members, so its rank is bounded by rank(a) plus a fixed finite ordinal; this remains below kappa. Thus g belongs to V_kappa and is also an internal choice function. Together with steps 1.1 and 2.1 this proves all ZFC axioms.

Fix alpha<kappa. All subsets of any ordinal below alpha, all functions between such ordinals (including functions into alpha), and all bijections between their power sets and ordinals below alpha have rank below kappa, by the finite-rank bounds of step 1.1. Thus V_kappa has exactly the witnesses testing cardinalhood and cofinality below alpha, and exactly the full power sets and cardinal comparisons testing $2^{\mu }<\alpha$ for cardinals mu<alpha. Uncountability is the comparison with the same actual omega. Each of these tests agrees in both directions, so alpha is inaccessible internally iff it is inaccessible externally.

No singleton belongs to U: if {xi} did, upward closure and properness would make U exactly the principal ultrafilter at xi. Thus every singleton complement belongs to U. If $\mathrm{\mid }A\mathrm{\mid }<\kappa$, intersect the complements indexed by an enumeration of A; completeness puts $\kappa \setminus A$ in U, so A is not in U.

For $f:\kappa \to \eta$ with $\eta <\kappa$, if no fibre belonged to U, intersecting all eta fibre complements would put empty in U. Hence some fibre belongs to U. If kappa were singular, a cofinal sequence of length eta<kappa would partition kappa into eta bounded pieces (assign alpha the least index whose bound exceeds it). Each piece has size below kappa and is forbidden by step 1.1, contradicting the fibre conclusion. Thus kappa is regular.

If for some cardinal mu<kappa there were an injection $e:\kappa \to \mathcal{P}(\mu )$, for each xi<mu let $A_{\xi }=\{\alpha :\xi \in e(\alpha )\}$. Take the uniquely U-large side of each A_xi and intersect them; completeness makes the intersection U-large. All its elements have identical e-images, so injectivity makes it have at most one element, contradicting step 1.1. AC compares the cardinality of P(mu) with kappa; absence of such an injection gives $2^{\mu }<\kappa$. Together with regularity and uncountability this is F3. Coordinate decisions were unique and did not themselves spend AC.

Equality sets show reflexivity because I is in U, symmetry directly, and transitivity because the intersection of the f=g and g=h sets is contained in the f=h set. The product is a set and is nonempty by F3; its equivalence classes and their quotient form sets by Separation and Replacement.

If each f_j is replaced by an equivalent g_j, intersect their finitely many equality sets to get E in U. On E, all function values and relation truth values agree. The function outputs are therefore equivalent by upward closure. For any two truth sets A,B agreeing on E, A in U implies $A\cap E\subseteq B$ and hence B in U; the converse is symmetric. Thus relations are independent as well. Empty arity gives E=I. Constant-symbol functions are uniquely specified. For the diagonal map, equality of [c_a] and [c_b] is equivalent to I in U when a=b and empty in U when a differs from b, proving injectivity.

Induction on terms shows the value of a term on classes [f_j] is represented by its coordinate values. Constants and variables give the base cases and function symbols give the induction step by F1. Thus equality and relation atoms satisfy the asserted equivalence. Negation uses the complementary truth set and F3; conjunction uses intersection, which is in U exactly when both factors are (finite closure and upward closure).

At an existential formula, a witness [g] in the quotient gives, by the induction hypothesis on its matrix, a U-large set of coordinates where g(i) witnesses that matrix. The coordinate existential truth set contains it, hence is in U. Conversely suppose that truth set E is in U. For each i in E, choose a matrix witness in M_i; outside E choose a default element of M_i. These choices are from a set family of nonempty subsets of the supplied carriers, so F4 applies and gives a product function g. Its matrix truth set contains E, and induction makes [g] a quotient witness. This proves both existential directions and completes formula induction.

In a constant family with constant parameter functions, each coordinate has the same formula truth value. Its truth set is I when the original structure satisfies the formula, and empty otherwise. Properness and step 2.1 show precisely that the diagonal map preserves and reflects each formula; F1 already gives injectivity.

U-equivalence is reflexive and symmetric, and transitive because the intersection of two coordinate equality sets is contained in the third. The function f itself witnesses a possible representative rank; minimize within rank(f)+1 among ranks attained by equivalent functions. The least rank rho is attained, and Separation in $V_{\rho +1}$ forms all equivalent functions of rank rho, a nonempty set. Equivalent f,g have the same equivalence class and hence the same minimum-rank set. Conversely equal Scott sets have a common representative, so f and g are equivalent by transitivity.

If f,f-prime and g,g-prime are respectively equivalent, their coordinate membership truth sets agree on the intersection of their two equality sets, which is in U. A truth set agreeing there with a U-large set is U-large by intersection and upward closure; this implication is symmetric. Thus E does not depend on the selected functions representing either Scott set.

Fix g and put $A=\bigcup \mathrm{ran}(g)\cup \{\mathrm{\varnothing }\}$. If [f] E [g], replace f by $h(i)=f(i)$ when $f(i)\in g(i)$ and by empty otherwise. Then h maps I to the set A and is U-equivalent to f. All predecessors are consequently among $\{[h{]}_U:h\in {}^{I}A\}$, a set by Replacement on the set of functions. Separate those satisfying E with [g] to get exactly the predecessor collection. The fallback is fixed empty, so this bounding argument uses no AC.

Fix the formula externally. Atomic equality and membership are the coordinate clauses of F1. Negation complements the truth set, and conjunction intersects two truth sets. A proper ultrafilter contains exactly one of a set and its complement, and contains an intersection exactly when it contains both factors. These prove the Boolean induction steps, as in F2, without using satisfaction for a proper-class structure.

Suppose the coordinate truth set $A=\{i:\mathrm{\exists }x\psi (x,f_1(i),\dots ,f_n(i))\}$ lies in U. For each i in A there is a least ordinal ${\rho }_i$ which is the rank of a witness: first bound the search by the rank of any one witness, then minimize ordinals. This defines rho_i uniquely, so Replacement collects these ordinals. For each i in A, Separation in $V_{{\rho }_i+1}$ gives the nonempty set $W_i$ of witnesses of rank rho_i. Replacement collects the family of W_i, and F3 supplies choices g(i) in W_i. Set g(i) to empty outside A. This is a set function on I. Its matrix truth set contains A, so the induction hypothesis gives a Scott-domain witness [g]. The choices were from sets, not proper classes.

Conversely a Scott-domain existential witness has the form [g] for a set function g. The matrix induction hypothesis says its coordinate matrix truth set belongs to U. This set is contained in the existential truth set, which therefore belongs to U by upward closure. Together with step 2.1 this completes the formula induction. For constant parameters the coordinate truth set is I or empty according to the ambient formula's truth; properness gives preservation and reflection by the constant map. Apply the proved schema to the single axiom of Extensionality, true in V: its coordinate truth set is I, so the Scott structure is extensional. No simultaneous truth definition over all formulas was used.

Assume U countably complete. If a nonempty set S of Scott classes has no E-minimal member, choose an initial a_0 in S. By F4 choose, for each a in S, a predecessor s(a) in S; recursion gives $a_{n+1}=s(a_n)$. By F2 and F4 choose representative functions f_n from the nonempty Scott sets a_n. Each $A_n=\{i:f_{n+1}(i)\in f_n(i)\}$ belongs to U. Countable completeness makes their intersection a member of U, hence nonempty. At any i in it, the set $\{f_n(i):n\in \omega \}$ has no membership-minimal member, contrary to Foundation. Thus every nonempty set of classes has an E-minimal member. This also suffices for definable subclasses: for any chosen member, its finite predecessor closure is a set by set-likeness and Replacement, and an E-minimal member of its intersection with the subclass is minimal in that subclass.

Conversely, if U is not countably complete, take A_n in U with intersection A not in U. Set $B_n=(I\setminus A)\cap {\bigcap }_{k\le n}{A}_k$. Each B_n is in U and their intersection is empty. For every i let e(i) be the least n with i not in B_n. Then $\{i:e(i)>n\}=B_n$. Put $g_m(i)=\max (e(i)-m,0)$, viewed as a finite von Neumann ordinal. On B_m, g_(m+1)(i) is strictly smaller than g_m(i), hence belongs to it. Consequently $[g_{m+1}{]}_{U}E[g_m{]}_U$ for all m. Their range is a nonempty set with no E-minimal member, so the ultrapower is not well-founded.

In the complete case, F1 gives extensionality, F2 gives set-likeness and step 1.1 gives well-foundedness. Apply F3 to obtain a definable collapse pi onto transitive M. Composing pi with the constant map yields a definable elementary j by F1. For each ordinal alpha, elementarity says j(alpha) is an ordinal in M; transitivity makes this an actual ordinal. The map on ordinals is strictly increasing since membership is preserved. Induction gives $j(\alpha )\ge \alpha$: j(alpha) is above all j(beta) for beta below alpha, hence above or equal to their required supremum alpha. Given any ordinal gamma, j(gamma+1) belongs to M and is larger than gamma, so transitivity puts gamma in M. Restrictions of pi and j to sets are sets by Replacement; no Global Choice is involved.

U is countably complete since kappa is uncountable, so F1 applies. For any nonempty set x with size eta<kappa, choose a bijection b from eta to x using F3. A predecessor [f] E [c_x] has f(i) in x on a U-large set. Replace f outside that set by b(0), without changing its class. Composing with the inverse of b gives a function to eta, hence has a constant U-large fibre by F2. Therefore [f]=[c_y] for some y in x. Conversely every y in x gives such a predecessor. For empty x there are no predecessors by properness. The collapse equation now gives $j(x)=\{j(y):y\in x\}$ whenever |x|<kappa.

Every ordinal alpha<kappa has size below kappa. By induction, step 1.1 gives $j(\alpha )=\{j(\beta ):\beta <\alpha \}=\alpha$, including alpha=0. The identity function always takes values in kappa, so its collapsed class d belongs to j(kappa), hence is an ordinal. For every alpha<kappa the tail $\{\xi :\alpha <\xi <\kappa \}$ is U-large, since its complement has size below kappa by F2. Thus alpha=j(alpha) belongs to d. Consequently $\kappa \le d<j(\kappa )$; kappa is moved and all earlier ordinals are fixed.

By F2 kappa is inaccessible and by F4 every x in V_kappa has size below kappa. Apply rank induction to such x. Every y in x has smaller rank and remains in V_kappa, so the induction hypothesis fixes y. Step 1.1 then gives $j(x)=\{j(y):y\in x\}=x$. The induction starts with empty and includes all limit ranks without a separate choice of representatives.

Suppose j has critical point kappa. Its ordinal map is increasing, fixes every alpha<kappa and has j(kappa)>kappa; since M is transitive and contains j(kappa), it contains kappa. Define $W=\{X\subseteq \kappa :\kappa \in j(X)\}$. F2 and Separation make W a set. Images of kappa and empty show it proper. Elementarity for complements and finite intersections, evaluated at kappa, proves the ultrafilter laws in F3. For singleton {alpha}, j({alpha})={alpha}, which omits kappa, so W is nonprincipal. If eta<kappa and every X_xi for xi<eta belongs to W, j fixes eta and the value of the image sequence at xi is j(X_xi). Thus kappa lies in the intersection of that image sequence, which is j of the original intersection. This proves kappa-completeness, including eta=0.

If f is regressive on S in W with zero omitted, then kappa belongs to j(S) and $j(f)(\kappa )<\kappa$. Let this ordinal be beta; j fixes beta. Elementarity applied to the beta-fibre says kappa belongs to $j(\{\alpha \in S:f(\alpha )=\beta \})$. That fibre therefore belongs to W. So W is normal. A measurable kappa gives the embedding by F1 and hence a normal W by this construction; a normal measure is itself a measure, and also gives the embedding by F1. This proves all three equivalences without asserting that the original measure was already normal. F4 is inherited in F1.

Let d be the collapsed identity class for U. By F1 it is an ordinal at least kappa. If U is normal, any predecessor [f] of the identity class has, on a U-large set omitting zero, ordinal values f(alpha)<alpha. Normality makes f constant there, so its collapsed class is an ordinal beta<kappa. Every beta<kappa is already below d by F1. Thus d=kappa. Conversely suppose d=kappa and f is regressive on a U-large S omitting zero. Extend f by zero outside S. Its collapsed class belongs to d=kappa, so equals beta for some beta<kappa. F1 identifies beta with the collapsed constant-beta class. Injectivity of the collapse and Scott equality give a U-large equality fibre; intersecting it with S proves normality.

For normal U and A_xi in U for xi<kappa, let $D=\{\alpha <\kappa :(\mathrm{\forall }\xi <\alpha )\alpha \in A_{\xi }\}$. If its complement were U-large, omit zero and assign to alpha the least failed xi<alpha. Normality gives a U-large constant fibre beta, disjoint from A_beta, contrary to properness. Hence D is in U. Conversely assume diagonal closure and let f be regressive on S in U, zero omitted. If no fibre were U-large, all fibre complements A_xi would belong to U. Their diagonal intersection D belongs to U, but every alpha in S fails its membership requirement at xi=f(alpha)<alpha. Thus S and D are disjoint U-members, a contradiction. This proves the stated compatibility of normality conventions.

Induct on the well-founded syntax tree in F1. The atomic cases are F2, and negation uses the ultrafilter decision between a set and its complement. For fewer than kappa component truth sets A_xi, their intersection belongs to U if all A_xi do, by F3; the converse follows by upward closure. Their union belongs to U if some A_xi does; if none does, F3 puts the intersection of their complements in U, excluding the union. These are precisely the conjunction and disjunction clauses, including empty operations.

Consider an existential block of eta<kappa variables. If its coordinate truth set A belongs to U, then for each i in A the witnessing tuples form a nonempty subset of the set $M_i^{\eta }$. By F4 choose one tuple at each such coordinate, and choose a default element of M_i outside A. Extend with the constant default tuple there. Each of the eta columns is a product representative; their matrix truth set contains A. The induction hypothesis gives a true matrix in the quotient, hence a quotient witness tuple. Conversely a witnessing quotient tuple has eta entries; F4 chooses product representatives for these entries from their nonempty set equivalence classes. The matrix induction hypothesis gives a U-large coordinate matrix truth set, contained in the coordinate existential set. Thus the latter is U-large. Eta=0 reduces exactly to the matrix, with the unique empty tuple. Universal blocks follow by negating an existential block of the negated matrix.

Finally replace any tuple of fewer than kappa parameter representatives by equivalent ones. Intersect their coordinate equality sets using F3. On this U-large intersection all parameter values agree, so set satisfaction of the fixed formula has the same truth value for both tuples. Intersecting a U-large truth set with this agreement set and using upward closure proves that either truth set belongs to U exactly when the other does. The induction already proved quotient truth equivalent to coordinate truth-set membership, so this also verifies the asserted representative invariance for infinitary parameters.

Assume the tree property and fix $c:[\kappa {]}^2\to \mu$, where 0<mu<kappa. Form a tree whose alpha-level consists of the functions $c(\cdot ,\beta )\upharpoonright \alpha$ for alpha<=beta<kappa. Restriction to gamma<alpha is realized by the same beta, so these levels form a tree under proper extension, with heights exactly their domains. Each level is nonempty and has at most ${\mu }^{\mathrm{\mid }\alpha \mathrm{\mid }}<\kappa$ members by F2. Thus a cofinal branch yields a function $h:\kappa \to \mu$ whose every initial segment occurs in the tree.

Recursively for xi<kappa let alpha_xi be the supremum of the ordinals beta_eta+1 for eta<xi (zero at xi=0). Regularity makes alpha_xi<kappa. Let beta_xi be the least beta>=alpha_xi realizing $h\upharpoonright {\alpha }_{\xi }=c(\cdot ,\beta )\upharpoonright {\alpha }_{\xi }$; such beta exists by step 1.1. F3 gives this strictly increasing sequence. For eta<xi, $c({\beta }_{\eta },{\beta }_{\xi })=h({\beta }_{\eta })$. One color is taken by h(beta_xi) for kappa many xi: otherwise the union of mu<kappa sets of size below kappa would have size below kappa by regularity and F2. The corresponding beta_xi form a homogeneous set of size kappa. This proves all the asserted nonzero-color arrows, in particular the two-color arrow.

Conversely assume the two-color arrow and let T be a kappa-tree. By F4 choose t_alpha at each level alpha, and give each level an injective labeling into an ordinal of size below kappa. Code a node t of height alpha by the sequence of labels of its unique ancestor at each gamma<=alpha, including t itself at gamma=alpha. Two distinct nodes have distinct codes: if their heights differ and all common coordinates agree the shorter node is an ancestor; if heights coincide their own labels differ. Order codes lexicographically, with a proper prefix smaller. For distinct codes the first differing coordinate exists by ordinal well-ordering, unless one is a proper prefix. This gives a linear order: transitivity follows by comparing the earliest coordinate at which any of three codes differ, with an ended code considered smaller than every next label. Including each node's own level label distinguishes distinct nodes at a limit level even when all earlier ancestors coincide.

Color alpha<beta by whether the code of t_alpha is smaller or larger than that of t_beta. A homogeneous H of size kappa gives a strictly monotone sequence of codes, indexed in the increasing order of H, which has order type kappa by regularity. Fix gamma<kappa and discard the bounded initial part at heights below gamma. Restriction of lexicographically ordered codes to the common length gamma+1 preserves their weak order, so their gamma-ancestor codes form a monotone sequence with fewer than kappa possible values. Such a sequence is eventually constant: for each value that occurs, take its first occurrence, and regularity bounds these fewer than kappa occurrence indices below some delta<kappa; after delta a change would either introduce a new value or revisit a departed value, the latter impossible for a monotone sequence. Let u_gamma be the eventual ancestor. For gamma<eta, a node sufficiently far out has both eventual ancestors u_gamma and u_eta, so u_gamma is the gamma-ancestor of u_eta. Thus the u_gamma form a cofinal branch. This proves the tree property and completes the equivalences.

For each nu<kappa every map nu to kappa has bounded range by regularity. For each bound eta<kappa, F2 gives fewer than kappa such maps into eta. Union over kappa bounds has size at most kappa, using the cardinal-square estimate in F2; constant maps give equality for nu>0. Thus ${\kappa }^{<\kappa }=\kappa$. Every syntax tree has fewer than kappa nodes: its nodes lie at finite path depths, each depth has fewer than kappa nodes by regularity and its branching bounds, and a countable union is still small. A formula therefore uses fewer than kappa symbols. The symbols of T number at most kappa. In any signature with at most kappa symbols and kappa variables, canonical labeled syntax trees are coded by fewer than kappa pairs of finite paths and labels, so their number is at most ${\kappa }^{<\kappa }=\kappa$. Restrict now to the symbols of T.

Add kappa fresh constants, including a designated default constant. In kappa stages perform the following operation: for every existential sentence $\mathrm{\exists }\bar{x}\psi (\bar{x})$ in the language so far, add a fresh tuple of constants ${\bar{c}}_{\psi }$ of the same length and the Henkin axiom $(\mathrm{\exists }\bar{x}\psi (\bar{x}))\to \psi ({\bar{c}}_{\psi })$. At limits take unions. Step 1.1 bounds the number of formulas and new constants at every stage by kappa, so the final signature and set H of these axioms have size kappa. Every sentence of the final language, including every substitution instance with constants, uses fewer than kappa constants, hence belongs to some stage by regularity; its existential witness axiom is supplied at the next stage. Given any original set structure, choose a default element and well-order the set of all its tuples of length less than kappa using F4. At each stage interpret each fresh witness tuple as the least tuple satisfying its matrix if one exists, and as the constant default tuple otherwise. Later stages preserve earlier interpretations. This constructs an expansion satisfying all H, with the original structure unchanged.

Let F be all sentences of the final language, including H and T, and enumerate F without repetition in type kappa; the added constants ensure size kappa. Write F_alpha for the first alpha sentences. At level alpha put the pairs (alpha,v), where $v:F_{\alpha }\to 2$ is the actual truth restriction of some expanded set structure satisfying H and $T\cap F_{\alpha }$. Such truth restrictions form a set by Separation in $2^{F_{\alpha }}$, using set satisfaction from F1; no selection from a proper class of models is made. The level is nonempty: T intersect F_alpha has size below kappa, so has a model, which step 2.1 expands. There are at most $2^{\mathrm{\mid }\alpha \mathrm{\mid }}<\kappa$ nodes. Order nodes by proper restriction with their levels. Restricting a realizing model's truth gives a node at every earlier level, so the resulting tree has height kappa and the F3 width bound.

A cofinal branch has union $v:F\to 2$. Every fewer-than-kappa collection of sentences is contained in some F_alpha by regularity. Therefore its assigned truth values are simultaneously realized in a set structure: take a branch node above alpha and its realizing structure. In particular v makes every sentence of T and H true, obeys negation, and obeys every fewer-than-kappa conjunction or disjunction together with all of its components. Equality of constants is an equivalence relation, and replacement of equal constants in any fixed infinitary sentence preserves its v-value: all the fewer-than-kappa equality instances, the sentence and its replacement fit together in one realized restriction.

Form a structure N whose carrier is the set of equivalence classes of constants under v-equality. It is nonempty. For each finite-arity function symbol and constant tuple, the logically true sentence $\mathrm{\exists }x(x=f(\bar{c}))$ has v-value one by step 4.1; its Henkin axiom supplies a constant naming the function value. Use that class as the function interpretation. Equality substitution in step 4.1 proves both independence of the selected value constant and of the argument representatives. Interpret a relation by the v-value of its constant instance; this is independent of representatives for the same reason. Original constants have their own classes. Induction on finite terms now gives a named value for every term and agreement of all atomic formulas with v.

Induct on formula syntax to show N satisfies a sentence with constant parameters exactly when its v-value is one. Atoms follow step 5.1; infinitary Boolean clauses follow step 4.1. If an existential block has v-value one, its Henkin axiom and the Boolean clauses give a witness tuple of constants with matrix value one, hence a witness in N by induction. Conversely a witness tuple in N has fewer than kappa classes; F4 chooses constant representatives. Induction makes that matrix instance have v-value one. The matrix instance together with the existential sentence is realized in one restriction from step 4.1, so the existential has v-value one too. Empty blocks have the unique empty tuple. This completes the truth induction, and all T holds in N. Any unused symbols from the original larger signature can be interpreted on this nonempty carrier by default-valued functions and empty relations.

If kappa is weakly compact, apply F2 to any theory in the assertion. F1 gives a cofinal branch in its truth tree, and F2 produces a model. Thus the L_(kappa,kappa) property holds. Every L_(kappa,omega) theory is a special case with finite blocks, so the latter compactness property follows.

Conversely assume the L_(kappa,omega) property and fix a kappa-tree S. It has kappa nodes: its kappa nonempty levels give the lower bound, and choosing injections of levels into kappa gives the upper bound by the cardinal-square estimate used in F2. Introduce a unary relation P_t for each node t and one constant d; write p_t for the sentence P_t(d). Take a theory consisting of the disjunction ${\bigvee }_{t\in S_{\alpha }}{p}_t$ for each alpha<kappa and the sentences $\mathrm{\neg }(p_s\wedge p_t)$ for each incomparable pair s,t. Every level disjunction has fewer than kappa terms, so this is already an L_(kappa,omega) theory (indeed it uses no quantifiers). Its language and theory have size at most kappa, using the same square bound.

Any subtheory of size below kappa has level-disjunction requirements at a bounded collection of levels, by regularity. Choose a node u above those levels. In a one-element structure interpret p_t as true exactly for t<=u. This meets every required level and violates no incomparable-pair prohibition, including prohibitions mentioning nodes at arbitrarily high levels. Hence every small subtheory is satisfiable. Compactness gives a full model. Its true p_t include a node at each level and never include incomparable nodes; they therefore form a cofinal branch of S. As S was arbitrary, F1 gives weak compactness. Together with step 1.1 this proves both equivalences.

We need an ordinal pairing that preserves every infinite cardinal. Order all ordinal pairs by their maximum coordinate, then lexicographically, and let p(a,b) be the order type of the predecessors of (a,b). Each predecessor collection is a set and this is a well-order, so p is definable and injective. For every infinite cardinal lambda and a,b<lambda, p(a,b)<lambda. To verify the size bound, induct on infinite cardinals theta: each proper initial segment of this order on theta squared is contained in (gamma+1) squared for some gamma<theta. By induction at the smaller cardinal |gamma+1|, or finite counting, that segment has cardinality below theta. Thus its order type is below theta, and the whole order has type at most theta (otherwise its first theta elements form a proper segment of size theta). The diagonal gives the reverse cardinal bound. This simultaneously proves the square bound and the asserted preservation for p. We will use b=0 or 1.

Induct on the cardinal $\gamma =\sup A$. Every subset used below inherits the disjoint-club hypothesis. If A is empty, use the empty function. If gamma=omega, A={omega} and g(omega)=0 works. If gamma is a successor cardinal lambda-plus, then gamma belongs to A and A without gamma has supremum at most lambda. Apply induction there; all its values are below lambda, even if lambda belongs to A. Extend by assigning gamma the value lambda. This remains injective and regressive.

Suppose gamma is a singular limit cardinal and put delta=cf(gamma)<gamma. Choose a strictly increasing continuous cofinal sequence of infinite cardinals $⟨{\mu }_{\xi }:\xi <\delta ⟩$ in gamma with mu_0>delta. Such a sequence is obtained from a cofinal sequence by choosing larger cardinals at successors and taking suprema at nonzero limits; at fewer than delta stages the supremum is below gamma by the definition of cofinality. The cardinals in A below mu_0, and those in each open interval (mu_xi,mu_(xi+1)), have supremum below gamma, so induction and F4 supply regressive injections on each piece. For the bottom piece use its injection unchanged. On an interval with lower endpoint mu_xi replace its injection f by $\alpha \mapsto {\mu }_{\xi }+f(\alpha )$. This is injective because ordinal addition is strictly increasing in its right argument, has values at least mu_xi, and is still below alpha: both summands have cardinality below the infinite cardinal alpha, and their finite sum does too by step 1.1. Distinct pieces now have disjoint ranges. Call their combined injection h.

The remaining elements of A in the singular case are sequence endpoints mu_xi and possibly gamma. Give an endpoint mu_xi its index xi, and gamma, if present, index delta. These indices are distinct and below mu_0, hence below their respective arguments. Map endpoints to p(index,0), and every nonendpoint alpha to p(h(alpha),1). Step 1.1 makes each value below its infinite-cardinal argument, and injectivity of p separates endpoints from gaps as well as separating within each part. Continuity of the sequence ensures this partition exhausts A: if alpha is neither an endpoint nor below mu_0, the least sequence value above alpha cannot have a limit index.

Finally suppose gamma is an uncountable regular limit cardinal. The hypothesis gives a club C in gamma disjoint from A intersect gamma. Enumerate C continuously in its increasing order, of length gamma; a shorter cofinal enumeration would contradict regularity. Partition A intersect gamma into the portion below min(C) and the open gaps between successive C elements. Closure ensures no other elements of A remain at limit accumulation points. Each piece has supremum below gamma, so induction and F4 give local injections. Shift an interval injection by its lower endpoint exactly as in step 3.1; leave the bottom injection unchanged. Their disjoint ranges yield a regressive injection h on A intersect gamma. Map these alpha to p(h(alpha),1), and, if gamma belongs to A, map gamma to p(0,0). Step 1.1 proves regressiveness and injectivity, including separation of the possible top endpoint. These cases exhaust infinite cardinals gamma and complete the induction.

Suppose, towards a contradiction, that S has no stationary initial segment at an uncountable regular rho<kappa. By F3 choose a club C of infinite strong-limit cardinals below kappa. Then A=S intersect C is a stationary set of infinite cardinals by F6. For each alpha<kappa, A intersect alpha satisfies F2's hypotheses: below kappa its initial segments are subsets of the assumed nonstationary S initial segments, and at any regular rho>=kappa it is bounded, hence nonstationary by F6. Thus every A intersect alpha admits a regressive injection.

At level alpha take all pairs (alpha,f), where f is an injective regressive function on A intersect alpha with values in alpha. This level is nonempty by step 1.1; at alpha=0 it contains the empty function. Its size is at most $2^{\mathrm{\mid }\alpha \times \alpha \mathrm{\mid }}<\kappa$ by F3 (the finite cases also satisfy the bound). Order nodes by restriction at earlier levels. Restrictions remain injective and regressive and have values in the earlier alpha because f(beta)<beta, so every node has the required full chain of predecessors. This is a kappa-tree. F1 supplies a cofinal branch whose union is a regressive injection on A. F4 makes some fibre stationary, whereas injectivity makes it have at most one element, impossible by F6. This contradiction proves reflection for every S. The argument retains F5 through its cited suppliers.

Let D be any club in kappa. It is stationary by F6, so step 2.1 gives an uncountable regular rho<kappa with D intersect rho stationary, hence unbounded in rho. Since D is closed and rho is a nonzero limit ordinal, rho belongs to D. Therefore every club meets the uncountable regular cardinals below kappa, proving Mahloness under F1's inherited definition. Finally intersect this stationary set with the strong-limit club C from F3. Every element of the intersection is uncountable, regular and strong limit, hence inaccessible, and the intersection is stationary by F6. This proves the last assertion.

Let U be a normal measure on kappa, supplied by F1, and fix a coloring $c:[\kappa {]}^2\to 2$. For each alpha<kappa the tail above alpha is measure one by F2. Its two color fibres are disjoint and cover that tail; exactly one belongs to U by the ultrafilter laws. Let i_alpha be this uniquely determined color and A_alpha its fibre. Exactly one of the sets $H_i=\{\alpha :i_{\alpha }=i\}$, i<2, belongs to U. Fix its color i. These selections are unique finite decisions, with no extra choice beyond the ambient F4.

By F1 the diagonal intersection $D=\{\beta <\kappa :(\mathrm{\forall }\alpha <\beta )\beta \in A_{\alpha }\}$ belongs to U. Thus H=H_i intersect D belongs to U and has size kappa by F2. If alpha<beta both belong to H, then alpha lies in H_i and beta lies in D, so beta belongs to A_alpha and c(alpha,beta)=i_alpha=i. Hence H is homogeneous. F2 makes kappa inaccessible, and F3 turns this two-color partition property into weak compactness.

Assume filter extension and fix lambda>=kappa. For a in P_kappa(lambda), let C_a be the cone of x containing a. The sets containing some C_a form a proper filter: every cone contains a itself, and C_a intersect C_b=C_(a union b). An intersection of eta<kappa such filter members contains the cone above the union of their witnessing a_xi. F3 selects those witnesses; regularity makes their union have size below kappa (bound all sizes below one cardinal below kappa and use the infinite-cardinal product bound). Thus the filter is kappa-complete. Extend it by F1. Since C_{alpha} belongs to it for each alpha<lambda, the extension is fine.

Assume the fine-measure assertion and fix a theory T as in the L_(kappa,kappa) assertion. Choose a cardinal lambda>=kappa and an injection e:T to lambda. Push a fine measure on P_kappa(lambda) forward by $x\mapsto e^{-1}[x]$ to get a proper kappa-complete ultrafilter W on P_kappa(T). Inverse images preserve all intersections and complements, proving these laws. For every t in T, the inverse image of the cone of small subtheories containing t contains the e(t)-cone, so W is fine.

Each small subtheory a has a set model in the common signature. For each a take the least rank rho_a of such a model code. This is uniquely defined by set satisfaction, and Replacement collects the ranks. Separation in V_(rho_a+1) gives the nonempty set of rank-rho_a model codes satisfying a; F3 chooses one for each a. This bounds the choices before AC and does not choose from classes of models. Take their set ultraproduct by W. For each t in T the coordinate truth set contains the cone of a containing t, hence is in W. F2 makes t true in the ultraproduct. Thus T has a model. The L_(kappa,omega) assertion follows by restriction of syntax.

Assume the L_(kappa,omega) assertion and let F be a proper kappa-complete filter on a set I. Introduce one constant d and one unary relation R_X for every subset X of I; abbreviate R_X(d) by r_X. Include r_I, not r_empty, the equivalences $r_{I\setminus X}\leftrightarrow \mathrm{\neg }{r}_X$, and $r_{{\bigcap }_{\xi <\eta }{X}_{\xi }}\leftrightarrow {\bigwedge }_{\xi <\eta }{r}_{X_{\xi }}$ for every eta<kappa and every such sequence of subsets. Also include r_X for each X in F. This is a set theory in L_(kappa,omega), using no quantifier blocks. For any subtheory of size below kappa, the fewer-than-kappa F-members explicitly required have a nonempty intersection by completeness and properness. Take i in it and interpret the predicates on a one-element carrier by r_X true exactly when i belongs to X. Every identity axiom is then true, even those mentioning other subsets, and all the chosen F-requirements hold. Empty collections use I, which is nonempty since F is proper.

Compactness yields a full model. Define U to be the subsets X for which r_X is true there. The top and bottom axioms give properness. The intersection identities give kappa-completeness; their binary instances also give upward closure, since X subset Y implies X intersect Y=X and r_X forces r_Y. Complement identities decide exactly one of X and its complement. Thus U is a kappa-complete ultrafilter, and the F-requirements give F subset U. This proves filter extension, closing the cycle of equivalences.

Kappa-completeness and uncountability imply countable completeness, so F2 gives the collapsed ultrapower and its formula-by-formula coordinate equivalence. At every coordinate x, x is a subset of lambda of size below kappa. The equivalence therefore says $s\in j(P_{\kappa }(\lambda ))$: M regards s as a subset of j(lambda) of size below j(kappa). As M is transitive, the subset statement also holds externally. For each alpha<lambda, the coordinate set where alpha belongs to x is U-large by F1, so j(alpha) belongs to s. All cardinal and collapse uses retain F3.

Suppose U normal. Any member of s is the collapsed class of a function f which selects f(x) in x on a U-large set S. On S these are ordinals below lambda, so F1 makes some fibre alpha U-large. Scott equality and injectivity of the collapse identify that member with j(alpha). Together with step 1.1 this proves s=j``lambda. Conversely suppose equality. Given f:S to lambda selecting an element of x on a U-large S, extend f by zero outside S. Its collapsed class belongs to s, hence is j(alpha) for some alpha<lambda. Scott equality says the extended f equals alpha on a U-large set. Intersect with S to obtain the required fibre of the original f. Thus U is normal.

At each coordinate, x is a set of ordinals, and its order type is below kappa: it has cardinality |x|<kappa and kappa is an initial ordinal. The formula defining the unique ordinal order type transfers by F2. Thus the collapsed class of x maps to otp(x) is the order type of s computed in M, and is below j(kappa). In the normal case the increasing map j restricted to lambda is an external order isomorphism of lambda with s by step 2.1. The order isomorphism supplied inside M is also an external one, since M is transitive and its graph and domain are sets; uniqueness of ordinal order types therefore makes its value exactly lambda. Hence lambda<j(kappa). This does not replace M's internal size bound by an unsupported external cardinal comparison in the merely fine case.

If kappa is strongly compact, take the fine U on P_kappa(lambda) from F1 and its j,s from F2. We check the critical point without assuming U is a measure on kappa. For every eta<kappa, a map from the index set to eta has a U-large constant fibre: otherwise intersecting the eta fibre complements gives empty in U. Induct on alpha<kappa. Each predecessor of the constant-alpha class, for alpha>0, can be modified outside its U-large membership set to take values in alpha; the fibre argument makes it constant. For alpha=0 there are no predecessors. The collapse equation then gives j(alpha)=alpha, exactly the predecessor reasoning whose critical-point terminology is F3.

If j(kappa)=kappa, F2's internal size bound gives in M an enumeration of s of ordinal length eta<kappa. This is also an external enumeration, since M is transitive. But s contains j``kappa=kappa by step 1.1, contradicting that kappa is a cardinal: choosing the least preimage of each ordinal below kappa injects kappa into eta. Hence j(kappa)>kappa (the ordinal map is increasing and cannot move it downward), and its critical point is kappa. This proves the required embedding property.

Conversely take such j,s for a fixed lambda. Its internal subset and size assertions mean precisely that s belongs to j(P_kappa(lambda)). Define $U=\{X\subseteq P_{\kappa }(\lambda ):s\in j(X)\}$. Definability and Separation make U a set. The seed lies in the image of the whole index set and not in j(empty); image complements, intersections and inclusions give properness, complement decisions and upward closure. If eta<kappa and X_xi are U-members, j fixes eta and the image sequence has entry j(X_xi) at xi. Thus s belongs to the intersection of that image sequence, equal to j of the intersection, proving kappa-completeness. For alpha<lambda the image of its point cone is the sets containing j(alpha); since j(alpha) belongs to s, that cone belongs to U. Hence U is fine. This holds for every lambda, so F1 gives strong compactness. No equality of s with j``lambda or sequence closure of M has been inferred.

From a normal fine U take j and s=j``lambda as in F1. Every map from its index set into eta<kappa has a constant U-large fibre, for otherwise kappa-completeness intersects all fibre complements to empty. Induct on alpha<kappa. Each predecessor of the constant-alpha class, for alpha>0, can be modified outside its U-large membership set to take values in alpha; the fibre argument makes it constant. For alpha=0 there are no predecessors. The collapse equation then gives j(alpha)=alpha. F1 gives j(kappa)>lambda>=kappa, so the critical point is exactly kappa.

Let $⟨a_{\alpha }:\alpha <\lambda ⟩$ be an ambient sequence of elements of M. The collapse has a unique Scott preimage for each a_alpha. Replacement therefore collects these nonempty set representatives; F3 chooses f_alpha from each one, so $\pi ([f_{\alpha }{]}_U)=a_{\alpha }$. Define the set function $F(x)=\{(\alpha ,f_{\alpha }(x)):\alpha \in x\}$. Its collapsed class G is exactly $\{(j(\alpha ),a_{\alpha }):\alpha <\lambda \}$. For the inclusion from right to left use fineness: on the alpha-cone the pair (alpha,f_alpha(x)) belongs to F(x), and coordinate pairing transfers through the collapse. Conversely, any represented member of [F] selects on a U-large set a unique pair with first component alpha(x) in x. Normality makes alpha(x) a fixed alpha on a U-large subset. The selected pair is then equivalent to (alpha,f_alpha(x)), giving the required collapsed pair. This proves both inclusions.

G belongs to M, and M has the increasing enumeration e of s of order type lambda by F1. Externally this enumeration is precisely alpha maps to j(alpha), by uniqueness of ordinal order type. Inside M compose the function with graph G with e. Its value at alpha is a_alpha, so the original ambient sequence belongs to M. The reindexing is essential: G itself has domain j``lambda, not generally lambda. Thus M has the asserted lambda-sequence closure.

Conversely suppose j satisfies the embedding and closure conditions. Each j(alpha) for alpha<lambda lies in M, so the set-restriction convention and closure put $j\upharpoonright \lambda$ in M. Its domain lambda and range s=j``lambda consequently belong to M. This increasing map exhibits there the order type lambda, so M regards |s| as at most |lambda| and hence below j(kappa), since lambda<j(kappa) and j(kappa) is a cardinal of M. Also s is a subset of j(lambda). Thus s belongs to j(P_kappa(lambda)). Define U by the displayed formula using Separation. Elementarity for empty, whole index set, complements and finite intersections makes U a proper ultrafilter. For eta<kappa, j fixes eta and maps a sequence of U-members to a sequence with those j-images at each fixed index; s belongs to their intersection, proving kappa-completeness. Each point cone is large because s contains every j(alpha), proving fineness.

For normality let f:S to lambda select an element of x for x in S, with S in U. Then s belongs to j(S), so j(f)(s) belongs to s=j``lambda. It equals j(alpha) for some alpha<lambda. Elementarity for that fibre gives $s\in j(\{x\in S:f(x)=\alpha \})$, so the fibre belongs to U. Hence U is normal, fine and kappa-complete, which is precisely lambda-supercompactness. All derived sets use the definable embedding convention; no Global Choice is required.

A supercompact kappa has a normal fine complete measure at every lambda>=kappa by its definition and F1. Forgetting normality gives the fine measures of F2, hence strong compactness. For a strongly compact kappa, consider the co-small filter $\{X\subseteq \kappa :\mathrm{\mid }\kappa \setminus X\mathrm{\mid }<\kappa \}$. It is proper and kappa-complete: a fewer-than-kappa union of small complements remains small by regularity and F7. Extend it by the defining property in F8. The extension contains every singleton complement, so contains no singleton and is nonprincipal. It is a kappa-complete ultrafilter on uncountable kappa, witnessing measurability.

F3 gives measurable implies weakly compact, and F4 gives weakly compact implies Mahlo. A Mahlo cardinal is inaccessible by the definition used in F4. These complete the displayed chain; all are implications about the same cardinal. If an inaccessible exists, F5 supplies its nonempty transitive V_kappa set model, and F6 gives Con(ZFC) in the ambient theory. This conditional conclusion does not assert that its inaccessible hypothesis is consistent.

For any adjacent arrow, let P and Q be the first-order cardinal properties at its stronger and weaker ends, expressed through the stated set-measure definitions when appropriate. The argument gives a finite ZFC proof of $(\mathrm{\exists }\kappa P(\kappa ))\to (\mathrm{\exists }\kappa Q(\kappa ))$. If the weaker extension of ZFC had a finite refutation, prepend this implication proof and the stronger existence axiom, and replace every use of the weaker existence axiom by its derived conclusion. The result is a finite refutation of the stronger extension. Contraposition gives Con(stronger) implies Con(weaker), and composing these transformations gives the nonadjacent implications. This is a transformation of finite proofs, not an assertion of any Con premise or a converse.

By F2 choose an embedding with critical point $\kappa$. F3 makes $\kappa$ measurable, and F4 makes it inaccessible. In particular $\kappa$ is regular uncountable. F5 gives $\mathrm{\mid }{V}_{\alpha }\mathrm{\mid }<\kappa$ for $\alpha <\kappa$, hence $\mathrm{\mid }{V}_{\kappa }\mathrm{\mid }=\kappa$: a union of $\kappa$ sets of size at most $\kappa$ has size at most $\kappa$, using AC and the cardinal-square theorem F13, while the ordinals below $\kappa$ give the reverse bound. If a critical-$\kappa$ embedding is given, it fixes $V_{\kappa }$ pointwise. Indeed enumerate any $y\in V_{\kappa }$ by $e:\beta \to y$ with $\beta <\kappa$. Then $j(y)=j(e)\mathrm{‘}\mathrm{‘}\beta =j\mathrm{‘}\mathrm{‘}y$, and induction on membership fixes all its members. AC is used for these set enumerations and subsequent cardinal comparisons.

We establish a closure observation. Let $M$ be a transitive class model of ZFC containing all ordinals and closed under ambient $\mu$-sequences, where $\mu$ is infinite. Any ambient set of at most $\mu$ elements of $M$ belongs to $M$: enumerate it on an ordinal at most $\mu$, pad to length $\mu$, use closure, and restrict internally; the empty case is immediate. Moreover $H_{{\mu }^{+}}\subseteq M$, with F10's root-inclusive convention. For $x\in H_{{\mu }^{+}}$, choose a bijection from an ordinal $\beta \le \mu$ to $\mathrm{TC}(\{x\})$, and code membership as a relation on $\beta$. The relation is a set of at most $\mu$ ordinal pairs, hence belongs to $M$ by the preceding observation and the cardinal-square theorem F13. It is well-founded and extensional in $M$, since it is so externally and $M$ is transitive. Its internal collapse is a set and is also an external collapse. F9's uniqueness identifies its distinguished root with $x$. The same argument gives agreement of cardinal comparisons at or below $\mu$ and of hereditary-size classes $H_{{\eta }^{+}}$ for $\eta \le \mu$: all relevant injections, bijections and their graphs belong to $M$.

Here is the exact factor comparison. Suppose $j:V\to M$ is $\theta$-closed, with $\theta \ge \kappa$ infinite cardinal and $j(\kappa )>\theta$. Put $I=P_{\kappa }(\theta )$, $s=j\mathrm{‘}\mathrm{‘}\theta$, and derive $U=\{A\subseteq I:s\in j(A)\}$ by F2. Let $j_0:V\to M_0$ be its collapsed normal fine ultrapower, supplied by F2 and F8. For a set function $f:I\to V$ define $k({\pi }_U([f{]}_U))=j(f)(s)\mathrm{.}$ Equality is preserved and reflected: its coordinate equality set belongs to $U$ precisely when its $j$-image contains $s$, precisely when the two evaluations agree. The same calculation for each fixed formula, using F7 and elementarity of $j$, proves that $k$ is a well-defined elementary injection. Constant functions show $k\circ j_0=j$. All maps are definable with the stated set parameters; restrictions are sets by Replacement. F6 identifies the seed $s_0=j_0\mathrm{‘}\mathrm{‘}\theta$ with the collapsed identity class, so $k(s_0)=s$.

Use AC to fix a set well-order $W$ of $V_{\kappa }$. Define $\mathrm{\ell }:\kappa \to V_{\kappa }$ by the following bounded recursion. At regular uncountable $\gamma <\kappa$, consider cardinals $\gamma \le \eta <\kappa$ and $x\in V_{\kappa }\cap H_{{\eta }^{+}}$ for which no normal fine $\gamma$-complete measure on $P_{\gamma }(\eta )$ has $j_U(\mathrm{\ell }\upharpoonright \gamma )(\gamma )=x$. If there are such pairs, take the least $\eta$ and the $W$-least corresponding $x$ as $\mathrm{\ell }(\gamma )$; otherwise put $\mathrm{\ell }(\gamma )=\mathrm{\varnothing }$. At other $\gamma$ also put empty. This is a uniquely specified set-valued rule on all histories, with an empty fallback for malformed histories. F11 supplies the function. Ultrapower evaluation is a definable set-collapse predicate by F8, so the rule is first-order in set parameters. It does not quantify over arbitrary elementary class embeddings. The explicit cutoff $\eta <\kappa$ and range $V_{\kappa }$ avoid assuming any reflection bound on unbounded failures at smaller stages.

For every $\alpha \le \theta$, the set $s_0\cap j_0(\alpha )=j_0\mathrm{‘}\mathrm{‘}\alpha$ has ordinal order type $\alpha$. Apply $k$ to the definable order-type operation: $k(\alpha )=\mathrm{otp}(s\cap j(\alpha ))=\alpha$. In particular $k$ fixes $\kappa$, including when $\theta =\kappa$. F2 says $M_0$ is $\theta$-closed, so step 1.2 puts $H_{{\theta }^{+}}$ inside $M_0$. Given $y$ in that hereditary class, an enumeration $e:\beta \to y$ with $\beta \le \theta$ belongs to $M_0$ by closure. Since $k$ fixes the indexing ordinal pointwise, $k(y)=k(e)\mathrm{‘}\mathrm{‘}\beta =k\mathrm{‘}\mathrm{‘}y$. Membership induction on $\mathrm{TC}(\{y\})$ now gives $k(y)=y$. Thus the factor fixes every anticipated object of hereditary size at most $\theta$, not just small ordinals.

Fix any $\mathrm{\ell }:\kappa \to V_{\kappa }$ and cardinal $\theta \ge \kappa$, and choose an infinite cardinal $\mu \ge \mathrm{\mid }\mathcal{P}(P_{\kappa }(\theta ))\mathrm{\mid }$. Let $j:V\to M$ be $\mu$-closed with $j(\kappa )>\mu$. For each cardinal $\kappa \le \eta \le \theta$, $M$ and $V$ have exactly the same normal fine $\kappa$-complete measures on $I=P_{\kappa }(\eta )$. Indeed step 1.2 puts every small ordinal subset and hence every element of $I$ in $M$, then puts $I$, all its subsets and all subsets of its power set in $M$. This last assertion uses $\mathrm{\mid }\mathcal{P}(I)\mathrm{\mid }\le \mu$. The sequences of length below $\kappa$ and selector functions used to test completeness and normality also belong to $M$, so those tests agree in both directions. The index and its cardinal comparisons are the same by step 1.2. The same step gives agreement on $H_{{\eta }^{+}}$.

The internal and external evaluations $j_U(\mathrm{\ell })(\kappa )$ agree for each measure in step 2.2. Here are details that avoid identifying internal Scott rank codes with external ones. In a normal fine ultrapower, the function $x\mapsto \mathrm{otp}(x\cap \kappa )$ represents $\kappa$: the normal seed intersected with $j_U(\kappa )$ is $j_U\mathrm{‘}\mathrm{‘}\kappa =\kappa$, and its order type is $\kappa$. Its coordinate values are below $\kappa$. Thus the desired value is the collapse of the class of $r(x)=\mathrm{\ell }(\mathrm{otp}(x\cap \kappa ))$. Put $T=\mathrm{TC}(\{\mathrm{\ell }\})\cup \kappa \cup \{\mathrm{\varnothing }\}$. This is transitive, contains all values of $r$, and has size at most $\kappa$ by step 1.1 and the union bound there. Every function $I\to T$ belongs to $M$ by closure. Their entire collection belongs to $M$ too: writing $\nu =\mathrm{\mid }I\mathrm{\mid }\ge \kappa$, its size is at most ${\kappa }^{\nu }\le (2^{\nu }{)}^{\nu }=2^{\nu }\le \mu$. Form the ordinary set quotient of these functions by coordinate $U$-equivalence. It and its coordinate membership relation are identical internally and externally. The relation is well-founded because a descending sequence would, by countable completeness, yield a descending membership sequence at one coordinate; AC supplies sequence representatives. It is extensional: for unequal function classes, on a large set their values differ, and choosing a member of their symmetric difference gives a distinguishing predecessor; transitivity of $T$ keeps that predecessor in this same quotient. Patching by empty gives every predecessor of every class from a function into $T$. F9's unique set collapse therefore agrees in both models and with the corresponding transitive part of the universe collapse. In particular the two evaluations of $[r]$ agree. This is an assertion about the collapse value, not equality of the two Scott representative codes.

Suppose this $\mathrm{\ell }$ fails F1's requirement. A target set and requested cardinal witnessing failure give a cardinal $\theta \ge \kappa$ dominating both that cardinal and the hereditary size of that set. Any normal fine $\theta$-measure anticipating the set would give an embedding meeting the original request by F2, so there is a failure for some such $\theta$. Choose the least cardinal $\theta \ge \kappa$ for which some $x\in H_{{\theta }^{+}}$ is not anticipated by any normal fine measure on $P_{\kappa }(\theta )$. Choose $\mu$ as in step 2.2 and a $\mu$-supercompact embedding $j:V\to M$ by F2. Step 1.1 gives $j(\mathrm{\ell })\upharpoonright \kappa =\mathrm{\ell }$. Steps 2.2 and 3.1 show that $M$ computes exactly the same least failure $\theta$, including all candidate objects and every smaller cardinal. This is the required anticipation absoluteness, with a bound large enough to contain the measures themselves.

Internally $j(\kappa )$ is inaccessible and $\theta <j(\kappa )$. Every candidate $x\in H_{{\theta }^{+}}^M$ belongs to $V_{j(\kappa )}^M$: its transitive closure has internal size at most $\theta$, and well-founded induction on that closure, using regularity of $j(\kappa )$, bounds the rank of each member below $j(\kappa )$. Consequently the transformed recursion at stage $\kappa$ excludes none of these failure witnesses by its range restriction or cutoff. It selects a failing object $a\in H_{{\theta }^{+}}$ and gives $j(\mathrm{\ell })(\kappa )=a$. The order $j(W)$ need not select any externally preselected witness; the argument only requires that its selected $a$ is a failure, which steps 2.2 and 3.1 make true externally too.

Apply steps 1.3 and 2.1 to this $j$ at $\theta$, deriving a normal fine $\theta$-measure and its factor $j_0$, with $k\circ j_0=j$. The factor fixes $\kappa$ and $a$. Hence $k(j_0(\mathrm{\ell })(\kappa ))=j(\mathrm{\ell })(\kappa )=a=k(a)\mathrm{.}$ Injectivity gives $j_0(\mathrm{\ell })(\kappa )=a$, contradicting the failure asserted in step 5.1. Thus no least failure exists. For arbitrary requested $\lambda \ge \kappa$ and arbitrary set $x$, choose $\theta \ge \lambda$ dominating its hereditary size. The resulting normal fine ultrapower anticipates $x$, moves $\kappa$ above $\theta$, and is $\theta$-closed, hence also $\lambda$-closed by padding sequences. This is precisely F1, including $x=\mathrm{\varnothing }$ and $\lambda =\kappa$. All choice uses are set choices; no Global Choice or inaccessible existence beyond the given supercompact was assumed.

Every element of $\mathbb{B}$ and each of its Boolean operation values lies in $M$, by transitivity. The operation tables and their finite identities agree internally and externally. Since $G$ is nonempty and upward closed, $1\in G$; by its domain $0\mathrm{\notin }G$. If $a,b\in G$, F2 gives a nonzero $r\in G$ below both. The Boolean meet bounds $r$ above and is nonzero, so $a\wedge b\in G$. Thus $G$ is a proper Boolean filter.

Let $A\in M$ be a subset of $\mathbb{B}$ and set $a=\bigvee {}^{M}A$. This is also the least upper bound among the actual elements of $\mathbb{B}$: every candidate upper bound lies in $M$ and the bounding relation quantifies only over the identical sets $A$ and $\mathbb{B}$. Put $D=\{p\mathrm{\ne }0:p\le \mathrm{\neg }a\text{ or }\mathrm{\exists }b\in A(p\le b)\}$, a set in $M$. To prove density, fix $p\mathrm{\ne }0$. If $p\wedge a=0$, then $p\le \mathrm{\neg }a$. If $p\wedge a\mathrm{\ne }0$, some $b\in A$ satisfies $p\wedge b\mathrm{\ne }0$: otherwise every $b\le \mathrm{\neg }p$, making $a\le \mathrm{\neg }p$ by leastness and contradicting this case. The nonzero meet $p\wedge b$ extends $p$ into $D$. Thus $D$ is dense.

Fix $b\in \mathbb{B}$. The set $D_b=\{p\mathrm{\ne }0:p\le b\text{ or }p\le \mathrm{\neg }b\}$ belongs to $M$ by Separation. It is dense: if $p\wedge b\mathrm{\ne }0$, this meet extends $p$ into $D_b$; otherwise distributivity gives $p\le \mathrm{\neg }b$. F1 makes $G$ meet $D_b$, and upward closure implies $b\in G$ or $\mathrm{\neg }b\in G$. Both cannot hold, since their meet is zero. Hence $G$ decides every element and is a proper ultrafilter.

If $a\in G$, meet $D$ using F1. A member of $G$ below $\mathrm{\neg }a$ would contradict properness, so the meeting condition lies below some $b\in A$ and upward closure gives $b\in G$. Conversely $b\in A\cap G$ and $b\le a$ imply $a\in G$. This proves both join directions. If $A=\mathrm{\varnothing }$, $a=0\mathrm{\notin }G$ and $A\cap G=\mathrm{\varnothing }$, as required.

Put $d=\bigwedge {}^{M}A=\mathrm{\neg }\bigvee {}^M\{\mathrm{\neg }b:b\in A\}$. The complemented family belongs to $M$ by Replacement. If $d\in G$, every $b\in A$ is above $d$, so $A\subseteq G$. Conversely suppose $A\subseteq G$ but $d\mathrm{\notin }G$. Step 2.1 puts $\mathrm{\neg }d$ in $G$, and step 2.2 gives some $b\in A$ with $\mathrm{\neg }b\in G$, contradicting $b\in G$. For empty $A$ this says $1\in G$; for singleton $A$ the equivalence is immediate. The only family to which join selection was applied is a member of $M$, so this proves no assertion for arbitrary external subsets of $G$. Every witness was used individually in an existence proof; no family of witnesses was selected.