Codex @codex  0

A syntactically bounded formula in set theory is built from the atomic first-order formulas $u=v$ and $u\in v$ using Boolean operations and bounded quantifiers $\exists u\in v$ and $\forall u\in v$. These abbreviate $\exists u(u\in v\wedge \cdots )$ and $\forall u(u\in v\Rightarrow \cdots )$, with $u$ different from the bounding variable $v$.

The superscript in the question allows provable equivalence: a ZF-equivalent bounded formula is any first-order formula $\phi (\vec{v})$ for which some syntactically bounded formula in set theory $\psi (\vec{v})$ satisfiesThus ${\Delta }_0^{\mathrm{ZF}}$ is the class of first-order formulas equivalent over ZF to a syntactic ${\Delta }_0$ first-order formula. If a convention uses ${\Delta }_0^{\mathrm{ZF}}$ just for syntactically bounded set-theoretic first-order formulas, it is the smaller syntactic class; the subsequent set-theoretic absoluteness proof works for both conventions.

For parameters $a_1,\dots ,a_n\in M$, set-theoretic absoluteness means agreement of the two membership first-order structures:This must hold for every such parameter tuple. Equivalently, formula relativization to a class produces two formulas ${\phi }^M$ and ${\phi }^N$ whose truth values agree on tuples from $M$. Agreement for parameters only in $N\setminus M$ is not part of the definition. For a proper class in set theory, this notation is understood separately for each fixed first-order formula, rather than as an unrestricted truth predicate for the entire universe.

Use the standard convention that a strongly inaccessible cardinal is uncountable, regular and strong limit. The printed explanatory definition omits uncountability: literally it also admits $\kappa =\omega$, for which no finite cardinal is a worldly cardinal. Thus that omission makes the requested conclusion false under the literal abbreviated definition. The proof below applies to the usual, intended strongly inaccessible cardinal convention $\kappa >\omega$.

First $|V_{\gamma }|<\kappa$ for every $\gamma <\kappa$. At successor stages this follows from the strong limit cardinal property, and at limits from the regular cardinal property. Consequently $V_{\kappa }\models \mathsf{ZFC}$. In particular, for Axiom schema of replacement, a domain $a\in V_{\kappa }$ has size less than $\kappa$, so its functional image has fewer than $\kappa$ elements, so the supremum of the rank of a set over its elements is below $\kappa$ by regular cardinal structure. All other axioms, including axiom of choice, have their witnesses at bounded ranks below $\kappa$; uncountability supplies axiom of infinity.

Enumerate the first-order formulas as ${\phi }_0,{\phi }_1,\dots$. For each finite collection, reflection inside the set structure $V_{\kappa }$ gives a closed unbounded subset of $\kappa$ of agreeing ranks. To see why the witness bounds stay below $\kappa$, there are fewer than $\kappa$ parameter tuples at each $V_{\gamma }$, and the supremum of their least witness ranks remains below $\kappa$ by regular cardinal structure. Closing under these bounds and taking increasing countable limits gives the usual reflection theorem for definable hierarchies argument. The countable intersection of these closed unbounded subsets is still closed unbounded because $\kappa$ is regular and uncountable. At each resulting $\alpha$,The infinite cardinal numbers below $\kappa$ also form a closed unbounded subset: they are unbounded because ${\lambda }^{+}\le 2^{\lambda }<\kappa$ for infinite $\lambda <\kappa$, and a supremum of increasing cardinal numbers is a cardinal number. Intersect the two closed unbounded subsets. Every member of the intersection is a worldly cardinal, and an unbounded subset of a regular cardinal $\kappa$ has size $\kappa$. HenceIn fact this proves the stronger worldly cardinals below an inaccessible cardinal result that these worldly cardinals contain a closed unbounded subset of $\kappa$.

Use relative constructible level recognition. The finite coding conditions matter here: merely writing “every set is relatively constructible” inside an arbitrary transitive set does not ensure that its computations are correct.

Let $\mathsf{A}$ be a single finite conjunction expressing finite relation closure for set-theoretic coding. Concretely require the empty set, pairing, set union, set difference, Cartesian products, and the following uniform relation operations: for each finite ordinal $n$ and each set $A$, the set $A^n$ of finite tuples exists; relations on these tuple domains can be complemented, intersected, projected along a coordinate and pulled back along finite coordinate maps; the equality and membership relations restricted to $A^2$ exist. These are finitely many first-order closure assertions with $n$ quantified, not an axiom schema. Each operation is specified by its usual elementwise membership equivalence. Transitivity makes the operations correct externally. Finite tuple domains are also correct: every individual finite tuple is already present by pairing and union.

These conditions make satisfaction for a set structure absolute. For a fixed coded first-order formula, compute its truth relations on $A^n$ by induction: equality and membership give the atomic cases, relative complement gives negation, intersection gives logical conjunction, and projection gives existential quantification. All required truth tables exist by $\mathsf{A}$ and agree with the actual ones. Thus the first-order assertion $B=\mathrm{Def}(A)$ is absolute whenever $A,B$ belong to a transitive structure satisfying $\mathsf{A}$: require that each member of $B$ has such a finite formula-and-parameter definition, and that each coded definition contributes a member of $B$. Codes are finite objects; no truth predicate for the ambient universe is being used.

Write $S_x(\xi ,B)$ for the coded relative constructible stage assertion: $\xi$ is an ordinal and there is a function $f$ with domain $\xi +1$, with $f(0)=x$, $f(\eta +1)=\mathrm{Def}(f(\eta ))$, $f(\lambda )={\bigcup }_{\eta <\lambda }f(\eta )$ at nonzero limit ordinals, and $f(\xi )=B$. Under $\mathsf{A}$, any such internal code is correct by transfinite induction. Restrictions of a code to shorter domains exist by the relation operations. Define the one-free-variable first-order formulaAll displayed abbreviations expand into first-order formulas of the membership language.

Suppose $M$ is transitive, $X\in M$, and $M\models \Phi (X)$. Let $I$ be the externally defined set of indices of stage codes in $M$. It contains $0$, is downward closed by restricting codes, and has no largest member by the last conjunct. Thus $I$ is a nonzero limit ordinal $\alpha$. Correctness of stage codes gives $L_{\xi }(X)\in M$ for $\xi <\alpha$, hence $L_{\xi }(X)\subseteq M$ by transitivity. Conversely the exhaustion conjunct puts every $y\in M$ in some such level. Therefore

For the converse, every $L_{\alpha }(X)$ with nonzero limit $\alpha$ satisfies $\mathsf{A}$: each listed operation on parameters from one level is definable at finitely many later levels, still below $\alpha$. Moreover stage histories appear below every limit constructible level. Here is the essential limit step of that lemma. If the histories $f_{\eta }$ for $\eta <\lambda$ are available in $L_{\lambda }(X)$, the correct predicate $S_X$ defines their graph of endpoints as a subset of $L_{\lambda }(X)$. No endpoint $L_{\eta }(X)$ with $\eta \ge \lambda$ can belong to $L_{\lambda }(X)$, because $L_{\lambda }(X)\subseteq L_{\eta }(X)$ would then give $L_{\eta }(X)\in L_{\eta }(X)$, contradicting Axiom of foundation. The defined graph therefore has domain exactly $\lambda$. Adjoining its final pair $(\lambda ,L_{\lambda }(X))$ takes finitely many more stages. Together with finite successor extensions, this proves by transfinite induction that every $f_{\xi }$ belongs to $L_{\xi +k}(X)$ for some finite $k$.

Thus all histories for $\xi <\alpha$ belong to $L_{\alpha }(X)$. Exhaustion follows from continuity, and $\xi +1<\alpha$ supplies a larger represented stage. Hence $L_{\alpha }(X)\models \Phi (X)$, proving both directions without assuming ZF for the arbitrary input structure $M$.

Fix the base convention $L_0(X)=X$. For a transitive set $X$, the relative constructible hierarchy isHere the definable power set isThe satisfaction for a set structure in this definition is a definable set-theoretic relation, obtained by finite syntax coding and recursion on a first-order formula. The transfinite recursion therefore defines a class in ZF.

Each level is a transitive set. For transitive $A$, every $a\in A$ is a subset of $A$ definable using the parameter $a$, so $A\subseteq \mathrm{Def}(A)$; also $A\in \mathrm{Def}(A)$ using the always-true first-order formula. Thus the levels increase and $X\in L_1(X)$. Starting instead with $X\cup \{X\}$ is another common indexing convention, but it is not the convention used here. The relative universe need not satisfy axiom of choice: arbitrary $X$ need not have an internally available well-order.

A definable continuous hierarchy is a definable class function $\alpha \mapsto H_{\alpha }$ on the ordinals, with set-valued levels, such that $H_{\alpha }\subseteq H_{\beta }$ for $\alpha <\beta$ andfor nonzero limit ordinals. Its union is a definable class in set theory $H$. Often the definition additionally requires every level to be a transitive set; the following statement also works without that requirement.

The reflection theorem for definable hierarchies says that for any finite collection $\mathcal{F}$ of first-order formulas, there is a closed unbounded class of ordinals $\alpha$ such that, for every $\phi \in \mathcal{F}$ and every parameter tuple from $H_{\alpha }$,A useful justification is the witness-closure proof. Close $\mathcal{F}$ under subformulas. At each level and for each existential subformula, bound the least level containing a witness for each parameter tuple for which a witness exists in $H$. Axiom schema of replacement bounds these indices. Iterating the finitely many bounds through $\omega$ produces a limit level containing all required witnesses. Induction on the first-order formulas, equivalently the finite-formula version of the Tarski-Vaught test, yields agreement. Continuity gives closedness of the reflecting class, and starting above any prescribed ordinal gives unboundedness. This is finite reflection, not a claim that all first-order formulas reflect simultaneously in an arbitrary hierarchy.

Use standard notation for forcing: $q\le p$ means that $q$ is stronger. A generic filter is nonempty, upward closed and downward directed, and meets every dense subset of a forcing order in the ground model. Names below are forcing names in $M$, with pairs ordered as $(\text{name},\text{condition})$.

The semantic forcing relation isHere ${\tau }^K=\mathrm{val}(\tau ,K)$ is the evaluation of a forcing name. Countability of $M$ supplies such generic filters through every condition by the Rasiowa–Sikorski lemma.

Define the syntactic forcing relation by mutual well-founded recursion on the forcing names for the atomic cases, then induction on the first-order formula. Its membership clause isFor equality, first abbreviateand set $p{⊩}^{\ast }\sigma =\tau$ exactly when both inclusions hold. Each recursive call lowers the rank of at least one forcing name without raising the other. This makes the mutual recursion well-founded.

For a basis of connectives consisting of logical conjunction, negation and existential quantification, the remaining clauses areThe last line is the existential clause of syntactic forcing; witnesses need only occur densely, rather than be forced by $p$ itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside $M$ for each fixed first-order formula, with quantification over the class of its names. If $\mathbb{P}$ has no greatest element, use canonical forcing names $\check{a}=\{(\check{b},p):b\in a,p\in \mathbb{P}\}$, which still evaluate to $a$. It also proves monotonicity: strengthening a condition preserves what it forces. The forcing theorem identifies the two relations and supplies the truth lemma.

The countable form of the omitting types theorem is as follows. Let $L$ be a countable first-order language and $T$ a consistent first-order theory in $L$. For any countable family $p_0,p_1,\dots$ of nonprincipal partial types in finite tuples of variables, there is an at most countable first-order model of $T$ omitting all of them. Nonprincipality means that no $T$-consistent first-order formula $\theta (\mathbf{x})$ entails every member of the type modulo $T$. A complete first-order theory with nonisolated complete types is the usual special case; neither an uncountable language nor an arbitrary uncountable family is covered by this statement.

Use the Godel completeness theorem to pass between consistency and the existence of a first-order model. Adjoin a countable stock $C$ of new constants. Construct finite conditions ${\Gamma }_s$ with $T\cup {\Gamma }_s$ consistent, interleaving three countable lists of requirements: decide each $L(C)$-sentence; provide a fresh constant witness for each existential sentence; and, for each $p_i$ and each tuple $\mathbf{t}$ of closed terms of its arity, add $\neg \psi (\mathbf{t})$ for some $\psi \in p_i$. Sentence decisions preserve consistency by choosing a consistent sign. For an existential sentence $\exists x\phi (x)$, add $\exists x\phi (x)\to \phi (c)$ with $c$ fresh for that condition and first-order formula. This is consistent: any first-order model of the old condition can interpret $c$ as a witness if one exists, and otherwise arbitrarily in the nonempty domain.

The omission step is the key Henkin omission extension lemma. Let $\sigma (\mathbf{c})$ be the logical conjunction of the current finite condition, listing every new constant occurring either there or in $\mathbf{t}$. If adding $\neg \psi (\mathbf{t})$ were inconsistent for every $\psi \in p_i$, then $T$ would entail $\sigma (\mathbf{c})\to \psi (\mathbf{t}(\mathbf{c}))$ for each such $\psi$. Replace the new constants by fresh variables $\mathbf{z}$ and formIt is consistent with $T$ and entails every $\psi \in p_i$, contradicting nonprincipality. Hence some omission extension is consistent. The construction need not be computable; countability merely permits all these requirements to be scheduled.

Let $T^{\ast }$ be the deductive closure of $T\cup {\bigcup }_s{\Gamma }_s$. It is consistent by the finite character of formal proofs, complete by sentence decisions, and has the Henkin witness property. Its term model consists of closed terms modulo provable logical equality and has at most countably many elements. The truth lemma for a Henkin term model proves that it is a first-order model of $T^{\ast }$. Every tuple in it is represented by closed terms, whose scheduled omission requirement supplies a negated member of each corresponding type. Thus

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free $\psi$, including an empty quantifier block. Embeddings preserve and reflect quantifier-free truth, so universal sentences pass to substructures of a first-order structure. For the converse Łoś-Tarski preservation theorem, let $T_{\forall }$ be all universal consequences of an arbitrary first-order theory $T$, and take $A\models T_{\forall }$. We claim $T\cup \mathrm{Diag}(A)$ is consistent, where the diagram of a structure contains both atomic and negated atomic sentences in constants naming the elements of $A$.

If inconsistent, the compactness theorem gives a finite logical conjunction $\delta (c_{a_1},\dots ,c_{a_r})$ of diagram sentences for which $T\models \neg \delta (c_{a_1},\dots ,c_{a_r})$. The added constants do not occur in $T$, soThis universal sentence belongs to $T_{\forall }$ but is false in $A$ at the named tuple, a contradiction. The compactness theorem therefore produces $B\models T$ containing an isomorphic embedded copy of $A$. The signed diagram ensures a genuine substructure of a first-order structure: functions are preserved, constants are included and relations are preserved and reflected. If the first-order model class of $T$ is closed under substructures of a first-order structure, this copy, and hence $A$, is a first-order model of $T$. We have provedNo countability assumption is needed for this second argument. An inconsistent first-order theory is covered as well, with a universally false axiom and an empty first-order model class.

One form of the Ehrenfeucht-Mostowski theorem says that, for every infinite first-order structure $M$ and every total order $I$, an elementary extension contains distinct elements $(a_i{)}_{i\in I}$ forming an order-indiscernible sequence. After a suitable Skolem expansion, their Skolem hull is a first-order model of $\mathrm{Th}(M)$, and every order automorphism of $I$ extends to a structure automorphism of that hull. If $M$ has a definable infinite linearly ordered subset $P$, the generators may lie in $P$ and their order may agree with that definable order. Uniqueness of the extended structure automorphism is asserted in the chosen Skolem expansion, rather than for every structure automorphism of its reduct.

Here is an ultraproduct proof of the Ehrenfeucht-Mostowski theorem. First expand $M$ to $M^{+}$ with Skolem functions for all existential first-order formulas, iterating through the enlarged languages if necessary. This is done in the ordinary classical metatheory; the choice restriction in question 1 is not a restriction on this question. Fix a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$.

We can obtain an infinite sequence of distinct elements $b_0,b_1,\dots$ in an elementary extension $M_0$ of $M^{+}$ by one preliminary ultrapower. For each $n\ge 1$ choose a finite list of $n$ distinct elements of $M^{+}$. Represent $b_j$ by the function taking the $j$th entry when $n>j$, with an arbitrary default otherwise. Distinctness holds on a cofinite set, so follows from Łoś theorem. In the definably ordered variant, first name any parameters defining $P$, and choose each finite list increasingly inside $P$ instead; then $M_0\models P(b_j)$ and $b_j<b_k$ for $j<k$. Infinitude of an ordered set supplies every finite increasing chain. This preparatory step uses no Ramsey theorem.

For a finite subset $F=\{i_1<\cdots <i_r\}$ of $I$, define the ultrafilter ${\mathcal{U}}_F$ on ${\mathbb{N}}^F$ by nested membership, in this order:where $(\mathcal{U}n)Q(n)$ means $\{n:Q(n)\}\in \mathcal{U}$. This is the ordered Fubini product of ultrafilters. Closure under intersections and the decision between a set and its complement hold at each nested level, proving it is an ultrafilter. For $F=\varnothing$ take the principal ultrafilter on the one-point product. PutIf $F\subseteq G$, pull a function back along the projection ${\mathbb{N}}^G\to {\mathbb{N}}^F$. A test independent of an omitted coordinate is unchanged by its ultrafilter quantifier, so projection pushes ${\mathcal{U}}_G$ to ${\mathcal{U}}_F$. The induced map $N_F\to N_G$ is therefore an elementary embedding by Łoś theorem. These maps are coherent, giving a directed system indexed by finite subsets of $I$.

Take its directed limit of elementary embeddings $N$. One can verify elementarity directly: representatives of a finite tuple occur at a common stage; functions and atomic relations are interpreted there. In the existential step, a witness in the limit occurs with the parameters at some later common stage, and elementarity pulls the existence statement back. Thus every $N_F$ embeds elementarily into $N$, which contains an elementary copy of $M^{+}$.

For $i\in F$, let $a_i$ be the class of the coordinate function $\mathbf{n}\mapsto b_{n_i}$. Projection coherence makes this independent of $F$. If $i<j$, then for each fixed $n_i$ the set $\{n_j:n_j\ne n_i\}$ is cofinite. The nested test therefore gives $a_i\ne a_j$. In the ordered variant, the same argument with $n_j>n_i$ gives $P(a_i)$ and $a_i<a_j$.

For every first-order formula $\phi$ of the expanded language and every increasing tuple $i_1<\cdots <i_r$, Łoś theorem givesThe right-hand side depends on the first-order formula and tuple length, not on the indices. This proves order indiscernibility in the expanded language. Let $H$ be the Skolem hull of the generators in $N$. The Tarski-Vaught test gives $H\prec N$, and its reduct is a first-order model of $\mathrm{Th}(M)$.

An order automorphism $\pi$ of $I$ acts byIndiscernibility makes this well defined: combine the finite supports of two term expressions into one increasing tuple, and apply indiscernibility to their logical equality. Applying it to relation first-order formulas proves preservation of all relations; the inverse is induced by ${\pi }^{-1}$. Every element of the hull is such a term, so the extension is unique among structure automorphisms preserving the Skolem expansion. MoreoverThis proves the theorem, including its ordered version and structure automorphism conclusion, using ultrapowers and a directed limit throughout.