Past exam of the mathematics course of the University of Cambridge / 2008 / iii / Paper 27 (Set Theory and Logic)

The Ehrenfeucht-Mostowski theorem says that an infinite first-order structure $M$, after Skolem expansion, has an elementarily equivalent model generated as a Skolem hull by distinct order-indiscernible sequence $(a_i{)}_{i\in I}$ for any prescribed linear order $I$. Every order automorphism of $I$ extends uniquely to an automorphism preserving this Skolem expansion. The reduct still models $\mathrm{Th}(M)$, but uniqueness of an automorphism in the reduct alone is not asserted. Iterate adjoining witness functions through all successively enlarged languages, so every existential formula in the final language has its own Skolem function. Write $M^{\ast }$ for the resulting expanded structure.

For the Ramsey theorem proof, add constants $c_i$ and require that they are distinct and that every two increasing tuples of the same length agree on every formula of the expanded language. Include $\mathrm{Th}(M^{\ast })$. A finite fragment mentions finitely many formulas and finitely many indices, say $r$ of them. Choose distinct $b_n\in M$. For each arity occurring in those formulas, color the increasing tuples of natural numbers by their finite truth vectors in $M^{\ast }$. Repeated applications of the infinite Ramsey theorem give an infinite subset homogeneous for all these finitely many colorings. Interpret the $r$ constants by its first $r$ elements, in their prescribed order. All the fragment's indiscernibility requirements hold. Thus compactness theorem produces a model $N^{\ast }$ of the whole scheme.

Let $H$ be the Skolem hull of the $c_i$. Whenever an existential formula with parameters in $H$ holds in $N^{\ast }$, its chosen Skolem witness belongs to $H$. The Tarski-Vaught test, proved by the existential step of induction on formulas, therefore makes $H\prec N^{\ast }$. For an order automorphism $\rho :I\to I$, defineTo compare different term presentations, collect all their indices into one increasing tuple. Indiscernibility transfers the equality of the terms to the transported tuple, so this map is well defined. The same argument transfers every relation; it preserves all functions by construction, and the map for ${\rho }^{-1}$ is its inverse. Since every hull element is a term in the generators, uniqueness follows.

For a genuinely ultraproduct proof, keep the distinct $b_n$ and choose a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$. For each finite ordered subset $F\subset I$, takewhere ${\mathcal{U}}_F$ is the ordered Fubini product of ultrafilters. Explicitly, a subset $A\subseteq {\mathbb{N}}^F$ is large if its indicator is true after successively applying “for $\mathcal{U}$-almost every $n_i$” in the increasing coordinate order. Projection to any sublist has exactly that sublist's product ultrafilter. Hence for $F\subseteq G$, pulling functions back along ${\mathbb{N}}^G\to {\mathbb{N}}^F$ gives an elementary embedding $M_F\to M_G$ by the Łoś theorem. These embeddings commute. Form their directed limit of elementary embeddings; each finite tuple lies in one stage, so induction on formulas makes the stage embeddings elementary.

At a stage containing $i$, let $a_i$ be the class of the coordinate function $\mathbf{n}\mapsto b_{n_i}$. If $i<j$, equality of these coordinate functions is small: for a fixed first coordinate there is only one possible equal second coordinate, and a singleton is not in $\mathcal{U}$. Thus $a_i\ne a_j$. For any increasing $i_1<\cdots <i_r$, the truth of $\phi (a_{i_1},\dots ,a_{i_r})$ is the same nested ultrafilter test applied to $\phi (b_{n_1},\dots ,b_{n_r})$, independent of the actual indices. This is precisely indiscernibility in the expanded language. Its Skolem hull, and the term-transport construction above, finish the second proof. Both constructions give the required model and the extended index automorphisms.

All consistency assertions here are relative: begin with a model of ZFC, obtainable from a model of ZF by its constructible universe as proved below. First use the Rieger-Bernays permutation model. Let $\pi$ exchange the old empty set with its old singleton and fix every other object, and defineAn old set $b$ is the extension, in the new relation, of ${\pi }^{-1}(b)$. This immediately verifies extensionality and gives explicit representatives for the new empty set, pairs, unions and power sets: the old extensions required are respectively $\varnothing$, $\{a,b\}$, ${\bigcup }_{u\in \pi (a)}\pi (u)$, and $\{{\pi }^{-1}(c):c\subseteq \pi (a)\}$. Translate any formula by replacing membership by $E$; old separation and replacement then give the desired new subsets and functional ranges, whose representatives are obtained by ${\pi }^{-1}$.

For infinity, recursively form the new empty object $e={\pi }^{-1}(\varnothing )$ and successors $s(x)={\pi }^{-1}(\pi (x)\cup \{x\})$. The old replacement axiom collects the sequence $e,s(e),s^2(e),\dots$; the representative of its range is a new inductive set. The old object $q=\varnothing$ has new extension $\pi (q)=\{q\}$, so $qEq$ and its singleton witnesses failure of the Axiom of foundation. Choice survives this full permutation construction: old choice applied to a family of nonempty new extensions selects its members, and new ordered pairs and a representative of their old set give the new choice function. Thus $\mathsf{ZF}-\mathsf{Foundation}+\mathsf{AC}+\neg \mathsf{Foundation}$ is relatively consistent. A well-founded starting model gives the opposite possibility for foundation.

To make choice fail, a symmetry restriction is essential. Here is an explicit pure-set construction with many Quine atoms. Take a countably infinite set $A$ of distinct tagged objects $a_n$. Give $a_n$ the extension $\{a_n\}$. For every subset $S$ of objects already constructed, introduce an object $c(S)$ with extension $S$, except that $c(\{a_n\})$ is defined to be $a_n$ itself. Use a disjoint tag for all other codes $c(S)$, so identical extensions have identical codes and distinct extensions have distinct codes. Iterate this operation transfinitely, taking unions at limits. Each level is an old set, and its subsets are an old set, so this is a definable class construction. Every non-atomic membership edge decreases construction rank. Atomic edges are just the prescribed self-loops. Consequently the resulting structure is extensional, has the required pairs, unions and power sets, and the old replacement axiom bounds ranks of definable functional ranges. Its pure finite ranks supply infinity.

Every permutation of $A$ extends recursively by $c(S)\mapsto c(\sigma S)$. An object is finitely supported if some finite $F\subset A$ has the property that every permutation fixing $F$ pointwise fixes that object. Retain objects all of whose members, and members' members, are finitely supported, with recursion stopping at the atomic self-loops. Call this class $N$, the hereditarily finite-supported Quine-atom model.

We must verify its set axioms, not merely declare it a symmetric model. Empty set, pairs and unions have supports given by finite unions of the supports of their arguments. For separation, a formula with finitely supported parameters and domain $a$ is invariant under permutations fixing the union of those supports; its selected extension is therefore supported, and all its elements already lie in $N$. For power set, take all codes $c(S)$ with $S\subseteq \mathrm{ext}(a)$ and $c(S)\in N$. They form an old set, by separation from the bounded code level. Permutations fixing a support of $a$ permute this entire collection, so its code is supported and belongs to $N$. For replacement, translate the relativized formula to the original universe and use old replacement to collect its unique values. Equivariance gives this range a support from the parameters and domain, and every range element lies in $N$. Infinity uses the pure natural-number construction, fixed by every atom permutation. This proves $N\models \mathsf{ZF}-\mathsf{Foundation}$.

The set $A$ and the collection of its two-element subsets have empty support and belong to $N$. Suppose the latter had a choice function $f\in N$, with finite support $F$. Choose distinct $a,b\in A\setminus F$. The transposition of $a,b$ fixes $F$, hence $f$, and fixes the unordered pair $\{a,b\}$. But it swaps whichever member $f(\{a,b\})$ selects, a contradiction. ThereforeTogether with the full permutation model satisfying choice, this proves independence of choice from ZF without foundation, using the same replacement of atoms by self-membered pure sets. The negated-choice model also fails foundation; this suffices for independence over the foundation-free base.

A partial computable function may return a natural-number output or diverge. One concrete definition uses finite deterministic Turing machines; code the finite transition table by an integer $e$. Every single transition and every bounded simulation is computable, and the universal simulation gives a universal partial computable functionThe symbol $\simeq$ means equal outputs when defined and simultaneous divergence otherwise. A total computable function is a partial computable function defined on every input. Different program codes may compute the same partial function; this distinction between syntax and computed behavior is crucial.

The equivalent recursive description starts with zero, successor and projections and closes under composition and primitive recursion, giving the primitive recursive functions. Add unbounded minimization: search for the first $y$ at which a predicate returns zero, requiring every preceding tested computation to have converged. This gives the partial recursive functions. To see the connection with machines, encode finite configurations and histories. Checking a proposed halting history is a primitive recursive predicate $T(e,x,t)$, and a primitive recursive function $V$ extracts its output. Thus a machine computation has the normal form $V(\mu tT(e,x,t))$. Conversely a machine can implement composition, primitive recursion and this successive search. This proves equivalence of the formal definitions. The Church–Turing thesis identifying them with informal effective calculability is a thesis, not an additional formal theorem used in the proof.

A computably enumerable set is one enumerated by a program, equivalently the domain of a partial computable function. For the forward implication wait until the given input is enumerated; for the reverse implication run all input computations by dovetailing, outputting those that halt. A set is decidable if its characteristic function is total computable. It is decidable exactly when both it and its complement are computably enumerable: dovetail their enumerators and stop when one lists the input.

The S-m-n theorem supplies effective specialization of parameters. Given a code for a program on $(a,x)$, compile the constant $a$ into a wrapper that writes it and then calls that program. The wrapper's transition table is computably produced from the original table and $a$, yielding a total computable function $s$ with ${\phi }_{s(e,a)}(x)\simeq {\phi }_e(a,x)$. This elementary code-construction proof is all the specialization machinery needed below.

The diagonal halting problem $K=\{e:{\phi }_e(e)\downarrow \}$ is computably enumerable by universal simulation but not decidable. If a total decider $h$ existed, the program that halts on $x$ precisely when $h(x)=0$ would have an index $d$. Evaluating it at $d$ gives $d\in K$ exactly when $d\notin K$, a contradiction.

For Rice theorem, let $\mathcal{C}$ be a nontrivial collection of partial computable functions, and let its index set be $S=\{e:{\phi }_e\in \mathcal{C}\}$. Membership must depend only on the computed function, not on its code. Let $\perp$ be the nowhere-defined function. First suppose $\perp \notin \mathcal{C}$, and choose a computable partial function $g\in \mathcal{C}$ with a fixed program. Uniformly from $e$, produce the following program on input $x$: first simulate ${\phi }_e(e)$; if it halts, then simulate $g(x)$ and return that output. Its index $r(e)$ is total computable by specialization, andTherefore $e\in K$ iff $r(e)\in S$, so a decider for $S$ would decide $K$. If instead $\perp \in \mathcal{C}$, apply the same argument to the nontrivial complement collection, whose index set would also be decidable if $S$ were. We concludeFor computably enumerable languages, use the same waiting program before beginning a fixed enumeration, taking the empty language as the bottom object. Properties such as having finite domain, computing a total function or recognizing a particular nontrivial language are therefore undecidable. Purely syntactic properties such as the parity of the code are excluded: they are not extensional. Rice's conclusion is undecidability, not that every such index set must fail to be computably enumerable.

The Godel completeness theorem is strong completeness: for any first-order theory $T$ and sentence $\sigma$,Equivalently every syntactically consistent theory has a model. Work in the ordinary classical metatheory with choice; the language need not be countable. Soundness is induction on a derivation: logical axioms hold under every assignment, modus ponens preserves truth, and the quantifier rule preserves truth when its variable is not free in the assumptions. We prove the nontrivial converse by a Henkin construction.

Start with a consistent $T$ and add a constant if the language has no closed term. Let $L_0$ be this language. At stage $n$, for every existential sentence $\exists x\phi (x)$ of $L_n$, add a fresh constant $c_{\phi }$ and the witness axiomAn axiom of this form is conservative for consistency: if a contradiction followed after adding it, the old theory would prove its negation, hence both $\exists x\phi (x)$ and $\neg \phi (c_{\phi })$. Since the constant is fresh, replace it by a fresh variable and generalize, obtaining $\forall x\neg \phi (x)$, a contradiction. Every finite set of new witness axioms can be handled one at a time, so each stage remains consistent. Their union $T_H$ is consistent because a finite proof uses only finitely many stages.

Well-order the sentences of $L_H={\bigcup }_n{L}_n$. Successively add a sentence if doing so is consistent, and otherwise add its negation. At least one of those two choices preserves consistency: otherwise the deduction theorem would give both its negation and its double negation in the previous theory. At limits take unions. The deductive closure $\Gamma$ of the resulting union is complete and consistent and retains all witness axioms. Every sentence of $L_H$ uses finitely many symbols and belongs to some $L_n$, so its existential witness was added at the next stage. Thus $\Gamma$ has the Henkin witness property even for formulas using the new constants.

Build its term model. The domain consists of closed terms modulo $s\sim t$ iff $\Gamma ⊢s=t$. Equality axioms make this an equivalence relation and a congruence. Interpret functions by forming their corresponding terms, and interpret a relation $R$ by $R([t_1],\dots ,[t_r])$ iff $R(t_1,\dots ,t_r)\in \Gamma$. Congruence makes this independent of representatives.

The truth lemma for a Henkin term model is proved by induction on formulas after substituting closed terms for their free variables. Atomic formulas are the definition. Completeness and consistency of $\Gamma$ give the Boolean steps. For existence, if $\exists x\phi (x,\bar{t})\in \Gamma$, a witness axiom yields a constant $c$ with $\phi (c,\bar{t})\in \Gamma$, and induction supplies a model witness. Conversely every domain element is a term class, so a model witness gives an instance in $\Gamma$, and existential introduction gives the existential sentence. Universality follows by negation and existence. The model therefore satisfies $\Gamma$, hence $T$.

Finally, if $T⊬\sigma$, then $T\cup \{\neg \sigma \}$ is consistent by the deduction theorem and classical logic. Its constructed model is a countermodel to $T\models \sigma$. This proves completeness, with an actual witness model rather than merely a finite-satisfiability assertion.

For nonempty first-order structures $(M_i{)}_{i\in I}$ and an ultrafilter $\mathcal{U}$ on $I$, define the ultraproduct by quotienting the product domain byFunctions are interpreted coordinatewise; a relation holds when its coordinate truth set belongs to the ultrafilter. Closure under finite intersections makes these interpretations independent of representatives. The Łoś theorem asserts, for every formula $\phi$,

Prove it by structural induction. A term evaluates coordinatewise, by induction on its construction, so atomic equality and relations are exactly their defining truth sets. Conjunction uses intersection; negation uses the ultrafilter property that exactly one of a set and its complement belongs to $\mathcal{U}$. These establish all Boolean connectives.

For the existential step put $A=\{i:M_i\models \exists x\psi (x,{\bar{a}}_i)\}$. If an ultraproduct witness $[b]$ exists, induction says $\{i:M_i\models \psi (b_i,{\bar{a}}_i)\}\in \mathcal{U}$, and this set is contained in $A$, so $A\in \mathcal{U}$. Conversely if $A\in \mathcal{U}$, choose a witness $b_i$ at every $i\in A$ and any domain element at the other coordinates. Induction makes $[b]$ a witness. This coordinatewise selection uses choice in the metatheory; nonemptiness of the factors is essential. Universal quantification follows from negation and existence, completing the proof.

For the requested compactness theorem, let $I=[T{]}^{<\omega }$. For each finite $F\subseteq T$, choose $M_F\models F$. For each sentence $\sigma \in T$, its cone $C_{\sigma }=\{F:\sigma \in F\}$ is nonempty, and intersections of finitely many cones contain the finite union of their requirements. These cones generate a proper filter. The ultrafilter lemma extends it to $\mathcal{U}$. The coordinate models satisfying $\sigma$ include $C_{\sigma }$, so the Łoś theorem makes their ultraproduct satisfy $\sigma$. Since this holds for each $\sigma \in T$, the ultraproduct is a model of $T$. No completeness theorem is needed in this second compactness proof.

Here is the first incompleteness theorem in its modern consistency form: every consistent computably enumerable theory $T$ extending Robinson arithmetic is incomplete. The original Gödel sentence proof assumes omega-consistency to obtain both unprovabilities; we give that proof and the strengthening that removes this assumption. We also give the second incompleteness conclusion for theories extending Peano arithmetic.

First arithmetize syntax. Code strings and finite derivations by natural numbers. If the axioms of $T$ are merely computably enumerable, include the finite enumeration certificate for each nonlogical axiom used in a proof. The resulting proof-checking relation ${\mathrm{Prf}}_T(p,q)$ is primitive recursive. Finite strings and computation histories are coded by finite sequences, with bounded local verification of every step; these give arithmetic formulas representing the coding operations. In Robinson arithmetic every true or false instance with fixed numeral inputs is provable with the appropriate sign. Set

The diagonal lemma gives, for any formula $\theta (x)$, a sentence $D$ with $Q⊢D\leftrightarrow \theta (┌D┐)$. To see the construction, let $d(e)$ be the computable syntactic operation substituting the numeral for $e$ into the formula coded by $e$. Form the formula $\delta (x)=\theta (d(x))$, interpreting the displayed coding function through its arithmetic representation, and let $n=┌\delta ┐$. Then $D=\delta (\bar{n})$, and $d(n)=┌D┐$. The representation proves that fixed computation, giving the asserted equivalence.

Apply the diagonal lemma to $\neg {\mathrm{Prov}}_T(x)$, obtainingIf $T⊢G$, an actual finite proof has code $n$, so $Q$ proves its proof-checking instance and $T$ proves ${\mathrm{Prov}}_T(┌G┐)$. The fixed-point equivalence gives its negation, contradicting consistency. Hence $T⊬G$. For each standard numeral $n$, $Q$ proves $\neg {\mathrm{Prf}}_T(\bar{n},┌G┐)$ because there is no such proof. If $T⊢\neg G$, the equivalence gives $T⊢\exists p{\mathrm{Prf}}_T(p,┌G┐)$, contrary to omega-consistency. Thus the original proof gives two unprovabilities under that hypothesis. It also shows that $G$ is true in the standard natural numbers when $T$ is consistent.

For consistency alone use the Rosser sentenceIf $T⊢R$ with code $n$, consistency excludes every proof of $\neg R$. In particular the finitely many codes $q\le n$ all fail their primitive recursive proof tests. Robinson arithmetic verifies those finitely many failures and the actual proof at $n$, and hence proves $\neg R$, a contradiction. If $T⊢\neg R$ with code $m$, consistency excludes every proof of $R$. For $p<m$, Robinson arithmetic verifies all the finitely many failed proof tests. For $p\ge m$, it verifies that $q=m$ is a proof of $\neg R$ with $q\le p$. The elementary arithmetic dichotomy between $p<m$ and $m\le p$ therefore proves the entire displayed condition, hence $R$, again a contradiction. Thus

For the Gödel second incompleteness theorem, now assume $T\supseteq \mathsf{PA}$ and use its ordinary certified proof predicate. PA formalizes proof concatenation and the verification of a coded proof, giving the derivability conditions: if $T⊢A$ then $T⊢{\mathrm{Prov}}_T(┌A┐)$; and inside $T$,The first internal implication is certified by combining two proofs; the second is certified by producing the arithmetic proof that a given finite proof passes its check, with existential introduction. Apply them to $G\to \neg {\mathrm{Prov}}_T(┌G┐)$. From ${\mathrm{Prov}}_T(┌G┐)$, the two internal implications yield provability of both ${\mathrm{Prov}}_T(┌G┐)$ and its negation, and hence provability of $\perp$. ConsequentlyA proof of this consistency sentence in a consistent $T$ would prove $G$, which the first argument excludes. Therefore $\boxed{T⊬\mathrm{Con}(T)}$. This concerns the standard arithmetic consistency sentence and the stated effective, arithmetic hypotheses; it is not a prohibition on proving consistency in a stronger theory.

The constructible hierarchy is $L_0=\varnothing$, $L_{\alpha +1}=\mathrm{Def}(L_{\alpha })$ and $L_{\lambda }={\bigcup }_{\alpha <\lambda }{L}_{\alpha }$ at limits; $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. Definability allows parameters from the current level. Satisfaction for a set-sized level is recursively definable, so this is a definable class construction in ZF. Induction shows its levels are sets, increasing and transitive, and contain every ordinal below their height.

We give the necessary reflection argument to check its full axiom schemes. For any finite collection $\Sigma$ of formulas, close it under subformulas and negation. Starting at any level containing the desired parameters, for every existential subformula and parameter tuple in that level for which a witness in $L$ exists, take the least constructibility stage containing such a witness. These least stages are uniquely definable ordinals; ambient replacement bounds all of them. Enlarge to a level beyond the bound, repeat countably many times, and take the union stage $\beta$. Every existential witness required by a tuple in $L_{\beta }$ is then already in $L_{\beta }$, because the tuple appeared at a previous stage. Induction on the finitely many formulas givesThis uses a truth definition for each fixed finite list, not a truth predicate for the entire ambient universe.

Extensionality and foundation hold in $L$ by transitivity. Pairs and unions of elements of a level are definable subsets of a sufficiently large transitive level. The hereditarily finite sets appear in $L_{\omega }$, and the set of its finite ordinals is definable there, so $\omega \in L$ and infinity holds. For separation on $a\in L$ with parameters in $L$, reflect the relevant formula into a level $L_{\beta }$ containing them and $a$. The desired subset of $a$ is then definable over $L_{\beta }$, so belongs to $L_{\beta +1}$.

For replacement, suppose $L$ says $\phi$ defines a unique value in $L$ for each $x\in a$. The relativization ${\phi }^L$ is an ambient formula. Ambient replacement collects its values, and replacement applied to their least constructibility stages bounds them all in some $L_{\gamma }$. Reflect the formula in a still larger level containing $a$, the parameters and those values. The range is now a definable subset of that level, so lies in $L$. For power set, the ambient set $\mathcal{P}(a)\cap L$ exists by separation. Its members' constructibility stages are bounded, say all members lie in $L_{\gamma }$ with $a\in L_{\gamma }$. Thenis definable over $L_{\gamma }$; transitivity makes the displayed bounded subset condition absolute. Thus this internal power set also belongs to $L$. We have proved $L\models \mathsf{ZF}$.

Finally define its canonical well-order recursively. At a successor stage, code a definition by its formula number and its finite tuple of parameters, ordered by the already constructed well-order of the previous level. Order new elements by their least definition codes, preserving earlier elements first. At a limit take the coherent union, with first-appearance stages providing the primary comparison. Induction makes every level well-ordered and gives a definable class well-order of $L$. Its restriction to any set in $L$ belongs to $L$ by separation, so every such set is internally well-orderable. HenceThe implication is a relative consistency argument, not a proof by ZF of its own consistency.

Now Shepherdson's wall explains the limitation of this method. If $W$ is a transitive inner model containing all ordinals, its constructible levels agree with the ambient ones. At successors both compute definable subsets of the same set-sized structure, with the same finite formulas and parameters; at limits both take the same union. Thus $L^W=L\subseteq W$. In an ambient universe satisfying $V=L$, this forces $W=V$. Therefore a uniform inner-model construction valid in every model of ZF cannot always yield an inner model with $V\ne L$, nor one failing choice or CH: apply the proposed construction in a model of ZF with $V=L$. The construction of $L$ removes nonconstructible sets and proves positive choice consistency; it cannot manufacture the nonconstructible sets needed for those negative results.

Use a relative consistency construction: a model of ZF gives one of ZFC through $L$, and we construct a model of New Foundations with urelements from it. In the language with membership and a unary predicate $S$, NFU requires that atoms have no members, extensionality holds between sets, and every stratified formula has a set extension. A type assignment gives equal variables equal types and raises type by one across membership. We prove the actual comprehension scheme, rather than invoke its consistency by name.

Start with a model $M\models \mathsf{ZFC}$ and Skolemize it. Apply the Ramsey construction from Question 1 to obtain increasing ordinal indiscernibles $(c_i{)}_{i\in \mathbb{Z}}$, all greater than $\omega +\omega$. The finite satisfiability step uses the infinite increasing list $\omega \cdot 3,\omega \cdot 4,\dots$ in the original model. Include the ordinal and ordering requirements in the finite truth colorings. Ramsey and compactness produce the indiscernibles; their Skolem hull $N$ still models ZFC. The index shift gives an external structure automorphism $j$ of $N$ with $j(c_i)=c_{i+1}$. Such a model is necessarily externally ill-founded: $(c_0,c_{-1},c_{-2},\dots )$ is an external descending ordinal sequence. No well-founded-model hypothesis is being smuggled in.

For every integer $i$, let $D_i$ be the external domain consisting of the objects of $N$ belonging internally to $V_{c_i}^N$. At type $i+1$, declare $S_{i+1}(y)$ iff $N$ says $y\subseteq V_{c_i}$. Use membership of $N$ only for flagged targets; an unflagged object has no typed members. A flagged object is a set of the preceding type. Set-extensionality holds since all members of a flagged set lie in $D_i$.

Every typed comprehension instance holds. Translate its finitely many typed quantifiers into quantifiers bounded by the appropriate sets $V_{c_r}^N$. Separation in $N$ gives its extension $A\subseteq V_{c_i}^N$ for the distinguished free variable of type $i$. Since $c_i+1\le c_{i+1}$, this subset is an object of $D_{i+1}$ and satisfies its set predicate. Also $j:D_i\to D_{i+1}$ is bijective and preserves the typed relations and flags. This is the required type-shifting automorphism.

Collapse to the single domain $D_0$ by definingIf $S(y)$, its image $j(y)$ is a subset of $V_{c_0}$, so its entire extension is visible in $D_0$. The flag is necessary: an unflagged object might otherwise have a partial visible extension. Flagged coextensive objects have equal images under $j$, by extensionality in $N$, and hence are equal; atoms have no $E$-members.

Now take a stratified untyped formula $\phi (x,\bar{a})$. Shift its type assignment so that $x$ has type zero, allowing negative integer types for other variables. Send a variable of assigned type $r$ to $j^r$ of its untyped value. Equality is preserved, and membership $uEv$ translates to flagged ordinary membership from type $r$ to type $r+1$. A set predicate translates to its flag at that type. Quantifiers correspond bijectively under $j^r:D_0\to D_r$. Thus induction on the formula gives exact agreement between its untyped truth and this typed translation.

Typed comprehension supplies an object $A\in D_1$, flagged at type one, containing exactly the type-zero solutions. Let $b=j^{-1}(A)\in D_0$. It is flagged at type zero, and for every $x\in D_0$, $xEb$ iff $x\in A$ iff $\phi (x,\bar{a})$. This proves all stratified comprehension, including an empty set and the universal set. We have constructedIf infinity is included in the convention for NFU, the same construction supports it: $\omega$ and its successor graph lie far below $c_{-1}$ and are fixed by $j$, since they are definable without parameters in $N$. The domain of the new set $\omega$ is the old $\omega$, since $j(\omega )=\omega$. An ordered pair in the new membership relation is $j^{-2}$ of the old Kuratowski pair. The old successor graph is fixed as a whole by $j$, so its elements are exactly these recoded pairs $(n,n+1)$ as $n$ ranges over $\omega$. It therefore supplies an actual new successor injection with proper range. This does not assume that $j$ fixes each nonstandard natural number. This is the rank-shifting automorphism construction of NFU; its logical ingredients are precisely the proved indiscernible-model construction and ordinary set separation in the typed domains.

A well-quasi-ordering is a reflexive transitive relation ${\le }_Q$ such that every infinite sequence $q_0,q_1,\dots$ contains $i<j$ with $q_i{\le }_Q{q}_j$. Such a pair is good; a sequence without one is bad. A better-quasi-ordering strengthens this condition from sequences to barrier arrays. A barrier in better-quasi-order theory on an infinite $A\subseteq \mathbb{N}$ is a family $B$ of nonempty finite increasing sequences whose underlying sets are inclusion-incomparable, such that every infinite subset of $A$ has an initial segment in $B$. Write $s◃t$ if both are initial segments of some increasing sequence $u$ and its first-term deletion, respectively. BQO means that every $f:B\to Q$ has $s◃t$ with $f(s){\le }_{Q}f(t)$. Singleton barriers give the WQO condition, so BQO implies WQO. These are the barrier-array conventions explained in the treatment of better-quasi-orders.

The labelled version of Kruskal's tree theorem states that finite rooted trees labelled by a WQO $Q$ are WQO under label-monotone tree embedding. An embedding is an injective vertex map preserving lowest common ancestors and increasing labels. In particular an edge may map to a nonempty path, and the source root may map below the target root. The unlabelled theorem follows by taking one label. We prove the stronger labelled assertion.

We first supply the word lemma needed in the proof. Every sequence in a WQO has an infinite nondecreasing subsequence: color pairs $i<j$ according to whether $q_i\le q_j$ and use Ramsey's theorem; the all-bad homogeneous possibility is excluded by WQO. Suppose finite words over $Q$ had a bad sequence. Choose a minimal bad sequence $w_n$, minimizing length at each stage among choices admitting a bad continuation. No word is empty. Write $w_n=v_n{a}_n$ and choose $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$. The sequencecannot be bad by minimality, since its new word at position $n_0$ is shorter. A good pair within the old prefix was already forbidden. A prefix word embedding in some $v_{n_r}$ embeds in $w_{n_r}$, also forbidden. A good pair $v_{n_r}\le v_{n_s}$ extends by the ordered last letters to $w_{n_r}\le w_{n_s}$, again forbidden. This proves the Higman lemma.

Assume next that labelled trees have a bad sequence. Choose $T_n$ minimally by number of vertices, again among choices admitting a bad continuation. Let $\mathcal{S}$ be the collection of all immediate child subtrees of all $T_n$. We claim it is WQO. If $S_0,S_1,\dots$ were a bad sequence in $\mathcal{S}$, attach to each $S_r$ a parent index $k_r$ with $S_r$ a proper child subtree of $T_{k_r}$. The indices must be unbounded on every tail: bounded indices provide only finitely many actual child subtrees, forcing a repeated tree and hence a good pair. Pass to a subsequence with strictly increasing parent indices $k_0<k_1<\cdots$. Thenis bad. Indeed a prefix tree embedding into $S_r$ also embeds into its host $T_{k_r}$, contrary to the original bad sequence, and the other possible good pairs were excluded already. But $S_0$ is smaller than $T_{k_0}$, contradicting minimality. This proves the claim.

Enumerate each tree's child subtrees in any chosen order. Higman's lemma makes the resulting finite words over $\mathcal{S}$ WQO. Products of two WQOs are WQO: choose a nondecreasing subsequence in the first coordinate and then a good pair in the second. Apply this to each root label and child word. Some $i<j$ has an increasing root label and an embedding of its child word into the other's child word. Map the first root to the second root and use the child-subtree embeddings in the matched distinct branches. Their images lie below distinct children, so their pairwise meets are the second root; within each branch the chosen embeddings preserve meets. This gives an embedding $T_i{⪯}_Q{T}_j$, contradicting badness. Hence Kruskal's theorem holds. If one requires roots to be preserved, label the root with a new label incomparable with all ordinary labels and apply the just-proved labelled version; its unique occurrence forces root preservation.

For Friedman's finite form of Kruskal's theorem, fix $k$. Consider bad finite sequences of unlabelled tree isomorphism types satisfying $|T_i|\le k+i$, with indices starting at one. Put them in a tree ordered by extension. At each position there are only finitely many isomorphism types with the allowed vertex bound, so this tree is finitely branching. If bad sequences had arbitrarily large lengths, the König infinity lemma would give an infinite branch, an infinite bad sequence contradicting Kruskal's theorem. ConsequentlyThe bound is uniform over all such sequences. Quotienting by tree isomorphism types is essential to the finite-branching argument; arbitrary vertex names would give infinitely many codes for the same finite tree. A fixed finite label alphabet can be included with the same argument.

Here “constructive ZF” is understood as full intuitionistic Zermelo–Fraenkel set theory, with power set, full separation, collection and set induction. It is not the predicative theory CZF with restricted separation and subset collection. We construct a negative inner interpretation of classical ZF. Its classical logic belongs to the interpreted universe, not to the ambient intuitionistic universe. A bare double-negation of the ordinary set axioms does not by itself solve the extensionality and power-set difficulties.

Work inside IZF. Let $1=\{0\}$ and regard subsets of $1$ as truth values. For $p\subseteq 1$, put $j(p)=\{0\in 1:\neg \neg (0\in p)\}$. Define the double-negation Boolean algebraMeets are intersections, joins are $j$ of unions, and complement is $\neg p=\{0\in 1:0\notin p\}$. Arbitrary intersections of stable predicates are stable. The laws $\neg \neg \neg P\leftrightarrow \neg P$ and $\neg \neg (P\vee \neg P)$ give complementation, and distributing a stable conjunction through a regularized disjunction gives distributivity. Thus $B$ is a complete Boolean algebra, constructively. In particular $p{\vee }_B\neg p=1$, even when their ordinary union is not known to be $1$.

Construct a class $W$ of Boolean-valued names. A name has a set of immediate subnames and a coefficient in $B$ on each; the subname relation is inductively well-founded. More concretely, take set-sized rooted-tree codes with Boolean labels on their edges, requiring that every progressive subset of their nodes contains every node. A subset is progressive when containing all children of a node implies containing that node. This set-quantified condition is definable using power set and supplies induction for each formula by separation. On these trees recursively code each root by the function assigning its children's coded names their edge coefficients; repeated equal codes can be combined by joining their coefficients. The class of these codes is definable by the existence of such a well-founded construction tree. Every set-indexed family of names with coefficients produces another name by adjoining a new root. Collection gathers a set of construction trees witnessing the given subnames, and gluing all these witnesses under the new root avoids choosing one witness tree for each subname; repetitions have identical codes and coefficients. Well-founded recursion on these trees collects compatible partial evaluations by collection; uniqueness identifies all overlapping evaluations, so no selection of witnesses is required. Double induction gives the corresponding recursion on pairs of trees. This avoids assuming a classical linear ordering of all constructive ordinals.

For names $a,b$, define valued membership and equality simultaneously:Here $p\Rightarrow q=\neg p{\vee }_{B}q$. Each recursive call replaces at least one argument by an immediate subname, so well-founded double recursion applies. Induction proves reflexivity, symmetry and transitivity of valued equality and its substitution laws. For example the diagonal term in the membership join gives $a(u)\le [[u\in a]]$, establishing reflexivity; expanding joins and using distributivity gives transitivity and substitution at the next step.

Interpret logical connectives by the Boolean operations, and quantifiers by meets and joins over names. Although $W$ is a class, the values being joined form a subset of the set $B$: for each fixed formula, full separation forms $\{p\in B:\exists a\in W(p=[[\phi (a)]])\}$. This defines each fixed formula's truth value inductively. It does not give a uniform truth predicate for all formulas of the ambient universe. Substitution and the complete Boolean algebra laws verify the classical logical rules, including excluded middle. We now verify the set axioms with explicit names.

The empty-domain name is empty. The name with domain $\{a,b\}$ and coefficient $1$ on both is a pair, since its membership value is $[[x=a]]{\vee }_B[[x=b]]$. For union of $a$, use domain ${\bigcup }_{u\in \mathrm{dom}a}\mathrm{dom}u$, with coefficient at $v$ equal to ${\bigvee }_{u}a(u)\wedge u(v)$, taking missing coefficients to be zero. The membership definition distributes to the required existential membership condition. Extensionality follows from the definition of valued equality: agreeing on the membership value of every name in particular implies both displayed inclusion conditions.

For separation, keep the domain of $a$ and replace its coefficient at $u$ by $a(u)\wedge [[\phi (u)]]$. Substitution makes membership in the resulting name equal to $[[x\in a]]\wedge [[\phi (x)]]$. For power set, write $d=\mathrm{dom}a$. Every function $h:d\to B$ gives a name $a_h$ with coefficients $a(u)\wedge h(u)$. The functions form the set $B^d$, so collect all $a_h$ as a domain with coefficient $1$. Each is a valued subset of $a$. Conversely, for an arbitrary name $c$, put $h(u)=[[u\in c]]$. If $t=[[c\subseteq a]]$, the membership and substitution formulas giveThus, to the full extent that $c$ is a subset of $a$, it belongs to the constructed power-set name. This proves the full power-set axiom without treating every external subset of a name as an internal subset.

The subtle point is collection for Boolean-valued names. For a fixed formula $\phi (u,v)$ form by full separation the setEvery pair in $S$ has a witness name. The ambient axiom schema of collection supplies a set $C$ of witness names covering all these pairs; separation discards any non-name elements. Make a name $b$ with domain $C$ and all coefficients $1$. For each $u\in d$, every value $a(u)\wedge [[\phi (u,v)]]$ occurring with an arbitrary name $v$ is itself a permissible $p$ in $S$. Its collected witness $w\in C$ has value at least $p$. HenceIf $t=[[\forall x\in a\exists y\phi (x,y)]]$, this inequality says $t\wedge a(u)$ is covered by the witnesses in $b$ for every $u$. The bounded universal truth formula therefore gives $t\le [[\forall x\in a\exists y\in b\phi (x,y)]]$. This is exactly the collection axiom's implication at value $1$. It also yields replacement under a uniqueness hypothesis. We collected all Boolean portions of the existential truth; no choice of a single top-valued witness was assumed.

For infinity, form the canonical names $\check{n}$ recursively, with domain $\{\check{m}:m<n\}$ and coefficients $1$, and the name $\check{\omega }$ with all $\check{n}$ in its domain. It is inductive. For set induction, let $p$ be the value of $\forall x[(\forall y\in x\psi (y))\to \psi (x)]$. Induction on the construction of a name $a$, using the bounded universal formula, gives $p\le [[\psi (a)]]$ from the same inequalities for all its subnames. Consequently $p\le [[\forall x\psi (x)]]$. Thus set induction has value $1$, and classical logic in the interpreted universe converts it to the usual foundation axiom.

We have proved all axioms of classical ZF in the Boolean-valued inner universe over intuitionistic set theory, with bottom distinct from top. Any finite classical proof of contradiction would translate, instance by instance, to an intuitionistic proof that $0=1$ in $B$, an ambient contradiction. ThereforeConversely classical ZF proves the intuitionistic set axioms and allows their logical rules, so the consistency strengths agree. This is a proof-translation argument, not an assertion that IZF proves its own consistency. The valued construction is an inner interpretation of the same negative-model kind as the stable-set approach. Closing arbitrary sets under the unbounded predicate $\neg \neg (x\in a)$ would require an additional double-complement axiom; the bounded truth-value construction above avoids that assumption. The distinction is discussed in the study of double complement; the treatment of intuitionistic valued models gives the broader semantic setting.

An ultrapower $A^I/\mathcal{U}$ comes with its diagonal elementary embedding $a\mapsto [i\mapsto a]$, by the Łoś theorem. A model-theoretic ultralimit is the direct limit of successive ultrapowers along these diagonal embeddings, with elementary unions at limit stages. It is not a topological ultrafilter limit. We prove the needed embedding lemma with parameters and then build the isomorphism.

If $A\equiv B$, name every element $b\in B$ by a constant $c_b$ and let $D(B)$ be its elementary diagram of a structure: all sentences true in this fully named structure. For each finite $F\subseteq D(B)$, the conjunction mentions finitely many constants. Its existential closure in the original language is true in $B$, hence in $A$. Choose an interpretation of those constants in $A$ making $F$ true, and give unmentioned constants arbitrary values. Index these interpretations by $I=[D(B){]}^{<\omega }$. Extend the filter of finite-diagram cones to an ultrafilter $\mathcal{U}$.

Map each $b$ to the class of its coordinate interpretations. Every diagram formula holds on the cone containing it, so the Łoś theorem says this map preserves every formula, including negated equalities between distinct named elements. It is therefore an elementary embeddingThis is the Frayne embedding lemma. Its relative version is crucial: if $A\prec C$, interpret all constants naming elements of $A$ constantly by those same elements. Every finite fragment of the diagram of $C$ with these fixed parameters is realized in $A$, since its existential closure with parameters from $A$ is true in $C$ and elementarity transfers it to $A$. The same construction embeds $C$ into an ultrapower of $A$ while extending exactly the diagonal embedding of $A$.

Now start with $A\equiv B$. Embed $B$ into an ultrapower $A_1$ of $A$. Apply the relative lemma to $B\prec A_1$ to embed $A_1$ into an ultrapower $B_1$ of $B$, extending the diagonal map on $B$. Apply it to $A_1\prec B_1$ to embed $B_1$ into an ultrapower $A_2$ of $A_1$, extending the diagonal map on $A_1$. Continue alternately. Replace structures by isomorphic copies to turn these elementary embeddings into inclusions; the commuting identities supplied by the relative lemma giveIn this common chain the map $A_n\to A_{n+1}$ is its ultrapower diagonal, and so is $B_n\to B_{n+1}$. The initial $A\to A_1$ is also diagonal. The union of the $A$-stages and the union of the $B$-stages are cofinal unions of the same chain, hence are the same structure after these coherent identifications. The elementary chain theorem follows by induction on formulas, with every finite tuple and every existential witness lying in some sufficiently late stage. It shows this union is elementary over all its stages. Thus the two constructed ultralimits are isomorphic.

Conversely every successive ultrapower and elementary union preserves the original complete theory. If ultralimits of $A$ and $B$ are isomorphic, they satisfy the same sentences, and their elementary embeddings of the original structures give $A\equiv B$. ThereforeThis proves Frayne theorem by an explicit alternating construction; it does not assume the stronger theorem about isomorphic single ultrapowers or any cardinal-arithmetic hypothesis.