A program that accepts exactly any desired finite set, in the right universe

One_small_step_(3598325560)Last year I made a post about the universal program, a Turing machine program $p$ that can in principle compute any desired function, if it is only run inside a suitable model of set theory or arithmetic.  Specifically, there is a program $p$, such that for any function $f:\newcommand\N{\mathbb{N}}\N\to\N$, there is a model $M\models\text{PA}$ — or of $\text{ZFC}$, whatever theory you like — inside of which program $p$ on input $n$ gives output $f(n)$.

This theorem is related to a very interesting theorem of W. Hugh Woodin’s, which says that there is a program $e$ such that $\newcommand\PA{\text{PA}}\PA$ proves $e$ accepts only finitely many inputs, but such that for any finite set $A\subset\N$, there is a model of $\PA$ inside of which program $e$ accepts exactly the elements of $A$. Actually, Woodin’s theorem is a bit stronger than this in a way that I shall explain.

Victoria Gitman gave a very nice talk today on both of these theorems at the special session on Computability theory: Pushing the Boundaries at the AMS sectional meeting here in New York, which happens to be meeting right here in my east midtown neighborhood, a few blocks from my home.

What I realized this morning, while walking over to Vika’s talk, is that there is a very simple proof of the version of Woodin’s theorem stated above.  The idea is closely related to an idea of Vadim Kosoy mentioned in my post last year. In hindsight, I see now that this idea is also essentially present in Woodin’s proof of his theorem, and indeed, I find it probable that Woodin had actually begun with this idea and then modified it in order to get the stronger version of his result that I shall discuss below.

But in the meantime, let me present the simple argument, since I find it to be very clear and the result still very surprising.

Theorem. There is a Turing machine program $e$, such that

  1. $\PA$ proves that $e$ accepts only finitely many inputs.
  2. For any particular finite set $A\subset\N$, there is a model $M\models\PA$ such that inside $M$, the program $e$ accepts all and only the elements of $A$.
  3. Indeed, for any set $A\subset\N$, including infinite sets, there is a model $M\models\PA$ such that inside $M$, program $e$ accepts $n$ if and only if $n\in A$.

Proof.  The program $e$ simply performs the following task:  on any input $n$, search for a proof from $\PA$ of a statement of the form “program $e$ does not accept exactly the elements of $\{n_1,n_2,\ldots,n_k\}$.” Accept nothing until such a proof is found. For the first such proof that is found, accept $n$ if and only if $n$ is one of those $n_i$’s.

In short, the program $e$ searches for a proof that $e$ doesn’t accept exactly a certain finite set, and when such a proof is found, it accepts exactly the elements of this set anyway.

Clearly, $\PA$ proves that program $e$ accepts only a finite set, since either no such proof is ever found, in which case $e$ accepts nothing (and the empty set is finite), or else such a proof is found, in which case $e$ accepts only that particular finite set. So $\PA$ proves that $e$ accepts only finitely many inputs.

But meanwhile, assuming $\PA$ is consistent, then you cannot refute the assertion that program $e$ accepts exactly the elements of some particular finite set $A$, since if you could prove that from $\PA$, then program $e$ actually would accept exactly that set (for the shortest such proof), in which case this would also be provable, contradicting the consistency of $\PA$.

Since you cannot refute any particular finite set as the accepting set for $e$, it follows that it is consistent with $\PA$ that $e$ accepts any particular finite set $A$ that you like. So there is a model of $\PA$ in which $e$ accepts exactly the elements of $A$. This establishes statement (2).

Statement (3) now follows by a simple compactness argument. Namely, for any $A\subset\N$, let $T$ be the theory of $\PA$ together with the assertions that program $e$ accepts $n$, for any particular $n\in A$, and the assertions that program $e$ does not accept $n$, for $n\notin A$. Any finite subtheory of this theory is consistent, by statement (2), and so the whole theory is consistent. Any model of this theory realizes statement (3). QED

One uses the Kleene recursion theorem to show the existence of the program $e$, which makes reference to $e$ in the description of what it does. Although this may look circular, it is a standard technique to use the recursion theorem to eliminate the circularity.

This theorem immediately implies the classical result of Mostowski and Kripke that there is an independent family of $\Pi^0_1$ assertions, since the assertions $n\notin W_e$ are exactly such a family.

The theorem also implies a strengthening of the universal program theorem that I proved last year. Indeed, the two theorems can be realized with the same program!

Theorem. There is a Turing machine program $e$ with the following properties:

  1. $\PA$ proves that $e$ computes a finite function;
  2. For any particular finite partial function $f$ on $\N$, there is a model $M\models\PA$ inside of which program $e$ computes exactly $f$.
  3. For any partial function $f:\N\to\N$, finite or infinite, there is a model $M\models\PA$ inside of which program $e$ on input $n$ computes exactly $f(n)$, meaning that $e$ halts on $n$ if and only if $f(n)\downarrow$ and in this case $\varphi_e(n)=f(n)$.

Proof. The proof of statements (1) and (2) is just as in the earlier theorem. It is clear that $e$ computes a finite function, since either it computes the empty function, if no proof is found, or else it computes the finite function mentioned in the proof. And you cannot refute any particular finite function for $e$, since if you could, it would have exactly that behavior anyway, contradicting $\text{Con}(\PA)$. So statement (2) holds. But meanwhile, we can get statement (3) by a simple compactness argument. Namely, fix $f$ and let $T$ be the theory asserting $\PA$ plus all the assertions either that $\varphi_e(n)\uparrow$, if $n$ is not the domain of $f$, and $\varphi_e(n)=k$, if $f(n)=k$.  Every finite subtheory of this theory is consistent, by statement (2), and so the whole theory is consistent. But any model of this theory exactly fulfills statement (3). QED

Woodin’s proof is more difficult than the arguments I have presented, but I realize now that this extra difficulty is because he is proving an extremely interesting and stronger form of the theorem, as follows.

Theorem. (Woodin) There is a Turing machine program $e$ such that $\PA$ proves $e$ accepts at most a finite set, and for any finite set $A\subset\N$ there is a model $M\models\PA$ inside of which $e$ accepts exactly $A$. And furthermore, in any such $M$ and any finite $B\supset A$, there is an end-extension $M\subset_{end} N\models\PA$, such that in $N$, the program $e$ accepts exactly the elements of $B$.

This is a much more subtle claim, as well as philosophically interesting for the reasons that he dwells on.

The program I described above definitely does not achieve this stronger property, since my program $e$, once it finds the proof that $e$ does not accept exactly $A$, will accept exactly $A$, and this will continue to be true in all further end-extensions of the model, since that proof will continue to be the first one that is found.

Same structure, different truths, Stanford University CSLI, May 2016

This will be a talk for the Workshop on Logic, Rationality, and Intelligent Interaction at the CSLI, Stanford University, May 27-28, 2016.

Abstract. To what extent does a structure determine its theory of truth? I shall discuss several surprising mathematical results illustrating senses in which it does not, for the satisfaction relation of first-order logic is less absolute than one might have expected. Two models of set theory, for example, can have exactly the same natural numbers and the same arithmetic structure $\langle\mathbb{N},+,\cdot,0,1,<\rangle$, yet disagree on what is true in this structure; they have the same arithmetic, but different theories of arithmetic truth; two models of set theory can have the same natural numbers and a computable linear order in common, yet disagree on whether it is a well-order; two models of set theory can have the same natural numbers and the same reals, yet disagree on projective truth; two models of set theory can have a rank initial segment of the universe $\langle V_\delta,{\in}\rangle$ in common, yet disagree about whether it is a model of ZFC. These theorems and others can be proved with elementary classical model-theoretic methods, which I shall explain. Indefinite arithmetic truthOn the basis of these observations, Ruizhi Yang (Fudan University, Shanghai) and I argue that the definiteness of the theory of truth for a structure, even in the case of arithmetic, cannot be seen as arising solely from the definiteness of the structure itself in which that truth resides, but rather is a higher-order ontological commitment.

Slides | Main article: Satisfaction is not absolute | CLSI 2016 | Abstract at CLSI

Every function can be computable!

I’d like to share a simple proof I’ve discovered recently of a surprising fact:  there is a universal algorithm, capable of computing any given function!

Wait, what? What on earth do I mean? Can’t we prove that some functions are not computable?  Yes, of course.

What I mean is that there is a universal algorithm, a Turing machine program capable of computing any desired function, if only one should run the program in the right universe. There is a Turing machine program $p$ with the property that for any function $f:\newcommand\N{\mathbb{N}}\N\to\N$ on the natural numbers, including non-computable functions, there is a model of arithmetic or set theory inside of which the function computed by $p$ agrees exactly with $f$ on all standard finite input. You have to run the program in a different universe in order that it will compute your desired function $f$.
$\newcommand\ZFC{\text{ZFC}}
\newcommand\PA{\text{PA}}
\newcommand\Con{\mathop{\text{Con}}}
\newcommand\proves{\vdash}
\newcommand{\concat}{\mathbin{{}^\smallfrown}}
\newcommand\restrict{\upharpoonright}
$
Theorem There is a Turing machine program $p$, carrying out the specific algorithm described in the proof, such that for any function $f:\N\to\N$, there is a model of arithmetic $M\models\PA$, or indeed a model of set theory $M\models\ZFC$ or more (if consistent), such that the function computed by program $p$ inside $M$ agrees exactly with $f$ on all standard finite input.

Tunnels of Time.jpg

The proof is elementary, relying essentially only on the ideas of the classical proof of the Gödel-Rosser theorem. To briefly review, for any computably axiomatized theory $T$ extending $\PA$, there is a corresponding sentence $\rho$, called the Rosser sentence, which asserts, “for any proof of $\rho$ in $T$, there is a smaller proof of $\neg\rho$.” That is, by smaller, I mean that the Gödel-code of the proof is smaller. One constructs the sentence $\rho$ by a simple application of the Gödel fixed-point lemma, just as one constructs the usual Gödel sentence that asserts its own non-provability. The basic classical facts concerning the Rosser sentence include the following:

  • If $T$ is consistent, then so are both $T+\rho$ and $T+\neg\rho$
  • $\PA+\Con(T)$ proves $\rho$.
  • The theories $T$, $T+\rho$ and $T+\neg\rho$ are equiconsistent.
  • If $T$ is consistent, then $T+\rho$ does not prove $\Con(T)$.

The first statement is the essential assertion of the Gödel-Rosser theorem, and it is easy to prove: if $T$ is consistent and $T\proves\rho$, then the proof would be finite in the meta-theory, and so since $T$ would have to prove that there is a smaller proof of $\neg\rho$, that proof would also be finite in the meta-theory and hence an actual proof, contradicting the consistency of $T$. Similarly, if $T\proves\neg\rho$, then the proof would be finite in the meta-theory, and so $T$ would be able to verify that $\rho$ is true, and so $T\proves\rho$, again contradicting consistency. By internalizing the previous arguments to PA, we see that $\PA+\Con(T)$ will prove that neither $\rho$ nor $\neg\rho$ are provable in $T$, making $\rho$ vacuously true in this case and also establishing $\Con(T+\rho)$ and $\Con(T+\neg\rho)$, for the second and third statements. In particular, $T+\Con(T)\proves\Con(T+\rho)$, which implies that $T+\rho$ does not prove $\Con(T)$ by the incompleteness theorem applied to the theory $T+\rho$, for the fourth statement.

Let’s now proceed to the proof of the theorem. To begin, we construct what I call the Rosser tree over a c.e. theory $T$. Namely, we recursively define theories $R_s$ for each finite binary string $s\in 2^{{<}\omega}$, placing the initial theory $R_{\emptyset}=T$ at the root, and then recursively adding either the Rosser sentence $\rho_s$ for the theory $R_s$ or its negation $\neg\rho_s$ at each stage to form the theories at the next level of the tree.
$$R_{s\concat 1}=R_s+\rho_s$$
$$R_{s\concat 0}=R_s+\neg\rho_s$$
Each theory $R_s$ is therefore a finite extension of $T$ by successively adding the appropriate Rosser sentences or their negations in the pattern described by $s$. If the initial theory $T$ is consistent, then it follows by induction using the Gödel-Rosser theorem that all the theories $R_s$ in the Rosser tree are consistent. Extending our notation to the branches through the tree, if $f\in{}^\omega 2$ is an infinite binary sequence, we let $R_f=\bigcup_n R_{f\upharpoonright n}$ be the union of the theories arising along that branch of the Rosser tree. In this way, we have constructed a perfect set of continuum many distinct consistent theories.

I shall now describe a universal algorithm for the case of computing binary functions. Consider the Rosser tree over the theory $T=\PA+\neg\Con(\PA)$. This is a consistent theory that happens to prove its own inconsistency. By considering the Gödel-codes in order, the algorithm should begin by searching for a proof of the Rosser sentence $\rho_{\emptyset}$ or its negation in the initial theory $R_{\emptyset}$. If such a proof is ever found, then the algorithm outputs $0$ or $1$ on input $0$, respectively, depending on whether it was the Rosser sentence or its negation that was found first, and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory. Then, it starts searching for a proof of the Rosser sentence of that theory or its negation. At each stage in the algorithm, there is a current theory $R_s$, depending on which prior proofs have been found, and the algorithm searches for a proof of $\rho_s$ or $\neg\rho_s$. If found, it outputs $0$ or $1$ accordingly (on input $n=|s|$), and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory.

If $f:\N\to 2=\{0,1\}$ is any binary function on the natural numbers, then let $R_f$ be the theory arising from the corresponding path through the Rosser tree, and let $M\models R_f$ be a model of this theory. I claim that the universal algorithm I just described will compute exactly $f(n)$ on input $n$ inside this model. The thing to notice is that because $\neg\Con(\PA)$ was part of the initial theory, the model $M$ will think that all the theories in the Rosser tree are inconsistent. So the model will have plenty of proofs of every statement and its negation for any theory in the Rosser tree, and so in particular, the function computed by $p$ in $M$ will be a total function. The question is which proofs will come first at each stage, affecting the values of the function. Let $s=f\restrict n$ and notice that $R_s$ is true in $M$. Suppose inductively that the function computed by $p$ has worked correctly below $n$ in $M$, and consider stage $n$ of the procedure. By induction, the current theory will be exactly $R_s$, and the algorithm will be searching for a proof of $\rho_s$ or its negation in $R_s$. Notice that $f(n)=1$ just in case $\rho_s$ is true in $M$, and because of what $\rho_s$ asserts and the fact that $M$ thinks it is provable in $R_s$, it must be that there is a smaller proof of $\neg\rho_s$. So in this case, the algorithm will find the proof of $\neg\rho_s$ first, and therefore, according to the precise instructions of the algorithm, it will output $1$ on input $n$ and add $\rho_s$ (the opposite statement) to the current theory, moving to the theory $R_{s\concat 1}$ in the Rosser tree. Similarly, if $f(n)=0$, then $\neg\rho_s$ will be true in $M$, and the algorithm will therefore first find a proof of $\rho_s$, give output $0$ and add $\neg\rho_s$ to the current theory, moving to $R_{s\concat 0}$. In this way, the algorithm finds the proofs in exactly the right way so as to have $R_{f\restrict n}$ as the current theory at stage $n$ and thereby compute exactly the function $f$, as desired.

Basically, the theory $R_f$ asserts exactly that the proofs will be found in the right order in such a way that program $p$ will exactly compute $f$ on all standard finite input. So every binary function $f$ is computed by the algorithm in any model of the theory $R_f$.

Let me now explain how to extend the result to handle all functions $g:\N\to\N$, rather than only the binary functions as above. The idea is simply to modify the binary universal algorithm in a simple way. Any function $g:\N\to \N$ can be coded with a binary function $f:\N\to 2$ in a canonical way, for example, by having successive blocks of $1$s in $f$, separated by $0$s, with the $n^{\rm th}$ block of size $g(n)$. Let $q$ be the algorithm that runs the binary universal algorithm described above, thereby computing a binary sequence, and then extract from that binary sequence a corresponding function from $\N$ to $\N$ (this may fail, if for example, the binary sequence is finite or if it has only finitely many $0$s). Nevertheless, for any function $g:\N\to \N$ there is a binary function $f:\N\to 2$ coding it in the way we have described, and in any model $M\models R_f$, the binary universal algorithm will compute $f$, causing this adapted algorithm to compute exactly $g$ on all standard finite input, as desired.

Finally, let me describe how to extend the result to work with models of set theory, rather than models of arithmetic. Suppose that $\ZFC^+$ is a consistent c.e. extension of ZFC; perhaps it is ZFC itself, or ZFC plus some large cardinal axioms. Let $T=\ZFC^++\neg\Con(\ZFC^+)$ be a slightly stronger theory, which is also consistent, by the incompleteness theorem. Since $T$ interprets arithmetic, the theory of Rosser sentences applies, and so we may build the corresponding Rosser tree over $T$, and also we may undertake the binary universal algorithm using $T$ as the initial theory. If $f:\N\to 2$ is any binary function, then let $R_f$ be the theory arising on the corresponding branch through the Rosser tree, and suppose $M\models R_f$. This is a model of $\ZFC^+$, which also thinks that $\ZFC^+$ is inconsistent. So again, the universal algorithm will find plenty of proofs in this model, and as before, it will find the proofs in just the right order that the binary universal algorithm will compute exactly the function $f$. From this binary universal algorithm, one may again design an algorithm universal for all functions $g:\N\to\N$, as desired.

One can also get another kind of universality. Namely, there is a program $r$, such that for any finite $s\subset\N$, there is a model $M$ of $\PA$ (or $\ZFC$, etc.) such that inside the model $M$, the program $r$ will enumerate the set $s$ and nothing more. One can obtain such a program $r$ from the program $p$ of the theorem: just let $r$ run the universal binary program $p$ until a double $0$ is produced, and then interprets the finite binary string up to that point as the set $s$ to output.

Let me now also discuss another form of universality.

Corollary
There is a program $p$, such that for any model $M\models\PA+\Con(\PA)$ and any function $f:M\to M$ that is definable in $M$, there is an end-extension of $M$ to a taller model $N\models\PA$ such that in $N$, the function computed by program $p$ agrees exactly with $f$ on input in $M$.

Proof
We simply apply the main theorem inside $M$. The point is that if $M$ thinks $\Con(\PA)$, then it can build what it thinks is the tree of Rosser extensions, and it will think that each step maintains consistency. So the theory $T_f$ that it constructs will be consistent in $M$ and therefore have a model (the Henkin model) definable in $M$, which will therefore be an end-extension of $M$.
QED

This last application has a clear affinity with a theorem of Woodin’s, recently extended by Rasmus Blanck and Ali Enayat. See Victoria Gitman’s posts about her seminar talk on those theorems: Computable processes can produce arbitrary outputs in nonstandard models, continuation.

Alternative proof.  Here is an alternative elegant proof of the theorem based on the comments below of Vadim Kosoy. Let $T$ be any consistent computably axiomatizable theory interpreting PA, such as PA itself or ZFC or what have you. For any Turing machine program $e$, let $q(e)$ be a program carrying out the following procedure: on input $n$, search systematically for a finite function $h:X\to\mathbb{N}$, with $X$ finite and $n\in X$, and for a proof of the statement “program $p$ does not agree with $h$ on all inputs in $X$,” using the function $h$ simply as a list of values for this assertion. For the first such function and proof that is found, if any, give as output the value $h(n)$.

Since the function $e\mapsto q(e)$ is computable, there is by Kleene’s recursion theorem a program $p$ for which $p$ and $f(p)$ compute the same function, and furthermore, $T$ proves this.  So the program $p$ is searching for proofs that $p$ itself does not behave in a certain way, and then it is behaving in that way when such a proof is found.

I claim that the theory $T$ does not actually prove any of those statements, “program $p$ does not agree with $h$ on inputs in $X$,” for any particular finite function $h:X\to\mathbb{N}$. If it did prove such a statement, then for the smallest such function and proof, the output of $p$ would indeed be $h$ on all inputs in $X$, by design. Thus, there would also be a proof that the program did agree with this particular $h$, and so $T$ would prove a contradiction, contrary to our assumption that it was consistent. So $T$ actually proves none of those statements. In particular, the program $p$ computes the empty function in the standard model of arithmetic. But also, for any particular finite function $h:X\to\mathbb{N}$, we may consistently add the assertion “program $p$ agrees with $h$ on inputs in $X$” to $T$, since $T$ did not refute this assertion.

For any function $f:\mathbb{N}\to\mathbb{N}$, let $T_f$ be the theory $T$ together with all assertions of the form “program $p$ halts on input $n$ with value $k$”, for the particular value $k=f(n)$.  I claim that this theory is consistent, for if it is not, then by compactness there would be finitely many of the assertions that enable the inconsistency, and so there would be a finite function $h:X\to\mathbb{N}$, with $h=f\upharpoonright X$, such that $T$ proved the program $p$ does not agree with $h$ on inputs in $X$. But in the previous paragraph, we proved that this doesn’t happen. And so the theory $T_f$ is consistent.

Finally, note that in any model of $T_f$, the program $p$ computes the function $f$ on standard input, because these assertions are exactly made in the theory. QED

Incomparable $\omega_1$-like models of set theory

This is joint work with Gunter Fuchs and Victoria Gitman.

Abstract. We show that the analogues of the Hamkins embedding theorems, proved for the countable models of set theory, do not hold when extended to the uncountable realm of $\omega_1$-like models of set theory. Specifically, under the $\diamondsuit$ hypothesis and suitable consistency assumptions, we show that there is a family of $2^{\omega_1}$ many $\omega_1$-like models of $\text{ZFC}$, all with the same ordinals, that are pairwise incomparable under embeddability; there can be a transitive $\omega_1$-like model of ZFC that does not embed into its own constructible universe; and there can be an $\omega_1$-like model of PA whose structure of hereditarily finite sets is not universal for the $\omega_1$-like models of set theory.

In this article, we consider the question of whether the embedding theorems of my article, Every countable model of set theory embeds into its own constructible universe, which concern the countable models of set theory, might extend to the realm of uncountable models. Specifically, in that paper I had proved that (1) any two countable models of set theory are comparable by embeddability; indeed, (2) one countable model of set theory embeds into another just in case the ordinals of the first order-embed into the ordinals of the second; consequently, (3) every countable model of set theory embeds into its own constructible universe; and furthermore, (4) every countable model of set theory embeds into the hereditarily finite sets $\langle\text{HF},{\in}\rangle^M$ of any nonstandard model of arithmetic $M\models\text{PA}$. The question we consider here is, do the analogous results hold for uncountable models? Our answer is that they do not. Indeed, we shall prove that the corresponding statements do not hold even in the special case of $\omega_1$-like models of set theory, which otherwise among uncountable models often exhibit a special affinity with the countable models. Specifically, we shall construct large families of pairwise incomparable $\omega_1$-like models of set theory, even though they all have the same ordinals; we shall construct $\omega_1$-like models of set theory that do not embed into their own $L$; and we shall construct $\omega_1$-like models of \PA\ that are not universal for all $\omega_1$-like models of set theory.

The embedding theorems are expressed collectively in the theorem below. An embedding of one model $\langle M,{\in^M}\rangle$ of set theory into another $\langle N,{\in^N}\rangle$ is simply a function $j:M\to N$ for which $x\in^My\longleftrightarrow j(x)\in^Nj(y)$, for all $x,y\in M$, and in this case we say that $\langle M,{\in^M}\rangle$ embeds into $\langle N,{\in^N}\rangle$; note by extensionality that every embedding is injective. Thus, an embedding is simply an isomorphism of $\langle M,{\in^M}\rangle$ with its range, which is a submodel of $\langle N,{\in^N}\rangle$. Although this is the usual model-theoretic embedding concept for relational structures, the reader should note that it is a considerably weaker embedding concept than commonly encountered in set theory, because this kind of embedding need not be elementary nor even $\Delta_0$-elementary, although clearly every embedding as just defined is elementary at least for quantifier-free assertions. So we caution the reader not to assume a greater degree of elementarity beyond quantifier-free elementarity for the embeddings appearing in this paper.

Theorem.

1. For any two countable models of set theory $\langle M,\in^M\rangle$ and $\langle N,\in^N\rangle$, one of them embeds into the other.

2. Indeed, such an $\langle M,{\in^M}\rangle$ embeds into $\langle N,{\in^N}\rangle$ if and only if the ordinals of $M$ order-embed into the ordinals of $N$.

3. Consequently, every countable model $\langle M,\in^M\rangle$ of set theory embeds into its own constructible universe $\langle L^M,\in^M\rangle$.

4. Furthermore, every countable model of set theory embeds into the hereditary finite sets $\langle \text{HF},{\in}\rangle^M$ of any nonstandard model of arithmetic $M\models\text{PA}$. Indeed, $\text{HF}^M$ is universal for all countable acyclic binary relations.

One can begin to get an appreciation for the difference in embedding concepts by observing that ZFC proves that there is a nontrivial embedding $j:V\to V$, namely, the embedding recursively defined as follows $$j(y)=\bigl\{\ j(x)\ \mid\ x\in y\ \bigr\}\cup\bigl\{\{\emptyset,y\}\bigr\}.$$

We leave it as a fun exercise to verify that $x\in y\longleftrightarrow j(x)\in j(y)$ for the embedding $j$ defined by this recursion. (See my paper Every countable model of set theory embeds into its own constructible universe; but to give a hint here for the impatient, note that every $j(y)$ is nonempty and also $\emptyset\notin j(y)$; it follows that inside $j(y)$ we may identify the pair $\{\emptyset,y\}\in j(y)$; it follows that $j$ is injective and furthermore, the only way to have $j(x)\in j(y)$ is from $x\in y$.} Contrast this situation with the well-known Kunen inconsistency, which asserts that there can be no nontrivial $\Sigma_1$-elementary embedding $j:V\to V$. Similarly, the same recursive definition applied in $L$ leads to nontrivial embeddings $j:L\to L$, regardless of whether $0^\sharp$ exists. But again, the point is that embeddings are not necessarily even $\Delta_0$-elementary, and the familiar equivalence of the existence of $0^\sharp$ with a nontrivial “embedding” $j:L\to L$ actually requires a $\Delta_0$-elementary embedding.)

We find it interesting to note in contrast to the theorem above that there is no such embedding phenomenon in the the context of the countable models of Peano arithmetic (where an embedding of models of arithmetic is a function preserving all atomic formulas in the language of arithmetic). Perhaps the main reason for this is that embeddings between models of PA are automatically $\Delta_0$-elementary, as a consequence of the MRDP theorem, whereas this is not true for models of set theory, as the example above of the recursively defined embedding $j:V\to V$ shows, since this is an embedding, but it is not $\Delta_0$-elementary, in light of $j(\emptyset)\neq\emptyset$. For countable models of arithmetic $M,N\models\text{PA}$, one can show that there is an embedding $j:M\to N$ if and only if $N$ satisfies the $\Sigma_1$-theory of $M$ and the standard system of $M$ is contained in the standard system of $N$. It follows that there are many instances of incomparability. Meanwhile, it is a consequence of statement (4) that the embedding phenomenon recurs with the countable models of finite set theory $\text{ZFC}^{\neg\infty}$, that is, with $\langle\text{HF},{\in}\rangle^M$ for $M\models\text{PA}$, since all nonstandard such models are universal for all countable acyclic binary relations, and so in the context of countable models of $\text{ZFC}^{\neg\infty}$ there are precisely two bi-embeddability classes, namely, the standard model, which is initial, and the nonstandard countable models, which are universal.

Our main theorems are as follows.

Theorem.

1. If $\diamondsuit$ holds and ZFC is consistent, then there is a family $\mathcal C$ of $2^{\omega_1}$ many pairwise incomparable $\omega_1$-like models of ZFC, meaning that there is no embedding between any two distinct models in $\mathcal C$.

2. The models in statement (1) can be constructed so that their ordinals order-embed into each other and indeed, so that the ordinals of each model is a universal $\omega_1$-like linear order. If ZFC has an $\omega$-model, then the models of statement (1) can be constructed so as to have precisely the same ordinals.

3. If $\diamondsuit$ holds and ZFC is consistent, then there is an $\omega_1$-like model $M\models\text{ZFC}$ and an $\omega_1$-like model $N\models\text{PA}$ such that $M$ does not embed into $\langle\text{HF},{\in}\rangle^N$.

4. If there is a Mahlo cardinal, then in a forcing extension of $L$, there is a transitive $\omega_1$-like model $M\models\text{ZFC}$ that does not embed into its own constructible universe $L^M$.

Note that the size of the family $\mathcal C$ in statement (1) is as large as it could possibly be, given that any two elements in a pairwise incomparable family of structures must be non-isomorphic and there are at most $2^{\omega_1}$ many isomorphism types of $\omega_1$-like models of set theory or indeed of structures of size $\omega_1$ in any first-order finite language. Statement (2) shows that the models of the family $\mathcal C$ serve as $\omega_1$-like counterexamples to the assertion that one model of set theory embeds into another whenever the ordinals of the first order-embed into the ordinals of the second.