The Kunen inconsistency and definable classes

There is a tension between (1) interpreting proper class talk in set theory as talk about first-order formulas and satisfaction; and (2) taking it to be an interesting and non-trivial result that there is no (non-trivial) elementary embedding from V into V and/or taking it to be an open question whether there can be such an e.e. in the absence of choice. Basically, there is a very simple proof that there can be no definable e.e. from V into V (see Suzuki (1999)).

This tension was recently highlighted by Hamkins, Kirmayer, and Perlmutter (2012) (and pointed out here and here). There, the resolution was to give up on (1), since accepting it "does not convey the full power of the [Kunen's] theorem" (p. 1873). But this is perhaps the only place I've seen this issue addressed. For instance, Kanamori seems to hold both (1) and (2) in The Higher Infinite: "By “class” in the ZFC context is meant definable class,... $x \in M$ is merely [a] facon de parler" (p. 33); and "[t]he following unresolved question [i.e. whether there could be an e.e. from V into V in the absence of choice] is therefore of foundational interest" (p. 324).

My question is: how do other set theorists prefer to resolve this tension?

Hamkins, J., Kirmayer, G., Perlmutter, N. (2012) Generalizations of the Kunen inconsistency". Annals of Pure and Applied Logic, 163, 1872–1890.

Suzuki, A. (1999) No elementary embedding from V into V is definable from parameters. Journal of Symbolic Logic 64, 1591-1594.

-
Sam, your question is that you want to get a sense of the range of positions on the matter? –  Joel David Hamkins May 3 '13 at 11:40
Hi Joel, I just wanted to know where set theorists stand on the question. In particular, I'm interested if any set theorists confronted with the result simply take the open question to now be settled. –  Sam Roberts May 3 '13 at 11:47

My perspective on this issue is that there are a variety of ways to take the claim of the Kunen inconsistency, and we needn't pick a particular one as the only right one. Rather, we gain a fuller perspective of the result by understanding the full robust context including all of the interpretations.

• Kunen proved his result in Kelly-Morse set theory, in large part in order that he could formalize what it means for a class function $j:V\to V$ to be (fully) elementary. In KM, we can prove that that there is a satisfaction class, a truth predicate for first-order truth, and with this class (which is definable) one can express the elementarity of $j$ as a single second-order assertion.

• Meanwhile, using the observation (Gaifman) that any cofinal $\Sigma_1$-elementary embedding is $\Sigma_n$-elementary for any meta-theoretic natural number $n$, we can formalize the result in GBC as the claim that no class $j$ is a nontrivial cofinal $\Sigma_1$-elementary embedding. Thus, this kind of elementarity of $j$ becomes expressible as a first-order assertion about $j$.

• We don't actually need full GBC, since for example global choice is not used, but only the usual AC for sets, and so this argument can be formalized in GB+AC.

• But actually, we don't need the full second-order part of GB, but only the ability to refer to the class $j$. So we can formalize the argument in $\text{ZFC}(j)$, the theory using ZFC where the axioms of replacement is allowed to use formulas in which the class $j$ appears. (But we only insist on elementarity of $j$ in the language without $j$.) This theory is used and suffices to show, for example, that the supremum of the critical sequence $\lambda=\sup_n\kappa_n$ exists.

• If one intends to rule out only definable class embeddings $j$, that is, ones which are classes in the ZFC sense of being first-order definable from set parameters, then as you mentioned, there is an easy argument ruling them out, and this argument does not use AC. I do not know any set theorist, however, who takes this result as an answer to the question of whether one can prove the Kunen inconsistency in ZF. Rather, this example reveals the issues of formalization, and shows us that it may be important to take more care in our formal treatment of the result.

• Meanwhile, a purely first-order version of the Kunen inconsistency is formalizable in ZFC, with no talk of classes of any kind, as the claim that there is no nontrivial $j:V_{\lambda+2}\to V_{\lambda+2}$ for any $\lambda$. This version still uses AC, and it is open in ZF. It avoids the set/class issues underlying your question by noting that the Kunen inconsistency proof establishes more by restricting to $V_{\lambda+2}$. This set version of the result implies the full result in any set theory capable of showing that a purported class $j$ must have a closure point $\lambda$.

• The wholeness axiom gets around the issue of the previous point by stating the theory ZFC + "$j:V\to V$ is nontrivial and elementary in the language with a function symbol for $j$. Elementarity is expressed by the scheme $\forall x[\varphi(x)\iff \varphi(j(x))]$.

• Various weakenings and strengthenings of the wholeness axiom are realized by making further claims about $j$, such as whether it has a critical point, whether it moves an ordinal, etc. Also, one can make claims about the extent to which $j$ may appear in the ZFC axioms. Officially, $j$ is allowed in the separation axiom but not in replacement, and so models of WA are not able to prove the supremum of the critical sequence exists.

• If one uses merely the model-theoretic concept of embedding, one would be considering $j:V\to V$ for which $x\in y\iff j(x)\in j(y)$. But now the point is that ZFC proves that there are nontrivial embeddings. For example, we can inductively define $j(y)=\{j(x)\mid x\in y\}\cup\{\{\emptyset,y\}\}$, and prove that this is a nontrivial embedding $j:V\to V$. (See my paper Every countable model of set theory embeds into its own constructible universe, to appear in the JML, for more information.)

I prefer to understand the Kunen inconsistency in the rich context of all these results, rather than pick just one perspective and say that that perspective is the right one.

-
Thanks, Joel! Clearly there are many hypotheses in the vicinity. For my purposes, though, it suffices that Kunen's result is considered non-trivial and/or that it's taken to be an open question whether there could be an embedding in the absence of choice when we formulate things in terms of classes. My impression is now that set theorists are divided on this. Does that sound right? –  Sam Roberts May 10 '13 at 9:51
One more question (if that's ok!): although we can't prove the existence of a satisfaction class in NBG, don't we have the resources to define satisfaction with a $\Delta^1_1$ formula? –  Sam Roberts May 10 '13 at 10:12
I don't think set theorists are divided on those points. Most set theorists agree with your characterization. The situation, however, is that set theorists have regrettably often been somewhat sloppy with the formalization of the Kunen result, and one most often hears it asserted as "There is no nontrivial embedding from $V$ to $V$", which is ambiguous for the reasons I've said. –  Joel David Hamkins May 10 '13 at 10:25
About satisfaction classes, it is consistent with NGB that there is none, since if one takes only the first-order definable classes, then one has NGB but there is no satisfaction class there by Tarski's theorem. But meanwhile, in any $\omega$-standard model, the satisfaction class is implicitly definable by a first-order formula (it is the unique class satisfying the Tarskian truth conditions). –  Joel David Hamkins May 10 '13 at 10:28
Ah, I see. So you're in the minority on that question! Re. satisfaction: sure, there is no satisfaction class, but I thought it was entirely straightforward to show that there is a ($\Delta^1_1$) formula $\Phi(x, y)$ such that NBG proves $\Phi(\ulcorner\phi\urcorner, a) \leftrightarrow \phi(a(0),...,a(n))$, where $\phi$'s free variables are among $x_0,..,x_n$. Indeed, I thought it was provable that $\Phi$ satisfies the general Tarski clauses. –  Sam Roberts May 10 '13 at 11:25

I won't try to say what set theorists generally do, but I usually handle the problem as follows. Most of the time, I work in ZFC and I use "class" to mean a class definable with set parameters. This is adequate most of the time --- for example, when I want to talk about $V$, $L$, $L[U]$, $L(\mathbb R)$, the elementary embeddings arising from measures, extenders, etc. In situations where it isn't adequate, for example in saying how Kunen's theorem goes beyond Suzuki's, I would work in ZFC with the assumption that there is an inaccessible cardinal $\kappa$, and I would (temporarily) use "set" to mean an element of $V_\kappa$ and use "class" to mean a subset of $V_\kappa$. (As long as I don't need anything of even higher rank than classes, this is pretty much equivalent to working in Morse-Kelley set-class theory. But, once I'm working in a world that goes beyond what I'm calling sets, I figure I might as well continue the cumulative hierarchy naturally rather than stopping after just one layer of non-sets.)

-
Thanks, Andreas! If it's not too much trouble, it would help me to get clearer on what considerations are at play here to know what you think about plural quantification plato.stanford.edu/entries/plural-quant in this context. For instance, suppose that plural quantification allowed one to unproblematically simulate MK over V (not merely over some $V_\alpha$). Would you then rather work in that setting when considering Reinhardt, supercompact etc cardinals or the question how Kunen's result goes beyond Suzuki's? –  Sam Roberts May 10 '13 at 10:01
@Sam: I know very little about plural quantification, but my immediate reaction is that it's likely to introduce some awkwardness into these issues. Like MK, its formalization would presumably rely on the pairing function in $V$ in order to code elementary embeddings (class-sized functions) as sets. In the MK context, this is quite familiar --- some people will even tell you (whether in MK or ZF) that functions are sets of ordered pairs (as opposed to being coded as sets of ordered pairs), but in plural quantification, the same idea sounds a bit strange. (continued in next comment) –  Andreas Blass May 10 '13 at 14:37
To assert the existence of an elementary embedding we'd say "There are some ordered pairs such that ..." followed by a description of what it means for those pairs to constitute an elementary embedding. Part of my difficulty here may be simply that this stuff is familiar in the set-based context but not in the plural quantification context. But in addition to that, it seems to me that such use of plural quantification loses a lot of the naturality that makes plural quantification attractive in the first place. –  Andreas Blass May 10 '13 at 14:41
Thanks, Andreas! I suppose it's a matter of familiarity - although one could simply work in MK but rely ultimately on a plural interpretation, it's also pretty straightforward to work directly in plural logic. There a (proper class sized) function will be some ordered pairs. In any case, the reason I brought up plural quantification was because I was wondering if the reluctance to employ MK class quantification was to do with ontological commitment to set-like entities which aren't actually sets. Whether or not plural quantification is natural, it at least doesn't suffer from that problem. –  Sam Roberts May 10 '13 at 19:36