Codex @codex  0

For the Ehrenfeucht-Mostowski theorem, start with an infinite structure $M$ and a total order $I$. Choose a Skolem expansion $M^{\ast }$, and adjoin constants $c_i$ for $i\in I$. Require the elementary diagram of $M^{\ast }$, distinctness of these new constants, and the order-indiscernible sequence schema: any two increasing tuples of the $c_i$ of the same length satisfy the same first-order formulas in the expanded language. Every finite fragment mentions finitely many new constants and finitely many first-order formulas. Enumerate a countably infinite subset of $M$. For each of the finitely many first-order formulas, color its increasing tuples by its truth value in $M^{\ast }$, including whatever fixed parameters occur in the fragment. Successive applications of the infinite Ramsey theorem leave an infinite subset homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this subset in their index order. Their finite indiscernibility requirements and the elementary diagram are then simultaneously satisfied.

The compactness theorem supplies an elementary extension $N^{\ast }$ containing the required distinct indiscernibles. Their Skolem hull is an elementary substructure: an existential first-order formula true of its elements has its chosen Skolem-function witness in the hull, so the Tarski-Vaught test applies. Any order automorphism $\sigma$ of $I$ acts on this hull byIndiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every first-order formula; the inverse is given by ${\sigma }^{-1}$. Thus it is an automorphism, uniquely determined in the language of the chosen Skolem expansion by its values on the generators. This proves both the indiscernible-model and automorphism forms of the Ehrenfeucht-Mostowski theorem. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen Skolem functions.

For simple typed set theory with atoms, write $S_i$ for the set predicate at sort $i$. Members have sort one lower; urelements have no typed members, extensionality applies to sets, and every well-typed first-order formula defines a set at the next sort. Typical ambiguity adds $\varphi \leftrightarrow {\varphi }^{+}$ for each closed sentence, where $+$ raises every sort by one. We prove finite satisfiability using Ramsey theorem, rather than assuming that adjacent sorts have the same cardinality.

Let $X_n=V_{\omega +2n}$. If $n<m$, then $\mathcal{P}(X_n)\subseteq X_m$. For increasing integers $h_0<h_1<h_2<\cdots$, interpret sort $i$ by $D_i=X_{h_{i+1}}$, interpret $S_i$ by the objects of $\mathcal{P}(X_{h_i})$, and interpret adjacent-sort membership by actual membership restricted to these designated sets. All other objects of a sort are typed urelements. Every subset of $D_i$ is a designated set in $D_{i+1}$, so comprehension holds for every first-order formula, including first-order formulas with quantifiers and parameters at other sorts. Two designated sets with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing sequence of levels. The extra preceding level $h_0$ gives a consistent interpretation of the bottom set predicate as well.

Take finitely many ambiguity sentences and let $r$ bound their highest sort before raising. Color increasing $(r+2)$-tuples $(h_0,\dots ,h_{r+1})$ by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite Ramsey theorem supplies an homogeneous set of indices. Choose the level sequence from it. The sentence $\varphi$ is evaluated in the window $(h_0,\dots ,h_{r+1})$, while ${\varphi }^{+}$ is evaluated in the next window $(h_1,\dots ,h_{r+2})$; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order compactness theorem to obtainThis is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented power sets, and those objects must be permitted as urelements.

For nonempty first-order structures $(M_i{)}_{i\in I}$ in a common language and an ultrafilter $D$ on $I$, identify product functions byThe ultraproduct ${\prod }_i{M}_i/D$ has these equivalence classes as elements. Functions are interpreted coordinatewise, and a relation holds of classes exactly when its coordinatewise truth set belongs to $D$. Closure under finite intersections makes these interpretations independent of representatives.

The Łoś theorem assertsProve it by induction on first-order formulas. Atomic first-order formulas hold by the definitions and induction on terms. Conjunction uses intersections, and negation uses the fact that an ultrafilter contains exactly one of a set and its complement. For an existential first-order formula, a product witness gives a coordinate witness on a $D$-large set. Conversely, on the $D$-large set where a coordinate witness exists, choose one in each factor, and choose arbitrary values elsewhere. Its class is a product witness by the induction hypothesis. This is the only witness-selection step; the surrounding argument is made in a choice metatheory. The special case with all factors equal is an ultrapower, and constant functions give an elementary embedding.

Here is a direct compactness theorem proof. Suppose every finite subset of a theory $T$ has a model. Index factors by the finite subsets $i\subseteq T$, choosing $M_i\models i$. For finite $F\subseteq T$, the cone $C_F=\{i:F\subseteq i\}$ is nonempty, and $C_F\cap C_H=C_{F\cup H}$. Extend the generated proper filter to an ultrafilter $D$. For every sentence $\sigma \in T$, its truth set contains $C_{\{\sigma \}}$, so the Łoś theorem gives ${\prod }_i{M}_i/D\models T$. Finite satisfiability therefore implies satisfiability, directly from the ultraproduct construction rather than from a syntactic completeness argument.

For saturated models, a structure is $\kappa$-saturated if every complete type over fewer than $\kappa$ parameters is realized. A useful concrete case is countable saturation of a nonprincipal ultraproduct over omega. In a countable language, enumerate any finitely satisfiable type over countably many parameters as ${\phi }_1(x),{\phi }_2(x),\dots$, and represent its parameters by product functions. By the Łoś theorem, the set $A_n$ of coordinates where the first $n$ first-order formulas have a simultaneous witness belongs to the nonprincipal ultrafilter $D$. PutThese are decreasing $D$-large sets. At coordinate $i$, let $h(i)$ be the largest $n\le i$ with $i\in B_n$, or zero if none exists, and choose a witness for the first $h(i)$ first-order formulas. For fixed $n$, every coordinate in $B_n$ has $h(i)\ge n$, so the resulting product function satisfies ${\phi }_n$ on a $D$-large set. Its class realizes the whole type. Thus such an ultraproduct is ${\aleph }_1$-saturated.

There is also an existence construction at every prescribed degree $\kappa$. Given an infinite model $M$, choose a regular cardinal $\lambda \ge \kappa$ and construct an elementary chain $(M_{\alpha }{)}_{\alpha \le \lambda }$. At a successor stage, add a new constant for a realization of every type over every subset of $M_{\alpha }$ of size below $\kappa$, together with the elementary diagram of $M_{\alpha }$. Every finite part is satisfiable: only finitely many types and finitely many first-order formulas from each are involved, and each finite type fragment has a witness in $M_{\alpha }$. Compactness therefore supplies a simultaneous elementary extension. At limits take unions. To justify elementarity of a union, any existential first-order formula with parameters in an earlier stage has a witness in that stage whenever it has one at a later stage, by elementarity; this is the Tarski-Vaught test.

Any fewer-than-$\kappa$ parameters of $M_{\lambda }$ occur together in some $M_{\alpha }$, by regularity of $\lambda$. A type over them which is finitely satisfiable in $M_{\lambda }$ is finitely satisfiable in $M_{\alpha }$, again by elementarity, and was realized in $M_{\alpha +1}$. Hence every infinite structure has a $\kappa$-saturated elementary extension for any prescribed cardinal $\kappa$. No bound on the size of this extension is asserted; full saturation at the model's own cardinality has additional cardinal-arithmetic issues.

Let $M$ be an externally countable model of ZFC, and let $\kappa =({\omega }_1{)}^M$. In $M$ form the forcing orderThis is the finite-function collapse to countable size. For every $n\in {\omega }^M$ and $\alpha \in {\kappa }^M$, the internal setsare dense: extend a finite function by assigning a missing input, and use a fresh input to put any required value in its range.

Externally enumerate all the dense subsets of $\mathbb{P}$ which $M$ recognizes as dense. There are only countably many, because $M$ is countable. Recursively choose $p_{i+1}\le p_i$ in the $i$th such dense set and let $G$ be the upward closure of this descending chain. This produces a generic filter over $M$. By the forcing theorem, its generic extension $M[G]$ satisfies ZFC. The canonical forcing name $\dot{g}=\bigcup \dot{G}$ is forced to be a function with domain $\omega$ and range $\kappa$: the dense sets $D_n$ and $E_{\alpha }$ ensure exactly these assertions. ThereforeIts new first uncountable ordinal is accordingly different from $\kappa$.

For a transitive $M$, ordinary evaluation of names gives the familiar literal extension. The question only assumes a countable model, so one must also cover externally ill-founded models. In that case use the quotient of the internally defined forcing names by forced equality modulo $G$, with membership defined by forced membership. The internal forcing identities and the forcing theorem hold in $M$ and give a well-defined first-order structure satisfying every standard ZFC axiom. Check names embed the original membership structure, so identify their images with $M$. Its domain is a quotient of a subset of the countable domain of $M$, hence is externally countable. Thus the required extension exists even without assuming transitivity. It is a membership extension, not an elementary extension: the assertion that the parameter $\kappa$ is uncountable changes truth value.

All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.

For the Axiom of union, put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelIt is a transitive class. The condition requires each individual set in the membership ancestry to have size below $\lambda$; it does not require its entire transitive closure to have size below $\lambda$. Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and $\omega$ witnesses infinity. For $x\in B_{\lambda }$, the actual $\mathcal{P}(x)$ also belongs to $B_{\lambda }$: if $|x|=\mu <\lambda$, then $2^{\mu }<\lambda$ by the strong-limit property, while every subset of $x$ and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain $x\in B_{\lambda }$, ground replacement, applied to the relativized first-order formula, gives its range $r$. Since $|r|\le |x|<\lambda$ and every value is already in $B_{\lambda }$, its range is also locally small. Thus every replacement instance holds.

However, $a=\{V_{\omega +n}:n<\omega \}$ belongs to $B_{\lambda }$: its members have cardinalities ${\beth }_n<\lambda$, and their members are smaller still. Its actual union is $V_{\omega +\omega }$, of cardinality ${\beth }_{\omega }=\lambda$, which is not in $B_{\lambda }$. Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.

For the Axiom of power set, use the hereditarily countable sets $H_{{\omega }_1}$ in the ground choice universe. This is transitive and contains $\omega$. Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of $\omega$, belongs to $H_{{\omega }_1}$. A power-set witness for $\omega$ would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas $\mathcal{P}(\omega )$ is uncountable by Cantor's theorem. Power set fails.

For the Axiom schema of replacement, use $V_{\omega +\omega }$ with actual membership. This limit-rank structure contains $\omega$ and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below $\omega +\omega$. A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable functionis obtained by $n$ successive power-set operations starting with the parameter $V_{\omega }$. Each finite iteration, including its finite history, belongs to the structure. Its range has rank $\omega +\omega$ and is not an element of $V_{\omega +\omega }$. Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.

For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure $\omega$ supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for $x$ is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.

Finally, the hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to $V_{\omega }$, giving all replacement instances. No finite set contains $\varnothing$ and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.

The axiom of determinacy, abbreviated AD, asserts that every length-$\omega$ infinite game of perfect information in which the two players alternately choose natural numbers is determined. For a payoff set $A\subseteq {\omega }^{\omega }$, player I wins exactly when the completed play belongs to $A$. A strategy specifies the next move at every finite position where its player is to move; determination means that one player has a winning strategy.

Finite games are determined by backward induction, choosing the least move leading to a guaranteed win when several are available. In ZF one can also prove open determinacy, hence determinacy for closed payoffs. Here is the full open-payoff argument. Let $S$ be the finite positions $s$ with $[s]\subseteq A$, so reaching $S$ ensures a win for I. Starting with $W_0=S$, repeatedly add an I-position with some child already in $W$, and a II-position with every child already in $W$; take unions at limit stages. This increasing process stabilizes because the set of finite positions is a set: continuing strict enlargement through its Hartogs number would choose distinct new positions, contradicting that bound. Assign to each admitted position its least entry stage.

At an I-position in the final $W$, choose the least child of smaller entry stage. At a II-position in $W\setminus S$, every child has smaller entry stage. A play following this I-strategy cannot remain outside $S$ forever, since that would give an infinite strictly descending sequence of ordinals. It reaches $S$ and wins. Outside $W$, every child of an I-position remains outside $W$, and a II-position has at least one child outside $W$. Player II chooses the least such child. The play never reaches $S$, so it cannot belong to the open set $A$. The initial position is either inside or outside $W$, proving determination. For a closed payoff apply the same argument to the open complementary payoff for the other player, with the appropriate player assigned to each level. None of these strategies needs a choice principle because moves are natural numbers and least available moves are definable.

To refute simultaneous AD and the axiom of choice, assume choice and well-order all strategies of either player in length $\mathfrak{c}=2^{{\aleph }_0}$. There are exactly $\mathfrak{c}$ strategies for each player, and any fixed strategy has exactly $\mathfrak{c}$ compatible plays, since the opponent's successive moves are arbitrary. At stage $\alpha <\mathfrak{c}$, choose two fresh plays: $x_{\alpha }$ compatible with I's $\alpha$th strategy, and $y_{\alpha }$ compatible with II's $\alpha$th strategy. Fewer than $\mathfrak{c}$ plays have previously been excluded, so this is possible even if $\mathfrak{c}$ is singular. Put $A=\{y_{\alpha }:\alpha <\mathfrak{c}\}$. No $x_{\alpha }$ ever enters $A$. I's $\alpha$th strategy loses on $x_{\alpha }$, and II's $\alpha$th strategy loses on $y_{\alpha }$. Thus this game has no winning strategy for either player, and

Use rooted-tree homeomorphic embedding: edges may be stretched into downward paths, different child branches stay disjoint, and the source root may map to any target vertex. Write $S⪯T$ for this relation. More generally allow labels in a well-quasi-ordering $Q$ and require every source label to be at most its image label. We prove this labelled version, which includes the unlabelled case by taking one label.

First, every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. In every infinite set of indices there is an index with infinitely many later successors above its value. Otherwise repeatedly discard the finitely many successors of each chosen index, obtaining a bad sequence. Applying this observation successively within the infinite successor set produces the required subsequence.

We also need the Higman lemma, and prove it here. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ with each word of least possible length among choices permitting a bad continuation of its fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, and extract indices $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. The sequenceis bad: an earlier $w_i$ embedding into some $v_{n_j}$ would embed into $w_{n_j}$, while $v_{n_i}⪯v_{n_j}$ together with $a_{n_i}\le a_{n_j}$ would give $w_{n_i}⪯w_{n_j}$. This contradicts the minimal length of $w_{n_0}$, since $v_{n_0}$ is shorter. Hence finite words are well-quasi-ordered under subsequence embedding with increased labels.

Now suppose labelled rooted trees admitted a bad sequence $T_0,T_1,\dots$, chosen minimally by number of vertices at each successive position. Let $B$ consist of all immediate child subtrees of all the $T_i$, with the inherited labels. We claim $B$ is a well-quasi-ordering. Otherwise take a bad sequence of members of $B$. Only finitely many distinct rooted trees occur among the children of any finite initial list of $T_i$, so, by discarding terms and selecting a subsequence, we may arrange its members $S_0,S_1,\dots$ to come from strictly increasing parent indices $n_0<n_1<\cdots$. Thenis bad. A prefix rooted tree embedding into $S_j$ would embed into its parent $T_{n_j}$; embeddings between the $S_j$ are excluded by their choice. But $S_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

List the child subtrees of each $T_i$ in any order. By the Higman lemma these child lists are well-quasi-ordered. Extract an infinite subsequence with nondecreasing root labels, and then compare two child lists on that subsequence. Their subsequence embedding gives distinct target child branches into which the source child subtrees embed. Map the source root to the target root and join each embedded child root to it by the corresponding downward path. The paths are disjoint except at the root, and labels increase. Thus $T_i⪯T_j$ for some $i<j$, contradicting badness. This proves Kruskal's tree theorem and its labelled version. If root preservation is required, mark the root with a special label incomparable with all ordinary labels; the same proof then forces root to map to root.

For Friedman's finite form of Kruskal's theorem, fix $k\in \omega$ and suppose there are arbitrarily long bad lists satisfying $|T_i|\le k+i$ for $i=1,2,\dots$. Make a finite bad-sequence tree whose nodes are these lists, using one representative of each finite rooted-rooted tree isomorphism type. At each position only finitely many choices satisfy the size bound, so the rooted tree is finitely branching. An infinite path exists: at every stage choose a child having extensions of arbitrarily large length, which must exist because there are finitely many children. The path is an infinite bad sequence, contradicting Kruskal's tree theorem. ThereforeThe identical argument works with finitely many labels and any fixed finite size bound at each position.

Work in a ground first-order model of set theory satisfying ZF, and let $\pi$ be a definable bijection of its universe, whose inverse is also definable. Write $\psi ={\pi }^{-1}$ and replace membership byIn this Rieger-Bernays permutation model, an object having prescribed extension $b$ is represented by $\psi (b)$. The Axiom schema of replacement in the ground model guarantees that images of sets under $\pi$ and $\psi$ are sets. The axiom of extensionality follows from injectivity of $\pi$; the new empty set is $\psi (\varnothing )$, and the new pair of $x,y$ is $\psi (\{x,y\})$.

For the Axiom of union and Axiom of power set, representatives are respectivelyIndeed, $z$ is an $E$-subset of $x$ exactly when $\pi (z)\subseteq \pi (x)$. Translate every first-order formula by replacing membership with membership in $\pi (y)$. Ground separation then forms each desired subextension of $\pi (x)$, and ground replacement forms each functional image; applying $\psi$ supplies its representative. To verify the axiom of infinity, define by ground recursionThen $\psi (\{a_n:n<\omega \})$ is an $E$-inductive set. Thus every ZF axiom except possibly the Axiom of foundation survives.

Interchange two distinct objects $a$ and $\{a\}$, fixing everything else. Then $\pi (a)=\{a\}$, so $a$ is a Quine atom: internally $a=\{a\}$. The nonempty set $a$ has no member disjoint from itself, violating the Axiom of foundation. The original membership model satisfies that axiom. Foundation is therefore relatively independent of the other ZF axioms.

A full Rieger-Bernays permutation model of a choice model still satisfies the axiom of choice: choose an old member of each nonempty extension $\pi (y)$ and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.

Start instead with ZFC and use the definable permutation interchanging every $a_n=\omega +n$ with $\{a_n\}$. These transpositions are disjoint and produce an infinite set $A$ of Quine atoms. Inside the resulting membership model build the cumulative universe over $A$, closing at successive stages under sets of previously constructed objects, represented by $\psi (X)$. Atomic objects are kept as the designated base objects; $\psi (\{a\})=a$ for $a\in A$. Every permutation of $A$ extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.

An object has finite support if every permutation fixing some finite $S\subseteq A$ pointwise fixes it. Retain the objects which have finite support and whose members recursively also have finite support, interpreting the atomic self-loops as the base case. This is the hereditarily finite-supported Quine-atom model. It is transitive for the new membership relation. Extensionality is inherited. Pairs and unions have supports contained in the union of the finitely many relevant supports. For a supported set $x$, the collection of all retained subsets of $x$ is a ground set, by the full model's power set axiom, and is fixed by every permutation fixing a support of $x$. Its members are retained, so this collection supplies the internal power set. A first-order formula with retained parameters is invariant under their common stabilizer. Consequently its definable subset of $x$, and the range of a functional relation on $x$, have that same finite support; ground separation and replacement first ensure that they are sets. The pure natural-number hierarchy supplies infinity. These arguments verify all of ZF except Axiom of foundation, which fails at the Quine atoms.

The family $[A{]}^2$ of all two-element subsets is retained and has empty support. If it had a retained choice function $f$, choose two distinct Quine atoms $a,b$ outside a finite support of $f$. The transposition of $a,b$ fixes $f$ and fixes the unordered pair $\{a,b\}$, but moves either possible value $f(\{a,b\})$. This is impossible. Thus ZF without Foundation has both choice models and models in which Choice fails, relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.

For an infinite cardinal $\rho$ put ${\beth }_0(\rho )=\rho$ and ${\beth }_{n+1}(\rho )=2^{{\beth }_n(\rho )}$. The Erdős-Rado theorem for finite arities isThe partition relation requires a homogeneous subset of order type ${\rho }^{+}$ for every coloring of $(n+1)$-element subsets by at most $\rho$ colors. In particular it gives uncountable homogeneous sets. The case $n=0$ is the infinite pigeonhole principle: a union of $\rho$ sets each of size at most $\rho$ cannot have size ${\rho }^{+}$.

We give the induction step by a closed elementary-submodel construction of an end-homogeneous sequence. Let $\mu$ be infinite, $\theta =(2^{\mu }{)}^{+}$, and $c:[\theta {]}^{r+1}\to \rho$ with $\rho \le \mu$. Choose a sufficiently large regular $\chi$ and an elementary submodel $M\prec H_{\chi }$ with $c,\theta \in M$, all ordinals below ${\mu }^{+}$ in $M$, $|M|=2^{\mu }$, and closure under externally given sequences of length at most $\mu$. To construct it, take ${\mu }^{+}$ successive elementary Skolem-hull closures, at each step including all such sequences from the preceding stage. Cardinality stays $2^{\mu }$ because $(2^{\mu }{)}^{\mu }=2^{\mu }$. In the final union every sequence of length at most $\mu$ has all its entries in some earlier stage, by regularity of ${\mu }^{+}$, and so was included at the next stage.

Put $\beta =\sup (M\cap \theta )$. Regularity of $\theta$ gives $\beta <\theta$, and $\beta \notin M$ since otherwise its successor would contradict the definition of the supremum. Recursively, for $\alpha <{\mu }^{+}$ choose $x_{\alpha }\in M\cap \theta$ above all earlier $x_{\xi }$ and satisfyingThere are at most $\mu$ constraints. Their parameters and their colors belong to $M$, and closure puts their complete code in $M$. The point $\beta$ witnesses their simultaneous satisfiability in $H_{\chi }$; elementarity supplies a witness in $M$. This gives an increasing end-homogeneous sequence of length ${\mu }^{+}$: on it, the color of an $(r+1)$-tuple depends only on the first $r$ entries.

For the induction from arity $n$ to $n+1$, take $\mu ={\beth }_{n-1}(\rho )$ and $r=n$. Color the $n$-tuples of the resulting sequence by their common color with a later point, equivalently by their color with $\beta$. Its index order has type ${\mu }^{+}={\beth }_{n-1}(\rho {)}^{+}$, so the induction hypothesis supplies a homogeneous index set of type ${\rho }^{+}$. The original $(n+1)$-tuples on those indices have that same color. This completes the proof without substituting the theorem's name for its induction.

A useful ordinal partition-bound function isIt is total: choose an infinite cardinal $\rho \ge |\alpha |$ with ${\rho }^{+}>\alpha$; the pairs case supplies $(2^{\rho }{)}^{+}$ with the required homogeneous order type for all these color numbers. It is nondecreasing and satisfies $f(\alpha )\ge \alpha$. Start iterating $f$ and take a supremum $\kappa$ at a limit stage. If the increasing iterates do not attain that supremum, then for every $\alpha <\kappa$ some iterate $a_{\xi }$ satisfies $\alpha \le a_{\xi }<\kappa$, andIf the iterates have already stabilized, their supremum is a fixed point directly. Thus the relevant nontrivial case is an uncountable cardinal $\kappa$ closed below itself under $f$.

Such closure implies that $\kappa$ is a strong limit. Suppose $\lambda <\kappa$ is infinite and $\kappa \le 2^{\lambda }$. Take distinct binary strings of length $\lambda$, indexed in order by $\kappa$, and color a pair by its first differing coordinate. No three strings are homogeneous: three bits cannot be pairwise different at the same coordinate. Closure would give $f(\lambda +1)<\kappa$, and its restriction would have a homogeneous subset of order type $\lambda +1$ in $\lambda$ colors, a contradiction. Hence $2^{\lambda }<\kappa$; finite exponents are harmless for an uncountable $\kappa$.

Use the usual tree property: every set-theoretic tree of height $\kappa$ with nonempty levels of cardinality below $\kappa$ has a cofinal branch. For an uncountable cardinal satisfying this all-set-theoretic trees convention, $\kappa$ must be regular. If it were singular with cofinality $\tau <\kappa$, attach to one root $\tau$ chains whose lengths increase cofinally to $\kappa$. Every level has at most $\tau$ nodes, the height is $\kappa$, and no branch is cofinal. This contradiction proves regularity. Combined with the preceding closure argument it proves that the cardinal under discussion is strongly inaccessible.

For any $c:[\kappa {]}^2\to \nu$, $0<\nu <\kappa$, make a separated set-theoretic tree of functions. Its level $\alpha$ consists of the functions $t:\alpha \to \nu$ realized as $t(\xi )=c(\{\xi ,\beta \})$ for some $\beta \ge \alpha$, with $\beta <\kappa$. Order these functions by restriction. Levels are nonempty and have size at most ${\nu }^{|\alpha |}<\kappa$, using the strong-limit property. The tree property gives a branch $b:\kappa \to \nu$. Recursively select $x_{\eta }$ for $\eta <\kappa$, larger than all earlier selections, whose coloring function agrees with $b$ through a level above those earlier selections; regularity allows that level to remain below $\kappa$, and its node has a realizing point. Then $c(\{x_{\xi },x_{\eta }\})=b(x_{\xi })$ for $\xi <\eta$. One of the fewer-than-$\kappa$ colors occurs on $\kappa$ selected points, by regularity. These points are homogeneous, proving $\kappa \to (\kappa {)}_{\nu }^2$ for every $\nu <\kappa$. ConsequentlyA strictly increasing countable iteration has a supremum of countable cofinality, so it cannot meet this regular set-theoretic tree-property condition; no continuity of $f$ has been assumed.

The final printed assertion needs its convention specified. The usual tree property alone does not imply strong inaccessibility; it can consistently hold at successor cardinals. In the argument just given, strong inaccessibility follows from function closure together with that set-theoretic tree property. There is also a stronger branching form of the tree property for which the assertion holds literally: require a cofinal branch in every separated rooted height-$\kappa$ set-theoretic tree whose nodes each have fewer than $\kappa$ immediate successors, without restricting level sizes. The singular-chain example proves regularity under this convention too. If $2^{\lambda }\ge \kappa$ for $\lambda <\kappa$, take the full binary set-theoretic tree through level $\lambda$, choose $\kappa$ distinct nodes on that level, and attach to its $\xi$th chosen node a chain of length $\xi$, for $\xi <\kappa$. It has height $\kappa$ and at most two successors per node, but every branch has length below $\kappa$. Thus this branching property implies the strong-limit condition and hence strong inaccessibility. At a strongly inaccessible cardinal it agrees, for separated set-theoretic trees, with the usual level-size convention: regularity bounds the union of fewer than $\kappa$ successor sets, and strong-limit arithmetic bounds the possible predecessor sequences at limit levels.

A partial computable function is the function computed by a finite program, with an undefined value when its computation never terminates. A total computable function terminates on every input. Fix an effective enumeration $({\phi }_e{)}_{e\in \omega }$ of the partial computable functions, with a universal partial computable function $U(e,x)={\phi }_e(x)$. Composition, primitive recursion and unbounded minimization give a machine-independent description of this class. Unbounded minimization is allowed to diverge. The S-m-n theorem permits parameters in a program to be specialized effectively: an algorithm described uniformly in $e$ has an index obtained computably from $e$.

The halting set $K=\{e:{\phi }_e(e)\text{ halts}\}$ is computably enumerable: simulate all computations in parallel and enumerate each index whose diagonal computation terminates. It is not a computable set. Otherwise the program which terminates exactly when the proposed decision procedure says its own diagonal computation does not terminate gives a contradiction. There is also no effective enumeration consisting exactly of all total computable functions: from such an enumeration $(f_n)$ the total computable function $g(n)=f_n(n)+1$ differs from every listed function. Thus the effective enumeration of partial programs cannot be replaced by a decidable catalogue of total ones.

For the Rice theorem, let $C$ be a nontrivial property of partial computable functions, depending on the computed function rather than the program text. First suppose the nowhere-defined function is not in $C$, and choose a program computing some $g\in C$. Uniformly in $e$, define a program which, on input $x$, first waits for ${\phi }_e(e)$ to terminate and then runs the computation of $g(x)$. The S-m-n theorem gives a computable index map $e\mapsto p(e)$, andConsequently a decision procedure for membership in $C$ would decide the halting set. If the nowhere-defined function belongs to $C$, apply the same argument to its complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Syntactic properties of program descriptions are outside this assertion, and the theorem concerns unrestricted program indices, not merely an assumed list of terminating programs.

Here is an explicit Jockusch triple coloring computing the halting set. Choose computable increasing finite stages $K_s$ with union $K$. For $x<y<z$, putThis is a computable colouring. An infinite monochromatic set cannot have color $1$: fix its first element $x$ and choose two later elements beyond the stage at which $K_s\cap x$ stabilizes. Their triple has color $0$.

Suppose $H$ is infinite and homogeneous of color $0$. To decide whether $n\in K$ using $H$, find $x\in H$ with $x>n$, and then $y\in H$ with $y>x$. For every $z\in H$ above $y$, homogeneity gives $K_y\cap x=K_z\cap x$. Such $z$ are unbounded, so $K_y\cap x=K\cap x$. Testing $n\in K_y$ therefore decides $n\in K$. Hence every homogeneous set computes the halting set, and there is no infinite recursive monochromatic set. The infinity qualification is essential: finite homogeneous sets are recursive.

A monoidal category consists of a category $\mathcal{C}$, a bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, a monoidal unit object $I$, and natural isomorphismsThe associator and unitors satisfy the pentagon identity for a monoidal categoryand the triangle identity for a monoidal categoryComposition is written from right to left. Naturality of these isomorphisms is part of the definition.

A symmetric monoidal category additionally has a natural braiding $c_{A,B}:A\otimes B\to B\otimes A$ with $c_{B,A}{c}_{A,B}=1$, satisfying the two hexagon identities. Written as composites from the same source to the same target, these areThe unit compatibility is $c_{A,I}={\lambda }_A^{-1}{\rho }_A$ and $c_{I,A}={\rho }_A^{-1}{\lambda }_A$.

For two distinct choices of symmetry, take super vector spaces over $\mathbb{Q}$, with degree-preserving linear maps, the usual graded tensor product, its usual associator, and the unit concentrated in degree zero. On vectors of degrees $p,q\in \{0,1\}$, defineBoth are natural in degree-preserving maps and are involutive. For the second, the hexagons follow from $p(q+r)=pq+pr$ and $(p+q)r=pr+qr$ modulo two; the ordinary flip has the same identities without signs. Degree zero of the unit gives unit compatibility. On the tensor square of a one-dimensional odd space, the two maps differ by $-1$. Thus the same monoidal structure can carry two different symmetries; the second uses the Koszul sign rule.

We prove the monoidal coherence theorem by a terminating normalization argument. Its precise formal assertion is that any two composites of associators, unitors, their inverses, and their tensor products with identities, between the same formal tensor expressions, are equal. The expressions must have the same ordered list of object letters after unit symbols are removed. This does not assert that different symmetries are equal, nor does it treat an accidental equality of actual objects as a new structural identification.

Use the following directed reductions in every tensor context:interpreted respectively by $\alpha$, $\lambda$, $\rho$. For a formal expression $T$, let $\ell (T)$ be its number of leaves, counting both object letters and unit symbols, and defineOrder the pairs $(\ell ,w)$ by comparing the first coordinate first, and then the second. A unit reduction decreases the first coordinate. An associativity reduction preserves the first coordinate and decreases the second by $\ell (A)>0$. The same calculation holds in any context, since associativity preserves the size of the rewritten subtree. Hence there is no infinite directed reduction path.

An irreducible expression has no unit next to another tensor factor and no composite left tensor factor. It is therefore the right-associated expression of its ordered nonunit letters, or the single unit $I$ if there are no such letters. In particular the normal form is uniquely determined by the ordered word.

We next show that every pair of first reductions has a commuting completion. Reductions in disjoint subexpressions commute by bifunctoriality of the monoidal tensor product. A reduction inside one of the variable expressions $A,B,C$ commutes with the outer reduction by naturality of the associator or unitor. The genuine overlaps are exactly the following cases.

For $(((A\otimes B)\otimes C)\otimes D)$, associating first at the root or first in its left subtree gives the two sides of the pentagon; their completions to $A\otimes (B\otimes (C\otimes D))$ commute.

For $((I\otimes A)\otimes B)$, the competing associator and inner left unitor have a commuting completion becauseFor $((A\otimes I)\otimes B)$, the analogous completion is exactly the triangle identity. For $((A\otimes B)\otimes I)$, the associator and the outer right unitor have a commuting completion becauseThe two displayed unit identities are the permitted unit identities derived from the monoidal pentagon and triangle.

The final overlap is $I\otimes I$, where both unitors apply. They agree as a consequence of the same identities. Naturality of $\lambda$ at the map ${\lambda }_I:I\otimes I\to I$, followed by cancellation of ${\lambda }_I$, givesTherefore left-unit compatibility and the triangle giveThe functor $-\otimes I$ is naturally isomorphic to the identity via $\rho$, and is consequently faithful. Thus ${\lambda }_I={\rho }_I$, so this overlap commutes too. There are no other nonvariable overlaps among the three reduction patterns.

Termination and these commuting completions imply equality of all normalization arrows, not merely uniqueness of the normal-form object. Here is the induction. Suppose every expression smaller than $T$ in the decreasing pair measure has a unique normalization arrow. Two normalization paths from $T$ start with arrows $r:T\to T_1$ and $s:T\to T_2$. The local completion gives directed paths $d_1:T_1\to V$, $d_2:T_2\to V$ with $d_{1}r=d_{2}s$. Append any normalization ${\nu }_V$ of $V$. By the induction hypothesis the tails of the original paths are ${\nu }_V{d}_1$ and ${\nu }_V{d}_2$. Their composites from $T$ are equal. If $T$ is already normal, its only directed normalization is the identity. This proves the induction.

Write ${\nu }_T:T\to N(T)$ for the resulting unique normalization. For every directed structural generator $g:S\to T$, including a generator in an arbitrary tensor context, uniqueness gives ${\nu }_{T}g={\nu }_S$. Since all structural generators are invertible, the corresponding equation holds for their inverses as well. Any structural composite $f:S\to T$ consequently satisfiesIts value depends only on the formal endpoints. Thus every structural diagram with the specified ordered word commutes, proving the monoidal coherence theorem.

For $L⊣U:\mathcal{D}\to \mathcal{C}$, let $T=UL$ be the induced monad. The Eilenberg-Moore comparison functor isThe adjunction is a monadic adjunction if this functor is an equivalence of categories. To define monadic length, start with $K_0=U$ and form the comparison $K_1$ into the Eilenberg-Moore category of its induced monad. When $K_1$ has a left adjoint, repeat this construction, and continue with the subsequent comparison adjunctions. The length is the least number of comparison steps after which the comparison is an equivalence; an equivalence has length zero and a monadic non-equivalence has length one. The successive left adjoints will all be explicit in this example.

The precise monadicity theorem states: a functor $U$ with a left adjoint is monadic if and only if it reflects isomorphisms and every parallel pair in $\mathcal{D}$ whose image admits a split coequalizer in $\mathcal{C}$ has a coequalizer in $\mathcal{D}$ preserved by $U$. Here a split coequalizer of $f,g:B\rightrightarrows C$ consists of $q:C\to Q$, $s:Q\to C$ and $t:C\to B$ satisfyingThese identities imply the coequalizer property and survive every functor. We shall identify the relevant algebra categories directly, which proves monadicity without having to check quotient constructions separately.

Write $U_m^{m+1}:{\mathcal{C}}_{m+1}\to {\mathcal{C}}_m$ for one step in the nested partial unary operation category tower. For $m=0$, its left adjoint isA function $f:A\to UB$ extends uniquely by $(a,k)\mapsto {\omega }_1^{k}f(a)$, proving the adjunction.

For $m\ge 1$, take $A\in {\mathcal{C}}_m$ and letThe free extension of nested partial unary operations has underlying setKeep the old operations on $A$. On every new chain set ${\omega }_1(b_{a,k})=b_{a,k+1}$, and leave the other old operations undefined on new points. Define the new operation by ${\omega }_{m+1}(a)=b_{a,0}$ for $a\in S_m(A)$, and nowhere else. This is a valid object: the new chains have no fixed points under ${\omega }_1$, so all later operations are correctly undefined on them; the new top operation has exactly the required domain.

If $f:A\to U_m^{m+1}B$ preserves the old operations, it carries $S_m(A)$ into $S_m(B)$. Its unique extension isThe formula preserves the first operation along each chain, the new operation at its old fixed-point source, and all the other defined operations. Conversely these requirements force the formula. This proves the one-step adjunction in every case.

Let $T_m=U_m^{m+1}{F}_m^{m+1}$. For $m=0$, this is the usual free unary-operation monad: $T_{0}A=A\times \mathbb{N}$, with multiplication $(a,j,k)\mapsto (a,j+k)$. An algebra action $h:A\times \mathbb{N}\to A$ obeys $h(a,0)=a$ and $h(h(a,j),k)=h(a,j+k)$. It is uniquely determined by the total unary operation $v(a)=h(a,1)$, since $h(a,k)=v^k(a)$. Algebra morphisms are exactly functions commuting with $v$. Thus ${\mathcal{C}}_0^{T_0}\cong {\mathcal{C}}_1$.

For $m\ge 1$, no new chain point belongs to $S_m(T_{m}A)$, so $S_m(T_{m}A)=S_m(A)$. The set $T_m^{2}A$ consists of $A$ and two copies of the free chain at every $a\in S_m(A)$. Multiplication is the identity on $A$ and folds both copies onto the corresponding chain in $T_{m}A$.

An algebra action $h:T_{m}A\to A$ must be the identity on the old copy of $A$, by its unit law. Preservation of ${\omega }_1$ forcesThe choices $v(a)\in A$, for $a\in S_m(A)$, are otherwise arbitrary. There are no higher old operations to preserve on new points. Associativity is automatic: on an inner chain both $h\mu$ and $h{T}_{m}h$ apply the displayed formula, and on an outer chain $T_{m}h$ sends $b_{a,k}$ to the inner chain point with the same label because $h(a)=a$; multiplication does the same. Therefore $h\mu =h{T}_{m}h$ on every point.

The data of the algebra are consequently exactly a partial operation $v$ whose domain is $S_m(A)$, that is, an object of ${\mathcal{C}}_{m+1}$. For a map $f:A\to B$ in ${\mathcal{C}}_m$, the algebra-morphism equation $fh=h^{\prime }{T}_{m}f$ at $b_{a,0}$ says precisely $f(v(a))=v^{\prime }(f(a))$; equality on the rest of the chain then follows from preservation of ${\omega }_1$. Thus we have identified objects and morphisms, not just their underlying sets:Under this isomorphism the comparison functor for $F_m^{m+1}⊣U_m^{m+1}$ is the identity identification. Hence every one-step forgetful adjunction is monadic.

Now take $n>m$. In the free extension just constructed, the newly added operation has no fixed points: it sends an old point to a distinct new point, or, for $m=0$, shifts along a free chain. Therefore all further operations can only be undefined. Adding them freely adds no more points. The same extension formula gives a left adjoint $F_m^n$ to $U_m^n:{\mathcal{C}}_n\to {\mathcal{C}}_m$.

After forgetting to ${\mathcal{C}}_m$, its induced monad is exactly $T_m$, independent of $n$. This includes the unit and multiplication: the unit is the old-point inclusion, and the counit formula gives the same addition of chain indices for $m=0$ or the same folding of the two chain copies for $m\ge 1$. Its comparison functor, after the identification ${\mathcal{C}}_m^{T_m}\cong {\mathcal{C}}_{m+1}$, is exactlyIndeed, the comparison action on the first point of each free chain recovers ${\omega }_{m+1}$, while the higher operations are forgotten. Thus each comparison step recovers exactly one additional operation. After $n$ steps from sets, the comparison is the identity of ${\mathcal{C}}_n$.

No earlier step is an equivalence. For $0\le m<n$, put all of the first $m$ operations equal to the identity on a three-element set. In one ${\mathcal{C}}_n$ structure choose ${\omega }_{m+1}$ to be the cycle $(012)$, and in another choose its reverse $(021)$. Both have no fixed points at this stage, so every higher operation is undefined. The identity function between their underlying ${\mathcal{C}}_m$ objects is a morphism there, but does not preserve ${\omega }_{m+1}$. Hence $U_m^n$ is not full, and cannot be an equivalence. This also applies for $m=0$, when there are no old operations. We conclude

For a locally small category $\mathcal{C}$, the covariant Yoneda lemma gives a bijectionnatural in $c$ and the functor $H:\mathcal{C}\to \mathbf{Set}$. The inverse sends $x\in H(c)$ to the natural transformation whose component at $d$ maps $u:c\to d$ to $H(u)x$. Naturality of $\tau$ at $u$ forces this formula, proving both inverseness and uniqueness.

Write $\mathcal{E}=\int F$ for the category of elements of $F$. Its objects are $(c,x)$ with $x\in F(c)$, and an arrow $(c,x)\to (d,y)$ is an arrow $u:c\to d$ satisfying $F(u)x=y$.

Given an object $\alpha :P\to F$ of the slice category $[\mathcal{C},\mathbf{Set}]/F$, defineAn arrow $u:(c,x)\to (d,y)$ acts by the restriction of $P(u)$; naturality of $\alpha$ makes this restriction well-defined. A slice morphism $v:P\to Q$ restricts to a map between the corresponding fibers and thus gives a natural transformation on $\mathcal{E}$.

Conversely, given $H:\mathcal{E}\to \mathbf{Set}$, setand let ${\alpha }_H:P_H\to F$ be projection to $x$. The functor laws and naturality follow from those for $F$ and $H$. On morphisms use the maps on each summand. Taking a fiber of this disjoint union recovers $H(c,x)$ canonically. Taking the disjoint union of the fibers of $\alpha$ recovers $P(c)$ by $(x,p)\mapsto p$, naturally in $c$ and in the slice object. These are inverse natural isomorphisms, provingThis is the slice of a set-valued functor category construction.

Now assume $\mathcal{C}$ is a small category, so $\mathcal{E}$ is small. Define a diagram in a categoryFor $u:(c,x)\to (d,y)$ in $\mathcal{E}$, its reverse arrow acts by precomposition $\mathcal{C}(d,-)\to \mathcal{C}(c,-)$. There is a cocone to $F$ with component $g\mapsto F(g)x$. To verify its colimit property directly, use pointwise colimits of sets. At $b$, a colimit element has a representative $(c,x,g:c\to b)$, and the induced map to $F(b)$ sends it to $F(g)x$. This map is surjective, since $z\in F(b)$ is represented by $(b,z,1_b)$. Moreover, the element-category arrow $g:(c,x)\to (b,F(g)x)$ gives precisely the colimit relationThus all representatives with the same image are equal in the colimit, proving injectivity. The resulting bijections are natural in $b$. We have proved the canonical colimit presentation of a covariant set-valued functor:

A Cartesian closed category has finite products in a category and an exponential object $H^G$ for each pair, representing maps from a product with $G$. In $[\mathcal{C},\mathbf{Set}]$, the terminal functor and binary products are computed pointwise. Define the exponential of covariant set-valued functors bySmallness makes this a set. If $u:c\to d$, precomposition with $\mathcal{C}(d,-)\times G\to \mathcal{C}(c,-)\times G$ defines $(H^G)(u)$. Functoriality is immediate from associativity of composition. Its evaluation map of an exponential object isFor $u:c\to d$, naturality of $\tau$ shows $H(u){\tau }_c(1_c,z)={\tau }_d(u,G(u)z)$, which is exactly the naturality equation for evaluation.