What we shall try to do here is
to axiomatize the types in as
simple a way as possible so that
everyone can agree that the
idea is natural.
Scott (Reference Scott1974, p. 208)
The following bare-bones story introduces the idea of a cumulative hierarchy of pure sets:Footnote 1
The Basic Story. Sets are arranged in stages. Every set is found at some stage. At any stage
$\mathbf {s}$
: for any sets found before
$\mathbf {s}$
, we find a set whose members are exactly those sets. We find nothing else at
$\mathbf {s}$
.
This story says nothing at all about the height of any hierarchy, and apparently says almost nothing about the order-type of the stages. It lays down nothing more than the bare idea of a pure cumulative hierarchy. Surprisingly, though, this bare idea already guarantees that the sets are arranged in well-ordered levels. Indeed, this bare idea is quasi-categorical. Otherwise put: the Basic Story pins down any cumulative hierarchy completely, modulo that hierarchy’s height, on which the Story takes no stance. The aim of this paper is to show all of this.
I begin by axiomatizing the Basic Story in the most obvious way possible, obtaining Stage Theory, ST. It is clear that any pure cumulative hierarchy satisfies ST. Unfortunately, ST has multiple primitives. To overcome this, I develop Level Theory, LT. Its only primitive is
$\in $
, but LT and ST say exactly the same things about sets (see Sections 1–4). As such, any cumulative hierarchy satisfies LT. Moreover, LT proves that the levels are well-ordered, and LT is quasi-categorical (see Sections 5 and 6).
My theory LT builds on work by Dana Scott, Richard Montague, John Derrick, and Michael Potter. I discuss their theories in Section 8, but I wish to be very clear at the outset: LT is significantly technically simpler than its predecessors, but it owes everything to them.
This paper is the first in a triptych. In Part 2, I explore potentialism, by considering a tensed variation of the Basic Story. In Part 3, I modify the Story again, to provide every set with a complement. Part 2 presupposes Part 1, but Parts 1 and 3 can be read in isolation.
0 Preliminaries
I use second-order logic throughout. Mostly, though, my use of second-order logic is just for convenience. Except when discussing quasi-categoricity (see Section 6), any second-order claim can be replaced with a first-order schema in the obvious way. In using second-order logic, I assume the Comprehension scheme,
$\exists F\forall x(F(x) \leftrightarrow \phi )$
, for any
$\phi $
not containing ‘F’.
For readability, I concatenate infix conjunctions, writing things like
$a \subseteq r \in s \in t$
for
$a \subseteq r \land r \in s \land s \in t$
. I also use some simple abbreviations (where
$\Psi $
can be any predicate whose only free variable is x, and
$\lhd $
can be any infix predicate):
$$ \begin{align*} (\forall x : \Psi)\phi&\mathrel{\mathord{:}\mathord{=}} \forall x(\Psi(x) \rightarrow \phi), & (\forall x \lhd y)\phi&\mathrel{\mathord{:}\mathord{=}}\forall x(x \lhd y \rightarrow \phi),\\ (\exists x : \Psi)\phi&\mathrel{\mathord{:}\mathord{=}}\exists x(\Psi(x) \land \phi),& (\exists x \lhd y)\phi&\mathrel{\mathord{:}\mathord{=}}\exists x(x \lhd y \land \phi). \end{align*} $$
When I announce a result or definition, I list in brackets the axioms I am assuming.
1 Stage Theory
The Basic Story, which introduces the bare idea of a cumulative hierarchy, mentions sets and stages. To begin, then, I will present a theory which quantifies distinctly over both sorts of entities. (It is a simple modification of Boolos’s Reference Boolos1989 theory; see Sections 8.1 and 8.2.)
Stage Theory, ST, has two distinct sorts of variables, for sets (lower-case italic) and for stages (lower-case bold). It has three primitive predicates:
-
∈: a relation between sets; read ‘
$a \in b$
’ as ‘a is in b’, -
<: a relation between stages; read ‘
$\mathbf {r} < \mathbf {s}$
’ as ‘
$\mathbf {r}$
is before
$\mathbf {s}$
’, -
⪯: a relation between a set and a stage; read ‘
$a \preceq \mathbf {s}$
’ as ‘a is found at
$\mathbf {s}$
’.
For brevity, I write
$a \prec \mathbf {s}$
for
$\exists \mathbf {r}(a \preceq \mathbf {r} < \mathbf {s})$
, i.e., a is found before
$\mathbf {s}$
. Then ST has five axioms:Footnote
2
-
Extensionality
$\forall a \forall b( \forall x(x \in a \leftrightarrow x \in b) \rightarrow a = b)$
, -
Order
$\forall \mathbf {r} \forall \mathbf {s}\forall \textbf {t}(\mathbf {r} < \mathbf {s} < \textbf {t} \rightarrow \mathbf {r} < \textbf {t})$
, -
Staging
$\forall a \exists \mathbf {s}\ \, a \preceq \mathbf {s}$
, -
Priority
$\forall \mathbf {s} (\forall a \preceq \mathbf {s})(\forall x \in a)x \prec \mathbf {s}$
, -
Specification
$\forall F \forall \mathbf {s}((\forall x : F)x \prec \mathbf {s} \rightarrow (\exists a \preceq \mathbf {s})\forall x(F(x) \leftrightarrow x \in a))$
.
The first two axioms make implicit assumptions explicit: whilst I did not mention Extensionality in the Basic Story of a cumulative hierarchy, I take it as analytic that sets are extensional;Footnote
3
similarly, Order records the analytic fact that ‘before’ is a transitive relation. The remaining three axioms can then be read off the Basic Story directly: Staging says that every set is found at some stage; Priority says that a set’s members are found before it; and Specification says that, if we find every F before
$\mathbf {s}$
, then we find the set of Fs at
$\mathbf {s}$
. So all of ST’s axioms are obviously true of the Basic Story. Otherwise put: any cumulative hierarchy obviously satisfies ST.Footnote
4
This is ST’s chief virtue. Its chief drawback is that it contains multiple primitives. To see why this is a defect, suppose that we were forced to axiomatize the bare idea of a cumulative hierarchy using something like ST’s two-sorted logic. In that case, our grasp of the (cumulative iterative) notion of set would unavoidably depend upon a concept which we had not rendered set-theoretically, namely, stage of a hierarchy. And that would somewhat undercut the commonplace ambition, that our notion of set might serve as a certain kind of autonomous foundation for mathematics.
2 Level Theory
To overcome this problem, I present Level Theory, LT. This theory’s only primitive is
$\in $
, but it makes exactly the same claims about sets as ST does. I begin with a definition, due to Scott and Montague (see Section 8.3), which forms the linchpin of this paper:Footnote
5
Definition 2.1 For any a, let a’s potentiation be
, if it exists.Footnote
6
The name potentiation emphasises the conceptual connection with powersets; note that
.Footnote
7
The next two definitions employ this notion of potentiation (and thereby simplify definitions due to Derrick and Potter; see Section 8.4):Footnote
8
Definition 2.2 Say that h is a history, written Hist
$(h)$
, iff
. Say that s is a level, written Lev
$(s)$
, iff
.
The intuitive idea behind this definition is that a history is an initial sequence of levels, and that the levels go proxy for stages. It is not obvious that this will work as described; indeed, the next two sections are dedicated to establishing this fact. But, using the notion of a level, LT has just three axioms:Footnote 9
-
Extensionality
$\forall a \forall b (\forall x(x \in a \leftrightarrow x \in b) \rightarrow a =b)$
, -
Separation
$\forall F \forall a \exists b \forall x(x \in b \leftrightarrow (F(x) \land x \in a))$
, -
Stratification
$\forall a(\exists s : \textit{Lev})a \subseteq s$
.
3 The well-ordering of the levels
In Section 4, I will show that LT makes exactly the same claims about sets as ST does. First, I must develop the elements of set theory within LT. To do so, I need some more definitions:
Definition 3.1 Say that a is transitive iff
$(\forall x \in a)x \subseteq a$
. Say that a is potent iff
$\forall x(\exists c(x \subseteq c \in a) \rightarrow x \in a)$
.
Transitivity is completely familiar. Potency is discussed in a few places, albeit with no standard name.Footnote 10 As my choice of name suggests, though, there is a tight link between the operation of potentiation (see Definition 2.1) and the property of potency:
Lemma 3.2 If
exists, then
is potent.
Lemma 3.3 Extensionality
a is potent iff
.
Recall the conventions: Lemma 3.2 follows from the definitions alone, but Lemma 3.3 requires Extensionality. I leave the trivial proofs to the reader.
My aim now is to prove several results about levels, in the sense of Definition 2.2.Footnote 11 These results do not need LT’s Stratification axiom, since any sets which were not subsets of levels would be irrelevant.Footnote 12
Lemma 3.4 Every level is potent and transitive.
Proof Fix a level, s, so
, for some history h. Potency follows by Lemma 3.2. For transitivity, fix
; so
$a \subseteq c \in h$
for some c, and
as h is a history; so
.
Lemma 3.5 Extensionality, Separation
If every F is potent and something is F, then there is an
$\in $
-minimal F. Formally:
$\forall F((\exists x F(x) \land (\forall x : F)x \mathrm{\ is\ potent}) \rightarrow (\exists a : F)(\forall x : F)x \notin a)$
.
Proof Let F be as described and let u be an F. Using Separation twice, let:
$$ \begin{align*} c &= \{x \in u : (\forall y : F)x \in y\} = \{x : (\forall y : F)x \in y\},\\ d &= \{x \in c : x \notin x\}. \end{align*} $$
Clearly
$d \notin c$
, since otherwise
$d \in d \leftrightarrow d \notin d$
; so there is some a which is F with
$d \notin a$
. Now if x is F, then
$d \subseteq c \subseteq x$
, but
$d \notin a$
and a is potent, so
$x \notin a$
.
Lemma 3.6 Extensionality, Separation
If some level is F, then there is an
$\in $
-minimal level which is F. Formally:
$\forall F((\exists s : \textit{Lev})F(s) \rightarrow (\exists s: \textit{Lev})(F(s) \land (\forall r : \textit{Lev})(F(r) \rightarrow r \notin s)))$
.
Lemma 3.7 Extensionality, Separation
Every member of a history is a level.
Proof For reductio, let h be a history with some non-level in it. Since
for all
$c \in h$
, every member of h is potent by Lemma 3.2. Using Lemma 3.5, let a be an
$\in $
-minimal non-level in h. Now
, and
$a \cap h = \{x \in a : x \in h\}$
exists by Separation. So, to obtain our desired contradiction, it suffices to show that
$a \cap h$
is a history. Fix
$b \in a \cap h$
. So b is a level, by choice of a, and
as
$b \in h$
. If
$x \in b$
, then
$x \subseteq b$
, since b is transitive by Lemma 3.4; so
$x \in a$
, since a is potent as above; hence,
$b \subseteq a$
. So
. Generalising,
$a \cap h$
is a history.
Lemma 3.8 Extensionality, Separation
, for any level s.
Proof Let s be a level. If
$a \subseteq r \in s$
, then
$a \in s$
, as s is potent by Lemma 3.4. If
$a \in s$
, then as
for some history h, we have
for some r, and r is a level by Lemma 3.7.
Lemma 3.9 Extensionality, Separation
All levels are comparable.Footnote
13
Formally:
$(\forall s: \textit{Lev})(\forall t : \textit{Lev})(s \in t \lor s = t \lor t \in s)$
.
Proof For reductio, suppose that some levels are incomparable. By Lemma 3.6, there is an
$\in $
-minimal level, s, which is incomparable with some level; and by Lemma 3.6 again, there is an
$\in $
-minimal level, t, which is incomparable with s. To complete the reductio, I will show that
$s = t$
.
To show that
$s \subseteq t$
, fix
$a \in s$
. So
$a \subseteq r \in s$
for some level r, by Lemma 3.8. Now r is comparable with t, by choice of s. But if either
$r = t$
or
$t \in r$
, then
$t \in s$
as s is transitive, contradicting our assumption; so
$r \in t$
. Now
$a \subseteq r \in t$
, so that
$a \in t$
as t is potent. Generalising,
$s \subseteq t$
.
Exactly similar reasoning, based on the choice of t, shows that
$t \subseteq s$
. So
$t = s$
.
Rolling Lemmas 3.6 and 3.9 together, we obtain the fundamental theorem of level theory:
Theorem 3.10 Extensionality, Separation
The levels are well-ordered by membership.
Combining this result with Stratification, we obtain a powerful tool, which intuitively allows us to consider the level at which a set is first found:
Definition 3.11 LT
Let
$\ell a$
be the
$\in $
-least level with a as a subset; i.e.,
$a \subseteq \ell a$
and
$\lnot (\exists s : \textit{Lev})a \subseteq s \in \ell a$
.
Lemma 3.12 LT
For all sets
$a, b$
, and all levels
$r, s{:}$
-
(1)
$\ell a$
and
both exist, and
, -
(2)
$a \notin \ell a$
, -
(3)
$r\subseteq s$
iff
$s\notin r$
, -
(4)
$s = \ell s$
, -
(5) if
$b \subseteq a$
, then
$\ell b \subseteq \ell a$
, -
(6) if
$b \in a$
, then
$\ell b \in \ell a$
-
(7)
, -
(8) if every member of a is a level, then
.
Proof (1)
$\ell a$
exists by Stratification and Theorem 3.10. Now if
$x \subseteq c \in a \subseteq \ell a$
, then
$x \in \ell a$
since
$\ell a$
is potent; so
exists by Separation.
(2) There is no level t with
$a \subseteq t \in \ell a$
, so
$a \notin \ell a$
by Lemma 3.8.
(3) If
$r \subseteq s$
then
$s \notin r$
by the well-ordering of levels. Conversely, if
$s \notin r$
, then either
$r \in s$
or
$r = s$
by comparability; and
$r \subseteq s$
either way, as s is transitive.
(4) By (2),
$s \notin \ell s$
. By (3),
$\ell s \notin s$
. So
$s = \ell s$
, by comparability.
(5) If
$b \subseteq a$
then
$b \subseteq \ell a$
. So
$\ell a \notin \ell b$
, by definition of
$\ell b$
, so
$\ell b \subseteq \ell a$
by (3).
(6) If
$b \in a$
then
$b \in \ell a$
. By (2),
$b \notin \ell b$
; so
$\ell a \nsubseteq \ell b$
, and hence
$\ell b \in \ell a$
by (3).
(7) Let
$k = \{\ell x : x \in a\}$
. If
then
$c \subseteq \ell x$
for some
$x \in a$
; now
$\ell x \in \ell a$
by (6), so
$c \in \ell a$
. Conversely, if
$c \in \ell a$
then
$c \subseteq r \in \ell a$
for some level r by Lemma 3.8; since
$a \nsubseteq r$
by definition of
$\ell a$
, there is some
$x \in a \setminus r$
; now
$\ell x \notin r$
as r is potent, so that
$r \subseteq \ell x$
by (3) and hence
$c \subseteq \ell x$
; so
.
(8) In this case,
$a = \{\ell x : x \in a\}$
by (4), so
by (7).
4 The set-theoretic equivalence of ST and LT
Having explained how to work within LT, I will now make good on my earlier promise, and show that LT and ST make exactly the same claims about sets. More precisely, I will prove the following:
Theorem 4.1
$\mathrm{ST} \vdash \phi $
iff
$\mathrm{LT} \vdash \phi $
, for any
$\mathrm{LT}$
-sentence
$\phi $
.
To show that ST says no more about sets than LT does, I define a translation,
$*$
, from ST-formulas into LT-formulas. In effect,
$*$
treats stages as levels, ordered by membership. Specifically, its non-trivial actions are as follows:Footnote
14
$$ \begin{align*} (\mathbf {s} < \textbf{t})^* &\mathrel{\mathord{:}\mathord{=}} \mathbf {s} \in \textbf{t}, & (x \preceq \mathbf {s})^* &\mathrel{\mathord{:}\mathord{=}} x \subseteq \mathbf {s}, & (\forall \mathbf {s} \phi)^* &\mathrel{\mathord{:}\mathord{=}} (\forall \mathbf {s} : \textit{Lev})(\phi^*). \end{align*} $$
After translation, we treat all first-order variables—whether bold or italic—as being of the same sort. Fairly trivially, for any LT-sentence
$\phi $
, if
$\mathrm{ST} \vdash \phi $
then
$\mathrm{ST}^* \vdash \phi $
. The left-to-right half of Theorem 4.1 now follows from this simple observation, together with the fact that
$* : \mathrm{ST} \longrightarrow \mathrm{LT}$
is an interpretation:
Lemma 4.2 LT
$\mathrm{ST}^*$
holds.
Proof Extensionality
$^*$
is Extensionality. Staging
$^*$
is Stratification. Order
$^*$
holds by Lemma 3.4. Note that Lemma 3.8 allows us to simplify
$(x \prec \mathbf {s})^*$
, i.e.,
$(\exists \mathbf {r}(x \preceq \mathbf {r} < \mathbf {s}))^*$
, to
$(x \in \mathbf {s})$
. Now Priority
$^*$
holds trivially. And Specification
$^*$
holds as if
$(\forall x : F)x \in \mathbf {s}$
, then
$\{x : F(x)\} \subseteq \mathbf {s}$
by Separation.Footnote
15
To obtain the right-to-left half of Theorem 4.1, I must first prove some quick results in ST:
Lemma 4.3 ST
Separation holds.
Proof By Staging,
$a \preceq \mathbf {s}$
for some
$\mathbf {s}$
. By Priority,
$(\forall x \in a)x \prec \mathbf {s}$
. Now use Specification.
Lemma 4.4 ST
$\forall \mathbf {s}\forall a(a \preceq \mathbf {s} \leftrightarrow (\forall x \in a)x \prec \mathbf {s})$
.
Proof Left-to-right is Priority. For right-to-left, suppose
$(\forall x \in a)x \prec \mathbf {s}$
; then
$\{x : x \in a\} = a \preceq \mathbf {s}$
by Extensionality and Specification.
I next introduce slices. These will turn out to be levels, in the sense of Definition 2.2. Here is the definition of a slice, and some elementary results concerning slices:
Definition 4.5 For each
$\mathbf {s}$
, let
$\check {\mathbf {s}} = \{x : x \prec \mathbf {s}\}$
, if it exists. Say that a is a slice iff
$a = \check {\mathbf {s}}$
for some
$\mathbf {s}$
.
Lemma 4.6 ST
For any
$\mathbf {s}$
:
-
(1)
$\check {\mathbf {s}}$
exists, -
(2)
$\forall \mathbf {r}\forall a(a \preceq \mathbf {r} \leq \mathbf {s} \rightarrow a \preceq \mathbf {s})$
, -
(3)
$\forall a(a \subseteq \check {\mathbf {s}} \leftrightarrow a \preceq \mathbf {s})$
, -
(4)
$\check {\mathbf {s}}$
is transitive, -
(5)
.
Proof (1) By Specification and Extensionality.
(2) Let
$a \preceq \mathbf {r} \leq \mathbf {s}$
. Now
$(\forall x \in a)x \prec \mathbf {r}$
by Priority, so
$(\forall x \in a)x \prec \mathbf {s}$
by Order, and
$a \preceq \mathbf {s}$
by Lemma 4.4.
(3)
$a \subseteq \check {\mathbf {s}}$
iff
$(\forall x \in a)x \in \check {\mathbf {s}}$
iff
$(\forall x \in a)x \prec \mathbf {s}$
iff
$a \preceq \mathbf {s}$
by Lemma 4.4.
(4) If
$a \in \check {\mathbf {s}}$
, then
$a \preceq \mathbf {r} < \mathbf {s}$
for some
$\mathbf {r}$
; hence
$a \preceq \mathbf {s}$
and
$a \subseteq \check {\mathbf {s}}$
by (2) and (3).
(5) If
$a \in \check {\mathbf {s}}$
, then
$a \preceq \mathbf {r} < \mathbf {s}$
for some
$\mathbf {r}$
; hence
$a \subseteq \check {\mathbf {r}} \preceq \mathbf {r} < \mathbf {s}$
by (3), so
$a \subseteq \check {\mathbf {r}} \in \check {\mathbf {s}}$
. If
$a \subseteq \check {\mathbf {r}} \in \check {\mathbf {s}}$
, then
$a \subseteq \check {\mathbf {r}} \preceq \textbf {t} < \mathbf {s}$
for some
$\textbf {t}$
; now
$a \subseteq \check {\mathbf {r}} \subseteq \check {\textbf {t}}$
by (3), so
$a \preceq \textbf {t}$
by (3), i.e.,
$a \in \check {\mathbf {s}}$
.
It is now easy to show that
$\in $
well-orders the slices: just transcribe the proofs of Lemmas 3.6 and 3.9 within ST, replacing ‘levels’ with ‘slices’, noting that ST proves Separation (see Lemma 4.3), and replacing appeal to Lemmas 3.4 and 3.8 with Lemmas 4.6.4 and 4.6.5. We can then go on to prove that the levels are the slices.
Lemma 4.7 ST
s is a level iff s is a slice.
Proof For induction on slices, suppose:
$(\forall \check {\textbf {q}} \in \check {\mathbf {s}})(\forall a \subseteq \check {\textbf {q}})(a \mathrm{\ is\ a\ slice} \leftrightarrow \textit{Lev}(a))$
. I will show that
$(\forall a \subseteq \check {\mathbf {s}})(a \mathrm{\ is\ a\ slice} \leftrightarrow \textit{Lev}(a))$
. The result will follow by Staging and Lemma 4.6.3.
First, fix a level
$r \subseteq \check {\mathbf {s}}$
. Let
$h = \{q \in r : \textit{Lev}(q)\}$
; so
by Lemma 3.8. (Note that ST proves all of Lemmas 3.2–3.9, verbatim, since ST proves Separation.) Fix
$a \in r$
; so
$a \in \check {\mathbf {s}}$
, so
$a \subseteq \check {\textbf {q}} \in \check {\mathbf {s}}$
for some
$\check {\textbf {q}}$
by Lemma 4.6.5; hence, by the induction hypothesis, a is a slice iff a is a level. So
$h = \{\check {\textbf {q}} : \check {\textbf {q}} \in r\}$
. Noting that
$h \subseteq \check {\mathbf {s}}$
, let
$\check {\textbf {t}}$
be the
$\in $
-least slice such that
$h \subseteq \check {\textbf {t}}$
. Since r is transitive and the slices are well-ordered,
$h = \{\check {\textbf {q}} : \check {\textbf {q}} \in \check {\textbf {t}}\}$
. So
by Lemma 4.6.5, i.e., r is a slice.
Next, fix
$\check {\mathbf {r}} \subseteq \check {\mathbf {s}}$
. Let
$h = \{\check {\textbf {q}} : \check {\textbf {q}} \in \check {\mathbf {r}}\}$
; so
by Lemma 4.6.5; and
$h = \{q \in \check {\mathbf {r}} : \textit{Lev}(q)\}$
by the induction hypothesis. Fix
$q \in h$
; since
$\check {\mathbf {r}}$
is transitive,
$q \cap h = \{p \in q : \textit{Lev}(p)\}$
, so that
by Lemma 3.8. So h is a history and
is a level.
This allows us to prove the last axiom of LT within ST:
Lemma 4.8 ST
Stratification holds.
Proof Fix a; by Staging,
$a \preceq \mathbf {s}$
for some
$\mathbf {s}$
, i.e.,
$a \subseteq \check {\mathbf {s}}$
by Lemma 4.6.3, and
$\check {\mathbf {s}}$
is a level by Lemma 4.7.
So
$\mathrm{ST} \vdash \mathrm{LT}$
, completing the proof of Theorem 4.1.
5 The inevitability of well-ordering
A simple argument now establishes that LT axiomatizes the bare idea of a cumulative hierarchy of sets:
-
(a) Any cumulative hierarchy of sets satisfies ST (see Section 1).
-
(b) LT is set-theoretically equivalent to ST (see Theorem 4.1).
-
(c) So: any cumulative hierarchy of sets satisfies LT (from (a) and (b)).
Otherwise put: LT is true of the Basic Story I told at the start of this paper, and which I repeat here for ease of reference:
The Basic Story. Sets are arranged in stages. Every set is found at some stage. At any stage
$\mathbf {s}$
: for any sets found before
$\mathbf {s}$
, we find a set whose members are exactly those sets. We find nothing else at
$\mathbf {s}$
.
In fact, (c) takes on an even deeper significance when we reflect on just how bare-bones this Basic Story is. The Story says that some stages are ‘before’ others, and we can safely assume that ‘before’ is a transitive relation on stages (hence ST’s Order axiom).Footnote 16 But it is not obvious, for example, that it would be inconsistent to augment the Story by saying for every stage there is an earlier stage, or between any two stages there is another stage. This might prompt us to start entertaining cumulative hierarchies which are ordered like the integers, or the rationals, or more exotically still. A very simple argument, however, puts an abrupt end to such speculation:
-
(d) LT proves the well-ordering of the levels (see Theorem 3.10).
-
(e) So: any cumulative hierarchy of sets has well-ordered levels (from (c) and (d)).
Scott was the first to prove a well-ordering result from a similarly spartan starting point (see Section 8.3), and he put the point beautifully: ‘This at first surprising result shows how little choice there is in setting up the type hierarchy’.Footnote 17 Scott’s deep observation deserves to be much more widely known.
The connection between ST and LT also helps to demystify the definition of level. Working in ST, suppose that h is an initial sequence of slices; if
$\check {\mathbf {s}} \in h$
, then
$\check {\mathbf {s}} \cap h$
is the set of all slices less than
$\check {\mathbf {s}}$
, so that
by Lemma 4.6.5. These observations motivate Definition 2.2. We say that h is a history iff
, in the hope that, so defined, a history will be an initial sequence of slices; if it is, then the next slice in the sequence is the potentiation of that history, by Lemma 4.6.5; and this is how we define levels.
6 The quasi-categoricity of LT
We just saw that every cumulative hierarchy of sets has well-ordered levels. In fact, we can push this point further. By design, LT says nothing about the height of any hierarchy. But, as I will show in this section, LT is quasi-categorical. Informally, we can spell out LT’s quasi-categoricity as follows:
-
(f) Any two hierarchies satisfying LT are structurally identical for so far as they both run, but one may be taller than the other.
Since every cumulative hierarchy satisfies LT, we obtain:
-
(g) Any two cumulative hierarchies are structurally identical for so far as they both run, but one may be taller than the other (from (c) and (f)).
So, echoing Scott: when we set up a cumulative hierarchy, our only choice is how tall to make it.
It just remains to establish (f), i.e., to show that LT is quasi-categorical. In fact, there are at least two ways to explicate the informal idea of quasi-categoricity, and LT is quasi-categorical on both explications. (Note that both ways make essential use of second-order logic; this is the only section of the paper where my use of second-order logic is not merely for convenience.)
The first notion of quasi-categoricity is familiar from Zermelo. Working in some (set-theoretic) model theory, we define the
$V_\alpha $
s as usual:
$$ \begin{align*} V_0 & = \emptyset; & V_{\alpha + 1} & = \wp V_\alpha; & V_{\alpha} &= \bigcup_{\beta \in \alpha} V_\beta \mathrm{\ when\ } \alpha \mathrm{\ is\ a\ limit}. \end{align*} $$
Each
$V_\alpha $
then naturally yields a set-theoretic structure,
$\mathcal {V}_\alpha $
, whose domain is
$V_\alpha $
, and which interprets ‘
$\in $
’ as membership-restricted-to-
$V_\alpha $
, i.e.,
$\{\langle x, y\rangle \in V_\alpha \times V_\alpha : x \in y\}$
. We then have the following result, using full second-order logic:
$\mathcal {M} \vDash \mathrm{ZF}$
iff
$\mathcal {M} \cong \mathcal {V}_\alpha $
for some strongly inaccessible
$\alpha $
.Footnote
18
There is an analogous quasi-categoricity result for LT:Footnote
19
Theorem 6.1 In full second-order logic
$\mathcal {M} \vDash \mathrm{LT}$
iff
$\mathcal {M} \cong \mathcal {V}_\alpha $
for some ordinal
$\alpha> 0$
.
This shows that any two hierarchies satisfying LT (read that phrase as ‘any models of LT’) are structurally identical (read that phrase as ‘are isomorphic’) for so far as they both run (read that phrase in the light of the well-ordering of the
$V_\alpha $
s, established in the model theory). In short, LT is quasi-categorical, on a model-theoretic (‘external’) way of understanding quasi-categoricity.
There is also, though, an object-language (‘internal’) way to understand quasi-categoricity.Footnote 20 Since this idea is less familiar, I will spend some time unpacking it.
In embracing Extensionality, LT assumes that everything is a pure set. There is a quick-and-dirty way to avoid this assumption. First, introduce a new predicate, Pure; intuitively, this should apply to the pure sets. Next, relativise LT to Pure, via the following formula:Footnote 21
$$ \begin{align*} \mathrm{LT}(\textit{Pure}, \mathrel{\varepsilon}) \mathrel{\mathord{:}\mathord{=}}{} & (\forall a : \textit{Pure})(\forall b : \textit{Pure})(\forall x (x \mathrel{\varepsilon} a \leftrightarrow x \mathrel{\varepsilon} b)\rightarrow a = b) \land {} \\ & \forall F(\forall a: \textit{Pure})(\exists b : \textit{Pure})\forall x(x \mathrel{\varepsilon} b \leftrightarrow (F(x) \land x \mathrel{\varepsilon} a)) \land {}\\ & (\forall a : \textit{Pure})(\exists s : \textit{Lev})a \subseteq s \land{}\\ & \forall x \forall y(x \mathrel{\varepsilon} y \rightarrow (\textit{Pure}(x) \land \textit{Pure}(y))). \end{align*} $$
The first three conjuncts tell us that the pure sets satisfy LT;Footnote
22
the last says that, when we use ‘
$\mathrel {\varepsilon }$
’, we restrict our attention to membership facts between pure sets. Using this formula, I can now state the internal quasi-categoricity result (I have labelled the lines to facilitate its explanation):
Theorem 6.2 This is a deductive theorem of impredicative second-order logic
$:$
$$ \begin{align} &\kern-96pt(\mathrm{LT}(\textit{Pure}_1, \mathrel{\varepsilon}_1) \land \mathrm{LT}(\textit{Pure}_2,\mathrel{\varepsilon}_2))\rightarrow\nonumber\\[2pt] &\kern-68pt \exists R(\forall v \forall y(R(v,y) \rightarrow (\textit{Pure}_1(v) \land \textit{Pure}_2(y))) \land {} \end{align} $$
$$ \begin{align} & \kern-16pt((\forall v : \textit{Pure}_1)\exists y R(v,y) \lor (\forall y : \textit{Pure}_2)\exists v R(v,y)) \land {} \end{align} $$
$$ \begin{align} & \kern10pt\forall v\forall y\forall x\forall z ((R(v, y) \land R(x, z)) \rightarrow (v \mathrel{\varepsilon}_1 x \leftrightarrow y \mathrel{\varepsilon}_2 z))\land {} \end{align} $$
$$ \begin{align} & \kern-58pt\forall v \forall y\forall z ((R(v,y) \land R(v,z)) \rightarrow y = z)\land {} \end{align} $$
$$ \begin{align} & \kern-55pt\forall y \forall v\forall x ((R(v,y) \land R(x, y)) \rightarrow v= x)\land {} \end{align} $$
$$ \begin{align} &\kern-51pt \forall v (\exists y R(v, y) \rightarrow (\forall x \subseteq_1 \ell_1{v}) \exists z R(x, z))\land {} \end{align} $$
$$ \begin{align} & \kern-58pt\forall y (\exists v R(v, y) \rightarrow (\forall z \subseteq_2 \ell_2{y}) \exists x R(x, z))). \end{align} $$
Intuitively, the point is this. Suppose two people are using their versions of LT, subscripted with ‘
$1$
’ and ‘
$2$
’ respectively. Then there is some second-order entity, a relation R, which takes us between their sets (1), exhausting the sets of one or the other person (2); which preserves membership (3); which is functional (4) and injective (5); and whose domain is an initial segment of one (6) or the other’s (7) hierarchy. Otherwise put: LT is (internally) quasi-categorical.
As a bonus, this internal quasi-categoricity result can be lifted into an internal total-categoricity result. To explain how, consider this abbreviation (where ‘P’ is a second-order function-variable):
This formalizes the idea that there are as many
$\Phi $
s as there are objects simpliciter, i.e., that there is a bijection between the
$\Phi $
s and the universe. We can use this notation to state our internal total-categoricity result:
Theorem 6.3 This is a deductive theorem of impredicative second-order logic
$:$
Intuitively, if both LT-like hierarchies are as large as the universe, then there is a structure-preserving bijection between them. To see the significance of this result, note that it is common to claim that there are absolutely infinitely many pure sets. Whatever exactly this is meant to mean, it must surely entail that
. So Theorem 6.3 tells us that absolutely infinite LT-like hierarchies are (internally) isomorphic.
7 LT as a subtheory of ZF
I have shown that any cumulative hierarchy satisfies LT, so that, in setting up a cumulative hierarchy, our only freedom of choice concerns its height. To make all of this more familiar, though, it is worth commenting on LT’s relationship to ZF, the ‘industry standard’ set theory.
Unsurprisingly, ZF proves LT. In more detail: working in ZF, define the
$V_\alpha $
s as usual; we can then show that the
$V_\alpha $
s are the levels;Footnote
23
so Stratification holds as every set is a subset of some
$V_\alpha $
.
Of course, ZF is much stronger than LT, since LT deliberately says nothing about the height of the cumulative hierarchy. If we want to set up a tall hierarchy, then three axioms naturally suggest themselves (where ‘P’ is a second-order function-variable in the statement of Unbounded):Footnote 24
-
Endless
$(\forall s : \textit{Lev})(\exists t : \textit{Lev})s \in t$
, -
Infinity
$(\exists s : \textit{Lev})((\exists q : \textit{Lev})q \in s \land\\ \phantom{$(\exists s : \textit{Lev})$} (\forall q : \textit{Lev})(q \in s \rightarrow (\exists r : \textit{Lev})q \in r \in s)),$
-
Unbounded
$\forall P\forall a (\exists s : \textit{Lev})(\forall x \in a) P(x) \in s$
.
Endless says there is no last level. Infinity says that there is an infinite level, i.e., a level with no immediate predecessor. Unbounded states that the hierarchy of levels is so tall that no set can be mapped unboundedly into it. We now have some nice facts, whose proofs I leave to the reader:Footnote 25
Proposition 7.1
-
(1) LT proves Separation, Union, and Foundation.
-
(2)
$\mathrm{LT} + \textrm{Endless}$
proves Pairing and Powersets. -
(3)
$\mathrm{LT} + \textrm{Endless} + \textrm{Infinity}$
proves Zermelo’s axiom of infinity.Footnote
26
-
(4)
$\mathrm{LT} + \textrm{Endless} + \lnot \textrm{Infinity}$
is equivalent to
$\mathrm{ZF}_{{\mathrm {fin}}}$
.Footnote
27
-
(5)
$\mathrm{LT} + \textrm{Infinity} + \textrm{Unbounded}$
proves Endless. -
(6)
$\mathrm{LT} + \textrm{Infinity} + \textrm{Unbounded}$
is equivalent to
$\mathrm{ZF}$
.
Facts (1)–(3) show that
$\mathrm{LT} + \textrm {Endless} + \textrm {Infinity}$
extends Zermelo’s Z. This extension is strict, since Stratification is independent from Z.Footnote
28
Fact (6) then offers a neat way to conceive of ZF, as extending the theory which holds of any cumulative hierarchy, i.e., LT, with specific claims about the hierarchy’s height.
8 Conclusion, and LT’s predecessors
The theory LT holds of every cumulative hierarchy. Since LT is also quasi-categorical, the only choice we have, in setting up a cumulative hierarchy, is over the hierarchy’s height.
I will close this paper by discussing LT’s predecessors, in roughly chronological order.
8.1 Scott
At a talk in 1957, Scott presented what seems to have been the first theory of stages. This was an axiomatic theory of ranks, in the sense of the
$V_\alpha $
s. Writing ‘
$a < b$
’ for ‘a has lesser rank than b’, Scott’s suggested axioms were Extensionality and:Footnote
29
-
$\forall a \forall b(a < b \leftrightarrow (\exists x < b)x\nless a)$
,
-
$\forall F(\forall a((\forall x < a)F(x) \rightarrow F(a)) \rightarrow \forall a F(a))$
,
-
$\forall F\forall a \exists b \forall x(x \in b \leftrightarrow (F(x) \land x < a))$
.
This 1957 theory is clearly satisfied in any
$\mathcal {V}_\alpha $
with
$\alpha> 0$
, when
$\in $
and
$<$
are given the obvious interpretations. However, it has some unintended models.
Example 8.1 Let the domain have two sets
$: \ \emptyset $
and a Quine atom
$a = \{a\}$
. Let
$a < \emptyset $
. This is a model of the 1957 theory, since
$<$
is trivially a well-order, and since the only sets given by the third axiom are
$\emptyset $
and
$\{a\} = a$
.
Example 8.2 Let the domain have four sets
$: \ \emptyset $
,
$\{\emptyset \}$
,
$\{\{\emptyset \}\}$
, and
$\{\emptyset , \{\emptyset \}\}$
. Permute the usual rank relation, so that
$\{\emptyset \} < \emptyset < \{\{\emptyset \}\}, \{\emptyset , \{\emptyset \}\}$
, with
$\{\{\emptyset \}\}$
and
$\{\emptyset , \{\emptyset \}\}$
incomparable.
At a talk in 1967, Scott provided a vastly improved theory of stages. I will present the 1967 theory in a slightly simplified form, starting with a definition given later by Potter (see Section 8.4):
Definition 8.3 For each set a, let
$\mathrm{Acc}\mkern 1mu a = \{x : (\exists c \in a)(x \in c \lor x \subseteq c)\}$
, if it exists.
Scott’s 1967 theory treats the notion of level as a primitive, which applies to certain sets. Temporarily using bold-face letters to range over these levels, the 1967 theory comprises just Extensionality, Separation, and two further axioms:Footnote 30
-
Accumulation
$\forall \mathbf {s}\ \, \mathbf {s} = \mathrm{Acc}\mkern 1mu \{\mathbf {r} : \mathbf {r} \in \mathbf {s}\}$
, -
Restriction
$\forall a \exists \mathbf {s}\ \, a \subseteq \mathbf {s}$
.
Scott’s 1967 theory (unlike his 1957 theory) does not explicitly state that the levels are well-ordered; instead, the 1967 theory proves the well-ordering of the levels (cf. Section 5).Footnote 31 We have Scott to thank for a truly remarkable bit of mathematics-cum-conceptual-analysis.
Scott’s 1967 theory obviously inspires ST: compare his Restriction axiom with my Staging (and Stratification), and his Accumulation axiom with my Lemma 4.6.5 (and Lemma 3.8). Moreover, Scott’s 1967 theory and ST make exactly the same claims about sets (cf. Theorem 4.1). But I used ST in Section 1, rather than Scott’s 1967 theory, since ST is easier to motivate. In particular, Scott simply instructs us to write ‘
$\mathbf {s} \in \textbf {t}$
’ for ‘
$\mathbf {s}$
is before
$\textbf {t}$
’, and his justification of Accumulation amounts to stipulating that ‘a given level is nothing more than the accumulation of all the members and subsets of all the earlier levels’.Footnote
32
Both claims are very natural, and they are true in LT; but it is not immediately obvious that they are true of the Basic Story I told in the introduction. (In fairness to Scott, he does not start with that story, but with a related justificatory tale.)
8.2 Boolos and Shoenfield
The second source of inspiration for ST is Boolos. He first presented a theory of stages in Reference Boolos1971, which included explicit axioms stating that the stages are well-ordered;Footnote 33 this theory has several similarities with Shoenfield’s Reference Shoenfield1967 theory.Footnote 34 Boolos then presented a better theory of stages in Reference Boolos1989, explicitly drawing from Scott’s 1967 theory to prove (rather than assume) a principle of induction for stages.Footnote 35 My theory ST tweaks Boolos’s Reference Boolos1989 theory in three ways.
First. Boolos has qualms about how to justify Extensionality;Footnote 36 I have no such qualms.
Second. Boolos aims to vindicate the traditional Zermelian axioms of Foundation, Union, Pairing, Separation, Powersets, and Infinity. To secure these last two axioms, his Reference Boolos1989 theory contains:
-
Inf
$\exists \textbf {t}(\exists \mathbf {r} \ \mathbf {r} < \textbf {t} \land (\forall \mathbf {r} < \textbf {t})\exists \mathbf {s}(\mathbf {r} < \mathbf {s} < \textbf {t}))$
, -
Net
$\forall \mathbf {r} \forall \mathbf {s} \exists \textbf {t}(\mathbf {r} < \textbf {t} \land \mathbf {s} < \textbf {t})$
.
Boolos’s Inf guarantees there is a stage with infinitely many predecessors, and his Net guarantees that there is no last stage. Since ST is deliberately silent on the height of any cumulative hierarchy, it has no similar axioms. However, if I had wanted to augment ST with the claim that there is no last stage, I would have offered
$\forall \mathbf {s} \exists \textbf {t}\, \ \mathbf {s} < \textbf {t}$
(cf. Endless, from Section 7). Boolos’s Net says more than this; it guarantees that stages are directed. Boolos’s proof of Pairing relies upon this directedness,Footnote
37
but I cannot see why Boolos felt independently entitled to adopt Net rather than the weaker principle.
Third. The remainder of Boolos’s Reference Boolos1989 theory comprises Order, Staging, and these two axioms:Footnote 38
-
When
$\forall \mathbf {s} \forall a(a \preceq \mathbf {s} \leftrightarrow (\forall x \in a)x \prec \mathbf {s})$
, -
Spec
$\forall F \forall \mathbf {s} ((\forall x : F)x \prec \mathbf {s} \rightarrow \exists a\forall x(F(x) \leftrightarrow x \in a))$
.
In the presence of Extensionality, the axioms When+Spec are equivalent to ST’s Priority+Specification; but we need Extensionality to prove the right-to-left direction of When from Priority+Specification (see Lemma 4.4). Moreover, given Boolos’s qualms about Extensionality, he cannot provide an intuitive justification for the right-to-left direction of When. If
$(\forall x \in a)x \prec \mathbf {s}$
, then there should certainly be some
$b \preceq \mathbf {s}$
such that
$\forall x(x \in b \leftrightarrow x \in a)$
; but only Extensionality can justify the assertion that
$b = a$
. Crucially for Boolos’s aims, though, Powersets can fail if we replace When+Spec with Priority+Specification in Boolos’s theory: without Extensionality or the right-to-left direction of When, we might keep finding new empty sets at every stage in the hierarchy; there will then be no stage by which every subset of a set has been found, and hence no stage at which any powerset can be found.
8.3 Scott and Montague
I now want to return to Scott’s 1967 theory. As mentioned in Section 8.1, this theory initially takes the notion of level as primitive. However, Scott notes that the primitive can be eliminated, by proving within the 1967 theory that s is a level iff
. Scott developed this ideologically-spartan theory in joint work with Montague; they described their theory as ‘rank free’, so I will call it RF.Footnote
39
It has just three axioms: Extensionality, Separation, and
-
Hierarchy
.
The point of calling it ‘rank free’ was to highlight that RF takes no stance on the number of ranks in the hierarchy. More precisely, we have the external quasi-categoricity result that
$\mathcal {M} \vDash \mathrm{RF}$
iff
$\mathcal {M} \cong \mathcal {V}_\alpha $
for some
$\alpha> 0$
(assuming full second-order logic; cf. Theorem 6.1). To establish this, Montague and Scott first say that h is a hierarchy iff
. They then let
for each a, and show that
$\mathrm{R}a$
serves the role of a’s ‘rank’ (cf. LT’s notion of
$\ell a$
, as laid down in Definition 3.11).
Unfortunately, as Scott himself put it, the deductions from these axioms and definitions ‘are quite lengthy’.Footnote 40 This led Scott to dismiss the significance of RF, writing: ‘there seems to be no technical or conceptual advantage in reducing the number of primitive notions to the minimum’.Footnote 41
Still, these lengthy deductions were intended to form a section of a monograph on axiomatic set theory. A complete manuscript of this monograph exists, Montague et al. (Reference Montague, Scott and Tarskiunpublished), containing very minor markups, handwritten notes to the printers, and an accompanying list of ‘Things to be Done’ which amounts to nothing more than writing an Introduction and dealing with the mundane logistics of publication. Everything, in short, was almost ready to print.
Sadly, it was never printed. This was a serious loss. As explained in Section 1, there are good philosophical reasons for ‘reducing the number of primitive notions to the minimum’. Moreover, whilst Montague’s and Scott’s deductions were ‘quite lengthy’, the axioms of RF are quite elegant. The lengthiness of the deductions from RF is down to the awkwardness of the definitions of hierarchy and
$\mathrm{R}a$
. If Montague and Scott had been aware of the definition of history and level, as given in Definition 2.2, they could have given some much briefer deductions. Indeed, these definitions make it easy to prove that RF and LT are equivalent. One direction of this equivalence is easy:
Proposition 8.4 LT
RF holds.
Proof It suffices to prove Hierarchy. Fix a, let
$h = \{s \in \ell a : \textit{Lev}(s)\}$
and fix
$k \subseteq h$
. Now
by Lemma 3.12.8; so if
, then
$\ell k \notin \ell a$
, so
by Lemma 3.12.3.
For the other direction of the equivalence, I must first prove some quick facts in RF:
Lemma 8.5 RF
For all
$a\!{:}$
-
(1) if
exists, then
, -
(2)
exists, -
(3) if every member of a is a level, then
is a level.
Proof (1) If
, then
. But this is impossible: by Separation, let
; then
.
(2) Fix a, and let h witness Hierarchy. Let
$k = h$
, so that
exists and
, i.e.,
by (1). Since
is potent by Lemma 3.2,
exists by Separation on
.
(3) Using Separation and (2), let
. I will first prove that
, and then that h is a history, so that
is a level.
To see that
: since
, we have
by Lemmas 3.2 and 3.3; and if
then
$x \subseteq r \in a$
for some level r, so
$r \in h$
, and hence
.
To see that h is a history, fix
$s \in h$
; it suffices to show that
. Since s is a level,
by Lemmas 3.3 and 3.4. To see that
, fix
$x \in s$
; now
$x \subseteq r \in s$
for some level r by Lemma 3.8; and
by Lemma 3.4, so
by Lemma 3.2 and hence
$r \in h$
; so
$x \subseteq r \in (s \cap h)$
, i.e.,
.
Proposition 8.6 RF
LT holds.
Proof It suffices to prove Stratification. Fix a, and let h witness Hierarchy, i.e.,
. Let
$k = \{s \in h : \textit{Lev}(s)\}$
. By Lemma 8.5.3,
is a level. Now if
, then
, contradicting Lemma 8.5.1; so
.
This last proof helps to explain the intuitive idea behind RF’s axiom Hierarchy.Footnote
42
Roughly, the h guaranteed to exist by Hierarchy has this property: for any initial sequence of levels
$k \subseteq h$
, the next level after all of them is
; and if a is not a subset of
, then
is in h; and hence (but here I invoke a transfinite induction) the members of h are all the levels up to the first level including a. In short, the fundamental idea behind RF is quite elegant.
8.4 Derrick and Potter
As mentioned in Section 2, my definition of level is inspired by Derrick and Potter,Footnote
43
but I have simplified it. Here is a little more detail about that simplification. In his 1990 book, Potter explicitly built on Scott’s 1967 theory and also on Derrick’s unpublished lecture notes.Footnote
44
Now, Scott’s Accumulation axiom (see Section 8.1) formalizes the claim that ‘a given level is nothing more than the accumulation of all the members and subsets of all the earlier levels’.Footnote
45
This suggests the use of the
$\mathrm{Acc}\mkern 1mu $
-operator, and so Potter offers Definition 8.3.Footnote
46
Potter then supplies the definition of history and level given in Definition 2.2, but using
$\mathrm{Acc}\mkern 1mu $
rather than
. So, Potter stipulates that h is a history iff
$(\forall x \in h)x = \mathrm{Acc}\mkern 1mu (x \cap h)$
, and that s is a level iff
$s = \mathrm{Acc}\mkern 1mu h$
for some history h. Potter then proves that, so defined, the levels are well-ordered. And his own theory of levels is, in effect, just LT, with this slightly different explicit definition of ‘Lev’.Footnote
47
But the use of
, rather than
$\mathrm{Acc}\mkern 1mu $
, simplifies things significantly, as illustrated by the brevity of Section 3.
Appendix A. Adding urelements
In this paper, I restricted my attention to pure sets.Footnote 48 This was only for ease of exposition; in this appendix and the next, I will remove this simplifying assumption.
To accommodate urelements, we must tweak the Basic Story. The easiest way to do this (which I revisit in Appendix B) is to assume that the urelements are ‘always’ available to be collected into sets:
The Urelemental Story. Sets are arranged in stages. Every set is found at some stage. At any stage
$\mathbf {s}$
: for any things, each of which is either a set found before
$\mathbf {s}$
or an urelement, we find a set whose members are exactly those things. We find nothing else at
$\mathbf {s}$
.
To formalize this Story, we need a new primitive predicate, enabling us to distinguish sets from urelements: we take Set as primitive, and define
${Ur}(x) \mathrel {\mathord {:}\mathord {=}} \lnot {Set}(x)$
. Stage Theory with Urelements, STU, now has six axioms:Footnote
49
-
Empty-U
$(\forall u : {Ur})\forall x\ \, x \notin u$
, -
Ext-U
$(\forall a : {Set})(\forall b : {Set})( \forall x(x \in a \leftrightarrow x \in b) \rightarrow a = b)$
, -
Order
$\forall \mathbf {r} \forall \mathbf {s}\forall \textbf {t}(\mathbf {r} < \mathbf {s} < \textbf {t} \rightarrow \mathbf {r} < \textbf {t})$
, -
Staging-U
$(\forall a : {Set})\exists \mathbf {s}\, \ a \preceq \mathbf {s}$
, -
Priority-U
$\forall \mathbf {s}(\forall a : {Set})(a \preceq \mathbf {s} \rightarrow (\forall x \in a)({Ur}(x) \lor x \prec \mathbf {s}))$
, -
Spec-U
$\forall F \forall \mathbf {s}((\forall x : F)({Ur}(x) \lor x \prec \mathbf {s}) \rightarrow \phantom{$\forall F \forall \mathbf {s}$}(\exists a : {Set})(a \preceq \mathbf {s} \land \forall x(F(x) \leftrightarrow x \in a))).$
Empty-U says that no urelement has any members; the other axioms relativise ST to sets. As in Section 1, any cumulative hierarchy obviously satisfies STU, on the assumption that the urelements are all ‘always’ available to be arbitrarily collected into sets.
We obtain Level Theory with Urelements, LTU, by tweaking LT’s key definitions. Specifically, I offer the following re-definition:Footnote 50
Definition A.1 For Appendix A only
Say that a is potent iff
$\forall x(({Ur}(x) \lor (\exists c: {Set})x \subseteq c \in a) \rightarrow x \in a)$
. Let
, if it exists. Say that Hist
$(h)$
iff
. Say that Lev
$(s)$
iff
.
The axioms of LTU are then Empty-U, Ext-U, Stratification (with ‘Lev’ as redefined), and:Footnote 51
-
Sep-U
$\forall F\forall a(\exists b : {Set})\forall x(x \in b \leftrightarrow (F(x) \land x \in a))$
.
The proofs of Sections 3 and 4 go now through with trivial changes. Specifically, the (redefined) levels are well-ordered, and STU and LTU make exactly the same demands on sets and urelements.
The (quasi-)categoricity results of Section 6 also carry over to LTU. Let
$\mathcal {A}$
and
$\mathcal {B}$
be models of LTU in full second-order logic, and suppose there is a bijection between their respective collections of urelements,
${Ur}^{\mathcal {A}}$
and
${Ur}^{\mathcal {B}}$
. This bijection can be lifted to a quasi-isomorphism:
$\mathcal {A}$
and
$\mathcal {B}$
are isomorphic ‘so far as they go’, but the levels of one may outrun the other. This external result can also be ‘internalised’, yielding results analogous to Theorems 6.2 and 6.3.
Note that LTU, like LT before it, takes no stance on the height of the hierarchy. In particular, it has no version of Replacement. In this regard, LTU differs sharply from ZF(C)U, which is something like the ‘industry standard’ for iterative set theory with urelements. It is particularly noteworthy that LTU allows that the set of urelements may be larger than any pure set.Footnote
52
(For a trivial example, suppose there are exactly three urelements and exactly two levels; for a less trivial example, suppose there are exactly
$\beth _{\omega +1}$
urelements but only an
$\omega +\omega $
sequence of levels.)
Appendix B. Adding absolutely infinitely many urelements
The Urelemental Story accommodates urelements in a humdrum way. However, there has been recent interest in a less humdrum approach, according to which there are absolutely infinitely many urelements. Here is a brisk, three-premise argument in favour of that approach, inspired by Christopher Menzel:Footnote 53
-
(a) There are absolutely infinitely many levels in the cumulative hierarchy.
-
(b) There are at least as many ordinals as there are levels in the cumulative hierarchy.
-
(c) Ordinals are not really sets; they are urelements.
Each premise is not implausible,Footnote 54 and they jointly entail that there are absolutely infinitely many urelements. In this appendix, I will explore that idea (without endorsing it).
B.1 Preliminary motivations and observations
There is an immediate technical issue: in this kind of cumulative setting, no set has absolutely infinitely many members.Footnote
55
This follows from a simple version of Cantor’s Theorem. For reductio, suppose that some set, a, has absolutely infinitely many members. As discussed in Section 6, this entails that
, i.e., there is a map, P, such that
$\forall x\ P(x) \in a$
and
$(\forall y \in a)\exists !\! x\ P(x) = y$
. By P’s injectivity and Separation,Footnote
56
there is some
$d = \{x \in a : x \notin P^{-1}(x)\}$
. Since
$P(d) \in a$
, contradiction follows familiarly.
So: if there are absolutely infinitely many urelements, then there is no set of all urelements.Footnote 57 But the existence of such a set is a trivial consequence of Spec-U, as laid down in Appendix A. So, those who think that there are absolutely infinitely many urelements must reject Spec-U. Furthermore, since Spec-U follows from the third sentence of the Urelemental Story of Appendix A, they must change their story.
Many alternative stories are possible, but the simplest approach is simply to bolt a Limitation of Size principle onto the Urelemental Story, insisting that the Basic Story remains correct of the pure sets, whilst denying that any set is absolutely infinite. This leads to the following:Footnote 58
The
relemental Story. Sets are arranged in stages. Every set is found at some stage. At any stage
$\mathbf {s}$
: for any things—provided both that (i) there are not absolutely infinitely many of them, and that (ii) each of them is either a set found before
$\mathbf {s}$
or an urelement—we find a set whose members are exactly those things. We find nothing else at
$\mathbf {s}$
. (NB: since the Basic Story is correct of the pure sets, we do not find absolutely infinitely many pure sets before
$\mathbf {s}$
.)
In the remainder of this appendix, I will briefly sketch (equivalent) stage-theoretic and level-theoretic formalizations of this Story. For readability, I leave all proofs to the reader, with hints in footnotes.
B.2 The stage-theoretic approach
To axiomatize the
relemental Story, we need a predicate, ‘Pure’, to pick out the pure sets (cf. Section 6). Since we have assumed that the Basic Story holds of the pure sets, we can define ‘Pure’ explicitly:
Definition B.1 Say that a is pure, Pure
$(a)$
, iff both Set
$(a)$
and there is some transitive
$c \supseteq a$
whose members are all sets.
To axiomatize the
relemental Story, we also need a way to formalize ‘there are absolutely infinitely many
$\Phi $
s’. There are familiar concerns about the possibility of formalizing this idea.Footnote
59
Nonetheless, if there are absolutely infinitely many
$\Phi $
s, then certainly
(cf. Section 6). Conversely, if
, then no property can have more instances than
$\Phi $
. So, ‘
’ will serve as our proxy for ‘there are absolutely infinitely many
$\Phi $
s’.Footnote
60
I can now lay down the theory
. Its axioms are Empty-U, Ext-U, Order, Staging-U, Priority-U, and the following:
-
Spec-
$\phantom{\forall F \forall \mathbf {s}}(\exists a : {Set})(a \preceq \mathbf {s} \land \forall x(F(x) \leftrightarrow x \in a)))$
, -
LoS-
, -
Pure-
, -
Many-
.
In brief: Spec-
restricts Spec-U to capture conditions (i) and (ii) of the
relemental Story; LoS-
enshrines Limitation of Size, which follows from condition (i) plus the fact that ‘we find nothing else’ at any stage; Pure-
formalizes the parenthetical ‘NB’ of the Story; and Many-
formalizes the claim that there are absolutely infinitely many urelements.
B.3 The level-theoretic approach
is a multi-sorted, stage-theoretic, formalization of the
relemental Story. That Story can instead be given a single-sorted formalization,
. To do this, I start by tweaking LT’s key definitions:
Definition B.2 For Appendix B only
Say that a is potent iff
$(\forall x : {Set})(\exists c(x \subseteq c \in a) \rightarrow x \in a)$
. Let
, if it exists. Say that Hist
$(h)$
iff
. Say that Lev
$(s)$
iff
.
Using these redefinitions, we can prove analogues of Lemmas 3.4–3.9 from Section 3. Specifically, given Ext-U and Sep-U, we can prove that the levels (so defined) are potent, transitive, pure,Footnote
61
and well-ordered by
$\in $
.
I can now lay down
. It uses a primitive one-place function symbol,
${\textbf {L}}$
, where ‘
${\textbf {L}}a$
’ should be read as a’s level-index. (I discuss the use of this primitive in Section B.4, below.) Then
has six axioms: Empty-U, Ext-U, LoS-
, Many-
, and two axioms governing
${\textbf {L}}$
:
-
Leveller
$(\forall a : {Set})((\exists s : \textit{Lev}){\mathbf{L}}a = s \land {}$
$\kern-2.5pc\phantom {(\forall a : {Set})(}(\forall x : {Set})(x \in a \rightarrow {\mathbf{L}}x \in {\mathbf {L}}a) \land {}$
$\kern-2.5pc\phantom {(\forall a : {Set})(}(\forall s : \textit{Lev})(s \in \mathrm{\textbf {L}}a \kern1.2pt{\rightarrow}\kern1.2pt (\exists x : {Set})$
$\kern-2.5pc\phantom {(\forall a : {Set})(}(x \kern1.2pt{\in}\kern1.2pt a \land s \kern1.2pt{\subseteq}\kern1pt {\mathbf {L}}x)))$
, -
Consolidation
.
To understand these axioms, note that
guarantees that the (pure) levels are well-ordered by membership.Footnote
62
Now, Leveller ensures that the levels index the sets; intuitively, a’s level-index is the least level greater than the level-index of every set in a. Consolidation then allows us to find all the impure sets we would want to find ‘at’ any given level. Finally, note that
proves a pure-analogue of Stratification:Footnote
63
Lemma B.3
If a is pure, then
$a \subseteq {\textbf{L}}a$
.
Consequently,
’s pure sets can be thought of as satisfying LT. Indeed, if we define ‘
$x \mathrel {\varepsilon } y$
’ as ‘
$\textit{Pure}(x) \land \textit{Pure}(y) \land x \in y$
’, then
, as defined in Section 6. It follows that
is externally and internally (quasi-)categorical: any two hierarchies satisfying
have quasi-categorical pure sets; moreover, if there is a bijection between the hierarchies’ urelemental bases, their impure sets are quasi-categorical. (However,
’s analogue of Theorem 6.1 is more restricted: if
$\mathcal {M}$
is a standard, set-sized, model of
, then
$|{Ur}^{\mathcal {M}}|$
is regular.)Footnote
64
In fact,
and
are provably equivalent, concerning sets and urelements. To prove that
interprets
, tweak the
$*$
-translation of Section 4, so that
$(x \preceq \mathbf {s})^* \mathrel {\mathord {:}\mathord {=}} {\textbf {L}}x \subseteq \mathbf {s}$
.Footnote
65
It is then easy to show that
(cf. Lemma 4.2).
To show that
interprets
, first note that
proves Sep-U and the converse of Priority-U (cf. Lemmas 4.3 and 4.4). Then tweak Definition 4.5 (cf. Definition B.2):
Definition B.4 For Appendix B only
Let
$\check {\mathbf {s}} \mathrel {\mathord {:}\mathord {=}} \{x \prec \mathbf {s} : \textit{Pure}(x)\}$
. Say that a is a slice iff
$a = \check {\mathbf {s}}$
for some
$\mathbf {s}$
.
It follows that the slices are the levels (in the senses of Definitions B.2 and B.4; cf. Lemma 4.7).Footnote
66
We can then interpret
’s unique primitive,
${\textbf {L}}$
, via
$\rho $
, defined as follows:Footnote
67
Definition B.5. For each set a, let
$\rho a \mathrel {\mathord {:}\mathord {=}} \bigcap \{\check {\mathbf {s}} : a \preceq \mathbf {s} \land \lnot \exists \mathbf {r}(a \preceq \mathbf {r} < \mathbf {s})\}$
.
Theorem B.6
iff
, for any
-sentence
$\phi $
, where
$\phi ^\rho $
is the formula which results from
$\phi $
by replacing each instance of
${\textbf{L}}$
with
$\rho $
.
The upshot is that no information about sets or urelements is lost or gained in moving from
to
. Since any hierarchy which is described by the
relemental Story satisfies
, it also satisfies
. And
is quasi-categorical. Our work on the
relemental Story is complete.
B.4 Eliminating primitives
Or rather: almost complete. Given the discussion of Section 1, we may want to eliminate
’s unique primitive,
${\textbf {L}}$
. This is easily done within second-order logic: just conjoin Leveller and Consolidation, and bind
${\textbf {L}}$
with a (second-order) existential quantifier. But if we are willing to make some further assumptions, then we can eliminate
${\textbf {L}}$
using certain first-order functions.Footnote
68
Roughly, a ranking-function: (1) has a transitive domain (setting aside urelements); and (2) behaves like
${\textbf {L}}$
where defined. More formally:
Definition B.7. Say that a function f is a ranking-function iff, for all
$a \in \mathrm{dom}(f)$
, both
$:$
-
(1) Set
$(a)$
and
$(\forall x : {Set})(x \in a \rightarrow x \in \mathrm{dom}(f));$
and -
(2) Lev
$(f(a))$
and
$(\forall x : {Set})(x \in a \rightarrow f(x) \in f(a))$
and
$(\forall s : \textit{Lev})(s \in f(a) \rightarrow (\exists x \in a)s \subseteq f(x))$
.
Say that Ranks
$(f, a)$
iff f is a ranking-function with
$a \in \mathrm{dom}(f)$
.
It is easy to show that ranking-functions agree wherever they are defined, i.e.:
Lemma B.8 Ext-U, Sep-U
If Ranks
$(f, a)$
and Ranks
$(g, a)$
, then
$f(a) = g(a)$
.
We can now replace Leveller, in
, with
$(\forall a : {Set})\exists f\, {Ranks}(f, a)$
. Note that this claim is independent of
: it guarantees that every set is a member of some set, and so guarantees that the hierarchy has no final stage (cf. Endless from Section 7). Still, this allows us to define
${\textbf {L}}a \mathrel {\mathord {:}\mathord {=}} \bigcap \{f(a) : {Ranks}(f, a)\}$
. We can use this definition in Consolidation, and prove Leveller via Definition B.7.
Acknowledgments
Thanks to Neil Barton, Sharon Berry, Luca Incurvati, Juliette Kennedy, Øystein Linnebo, Michael Potter, Chris Scambler, Will Stafford, James Studd, Rob Trueman, Gabriel Uzquiano, Sean Walsh, and anonymous referees for this journal.
