The Quine systems go back to an article by Quine in 1937. We do not assume familiarity with this article; we calculate that anyone moved to read what we write below will have already digested the relevant Wikipedia and Stanford Encyclopedia articles.
Why are the Quine systems so unpopular? Well, one thing they all do is assert the existence of a Universal Set. And, as Any Fule Kno, the universal set is a paradoxical object. Well no actually, it isn’t. The nonexistence of the Russell class is a theorem of constructive FOL (you don’t even need extensionality); however for the nonexistence of V you need separation, so we are in set theory, and as we all know, set theory is a building site. Somewhere in this building site there might be a universal set.
However, for most people wishing to make use of set theory their point of departure is of course ZFC. So why should they pay attention to NF? One reason is that the parts of NF that ZF cannot reach might contain answers to mainstream questions like CH. Nevertheless the attitude of the ZFistes towards the Quine systems is rather like that attributed to the people who burnt the library of Alexandria. Either it is syntactic sugar for ZFC in which case it is superfluous, or it isn’t, in which case it’s wrong. Thus either way—nonconstructively at least—it’s a waste of our timeFootnote 1 . We invite our readers to choose the horn that says that NF has something different to say, and that that something matters. The two views may at bottom be equivalent, but each view may have advantages for different purposes, and it may be useful to know that one can wear glasses of different colours to look at the same world.
The idea that NF might or might not “mean the same” as ZF, and that issues of substance might hang on this question was considered in philosophical circles forty years ago. There are transcripts of conversations between Dreben, Quine, and Davidson, but they did not issue in actual theorems …not least because the mathematical theory of interpretation and synonymy was not as well developed then as it is now. See [Reference Smith17] (Thanks to Benjamin Marschall for showing us Smith’s commentary) The second author has done extensive work with “simple and obvious” unstratified axioms adjoined to NFU which give unexpectedly strong large cardinal principles [Reference Holmes11]: supporting the idea that working in a Quine-style system may give a different vantage point on the same mathematics we find in the Zermelo-style systems. Solovay and Enayat have also worked on strong axioms of infinity in NFU: see for example Solovay’s [Reference Solovay16] and Enayat’s [Reference Enayat, Enayat and Kossak4]: this work also supports the proposition that innocent and natural seeming unstratified assumptions adjoined to NFU have surprising strength.
It would help to dispel the sense of anomaly that surrounds the Quine systems if we knew what they were about…“Was sind und was sollen die Quinische Systeme?”. The customary gibe is that there is no intuitive picture of the world of sets that is captured by them, and the motivation that is offered is purely a syntactic trick. ‘Syntactic’ is fair; ‘trick’ is notFootnote
2
. At the same time as the mathematical public is tiring of the territorial (sorry, we meant foundationalist) claims of Set Theory and is looking instead to type-theoretic analyses to describe its praxis, it is becoming clearer to all that there is a story to be told about how the stratificationFootnote
3
discipline invoked by NF marries very well the informal typing of ordinary mathematics just mentioned; indeed the first author started writing a book about it but it seems now no longer necessary. So if we accept that NF is in fact reporting on some different but genuine mathematics one might be interested in reading some of its reports. So, this is the key question: “is the news from the NF marches different from the insights safeguarded in the Pale of ZFC?” So: what do the Quine systems have to tell us? The point of departure is NF. The literature does contain some strengthenings, but they are of course not of much interest until we have some consistency proofs for them! Most of the literature concerns weakenings. One obvious way to weaken NF is to restrict the comprehension scheme, and the obvious way to do that is to restrict it to formulæ with a bounded number of levels. NF
$_2$
is the fragment of NF where we assume the existence of
$\{x:\phi \}$
(parameters allowed) as long as
$\phi $
is stratifiable using only two levels. (There is also NF
$_3$
but we are not going to talk about it much here…and NF
$_4 =$
NF.) In 1974 Church showed us a way of end-extending models of theories like ZF to models of NF
$_2$
. He even axiomatised these models, with a theory that has come to be known as CUS. It is clear from Church’s writings at this time that he was interested in set theories with a universal set. The ease and naturalness of this construction of Church—it was even discovered independently about the same time by Urs Oswald—suggest that CUS might be merely syntactic sugar for ZF, and so (as we shall see, [Reference Button2]) it will turn out. Now Church’s construction does not appear to work for systems significantly stronger than NF
$_2$
(although quite where it stops working is not yet clear) so we shouldn’t expect NF to be syntactic sugar for ZF. All will be revealed below.
There is unpublished work by the first author at https://www.dpmms.cam.ac.uk/~tf/COmodels.pdf on spicing up CO constructions to add more “big” sets beyond those supplied in Church’s original construction. Plenty of things can be added in this way: for example the set of all isomorphism classes of all wellorderings of low sets (roughly, sets the same size as a copy of a set in the original model); however the set of all isomorphism classes of all wellorderings of all sets has resisted construction, although NF does say that it exists. Sets of this kind—that NF insists exist, but which nevertheless (apparently) cannot be constructed by CO methods or be proved to exist by ZF—live in a part of the NF universe that Andrey Bovykin calls “The Attic”. It’s worth noting that the treasures in the Attic seem to come at no cost: as far as we know NF does not contradict any set existence theorem of ZF. If ZF
$\vdash (\exists x)(\forall y)(y \in x \longleftrightarrow \phi (y))$
then—as far as we can tell—NF
$\not \vdash \neg (\exists x)(\forall y)(y \in x \longleftrightarrow \phi (y))$
. The obvious question is whether these Mrs Rochester entities have any secrets to spill about life downstairs. Does NF have anything to say about CH, for example? The answer to this is not known, although the best guess is that it doesn’t.
The authors have been playing Grace Poole for a long time.
The question of whether or not it has anything new to tell us can be addressed by the modern study of interpretations between theories. Time for some definitions.
1 Definitions, of synonymy etc
Two (first-order) theories are synonymous if there are two interpretations, of one into the other and the other into the one, which are mutually inverse up to logical equivalence. A nonthreatening trivial example to start with is the theory of posets expressed in the language with
$\leq $
and the theory of posets expressed in the language with
$\geq $
. The interpretation that sends
$x \leq y$
to
$y \geq x$
interprets the first theory in the second and the obvious interpretation in the other direction is inverse up to logical equivalence. Too trivial to mention, perhaps. Slightly less trivial is the case of the two theories of “partial order” and of “strict partial order”. Less trivial still, the theories of Boolean rings and of Boolean algebras are synonymous. Synonymous theories “have the same models” and in some sense report the same mathematics.
Another idea we were grateful to be taught by Enayat and Visser was that of a tight theory. A theory T is tight if any pair
$T'$
and
$T"$
of synonymous extensions of T are actually identical. Apparently ZFC and PA are tight—see [Reference Enayat, van Eijk, Iemhoff and Joosten5], [Reference Friedman and Visser9] and [Reference Freire and Hamkins10]. We prove below (Theorem 2) that NF is not tight, but that it is in some sense stratified-tight. Theorem 2 is inspired by a project of André Pétry from the last century, to relativise all of first-order logic to stratifiable formulæ. See [Reference . Pétry14].
The Church–Oswald construction is so neat and so invertible that it gives one the idea that Church’s CUS [Reference Church and Henkin3] might really be nothing more than syntactic sugar for ZF(C), For years the first author tried to persuade his Ph.D. students to prove that CUS and ZFC were synonymous, but none of them would be drawn. Our motive was a polemical one. As NFistes we have had to listen, over the years, to a lot of unthinking stereotyped nonsense about how it is obvious that there is no universal set. Better men than we have been irritated by this, Alonzo Church for one. Church makes it clear that (one of his) motives in formulating CUS was to make the point that the universe, V (unlike the Russell class) is not a paradoxical object, and that—further—a theory with a universal set could be interpreted in ZF. Our motive in (going further still and) praying for a proof of actual synonymy for ZF(C) and (something like) CUS was to make the point that, since (in virtue of their synonymy) they capture the same mathematics, and since they disagree about whether or not there is a universal set, then it follows that the existence or otherwise of a (the?) universal set is not a mathematical question at all, but is purely a matter of choice of formalism. Recently Tim Button [Reference Button2] has proved a synonymy result of the kind we have been looking for—though we will not go into specifics here. Will CO constructions ever give us a model of anything like NF? Years ago KayeFootnote 4 said to us that that will never happen. We think we may have attached more importance to this remark of theirs than they ever did, since although we have remembered it ever since and it has been a spur to our thinking, we don’t believe they have ever published it. Now that we have met ideas of synonymy-of-theories we have been moved to consider a version of Kaye’s conjecture that makes use of them:
$$\begin{align} "\mathit{No\ extension\ of\ NF\ is\ synonymous\ with\ any\ theory\ of\ wellfounded\ sets}" \end{align}$$
This modification suggests itself to us because of the thought that CO constructions might be the only way of establishing such synonymy. We are pleased to be able in what follows to present to the public a proof of something that sounds like Kaye’s conjecture.
The other way of weakening NF is to modify the axiom of extensionality to allow urelemente. Somewhat unexpectedly this results in a consistency proof for the weakened system. This was an insight of Jensen [Reference Jensen13]. However it gradually became clear—starting from work of Boffa built on by Solovay and the second author—that NFU was intimately related to the study of nonstandard models of theories of wellfounded sets, models with (external) automorphisms. This will give rise to synonymy results which we will explain below.
An important observation here is that NFU + Infinity + Choice also satisfies Kaye’s conjecture as we formulate it. This result is significant for interpreting the results of this paper: NFU + Infinity + Choice is seen to be like NF rather than like ZFC in terms of whatever phenomenon our results here are detecting, which means that the strangeness of the Quine systems observed here has nothing to do with the consistency problem for NF or Specker’s proof that choice fails in NF (the manifest strangenesses of NF itself).
There are certain characteristically NF-flavoured ideas used below, such as invariant formula, Rieger–Bernays permutation models, stratimorphism,
$j(\sigma )$
(
$\sigma $
a permutation), NF
$_3$
…which may not be familiar to all readers, but are all explained in [Reference Forster7]. CO models go back to Church [Reference Church and Henkin3]. Stratimorphisms are introduced in [Reference Forster6].
2 The results
As mentioned above Tim Button [Reference Button2] has proved a kind of omnibus synonymy result for ZF and systems obtained by CO constructions. We look forward to a detailed exposition of his work.
The behaviour of NF is very different.
2.1 NF not synonymous with any theory of wellfounded sets
Recently Nathan Bowler and the first author [Reference Bowler and Forster1] have been able to prove that every model of NF has a (Rieger–Bernays–style) permutation model containing an
$\in $
-automorphism, a fact which we will put to good use below.
We state the following illuminating elementary lemma at the suggestion of the referee. (We recall from Friedman and Visser [Reference Friedman and Visser9] that a direct interpretation is one that preserves = and the domain.)
Lemma 1. Let ER be the theory with two axioms: Extensionality and Regularity.
No consistent invariant extension of NF directly interprets ER.
Proof. Let NFe be a consistent invariant extension of NF. Suppose for reductio that there is a direct interpretation I: ER
$\to $
NFe. Working in NFe, suppose that some set
$\sigma $
is a nontrivial
$\in $
-automorphism. Let a be
$\{x: x \not = \sigma (x)\}$
. a is nonempty because
$\sigma $
is nontrivial. By regularity
$^I$
(I preserves the domain) there is
$b \in ^I a$
s.t.
$(\forall x \in ^I b)(x \not \in ^I a)$
, that is,
$(\forall x \in ^I b)(\sigma (x) = x)$
. Now
$\sigma $
is an
$\in ^I$
-automorphism (since it is an
$\in $
-automorphism); so, by extensionality
$^I$
(I preserves =)
$\sigma (b) = b$
, whence
$b\not \in a$
, a contradiction.
We have the immediate corollary.
Theorem 1. No invariant extension of NF is synonymous with any theory of wellfounded sets.
The foundational significance of this is that NF (unlike CUS) is telling us about some mathematics that is genuinely different from the mathematics reported on by ZF.
The second author remarks that the situation in NFU (described later in the paper) should give one pause (or at least encourage one to be very careful). We show below that there can be a well-founded set relation which has an unstratified definition which presents a model of NFU (with an additional axiom) as in effect a model of a theory of well-founded sets. And the relative consistency proof for existence of an
$\in $
-automorphism works perfectly well in NFU + Infinity + Choice, or indeed in any stratified extension of NFU. The situation is saved (the argument above does not go through for the theory for which we do give a synonymy result) because the additional axiom added to NFU is unstratified and not invariant under the Rieger–Bernays permutation methods used to adjoin an
$\in $
-automorphism.
2.2 And it’s not tight either
Theorem 2. No invariant extension of NF is tight.
Proof. Let T be any invariant extension of NF and consider the theories “T +
$\exists !$
Quine atom” and “T + there are no Quine atoms”. These theories are clearly distinct. It is standard that they are both consistent if T is (this goes back to Scott [Reference Scott and Nagel15]). It remains to show that they are synonymous.
Let
${\mathfrak M}$
be a model of T containing no Quine atoms, and consider the transposition
$(\emptyset ,\{\emptyset \})$
. In
${\mathfrak M}^{(\emptyset ,\{\emptyset \})}$
the old empty set has become a (unique) Quine atom, which we are going to call ‘a’. Working in this new model, consider the transposition
$(a,\emptyset )$
. This gives us a new permutation model which is isomorphic to
${\mathfrak M}$
.
(Observe that the same Rieger–Bernays permutation we have used here can be tweaked to explain the fact proved in [Reference Enayat, van Eijk, Iemhoff and Joosten5] that it is ZF(C) that is tight rather then the version without foundation. By the above construction ZF(C) is synonymous with the theory obtained from it by replacing foundation with the axiom “there is a Quine atom a s.t. every set lacking an
$\in $
-minimal member contains a”.)
So NF is not tight. Nevertheless the two theories in Theorem 2, distinct though they are, do at least agree on stratifiable formulæ. This prompts the thought that NF might be “stratified-tight”, if only we knew exactly what that meant. We thank the referee for some comments that have helped clarify our thoughts in that regard.
Definition 1. Two theories are stratified-synonymous if there are interpretations witnessing synonymy whose data are given using only stratified formulæ.
A Theory is stratified-tight if any two stratified-synonymous extensions of it by stratifiable formulæ are identical.
2.2.1 Though it is stratified-tight.
We can prove the following
Lemma 2. Suppose
${\mathfrak M}_1$
and
${\mathfrak M}_2$
are two models of NF with the same carrier set;
Suppose further that
$Th({\mathfrak M}_1)$
and
$Th({\mathfrak M}_2)$
are stratified-synonymous.
Then
${\mathfrak M}_1 \equiv _{\mathrm strat}{\mathfrak M}_2$
(they satisfy the same stratified sentences).
Proof. We will show that in these circumstances the two structures
$\langle V, \in _1 \rangle $
and
$\langle V, \in _2 \rangle $
are stratimorphic. That is to say, if one obtains two models of TST by making
$\omega $
copies of
$\langle V,\in _1 \rangle $
and of
$\langle V, \in _2 \rangle $
then these two models of TST are isomorphic (as models of TST). The key idea in a stratimorphism is that even if all levels of each model have the same carrier set the bijections
$f_n$
between the two nth levels need not all be the same but can depend on n. Naturally
$f_0$
—the bijection between the two
$0$
th levels—is the identity. For the recursion it is important that the
$f_i$
should have definitions that are stratified. What about
$f_1$
? What must the stratimorphism send an element
$x_1$
of level
$1$
of
${\mathfrak M}_1$
to? It has a handful of members-in-the-sense-of-
$\in _1$
. We must send it to that element of
${\mathfrak M}_2$
that has precisely those members …in the sense of
$\in _2$
. But this is easy. By assumption ‘
$y \in _1 x$
’ is a stratifiable expression of
${\cal L}(\in _2,=)$
. Higher levels are analogous.
Corollary 1. NF is stratified-tight.
Proof. Let
$T_1$
and
$T_2$
be stratified-synonymous extensions of NF by stratifiable formulæ. Using stratified synonymy and Lemma 2 any model
${\mathfrak M} \models T_1$
can be treated as a model
${\mathfrak M}_2\models T_2$
such that
${\mathfrak M}_1 \equiv _{\mathrm {strat}} T_2$
. So, if
$\phi $
is stratifiable and
$T_2 \vdash \phi $
, then
$T_1 \vdash \phi $
. The other direction is similar. But since
$T_1$
and
$T_2$
are stratified theories we are done.
The point is sometimes made that tightness is something to do with second-order categoricity (ZFC, Zermelo + “ranks” and PA are tight, and their second-order versions are in some sense categorical) and it is worth thinking about how the stratified-tightness of NF will play out. Higher-order TST is uncountably categorical, but there may be more to be said…perhaps there is a stratified second-order theory somewhere down the back of the sofa.
The next challenge is to show that every invariant extension of NF is stratified-tight.
Theorem 1 concerned invariant extensions of NF. At this stage we have no results concerning extensions of NF that are not invariant.
2.3 Synonymy questions concerning NFU
NFistes have always known that NF and NFU have a very different feel to them. We are now in a position to give tangible form to this feeling.Footnote 5 In contrast to Theorem 1 we here announce a substantial and surprising result about synonymy of NFU (plus stuff) with a variation of ordinary Zermelo-style set theory. When it first came up (in [Reference Holmes12]) we did not think of it as a result about synonymy, so the discussion will be recast a bit here: the question originally was whether the urelements in a model of NFU can be indiscernible, and we started with the view that they were in the models of NFU obtained by the usual construction of models of NFU (ascribed to Boffa) using a nonstandard initial segment of the usual cumulative hierarchy of sets with an external automorphism moving a type.
But they aren’t, and the way the second author proved this was to show that all information in the model of ordinary set theory with automorphism is preserved in the model construction, and in particular the extension of an urelement as a set in the original model can be divined. This was deeply surprising, because it seems as if all information about the extension of the urelements is discarded in the construction, and it is shown in [Reference Forster7] that the urelements are indiscernible with respect to stratified predicates.
See [Reference Holmes12] for the original discussion.
This unwanted preservation theorem has some upside in the form of the synonymy result which follows below. To recast the result of [Reference Holmes12] as a result about synonymy we need to present two theories. The formulation given here differs in details from the exposition in [Reference Holmes12], but is not essentially novel.
2.3.1 Axiomatization of NFU + Endomorphism.
The first is NFU, which we suppose familiar to the reader, with an additional axiom. We reserve the name NFU
$^*$
for the full theory, if a name for this theory proves useful. The primitive notions of this theory are equality, membership, and the empty set
$\emptyset $
.
-
Axiom of the Empty Set:
$(\forall x:x \not \in \emptyset )$
. -
Definition:
${\texttt {set}}(x)$
[x is a set] is defined as holding if
$(\exists y:y \in x ) \vee x=\emptyset $
. -
Axiom of (weak) Extensionality:
$$\begin{align*}(\forall xyz:(z \in x \wedge (\forall u:u \in x \leftrightarrow u \in y))\rightarrow x=y).\end{align*}$$
-
Axiom Scheme of (stratified) Comprehension: If
$\phi $
is a stratifiable formula not mentioning the variable A, then
$(\exists A:(\forall x:x \in A \leftrightarrow \phi ))$
is an axiom. The set witness to this axiom, unique by extensionality and the existence of the empty set, is called
$\{x:\phi \}$
.It is worth noting that this axiom can be replaced by a finite set of its instances, removing the need for the notion of stratification.
-
Axiom of Endomorphism: This is the new axiom, not in the definition of NFU. It comes in three parts.
-
1. There is an injection E from the collection of singletons into the collection of sets such that if x is a set,
$\textbf {E}(\{x\}) = \{{\textbf E}(\{y\}):y \in x\}$
, and that the range of E includes all subsets of its elements.Notice that the image of an atom cannot be a set of images under
$\textbf {E}$
. It is beyond the scope of this paper to show this, but we note that the axiom of endomorphism implies the existence of atoms; it is not consistent with NF. -
2. Further, a relation E is then definable as
$x {\, } E {\, } y \equiv _{\texttt {def}} x \in \textbf {E}(\{y\})$
. This relation is implementable as a set.The axiom further asserts that E is a well-founded relation: we have called this the Axiom of Foundation, but note that NFU + the Axiom of Endomorphism + the Axiom of Foundation certainly contains ill-founded sets in the usual sense.
-
3. Note that any object has an ordinal rank in the well-founded relation E in a quite standard sense (we will not detour into technicalities of defining ordinal ranks in NFU except to assert that it can be done, and this is well understood). The axiom further asserts that for every
$\alpha $
such that there is an object of rank
$\alpha $
in E, the set of objects of rank
$<\alpha $
in E (and so each of its subsets) is in the range of
$\textbf {E}$
.We insert the technicalities about ranks in well-founded relations in NFU, which a reader may find really are best avoided. A relation R is well-founded if for any subset A of
${\texttt fld}(R)$
there is
$a \in A$
such that there is no b such that
$b {\, } R {\, } a$
. For any subset A of
${\texttt fld}(R)$
we give the nonce definition
$A^+$
for the collection of all elements b of
${\texttt fld}(R)$
which are either in A or have
$a \in A$
such that
$a {\, } R {\, } b$
. We then define the collection of ranks in R as the smallest collection of subsets of
${\texttt fld}(R)$
which contains
$\emptyset $
, is closed under
$^+$
and is closed under unions of its subsets. It is straightforward to show that the collection of ranks is well-ordered under inclusion and the rank of an element of
${\texttt fld}(R)$
could be defined as the order type of the inclusion order on the ranks which do not include it as an element. One should note that there is a type displacement between the ordinal associated with the rank and the elements of the rank; this is not strictly speaking a function. Different technical decisions could be made in this definition, and as we say, we regard its details as not particularly helpful. One has to recall here that an ordinal in NFU is an equivalence class of well-orderingsFootnote
6
under similarity.
It is important to remark that NFU proves that there can be at most one object with the properties stated for E, so this does not need to be a primitive notion of the theory. We demonstrate this below, but it is important to remark on it here.
-
Lemma 3. For all
$x,y$
,
$x {\, } E {\, } y \leftrightarrow \textbf {E}(\{x\}) {\, } E {\, }\textbf {E}(\{y\})$
.
Proof. For any set A,
$x \in A \leftrightarrow \textbf {E}(\{x\}) \in \textbf {E}(\{A\})$
by the first clause of the axiom of endomorphism. Apply this to
$x {\, } E {\, } y$
, that is,
$x \in \textbf {E}(\{y\})$
, using the fact that
$\textbf {E}(\{y\})$
is a set, and we obtain that
$x {\, } E {\, } y$
is equivalent to
$\textbf {E}(\{x\}) \in \textbf {E}(\{\textbf {E}(\{y\})\})$
, that is,
$\textbf {E}(\{x\}) {\, } E {\, } \textbf {E}(\{y\})$
.
Lemma 4. By the previous Lemma, the image of any part of the graph of E under the operation of applying
$\textbf {E}(\{\cdot \})$
to every node is part of the graph of E. It follows that if x has rank
$\alpha $
in E,
$\textbf {E}(\{x\})$
has rank
$T(\alpha )$
, where T is the operation on ordinals induced by applying the singleton map termwise to the well-orderings belonging to the ordinal (a familiar concept in NF studies).
Theorem 3. There can be no more than one relation E satisfying the conditions of the Axiom of Endomorphism (which means that we do not need to introduce the operation it describes as a primitive of the theory).
Proof. Suppose that there were two distinct relations
$\mathbf {E_1}$
and
$\mathbf {E_2}$
each satisfying their own version of the axiom. There must be a minimal rank x in the relation
$E_1$
(which is to
$\mathbf {E_1}$
as E is to
$\mathbf {E}$
) such that
$\mathbf {E_1}(\{x\}) \neq \mathbf {E_2}(\{x\})$
. Let
$\gamma $
be its rank in
$E_1$
. Note that
$$\begin{align*}\mathbf{E_1}(\{\{x\}\}) = \{\mathbf{E_1}(\{x\})\} \neq \{{\mathbf E_2}(\{x\})\}=\mathbf{E_2}(\{\{x\}\}). \end{align*}$$
The rank of
$\{x\}$
is
$T\gamma +1$
, so we must have
$T\gamma +1 \geq \gamma $
, so in fact we must have
$T\gamma \geq \gamma $
(
$T\gamma $
cannot be the predecessor of
$\gamma $
: its finite part has the same parity). Note that since there is a counterexample which is a set, we can further qualify our choice of x as the least rank counterexample which is a set.
$T\gamma \geq \gamma $
follows just as above. Now consider
$y \in x$
. We have
$\mathbf {E_1}(\{y\}) \in \mathbf {E_1}(\{x\})$
because x is a set. It follows that the rank of
$\mathbf {E_1}(\{y\})$
, which is the image under T of the rank of y, is less than the rank of x, which is in turn less than or equal to the image under T of the rank of x, so the rank of y is less than the rank of x. So no element of x can be an exception. Thus
$$\begin{align*}\mathbf{E_1}(\{x\})=\{\mathbf{E_1}(\{y\}):y \in x\}=\{\mathbf{E_2}(\{y\}):y \in x\}=\mathbf{E_2}(\{x\}),\end{align*}$$
which is a contradiction. Note that rank in
$E_2$
is never used: there can be no
$\mathbf {E}_2$
distinct from
$\mathbf {E}_1$
which even satisfies the first clause of the axiom of endomorphism.
2.3.2 Axiomatization of the theory of a stage of the cumulative hierarchy with an endomorphism.
The second theory is intended to be the theory of a stage of the usual cumulative hierarchy with an external endomorphism to a lower stage. Note that the stage whose theory we are considering is not one of the stages
$V_\alpha $
we describe below in its internal theory: it may be supposed to be the first stage not appearing in its internal theory. Its primitives are membership, which we will write
$\varepsilon $
for this theory, and the endomorphism j. (Note repurposing of the letter j). We define
$x \subseteq _\varepsilon y$
as
$(\forall z:x \varepsilon x \rightarrow z \varepsilon y)$
.
If a name for it is desired, we will call it BZJ for “bounded Zermelo set theory with an automorphism (j)”. The senses in which it is bounded are eccentric.
The axioms are
-
Extensionality: Strong extensionality (no atoms) as in the usual set theory.
-
Separation: For any set A,
$[x {\, } \varepsilon {\, } A:\phi ]$
is a set as in the usual set theory, where
$\phi $
is a formula not mentioning A or j:
$x {\, } \varepsilon {\, } [x {\, } \varepsilon {\, } A:\phi ] \leftrightarrow x {\, } \varepsilon {\, } A \wedge \phi $
. Note that we are keeping our notation distinct from that of the other theory.Footnote
7
-
Isomorphism:
$j(x)=j(y) \leftrightarrow x = y$
;
$j(x)\varepsilon j(y) \leftrightarrow x \varepsilon y$
;
$x \varepsilon j(y)$
or
$x \subseteq _\varepsilon j(y)$
imply that for some z,
$x=j(z)$
. -
Binary union: For any sets
$x,y$
there is a set
$x \cup _\varepsilon y$
with
$z {\, } \varepsilon {\, } x \cup _\varepsilon y$
if
$z {\, } \varepsilon {\, } x \vee z {\, } \varepsilon {\, }y$
. Notice that it follows that if
$x \varepsilon a$
and
$y \varepsilon b$
we can define
$[a,b] = [z {\, }\varepsilon {\, }a \cup _\varepsilon b {\, } | {\, } z=a \vee z=b]$
; we can define unordered pairs of elements, so we can define ordered pairs of elements using the usual definition due to Kuratowski, and define relations and functions as sets of ordered pairs in familiar ways.The reader should note that we are avoiding assuming that all sets are elements, so this is a weak form of pairing. Notice that an element of the domain of a function must be an element of an element of an element, as projections of an ordered pair are elements of its elements.
-
Definition: An ordinal is a non-self-membered set which is transitive and strictly well-ordered by the membership relation.Footnote 8 One proves by quite standard methods that the collection of all ordinals is transitive and strictly well-ordered by the proper inclusion relation, and cannot be the extension of a set.
-
Definition (partial stage function) A partial stage function is a function W from an ordinal
$\alpha $
to sets such that, for each
$\beta {\, } \varepsilon {\, } \alpha $
,
$$\begin{align*}x \varepsilon W(\beta) \leftrightarrow (\exists \gamma {\, } \varepsilon {\, } \beta:x \subseteq_\varepsilon W(\gamma)).\end{align*}$$
It is straightforward to prove that any two partial stage functions will agree on the intersection of their domains.
-
Axiom of stages: For each ordinal
$\alpha $
which is capable of being in the domain of a function (which is an element of an element of an element) we provide that there is a stage function W with
$\alpha $
in its domain and define
$V_\alpha $
as
$W(\alpha )$
. We provide that
$V_\alpha $
is definable for each ordinal which is not an element of an element of an element, as either the collection of all subsets of
$V_\beta $
, where
$\beta $
is the maximal element of
$\alpha $
, or as the union of all
$V_\beta $
where
$\beta {\, } \varepsilon {\, } \alpha $
, if
$\alpha $
has no maximum element (we stipulate as part of the axiom that these sets exist if the case arises). This definition will succeed with no need to work with more than a small finite number of exceptional cases: any ordinal which is limit has all smaller ordinals elements of elements of elements and so the extended definition works; an ordinal of the form
$\alpha +3$
has
$\alpha $
an element of an element of an element, and so can be handled; an ordinal
$\alpha $
of the form
$\lambda +1$
or
$\lambda +2$
,
$\lambda $
limit, can evidently be handled by the extended definition.We call
$V_\alpha $
a stage, and the stage indexed by
$\alpha $
. We assert further that every set is a subset of some stage.Note that we have
$$\begin{align*}x \varepsilon V_{\beta} \leftrightarrow (\exists \gamma{\, } \varepsilon{\, } \beta:x \subseteq_\varepsilon V_\gamma).\end{align*}$$
It is evident that if W is a partial stage function, so is
$j(W)$
, and that
$V_{j(\alpha )} = j(V_\alpha )$
for this reason (with a little technical work (but not very much) if
$\alpha $
is not an element of an element of an element). We briefly indicate how this works in the easy case: for any
$\alpha $
an element of an element of an element,
$[\alpha ,V_\alpha ] \varepsilon W$
for some partial stage function W; thus
$[j(\alpha ),j(V_\alpha )] \varepsilon j(W)$
;
$j(W)$
is a partial stage function so
$V_{j(\alpha )} = j(V_\alpha )$
. The situation where
$\alpha $
is not an element of an element of an element is similarly handled by the fact that j preserves equality and membership.We say that an object is of rank
$\alpha $
in the sense of the second theory if it is
$\varepsilon {\, } V_{\alpha +1} \setminus V_\alpha $
.Notice that we are not claiming that every well-ordering has an order type which is a (von Neumann) ordinal. This will not be the case, as a rule.
We are further not claiming that existence of
$V_\alpha $
implies existence of
$V_{\alpha +1}$
: there can in principle be a final stage which is not an element and whose index is not an element. -
Nontriviality: The collection
$j"V$
of all images under j is a set. -
Definition: Define
$j^n"V$
as
$j^{n-1}(j"V)$
.
The reader should think that this theory should be a variation on the familiar set theory of Zermelo, and indeed it is, but it has significant oddities. We attempt some clarification of the consequences of these axioms and their relationship to the axioms of Zermelo set theory. Note that it is not a consequence of these axioms that every set is an element (we should not expect this from our motivation: the stage of the cumulative hierarchy that we consider might not be limit).
Before we review the axioms we establish the existence of a special rank.
We prove that
$j"V$
is a rank, specifically
$V_\Omega $
where
$\Omega $
is the set of all ordinals
$j(\alpha )$
, the smallest ordinal not in the range of j [this is not to be confused with the use of
$\Omega $
for the order type of the natural well-ordering on the ordinals in NFU, though this ordinal has a similar “ultimate” quality: it is not as a rule the same ordinal!]. There must be such an ordinal: it can be defined as the set of all ordinals in
$j"V$
, which must exist by separation, is transitive and strictly well-ordered by membership, and cannot be an element of itself because if it were it would be a self-membered ordinal, and finally cannot be in
$j"V$
because it would then be an element of itself. Every element x of
$V_\Omega $
is a subset of
$V_\beta $
for some
$\beta <\Omega $
, whence
$\beta = j(\gamma )$
for some
$\gamma $
, so
$x \subseteq _\varepsilon V_{j(\gamma )} = j(V_\gamma )$
, so
$x = j(y)$
for some y, so
$x \varepsilon j"V$
. Every element x of
$j"V$
is
$j(y)$
for some y,
$y \subseteq _\varepsilon V_\beta $
for some
$\beta $
, so
$x \subseteq _\varepsilon V_{j(\beta )}$
, so
$x \varepsilon V_\Omega $
.
We add the remark that where we talk about “the stage of the cumulative hierarchy that we are considering” we are talking about the entire universe of the theory, which is not one of the stages we consider inside the theory (not even one which fails to be an element). It is as it were the next stage past all the ones we consider internally. Its features are visible to us internally to a limited extent because
$V_{\Omega }$
is in effect its elementwise image under j.
We review the status of the axioms of Zermelo set theory in BZJ.
Pairing holds in a limited sense, as described above: if two sets are elements, their unordered pair exists.
Power set holds for elements: if A is an element, it belongs to a set B, which is included as a subset in a stage
$V_\gamma $
, so
$A \varepsilon V_\gamma $
and any subset of A belongs to
$V_\gamma $
, and we can define
${\cal P}(A)$
as
$[C{\, } \varepsilon {\, } V_\gamma :C \subseteq _\varepsilon A]$
. Again, if the stage of the cumulative hierarchy that we are considering is not a limit stage, a set of highest rank cannot have a power set; if the stage we are considering is a limit stage, power set holds for all sets.
The axiom of union is a consequence of the axioms. Any set A is included in a rank
$V_\gamma $
for a smallest ordinal
$\gamma $
: its elements are all elements of this
$V_\gamma $
, and
$\bigcup A$
is definable by separation from
$V_\gamma $
.
Infinity is not a consequence of the axioms; it would be if we added the supposition that the stage of the cumulative hierarchy which we are considering is a limit stage.
We can suppose Choice if we wish, though we have not included it in our axiom set. Foundation is not part of the original Zermelo system, but does hold here.
The simplest additional assumption which would give us an extension of Zermelo set theory is simply that every set is an element (and we would need to add to our assumptions in NFU that the rank of E is limit). This would imply that pairing, power set, and infinity hold. It is actually somewhat stronger, implying the existence of
$\beth _\omega $
[in fact, rather more than that]. We prefer to keep our result applicable to weaker theories.
Now, if we make this stronger assumption that every object is an element, we assume that every
$V_\alpha $
is an element, and so must be an element of
$V_{\alpha +1}$
. This means that for any
$V_\alpha $
with
$\alpha <\Omega $
, that is, for any
$V_{j(\beta )}$
,
$V_{j(\beta )+1} = j(V_{\beta +1})$
, because the latter exists, so
$j(\beta )+1=\alpha +1<\Omega $
as well. So
$\Omega $
is a limit ordinal, which establishes Infinity and the existence of
$\beth _\omega $
. Actually, since
$j^i(\Omega )$
will also be limit for each i, the existence of any concrete finite number of limit ordinals is established. This extension of BZJ does have models in which
$\beth _{\omega ^2}$
does not exist.
If
$\Omega $
is not a limit ordinal then it is
$j(\beta )+1$
for some ordinal
$\beta $
, and
$\beta +1$
cannot exist, because if it did, we would have
$j(\beta +1) = \Omega $
, contrary to the definition of
$\Omega $
. So the ordinal
$\beta $
is not an element. Existence of an ordinal which is not an element or a rank which is not an element is exactly equivalent to
$\Omega $
being successor.
It is worth noting that this theory is a theory of well-founded sets though its models are not well-founded in the external sense. Any nonempty set has an
$\varepsilon $
-minimal element, though it is clear that a subcollection like
$\{j^i"V:i \varepsilon {\mathbb N}\}$
of a model of this theory has no
$\varepsilon $
-minimal element: it is not obliged to, as it is not a set in this theory.
2.4 The synonymy result stated and proved
Theorem 4. The two theories presented above, the extension NFU
$^*$
of NFU with the Axiom of Endomorphism and the theory BZJ desdcribed above of a stage of the cumulative hierarchy with an endomorphism, are synonymous.
Proof. To facilitate discussion of synonymy, we keep our notations disjoint. Note use of
$\in $
in NFU
$^*$
and
$\varepsilon $
in the second theory, and use of notations
$\{x:\phi \}$
for NFU
$^*$
and
$[x {\, } \varepsilon {\, } A:\phi ]$
in the second theory. We will specify distinct notations in the two theories wherever necessary for clarity.
We state the definitions of the notions of each theory in terms of the other, which provide the framework for the synonymy.
$x {\, } \varepsilon {\, } y$
is defined as
$x {\, } E {\, } y$
.
$j(x)$
is defined as
$\textbf {E}(\{x\})$
.
Where
$V_\Omega = j"V$
is the rank containing all the images under j, we define
$x \in y$
as
$j(x) {\, } \varepsilon {\, } y \wedge y {\, } \varepsilon {\, } V_{\Omega +1}$
. We note that this implies that
$\{x\}$
is the set
$[u {\, } \varepsilon {\, } V_\Omega :u=j(x)]$
which we will write
$[j(x)]$
. So (noting how
$j(x)$
is defined above), we define
$\textbf {E}$
so that
$\textbf {E}([j(x)]) = j(x)$
: it sends singletons (in the sense of the second theory) of elements of
$V_\Omega $
to their elements.
Now we need to verify that the axioms of each theory imply the translations of the axioms of the other via these definitions.
That the weak extensionality of NFU
$^*$
follows from the axioms of the second theory is evident. If
$z \in x$
and
$(\forall u:u \in x \leftrightarrow u \in y)$
, then
$j(z) {\, } \varepsilon {\, } x$
and
$x {\, } \varepsilon {\, } V_{\Omega +1}$
. We also have
$z \in y$
, so we also have
$y {\, } \varepsilon {\, } V_{\Omega +1}$
. The assertion
$(\forall u:u \in x \leftrightarrow u \in y)$
translates to
$(\forall u:j(u) {\, } \varepsilon {\, } x \leftrightarrow j(u) {\, } \varepsilon {\, } y)$
(eliminating the simply true
$x,y {\, } \varepsilon {\, } V_{\Omega +1}$
side conditions). Since
$x,y \varepsilon V_{\Omega +1}$
it follows that all preimages of x or y under
$\varepsilon $
are images under j, so we have
$(\forall v:v {\, } \varepsilon {\, } x \leftrightarrow v {\, } \varepsilon {\, } y)$
, whence
$x=y$
.
Empty objects in the sense of NFU
$^*$
are either the empty object in the second theory (which we regard as the empty set for both theories) or objects which are not
$\varepsilon {\, } V_{\Omega +1}$
, which we regard as urelements in NFU
$^*$
.
We verify that the translation of the stratified comprehension scheme of NFU
$^*$
gives a theorem scheme in the second theory.
Let
$\{x : \phi \}$
be a stratified set abstract. We perform a series of transformations on the formula
$\phi $
. Let type be a name for a stratification of
$\phi $
.
$\phi _1$
is obtained by translating each
$u \in v$
to
$j(u) {\, } \varepsilon {\, } v \wedge v {\, } \varepsilon {\, } V_{\Omega +1}$
and each
$\textbf {E}(\{x\})$
to
$j(x)$
. Clearly
$\phi _1$
is equivalent to
$\phi $
.
Choose an integer N larger than any element of the range of type.
$\phi _2$
is obtained by applying j to both sides of each atomic subformula a certain number of times cleverly. We transform each
$j(u)\, \varepsilon \, v \wedge v\, \epsilon \, V_{\Omega +1}$
and each
$u=v$
by applying
$j^{N-{\texttt{type}}(v)}$
to both sides of each constatomic formula. Note that this does not affect the truth value of any sentence (because j is applied the same number of times to both sides of any atomic subformula), and it has the effect that each variable w appears only in the context
$j^{N-{\texttt{type}}(w)}(w)$
with no further applications of j, since
$j^{N-{\texttt{type}}(v)}(j(u)) = j^{N-{\texttt{type}}(u)}(u)$
in the first kind of sentence because
${\texttt{type}}$
is a stratification.
$\phi _3$
is obtained by replacing each
$j^{N-{\texttt{type}}(u)}(u)$
where u is bound with simply u, the quantifier being restricted to
$j^{N-{\texttt{type}}(u)}"(V)$
. Note that
$\phi _3$
has the same truth value as
$\phi _1$
.
Further, obtain
$\phi _4$
by replacing
$j^{N-{\texttt{type}}(x)}(x)$
with x.
$[x \varepsilon j^{N-{\texttt{type}}(x)}"V | \phi _4]$
exists by separation. Call this X. Consider
$X_2 = j^{1-(N-{\texttt{type}}(x))}(X)$
. [Any subset Y of a
$j^n"V$
for
$n>1$
has inverse image under j because it is a subset of
$j(j^{n-1}"V)$
; repeated application gives the existence of
$j^{1-n}(Y)$
].
$j(x) \varepsilon X_2$
is equivalent to
$j^{(N-{\texttt{type}}(x))-1}(j(x)) \varepsilon X$
, and so to
$j^{N-{\texttt{type}}(x)}(x) \varepsilon X$
, and so to
$\phi _3$
, and so to
$\phi _1$
. From this it follows that
$x \in X_2$
if
$\phi $
, the desired conclusion:
$X_2$
is a witness to the desired instance of stratified comprehension as translated into the language of the second theory.
That E is well-founded in NFU
$^*$
follows directly from the fact that all sets are well founded in the second theory (not provided as an axiom but an obvious consequence of the axiom of stages: every set has an element of minimal rank, and nothing in the set can be an element of that, so every set has an
$\varepsilon $
-minimal element; we have noted that in the metatheory it is seen that models of the second theory are not actually well-founded, but this is not visible internally to the theory).
$x {\, } E {\, } y$
is defined as
$x \in \textbf {E}(\{y\})$
, which translates to
$j(x) {\, } \varepsilon {\, } j(y)$
, which is equivalent to
$x {\, } \varepsilon {\, } y$
.
If x is a set in NFU
$^*$
(this means
$x \varepsilon V_{\Omega +1}$
) then every element of x in terms of BZJ is an image under j, so
$$\begin{align*}\textbf{E}(\{x\}) = j(x) = [j^2(u):j(u) \varepsilon x] = \{j(u):u \in x\} = \{\textbf{E}(\{u\}):u \in x\}.\end{align*}$$
j is an external injection from the universe into
$V_{\Omega }$
, whence it is evident that E is an injection (in NFU terms) from singletons into sets. The fact that every subset of an image under j is an image under j translates to the fact that the range of E includes all subsets of its elements.
In terms of the second theory, each object x is a subset of a rank
$V_\alpha $
for a smallest
$\alpha $
. The rank assigned to x in
${E}$
in terms of the first theory is determined by this ordinal
$\alpha $
in a way which involves annoying bookkeeping: it is the order type of the first-theory well-ordering of the second-theory ordinals
$\beta \varepsilon \alpha $
under the inclusion order of the second theory. The rank of any object will be the smallest rank greater than the ranks of each of its preimages under
$\varepsilon $
(elements in the terms of the second theory). The collection of objects of rank less than
$\alpha $
in terms of the first theory is precisely the union of the
$V_\beta $
’s for
$\beta <\alpha $
, which does exist in the second theory. The objects which are not elements of the range of E in the first theory are all seen to be of the final rank
$\lambda $
(which exists in this case) since this corresponds precisely to not being an element in terms of the second theory.
In the last few paragraphs, we have verified that a model of the second theory satisfies the translation of the Axiom of Endomorphism.
Now we need to verify the axioms of the second theory from their definitions from NFU
$^*$
concepts.
We verify extensionality.
$$\begin{align*}(\forall z:z{\, } \varepsilon{\, } x \leftrightarrow z{\, } \varepsilon{\, } y)\end{align*}$$
translates to
$$\begin{align*}(\forall z:z \in \textbf{E}(\{x\}) \leftrightarrow z \in {\textbf E}(\{y\})),\end{align*}$$
which implies
$\textbf {E}(\{x\}) = \textbf {E}(\{y\})$
because these are sets, which further implies
$x=y$
. (This does require us to be assuming in the background of our NFU that we can identify an empty set among the urelements: this is required simply for the statement of the Axiom of Endomorphism.)
We verify the axiom of binary union of BZJ: for any
$x,y$
,
$\textbf {E}(\{x\}) \cup \textbf {E}(\{y\})$
in the sense of NFU
$^*$
exists and is
$\textbf {E}(\{z\})$
for some z (because it is a subset of
$\textbf {E}(\{V\})$
), and this z is directly seen to be
$x \cup _\varepsilon y$
in the sense of BZJ.
$j(x) = j(y)$
means
$\textbf {E}(\{x\}) = \textbf {E}(\{y\})$
which is clearly true if
$x=y$
.
$x\ {\, } \varepsilon {\, } y$
means
$x \in \textbf {E}(\{y\})$
, which is true if
$\textbf {E}(\{x\}) \in \textbf {E}(\{\textbf {E}(\{y\})\})$
because
${\textbf E}(\{y\})$
is a set (more generally, if A is a set,
$x \in A$
if
${\textbf E}(\{x\}) \in \textbf {E}(\{A\})$
), and
$\textbf {E}(\{x\}) \in {\textbf E}(\{\textbf {E}(\{y\})\})$
is the translation of
$j(x) {\, } \varepsilon {\, } j(y)$
.
That
$x {\, } \varepsilon {\, } j(y)$
implies that
$x \in \textbf {E}(\{\textbf {E}(\{y\})\}) = \{\textbf {E}(\{u\}): u \in {\textbf E}(\{y\})\}$
so x is some
$\textbf {E}(\{u\})$
and so some
$j(u)$
. That
$x \subseteq _\varepsilon j(y)$
implies that x is a subset of
$j(y)$
in NFU
$^*$
unless x is an urelement. But an urelement in the sense of NFU
$^*$
must have a preimage under E which is not itself a preimage under E, and we have already shown (first result of this paragraph) that
$j(y)$
has no preimage under E which is not an image under E. So x is a subset of
$j(y)$
, which is in the range of
$\textbf {E}$
, so x is in the range of
$\textbf {E}$
, so
$x=j(u)$
for some u.
The axiom of stages for the second theory follows directly from the rank component of the Axiom of Endomorphism in NFU
$^*$
. A rank in E in NFU
$^*$
translates via the interpretation to a stage in the second theory. The rank component of the Axiom of Endomorphism in NFU in effect tells us that if any element of
$V_{\alpha +1} \setminus V_\alpha $
(object of rank
$\alpha $
) is implemented as a
$\varepsilon $
extension,
$V_\alpha $
itself must be implemented as a
$\varepsilon $
extension. If
$\alpha $
is implemented, it triggers the implementation of
$V_\alpha $
.
Separation follows from the fact that the range of
$\textbf {E}$
is downward closed under inclusion, and the fact that formulas of the language of the second theory not mentioning j have stratified translations.
We observe that in NFU,
$\textbf {E}(\{V\}) = \{\textbf {E}(\{x\}):x \in V\}$
, so every
$j(x) \in j(V)$
, so every
$j(x) E V$
, so every
$j(x) {\, }\varepsilon {\, } V$
. Clearly also if
$u {\, } \varepsilon {\, } V$
, then
$u {\, } \in {\, } \textbf {E}(\{V\}) = \{\textbf {E}(\{x\}):x \in V\}$
, so
$u = j(x)$
for some x: the universe of NFU is
$j"V$
in the second theory.
This is very striking. The Boffa model construction gives us the models of NFU that we are familiar with. It seems that lots of information about the urelements (in some senses, most of the elements of the nonstandard stage used as the domain of the model!) is being discarded, since we seem to abandon their extensions. But this is not the case. The theory of the nonstandard stage and the theory of the resulting model of NFU are the same: their mathematics are exactly the same mod a difference of terminology. It seems quite magical to us that all the extensions of the urelements are packed into the existence of a single function in the model of NFU!
3 Is there a moral?
Yes, we think there is. A picture is emerging according to which theories like CUS (which is really just a sexed-up version of NF
$_2$
) can be synonymous with theories of wellfounded sets, whereas stronger theories like NF can’t. And that the obstacle (well, one obstacle) to NF being synonymous with theories like ZF is the fact that NF has stronger comprehension than NF
$_2$
and proves the existence of interesting and dangerous sets such as NO (the set of all ordinals) which no-one has ever succeeded in adding by a CO constructionFootnote
9
. These are (among) the sets that feature in what in [Reference Forster8] the first author called the recurrence problem. So there is a huge divide between NF
$_2$
and NF; on which side of that divide sits NF
$_3$
?
What about NFU? The basic synonymy result (our Theorem 1) tells us that neither NF nor NFU + Infinity + Choice (nor any invariant extension of either of these theories) can be synonymous with a theory of well-founded sets. However, any model of NFU built by the standard procedure adapted by Boffa from Jensen’s proof (see discussion in [Reference Forster7], p. 68) will satisfy the Axiom of Endomorphism and so support a theory synonymous with a theory of well-founded sets as exhibited here. The theory of the usual sort of model of NFU that we know how to construct is thus quite different from NF or even from stratified extensions of NFU in the respects discussed here.
Acknowledgments
The authors are grateful to Ali Enayat, Tim Button, Albert Visser, Nathan Bowler, John Truss, and Zachiri McKenzie for profitable and collegial conversations.
