Like all walls it was ambiguous,
two-faced. What was inside it
and what was outside it
depended upon which side you
were on.
Le Guin (Reference Le Guin1974, p. 1)
Building on work by Alonzo Church and Urs Oswald, Thomas Forster has provided a pleasingly different way to think about sets. As in the ordinary cumulative hierarchy, the sets are stratified into well-ordered levels. But, unlike the ordinary cumulative picture, the sets form a boolean algebra. In particular, every set has an absolute complement, in the sense that
$\forall a \exists c \forall x(x \in a \leftrightarrow x \notin c)$
. In this paper, I develop an axiomatic theory for this conception of set: Boolean Level Theory, or BLT.
I start by outlining the bare-bones idea of a complemented hierarchy of sets, according to which sets are arranged in stages, but where each set is found alongside its complement. I axiomatize this bare-bones story in the most obvious way possible, obtaining Boolean Stage Theory, BST. It is clear that any complemented hierarchy satisfies BST (see Sections 1 and 2). Unfortunately, BST has multiple primitives. To overcome this, I develop Boolean Level Theory, BLT. The only primitive of BLT is
$\in $
, but BLT and BST say exactly the same things about sets. As such, any complemented hierarchy satisfies BLT. Moreover, BLT is quasi-categorical (see Sections 3–5). I then provide two interpretations using
$\mathrm{BLT}_{\mathrm{ZF}}$
(an obvious extension of BLT): we can regard ZF as a proper part of
$\mathrm{BLT}_{\mathrm{ZF}}$
; but ZF is definitionally equivalent to
$\mathrm{BLT}_{\mathrm{ZF}}$
(see Sections 6 and 7). I close by explaining how to implement Conway’s games and surreal numbers in BLT (see Section 8).
This paper is the third in a triptych. It closely mirrors Part 1, but can be read in isolation. Let me repeat, though, that Part 1 is hugely indebted to the work of Dana Scott, Richard Montague, George Boolos, John Derrick, and Michael Potter; this paper inherits those debts.Footnote 1
Some remarks on notation (which is exactly as in Pt.1 Section 0). I use second-order logic throughout. Mostly, though, this is just for convenience. Except when discussing quasi-categoricity (see Section 5), any second-order claim can be replaced with a first-order schema in the obvious way. I 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*} $$
I also 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$
. And I run these devices together; so
$(\forall x \notin x \in a)x \subseteq a$
abbreviates
$\forall x((x \notin x \land x \in a) \rightarrow x \subseteq a)$
. When I announce a result or definition, I list in brackets the axioms I am assuming. For readability, all proofs are relegated to the appendices.
1 The complemented story
Here is a very natural image of sets: sets are not just collections of objects; sets partition the universe, and both sides of the partition yield a set. There is the set of sheep; and there is the set of non-sheep. There is the set of natural numbers; and there is the set of everything else. There is the empty set; and there is the universal set.
Many will reject this image out of hand. Supposedly, the paradoxes of naïve set theory have taught us that there is no universal set; for if there were a universal set
$V = \{x : x=x\}$
, then Separation would entail the existence of the Russell set
$\{x : x \notin x\}$
, which is a contradiction.
That reasoning, though, is too quick. Separation is incompatible with the existence of V.Footnote 2 More generally, Separation is incompatible with the principle of Complementation (i.e., with the principle that every set has an absolute complement). But it does not immediately follow that Complementation is false; only that we must choose between Separation and Complementation.
Both principles are very natural. Separation, however, has the weight of history behind it; and this might not merely be a historical accident. There is a serious argument in favour of Separation and against Complementation, which runs as follows. The paradoxes of naïve set theory forced us to develop a less naïve conception of set. The best such conception (according to this argument) is the cumulative iterative conception, as articulated by this bare-bones story (recycled from Pt.1):
The Basic Story. Sets are arranged in stages. Every set is found at some stage. At any stage s: for any sets found before s, we find a set whose members are exactly those sets. We find nothing else at s.
It is easy to see that this conception of set yields Separation rather than Complementation: any subset of a set a occurs at (or before) any stage at which a itself occurs. So (the argument concludes) we should embrace Separation and reject Complementation.
I take this argument very seriously. However, its success hinges on whether the ordinary cumulative iterative conception really is the ‘best’ conception of set. Whatever exactly ‘best’ is supposed to mean, the argument lays down a challenge: produce an equally good or better conception of set, which accepts Complementation and rejects Separation.
This paper considers a very specific reply to this challenge, due to Forster’s development of work by Church and Oswald.Footnote 3 Forster’s idea is to make a small tweak to the story of the ordinary hierarchy, so that ‘each time we [find] a new set…we also [find] a companion to it which is to be its complement’.Footnote 4 In slightly more detail, we offer the following bare-bones story:
The Complemented Story. Sets are arranged in stages. Every set is found at some stage. At any stage s: for any sets found before s, we find both
-
(Lo) a set whose members are exactly those sets, and
-
(Hi) a set whose non-members are exactly those sets.
We find nothing else at s.
According to our new story, we find each set using either clause (Lo) or clause (
${Hi}$
). Moreover, if we find a set using clause (Lo), then we find its absolute complement using clause (
${Hi}$
), and vice versa. This is the absolute complement since, in clause (
${Hi}$
), we quantify over all sets that will ever be discovered, not just those discovered before stage s. This story therefore secures Complementation; it describes the bare idea of a complemented hierarchy of sets. But it only describes the bare idea, since, for example, it says nothing about the height of the hierarchy.
In what follows, I will develop an axiomatic theory of this story, and explore that theory’s behaviour. To be clear: I am not claiming that we should reject the ordinary hierarchy in favour of the complemented. My aim is only to provide a coherent (and surprisingly elegant) conception of set which allows for Complementation rather than Separation.
In what follows, I will speak of low sets and high sets.Footnote
5
A set is low iff we find it using clause (Lo); we characterize low sets by saying ‘exactly these things, which we found earlier, are this set’s members’. The limiting case of a low set is the empty set,
$\emptyset $
. A set is high iff we find it using clause (
${Hi}$
); we characterize high sets by saying ‘exactly these things, which we found earlier, are omitted from this set’. The limiting case of a high set is the universe, V. (Note that low sets can have high sets as members, e.g.,
$\{V\}$
would be a low set with a high member.)
2 Boolean Stage Theory
Given a model of ZF, there are simple methods for constructing models of the complemented hierarchy.Footnote 6 However, if the idea of a complemented hierarchy is genuinely to rival that of the ordinary hierarchy, it cannot remain parasitic upon ZF; it needs a fully autonomous theory. I will provide such a theory over the next two sections.Footnote 7
The Complemented Story, which introduces the bare-bones idea of a complemented hierarchy, speaks of both stages and sets. To begin, then, I will present a theory which quantifies distinctly over both sorts of entities. Boolean Stage Theory, or BST, has two distinct sorts of first-order variable, for sets (lower-case italic) and for stages (lower-case bold). It has five 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}$
’ -
$\preceq:$
a relation between a set and a stage; read ‘
$a \preceq \mathbf{s}$
’ as ‘a is found at
$\mathbf{s}$
’
-
Lo: a property of sets; read ‘
${Lo}(a)$
’ as ‘a is low’, i.e., we find a using clause (Lo) -
Hi: a property of sets; read ‘
${Hi}(a)$
’ as ‘a is high’, i.e., we find a using clause (
${Hi}$
)
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 BST has eight axioms:Footnote
8
-
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 \mathbf{t}(\mathbf{r} < \mathbf{s} < \mathbf{t} \rightarrow \mathbf{r} < \mathbf{t})$
-
Staging
$\forall a \exists \mathbf{s}\, \ a \preceq \mathbf{s}$
-
Cases
$\forall a({Lo}(a) \lor {Hi}(a))$
-
Priority
$_{{Lo}}$
$\forall \mathbf{s} (\forall a : {Lo})(a \preceq \mathbf{s} \rightarrow (\forall x \in a)x \prec \mathbf{s})$
-
Priority
$_{{Hi}}$
$\forall \mathbf{s}(\forall a: {Hi})(a \preceq \mathbf{s} \rightarrow (\forall x \notin a)x \prec \mathbf{s})$
-
Specification
$_{{Lo}}$
$\forall F \forall \mathbf{s}((\forall x : F)x \prec \mathbf{s} \rightarrow \hspace{10pt}(\exists a : {Lo})(a \preceq \mathbf{s} \land \forall x(F(x) \leftrightarrow x\in a)))$
-
Specification
$_{{Hi}}$
$\forall F \forall \mathbf{s}((\forall x : F)x \prec \mathbf{s} \rightarrow \hspace{10pt}(\exists a : {Hi})(a \preceq \mathbf{s} \land \forall x(F(x) \leftrightarrow x \notin a)))$
I will now explain how to justify each axiom.
The first two axioms make implicit assumptions explicit. Whilst I did not mention Extensionality when I told the story of the complemented hierarchy, I take it as analytic that sets are extensional.Footnote 9 Similarly, Order records the analytic fact that ‘before’ is transitive. Note, though, that I do not explicitly assume that the stages are well-ordered,Footnote 10 as it is unclear at this point what would justify that assumption. (After all, if we are willing to countenance entities as ill-founded as V, then it is not immediately obvious that we should refuse to countenance a hierarchy with infinite descending chains of stages. And the Complemented Story does not explicitly require that the stages be well-ordered.)
Informally, Staging says that every set is discovered at some stage; this claim appears verbatim in the Complemented Story. Likewise, Cases says that every set is either low or high, and this is immediate from the fact that every set is discovered using either clause (Lo) or clause (
${Hi}$
). (Note, though, that I do not assume at the outset that this is an exclusive disjunction; initially, we should be open to the thought that one set could be discovered using both clauses.)Footnote
11
Next, Priority
$_{{Lo}}$
and Priority
$_{{Hi}}$
say that if we find a low set at a stage, then we find all its members earlier, and if we find a high set at a stage, then we find all its non-members earlier; both claims follow from clauses (Lo) and (
${Hi}$
). Finally, Specification
$_{{Lo}}$
and Specification
$_{{Hi}}$
say that if every F was found before a certain stage, then at that stage we find both the low set of all Fs, and the high set of all non-Fs; again, both claims follow from (Lo) and (
${Hi}$
).
Since all eight axioms hold of the Complemented Story, any complemented hierarchy satisfies BST.
3 Boolean Level Theory
Unfortunately, BST contains rather a lot of primitives. Fortunately, most of them can be eliminated. In this section, I present Boolean Level Theory, or BLT. This theory’s only primitive is
$\in $
, but it makes exactly the same claims about sets as BST does.Footnote
12
I start with a key definition:Footnote
13
Definition 3.1. For any a, let a’s absolute complement be
$\overline {a} = \{x : x \notin a\}$
, if it exists. Let
$\mathbf{P}{a} = \{x : (\exists c \notin c \in a)(x \subseteq c \lor \overline {x} \subseteq c)\}$
, if it exists.Footnote
14
The definition of
$\overline {a}$
needs no comment, but the definition of
$\mathbf{P}{a}$
merits explanation. It turns out that BST proves that a is low iff
$a \notin a$
, and a is high iff
$a \in a$
(see Lemma B.7). Seen in this light,
$\mathbf{P}{a}$
collects together all the subsets of low members of a, and all the complements of such subsets. As a specific example, if b is low, then
$\mathbf{P}{\{b\}} = \{x : x \subseteq b \lor \overline {x} \subseteq b\}$
, i.e., it is the result of closing b’s powerset under complements. We use this operation in this next definition (where ‘bistory’ is short for ‘boolean-history’, and ‘bevel’ is short for ‘boolean-level’):Footnote
15
Definition 3.2. Say that h is a bistory, written
${Bist}(h)$
, iff
$h\notin h \land (\forall x \in h)x = \mathbf{P}(x \cap h)$
. Say that s is a bevel, written
$\mathit{Bev}(s)$
, iff
$(\exists h : {Bist}) s = \mathbf{P}{h}$
.
The intuitive idea behind Definition 3.2 is that the bevels go proxy for the stages of the Complemented Story, and each bistory is an initial sequence of bevels. (It is far from obvious that these definitions work as described, but we will soon see that they do.) Using these definitions, BLT has just four axioms:Footnote 16
-
Extensionality
$\forall a \forall b(\forall x(x \in a \leftrightarrow x \in b) \rightarrow a = b)$
-
Complements
$\forall a(\exists c = \overline {a})(a \notin a \leftrightarrow c \in c)$
-
Separation
$_{\notin }$
$\forall F(\forall a \notin a)(\exists b \notin b)\forall x(x \in b \leftrightarrow (F(x) \land x \in a))$
-
Stratification
$_{\notin }$
$(\forall a \notin a)(\exists s : \mathit{Bev}) a \subseteq s$
Intuitively, Complements tells us that every set has a complement, and a set is low iff its complement is high; Separation
$_{\notin }$
tells us that arbitrary subsets of low sets exist (and are low); and Stratification
$_{\notin }$
tells us that every low set is a subset of some bevel (which corresponds to the thought that it is found at some stage). These axioms and definitions are vindicated by this next result, which shows that BLT has exactly the same set-theoretic content as BST (see Appendix B for the proof):
Theorem 3.3.
$\mathrm{BST} \vdash \phi $
iff
$\mathrm{BLT} \vdash \phi $
, for any BLT-sentence
$\phi $
.
Otherwise put: no information about sets is gained or lost by moving between BST and BLT. Moreover, since every complemented hierarchy satisfies BST, every complemented hierarchy satisfies BLT. In what follows, then, I will treat BLT as the canonical theory of complemented hierarchies.
4 Characteristics and extensions of BLT
To give a sense of how BLT behaves, I will state some of its ‘characteristic’ results (the proofs are in Appendix A). The first two results allow us to characterize BLT with a simple slogan: a boolean algebra of sets arranged in well-ordered levels.
Theorem 4.1 BLT
The bevels are well-ordered by
$\in $
.
Theorem 4.2 BLT
The sets form a boolean algebra under complementation,
$\cap $
and
$\cup $
.
This first result is quite surprising:Footnote 17 the Complemented Story does not explicitly specify that the stages must be well-ordered (see Section 2); but, since every complemented hierarchy satisfies BLT (see Section 3), every complemented hierarchy has well-ordered levels.
The well-ordering of the bevels yields a powerful tool, which intuitively allows us to consider the bevel at which a set is first found:
Definition 4.3 BLT
If
$a \notin a$
, let
$\mathbf{B}a$
be the
$\in $
-least bevel with a as a subset; i.e.,
$a \subseteq \mathbf{B}a$
and
$\lnot (\exists s : \mathit{Bev})a \subseteq s \in \mathbf{B}a$
. If
$a \in a$
, let
$\mathbf{B}a = \mathbf{B}\overline {a}$
.
Note that
$\mathbf{B}a$
exists for any a, by Stratification
$_{\notin }$
, Complements and Theorem 4.1.
A third characteristic result is that there is a contra-automorphism on the universe.Footnote 18 Roughly put: replacing membership with non-membership (and vice versa) yields an isomorphic universe. Formally:
Definition 4.4. We recursively define a’s negative, written
$\mathord {-} a$
, as follows:
$$ \begin{align*} \mathord{-} a &\mathrel{\mathord{:}\mathord{=}} \overline{\{\mathord{-} x : x \in a\}} \text{, if }a \notin a & \mathord{-} a&\mathrel{\mathord{:}\mathord{=}} \{\mathord{-} x : x \notin a\} \text{, if }a \in a \end{align*} $$
Theorem 4.5 BLT
$\forall a \forall b(a \in b \leftrightarrow \mathord {-} a \notin \mathord {-} b)$
This immediately yields a nice duality:
Corollary 4.6 BLT
$\phi \leftrightarrow \phi ^\circlearrowleft $
, for any BLT-sentence
$\phi $
, where
$\phi ^\circlearrowleft $
is the sentence which results from
$\phi $
by replacing every ‘
$\in $
’ with ‘
$\notin $
’ and vice versa.
These results highlight some of BLT’s deductive strengths. Now let me comment on its (deliberate) weakness. By design, BLT axiomatizes only the bare idea of a complemented hierarchy, and so makes no comment on the hierarchy’s height.Footnote
19
If we want to ensure that our hierarchy is reasonably tall, three axioms suggest themselves (where ‘P’ is a second-order function-variable in the statement of Unbounded
$_{\notin }$
):
-
Endless
$_{\notin }$
$(\forall s : \mathit{Bev})(\exists t : \mathit{Bev})s \in t$
-
Infinity
$_{\notin }$
$(\exists s : \mathit{Bev})((\exists q : \mathit{Bev})q \in s \land \hspace{10pt}(\forall q : \mathit{Bev})(q \in s \rightarrow (\exists r : \mathit{Bev})q \in r \in s))$
-
Unbounded
$_{\notin }$
$\forall P(\forall a \notin a)(\exists s : \mathit{Bev})(\forall x \in a) P(x) \in s$
Endless
$_{\notin }$
says there is no last bevel. Infinity
$_{\notin }$
says that there is an infinite bevel, i.e., a bevel with no immediate predecessor. Unbounded
$_{\notin }$
states that the hierarchy of bevels is so tall that no low set can be mapped unboundedly into it (recall that the low sets are precisely the non-self-membered sets).
To make all of this more familiar, here are some simple facts relating BLT to ZF. Let
$\mathrm{BLT}_{+}$
stand for
$\mathrm{BLT} + \text {Endless}_{\notin }$
, and
$\mathrm{BLT}_{\mathrm{ZF}}$
stand for
$\mathrm{BLT} + \mathrm{Infinity}_{\notin } + \mathrm{Unbounded}_{\notin }$
; then:Footnote
20
Proposition 4.7. (1) BLT proves the Axiom of Empty Set, i.e.,
$\exists a \forall x\phantom {(}x \notin a$
.
(2) BLT proves Union, i.e.
$\forall a(\bigcup a\ \mathrm{exists})$
.
(3)
$\mathrm{BLT}_{+}$
proves Pairing, i.e.,
$\forall a \forall b(\{a, b\}\ \mathrm{exists})$
, but BLT does not.
(4)
$\mathrm{BLT}_{+}$
proves Powersets-restricted-to-low-sets, i.e.,
$(\forall a \notin a)(\wp {a}\ \mathrm{exists})$
, but BLT does not.
(5) BLT contradicts Powersets, i.e., it proves
$\exists a \lnot \exists b \forall x(x \in b \leftrightarrow x \subseteq a)$
.
(6) BLT proves Foundation-restricted-to-high-sets, i.e.,
$(\forall a \in a)(\exists x \in a)a \cap x = \emptyset $
.
(7)
$\mathrm{BLT}_{+}$
contradicts Foundation, i.e., it proves
$(\exists a \neq \emptyset )(\forall x \kern-1pt\in a)a \cap\kern-1pt x \neq\kern-1pt \emptyset $
.
(8)
$\mathrm{BLT}_{\mathrm{ZF}}$
proves Endless
$_{\notin }$
.
If we want to state this result with maximum shock value: of the standard axioms of ZF, BLT validates only Extensionality, Empty Set, and Union (though BLT is also consistent with Pairing and standard formulations of Infinity).
5 The quasi-categoricity of BLT
We have seen that every complemented hierarchy satisfies BLT, so that every complemented hierarchy has well-ordered bevels. In fact, we can push this point further, by noting that BLT is quasi-categorical.Footnote 21
Informally, we can spell out BLT’s quasi-categoricity as follows: Any two complemented hierarchies are structurally identical for so far as they both run, but one may be taller than the other. So, when we set up a complemented hierarchy, our only choice is how tall to make it.
In fact, there are at least two ways to explicate the informal idea of quasi-categoricity, and BLT is quasi-categorical on both explications.Footnote 22 The first notion of quasi-categoricity should be familiar from Zermelo’s results for ZF, and uses the full semantics for second-order logic:
Theorem 5.1. Given full second-order logic:
(1) The bevels of any model of BLT are well-ordered.Footnote 23
(2) For any ordinal
$\alpha> 0$
, there is a model of BLT whose bevels form an
$\alpha $
-sequence.Footnote
24
(3) Given any two models of BLT, one is isomorphic to an initial segment of the other.Footnote 25
Since this result involves semantic ascent, it is an external quasi-categoricity result. There is also an internal quasi-categoricity result for BLT, which is a theorem of the (second-order) object language, but this point requires a little more explanation.
In embracing Extensionality, BLT assumes that everything is a pure set. Here is an easy way to avoid making that assumption. Consider the following formula, which relativises BLT to a new primitive predicate, Pure:Footnote 26
The first four conjuncts say that the pure sets satisfy BLT;Footnote
27
the last says that, when we use ‘
$\mathrel {\varepsilon }$
’, we restrict our attention to membership facts between pure sets. This avoids the assumption that everything is a pure set. Moreover, I can use this formula to state our internal quasi-categoricity result (I have labelled the lines to facilitate its explanation):Footnote
28
Theorem 5.2. This is a deductive theorem of impredicative second-order logic:
$$ \begin{align}&\kern-50pt (\mathrm{BLT}({Pure}_1, \mathord{\mathrel{\varepsilon}_1}) \land \mathrm{BLT}({Pure}_2, \mathord{\mathrel{\varepsilon}_2})) \rightarrow {}\nonumber\\&\kern-26pt\exists R( \forall v \forall y(R(v,y) \rightarrow ({Pure}_1(v) \land {Pure}_2(y))) \land {} \end{align} $$
$$ \begin{align} &\qquad ((\forall v : {Pure}_1)\exists y R(v,y) \lor (\forall y : {Pure}_2)\exists v R(v,y)) \land{} \end{align} $$
$$ \begin{align} &\qquad\qquad\quad\kern1pt \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-24pt \forall v \forall y\forall z ((R(v,y) \land R(v,z)) \rightarrow y = z)\land {} \end{align} $$
$$ \begin{align} &\kern-22pt \forall v\forall x \forall y ((R(v,y) \land R(x, y)) \rightarrow v= x)\land {} \end{align} $$
$$ \begin{align} &\qquad\kern-4pt \forall v \forall x \forall y ((\mathbf{B}_1{x} \subseteq_1 \mathbf{B}_1{v} \land R(v, y)) \rightarrow \exists z R(x, z))\land {} \end{align} $$
$$ \begin{align} &\qquad\kern-12pt \forall v \forall y \forall z((\mathbf{B}_2{z} \subseteq_2 \mathbf{B}_2{y} \land R(v, y)) \rightarrow \exists x R(x, z))) \end{align} $$
Intuitively, the point is this. Suppose two people are using their versions of BLT, 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: BLT 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 is a bijection between the
$\Phi $
s and the universe (see Pt.1 Section 6). Using this notation, we can state our internal total-categoricity result:
Theorem 5.3. This is a deductive theorem of impredicative second-order logic:
Intuitively, if both BLT-like hierarchies are as large as the universe, then there is a structure-preserving bijection between them.
6 Ordinary set theory as a proper part of BLT
The Complemented Story provides two clauses for finding sets. Clause (Lo) tells us that, at each stage s and for any sets found before s, we find a set whose members are exactly those sets. But this is exactly what we would find according to the Basic Story (see Section 1), which deals with ordinary, uncomplemented hierarchies. Intuitively, then, we should be able to recover an ordinary hierarchy by considering a complemented hierarchy whilst ignoring any use of clause (
${Hi}$
). This intuitive idea is exactly right; the aim of this section is to explain it carefully.
First, I must formalize the notion of a set which we find without ever using clause (
${Hi}$
). I call such sets hereditarily low, or helow for short. So: helow sets are low, their members are low, the members of their members are low, etc. Here is the precise definition:
Definition 6.1. Say that a is helow, or
${Helo}(a)$
, iff there is some transitive
$c \supseteq a$
such that
$(\forall x \in c)x \notin x$
.
To restrict our attention to the ordinary (uncomplemented) hierarchy, we then just restrict our attention to the helow sets. To implement this formally, for any formula
$\phi $
, let
$\phi ^{\triangledown }$
be the formula which results by restricting all of
$\phi $
’s quantifiers to helow sets. Using this notation, we can then prove results of this shape: If some theory of uncomplemented hierarchies proves
$\phi $
, then some suitable theory of complemented hierarchies proves
$\phi ^{\triangledown }$
.
To state these results precisely, we need a suitable theory of uncomplemented hierarchies. That theory is LT, discussed in Pt.1. In a nutshell, LT stands to uncomplemented hierarchies exactly as BLT stands to complemented hierarchies. I will now briefly recap LT’s key elements. To formalize the Basic Story, we define a predicate, Lev, to capture the notion of a level of an uncomplemented hierarchy (Pt.1 Definition 2.2); then LT is the theory whose axioms are Extensionality, Separation, and Stratification, which states that
$\forall a (\exists s : \mathit{Lev})a \subseteq s$
(see Pt.1 Section 2). It transpires that LT is quasi-categorical, and that every uncomplemented hierarchy satisfies LT, regardless of its height (see Pt.1 Sections 5–6). If we want to secure a tall uncomplemented hierarchy, we can consider the axioms Endless, Infinity and Unbounded (see Pt.1 Section 7); these are exactly like Endless
$_{\notin }$
, Infinity
$_{\notin }$
and Unbounded
$_{\notin }$
(see Section 3 of this part), except that they replace ‘
$\mathit{Bev}$
’ with ‘
$\mathit{Lev}$
’. Let
$\text {LT}_{+}$
stand for
$\text {LT} + \mathrm{Endless}$
; it turns out that ZF is deductively equivalent to
$\text {LT} + \mathrm{Infinity} + \mathrm{Unbounded}$
; so LT,
$\text {LT}_{+}$
, and ZF are three theories which axiomatize uncomplemented hierarchies, making successively stronger demands on the hierarchy’s height. With this background in place, here is the result which intuitively states that the helow part of any complement hierarchy is an ordinary (uncomplemented) hierarchy (see Appendix C for the proof):
Theorem 6.2. For any LT-sentence
$\phi $
:
(1) If
$\mathrm{LT} \vdash \phi $
, then
$\mathrm{BLT} \vdash \phi ^{\triangledown }$
(2) If
$\mathrm{LT}_+ \vdash \phi $
, then
$\mathrm{BLT}_+ \vdash \phi ^{\triangledown }$
(3) If
$\mathrm{ZF} \vdash \phi $
, then
$\mathrm{BLT}_{\mathrm{ZF}} \vdash \phi ^{\triangledown }$
7 Definitional equivalence
Theorem 6.2.3 allows us to regard ZF as the result of restricting attention to the helow-fragment of
$\mathrm{BLT}_{\mathrm{ZF}}$
’s universe of sets. But we also have a much deeper interpretative result, as follows (see Appendix D):Footnote
29
Theorem 7.1.
ZF and
$\mathrm{BLT}_{\mathrm{ZF}}$
are definitionally equivalent, as are
$\mathrm{LT}_{+}$
and
$\mathrm{BLT}_{+}$
.
As an immediate consequence, ZF and
$\mathrm{BLT}_{\mathrm{ZF}}$
are equiconsistent, as are
$\text {LT}_{+}$
and
$\mathrm{BLT}_{+}$
. However, definitional equivalence is much stronger than mere equiconsistency.
Roughly, to say that two theories are definitionally equivalent is to say that each theory can define all the primitive expressions of the other, such that each theory can simulate the other perfectly, and where combining the two simulations gets you back exactly where you began.Footnote
30
So, in some purely formal sense, ZF and
$\mathrm{BLT}_{\mathrm{ZF}}$
can be regarded as notational variants; as wrapping the same deductive content in different notational packaging.
One might be tempted to go further, and suggest that Theorem 7.1 shows that there is no relevant difference between ZF and
$\mathrm{BLT}_{\mathrm{ZF}}$
. That, however, would require further argument.Footnote
31
Precisely because definitional equivalence is a purely formal property, it ignores all non-formal matters, and these may be philosophically significant. There is more philosophical discussion to be had about the significance of Theorem 7.1, but that must wait for another time.
8 Conway games and surreal numbers in BLT
Since ZF and
$\mathrm{BLT}_{\mathrm{ZF}}$
are definitionally equivalent, there is a sense in which each can do anything that the other can. Still,
$\mathrm{BLT}_{\mathrm{ZF}}$
can do some things more easily than ZF. This is neatly illustrated by considering John Conway’s theory of games and surreal numbers.Footnote
32
Consider two-player games in which players move alternately, with no element of chance, where the game must end in a win or loss. (Think of chess, but without the possibility of stalemate.) Abstractly, such games can be thought of as specifications of permissible positions: to make a move in such a game is just to select a new position which is permissible given the current game state; and you lose when it is your turn to move but there is no permissible position. (Think of being checkmated: you must move to a position where your King is not in check, but no such move is available.) Crucially, any position in any such game can be considered as a game in its own right. (Imagine the version of chess which always starts with the pieces arranged as after the Queen’s Gambit in regular chess.) So every game can be regarded, abstractly, as nothing other than a specification of which games each player can move to. Otherwise put, if we call the two game-players Low and High, then a game is just a specification of low options, i.e., games that Low can move to, and high options, i.e., games that High can move to.
The idea is very natural. However, as Conway remarked, formalizing it ‘in ZF destroys a lot of its symmetry.’ He therefore suggested that ‘the proper set theory in which to perform such a formalisation would be one with two kinds of membership’: a game would just be a set with ‘low-members’ (low options) and ‘high-members’ (high options).Footnote 33 However, we can easily implement this idea in BLT, using only one kind of membership. We start by saying that the games are the sets, and then stipulate:
Definition 8.1 BLT
If a is low, the set of a’s low options is
$\textrm {{L}}{a} \mathrel {\mathord {:}\mathord {=}} \{x \in a : x\notin x\}$
; the set of a’s high options is
$\textrm {{H}}{a} \mathrel {\mathord {:}\mathord {=}} \{x \in a : x \in x\}$
. If a is high,
$\textrm {{L}}{a} \mathrel {\mathord {:}\mathord {=}} \textrm {{L}}{\overline {a}}$
and
$\textrm {{H}}{a} \mathrel {\mathord {:}\mathord {=}} \textrm {{H}}{\overline {a}}$
.
Intuitively, then, a and
$\overline {a}$
represent the same game. Moreover, there is a natural algebra on the games, given as follows (I explain the definitions below):Footnote
34
Definition 8.2 BLT
With
$\mathord {-}$
as in Definition 4.4, define
$+$
and
$\leq $
recursively:
$$ \begin{align*} a + c &\mathrel{\mathord{:}\mathord{=}} \{x + c : x \in \textrm{{L}}{a}\} \cup \{a + x : x \in \textrm{{L}}{c}\} \cup \{\overline{y + c} : y \in \textrm{{H}}{a}\}\\&\qquad \cup \{\overline{a + y} : y \in \textrm{{H}}{c}\}\\ a \leq c &\text{ iff } (\forall y \in \textrm{{H}}{c})y \nleq a \land (\forall x \in \textrm{{L}}{a})c \nleq x \end{align*} $$
We stipulate that
$a \equiv c\text { iff }a \leq c \leq a$
, and define
$a - c \mathrel {\mathord {:}\mathord {=}} a + (\mathord {-} c)$
.
We can make these algebraic operations intuitive as follows. To take the negative of a game is to reverse the players’ roles (cf. Theorem 4.5). To add two games is to place them side-by-side, allowing a player to move in one game without affecting the other. But the partial-order requires slightly more explanation. Suppose High plays first on the game a; then Low has a winning strategy iff whatever move High makes, i.e., for all
$y \in \textrm {{H}}{a}$
, if Low plays first on y then High has no winning strategy. Similarly, suppose Low plays first on a; then High has a winning strategy iff for all
$x \in \textrm {{L}}{a}$
, if High plays first on x then Low has no winning strategy. So, if we gloss ‘
$\emptyset \leq z$
’ as ‘Low has a winning strategy as second player on z’ and gloss ‘
$z \leq \emptyset $
’ as ‘High has a winning strategy as second player on z’, this motivates two important special cases of the partial order:
$$ \begin{align*} \emptyset \leq a&\text{ iff }(\forall y \in \textrm{{H}}{a})y \nleq \emptyset& a \leq \emptyset& \text{ iff }(\forall x \in \textrm{{L}}{a})\emptyset \nleq x. \end{align*} $$
The remainder of Definition 8.2 is then set up so that
$a - b \leq \emptyset $
iff
$a \leq b$
. More generally, we have the following foundational result:
Theorem 8.3 BLT
The sets form a partially-ordered abelian Group, with
$\emptyset = 0$
and
$+, -, \leq $
as in Definition 8.2, all modulo
$\equiv $
.Footnote
35
We can obtain a totally-ordered Field by restricting our attention to surreals:
Definition 8.4 BLT
We specify that a is surreal iff: for all
$x \in \textrm {{L}}{a}$
and all
$y \in \textrm {{H}}{a}$
, both x and y are surreal and
$x \ngeq y$
. We define multiplication on surreals thus:
$$ \begin{align*} a \cdot c \mathrel{\mathord{:}\mathord{=}} {}& \{x \cdot c + a \cdot y - x \cdot y : (x \in \textrm{{L}}{a} \land y \in \textrm{{L}}{c}) \lor (x \in \textrm{{H}}{a} \land y \in \textrm{{H}}{c})\} \cup {}\\ & \{\overline{x\cdot c + a\cdot y - x\cdot y} : (x \in \textrm{{L}}{a} \land y \in \textrm{{H}}{c}) \lor (x \in \textrm{{H}}{a} \land y \in \textrm{{L}}{c})\}. \end{align*} $$
We say that a is a surreal-ordinal iff a is both helow and surreal.
Theorem 8.5 BLT
The surreals form a totally-ordered Field, modulo
$\equiv $
.
Summing up: Conway’s beautifully rich, nonstandard, theory of surreal numbers is available, essentially off-the-shelf, within BLT.
9 Conclusion
The Complemented Story lays down a conception of set which rivals the (ordinary) cumulative notion, but which accepts Complementation and rejects Separation (see Section 1).
I have shown that any complemented hierarchy satisfies BLT (see Sections 2–3). So, given the characteristic results of BLT, the sets of any complemented hierarchy are arranged into well-ordered bevels, and constitute a boolean algebra (see Section 4). Moreover, BLT is quasi-categorical (see Section 5); so our only choice, in setting up a complemented hierarchy, is how tall to make it.
The theory
$\mathrm{BLT}_{\mathrm{ZF}}$
arises from BLT just by adding axioms which state that the complemented hierarchy is quite tall (see Section 4). And we can regard ZF as either a proper part of
$\mathrm{BLT}_{\mathrm{ZF}}$
(see Section 6), or as a notational variant (in a purely formal sense) of
$\mathrm{BLT}_{\mathrm{ZF}}$
(see Section 7). But both interpretations suggest that there is no obvious a priori reason to favour Separation over Complementation. And in some settings, such as the discussion of Conway games, using Complementation is extremely natural (see Section 8).
Appendix A Characteristics of BLT
The remainder of this paper consists of proofs of the results discussed in the main text. Many of the simpler proofs are similar to results for Pt.1; in such cases, I omit the proof and refer interested readers to the appropriate result from Pt.1.
This first appendix deals with the results from Section 4. Initially, I will work in ECS, the subtheory of BLT whose only axioms are Extensionality, Complements and Separation
$_{\notin }$
(see Section 3). I start with some simple results and definitions:
Lemma A.1 ECS
If
$c \subseteq a \notin a$
, then
$c \notin c$
; if
$a \in a \subseteq c$
, then
$c \in c$
.
Proof If
$c \subseteq a \notin a$
, then
$c \notin c = \{x \in a : x \in c\}$
by Separation
$_{\notin }$
and Extensionality. If
$a \in a \subseteq c$
, then
$\overline {c} \subseteq \overline {a} \notin \overline {a}$
by Complements, so that
$ \overline {c} \notin \overline {c}$
as before, and
$c \in c$
by Complements.
Definition A.2. Say that a is potent
$_{\notin }$
iff
$\forall x(\exists c(x \subseteq c \notin c \in a) \rightarrow x \in a)$
. Say that a is transitive
$_{\notin }$
iff
$(\forall x \notin x \in a)x\subseteq a$
. Say that a is complement-closed iff
$\forall x(x \in a \leftrightarrow \overline {x} \in a)$
.
Lemma A.3 ECS
If
$\mathbf{P}{a}$
exists (see Definition 3.1), then:
(1)
$(\forall x \notin x \in \mathbf{P}{a})\exists c(x \subseteq c \notin c \in a)$
.
(2)
$\mathbf{P}{a}$
is potent
$_{\notin }$
.
(3)
$\mathbf{P}{a}$
is complement-closed.
Proof
(1) Fix
$x \notin x \in \mathbf{P}{a}$
; so for some
$c \notin c \in a$
, either
$x \subseteq c$
or
$\overline {x} \subseteq c$
. But
$\overline {x} \in \overline {x}$
by Complements, so
$\overline {x} \nsubseteq c$
by Lemma A.1.
(2) Fix
$x \subseteq c \notin c \in \mathbf{P}{a}$
; so
$x \subseteq c \subseteq b \notin b \in a$
for some b by (1); hence
$x \in \mathbf{P}{a}$
.
(3) Fix
$x \in \mathbf{P}{a}$
. If
$x \subseteq c$
for some
$c \notin c \in a$
, then
$x= \overline {\overline {x}} \subseteq c$
so that
$\overline {x} \in \mathbf{P}{a}$
; if
$\overline {x} \subseteq c$
for some
$c \notin c \in a$
, then
$\overline {x} \in \mathbf{P}{a}$
straightforwardly.
It follows that bevels (see Definition 3.2) have several important closure properties:
Lemma A.4 ECS
Every bevel is transitive
$_{\notin }$
, potent
$_{\notin }$
, complement-closed, and non-self-membered.
Proof Let s be a bevel, i.e.,
$s = \mathbf{P}{h}$
for some bistory h. So s is potent
$_{\notin }$
and complement-closed by Lemma A.3. For transitivity
$_{\notin }$
, fix
$a \notin a \in s = \mathbf{P}{h}$
; so
$a \subseteq c \notin c \in h$
for some c by Lemma A.3.1; and
$c = \mathbf{P}(c \cap h)$
as h is a bistory; so
$a \subseteq \mathbf{P}(c \cap h) \subseteq \mathbf{P}{h} = s$
. To see that
$s \notin s$
, suppose
$s\in s$
for reductio. Then
$\overline {s} \notin \overline {s} \in s$
by Complements, so
$\overline {s} \subseteq s$
by transitivity
$_{\notin }$
, so
$s = V$
. Since
$h \notin h$
by definition, and
$h \in V = s = \mathbf{P}{h}$
, by Lemma A.3.1 there is some c such that
$h \subseteq c \notin c \in h$
. Since h is a bistory,
$c = \mathbf{P}{(h \cap c)} = \mathbf{P}{h} = V$
, contradicting the fact that
$c \notin c$
.
From here, we can prove the well-ordering of the bevels, by proving a sequence of results like those from Pt.1 Section 3; I leave this to the reader:Footnote 36
Lemma A.5 ECS
If there is an F, and all Fs are non-self-membered and potent
$_{\notin }$
, then there is an
$\in $
-minimal F. Formally:
$\forall F((\exists x F(x) \land (\forall x : F)(x \notin x \land x\text { is potent}_{\notin }{})) \rightarrow (\exists a : F)(\forall x : F)x \notin a)$
Lemma A.6 ECS
If some bevel is F, then there is an
$\in $
-minimal bevel which is F. Formally:
$\forall F((\exists s : \mathit{Bev})F(s) \rightarrow (\exists s: \mathit{Bev})(F(s) \land (\forall r : \mathit{Bev})(F(r) \rightarrow r \notin s)))$
Lemma A.7 ECS
Every member of a bistory is a bevel.
Lemma A.8 ECS
$s = \mathbf{P}{\{r \in s : \mathit{Bev}(r)\}}$
, for any bevel s.
Lemma A.9 ECS
All bevels are comparable, i.e.,
$(\forall s: \mathit{Bev})(\forall t : \mathit{Bev})(s \in t \lor s = t \lor t \in s)$
Combining Lemmas A.6 and A.9, ECS proves that the bevels are well-ordered by
$\in $
; this is Theorem 4.1. This licenses our use of the
$\mathbf{B}$
-operator (see Definition 4.3). Here are some simple results about that operator, which can be proved by tweaking the proof of Pt.1 Lemma 3.12:
Lemma A.10 BLT
For any sets
$a, c$
, and any bevels
$r, s$
:
(1)
$\mathbf{B}a$
exists
(2)
$a \notin \mathbf{B}a$
(3)
$r\subseteq s$
iff
$s\notin r$
(4)
$s = \mathbf{B}s$
(5) if
$c \subseteq a \notin a$
or
$a \in a \subseteq c$
, then
$\mathbf{B}c \subseteq \mathbf{B}a$
(6) if
$c \in a \notin a$
or
$c \notin a \in a$
, then
$\mathbf{B}c \in \mathbf{B}a$
Moreover, we can now show that sets are closed under arbitrary pairwise intersection:
Lemma A.11 BLT
For any sets a and c, the set
$a \cap c = \{x : x \in a \land x \in c\}$
exists.
Proof First suppose that either
$a \notin a$
or
$c\notin c$
(or both); without loss of generality, suppose
$a \notin a$
; now
$a \cap c = \{x \in a : x \in c\}$
exists by Separation
$_{\notin }$
. Next suppose that both
$a \in a$
and
$c \in c$
. So both
$\overline {a} \notin \overline {a}$
and
$\overline {c} \notin \overline {c}$
by Complements. Let s be the maximum of
$\mathbf{B}\overline {a}$
and
$\mathbf{B}\overline {c}$
. Since s is potent
$_{\notin }$
, both
$\overline {a} \subseteq s$
and
$\overline {c} \subseteq s$
, so
$\overline {a} \cup \overline {c} = \{x \in s : x \in \overline {a} \lor x \in \overline {c}\}$
exists by Separation
$_{\notin }$
. Now
$a \cap c = \overline {\overline {a} \cup \overline {c}}$
exists by Complements.
This immediately entails that the sets form a boolean algebra, which is Theorem 4.2. Our next result shows that the universe is contra-automorphic:Footnote 37
Theorem 4.5 BLT
$\forall a \forall b(a \in b \leftrightarrow \mathord {-} a \notin \mathord {-} b)$
Proof Recall that negative is given as in Definition 4.4 by
$$ \begin{align*} \mathord{-} a &\mathrel{\mathord{:}\mathord{=}} \overline{\{\mathord{-} x : x \in a\}} \text{, if }a \notin a & \mathord{-} a&\mathrel{\mathord{:}\mathord{=}} \{\mathord{-} x : x \notin a\} \text{, if }a \in a. \end{align*} $$
Fix a bevel s and for induction suppose that, for any
$x, y \in s$
:
(1)
$\mathord {-} x$
is well-defined and
$\mathbf{B}x = \mathbf{B}(\mathord {-} x)$
, and
(2)
$x = y$
iff
$\mathord {-} x = \mathord {-} y$
.
It suffices to show that both properties hold of
$a, b$
when
$\mathbf{B}a = \mathbf{B}b = s$
.
Concerning (1). Suppose
$a \notin a$
. If
$x \in a$
, then
$\mathbf{B}(\mathord {-} x) = \mathbf{B}x \in \mathbf{B}a$
by induction assumption (1) and Lemma A.10.6. Using Separation
$_{\notin }$
, let
$c \notin c = \{v \in \mathbf{B}a : (\exists x \in a)v = \mathord {-} x\} = \{\mathord {-} x : x \in a\}$
. Moreover,
$\mathbf{B}c = \mathbf{B}a$
, by the well-ordering of bevels and since
$\mathbf{B}(\mathord {-} x) = \mathbf{B}x \in \mathbf{B}a$
for all
$x \in a$
. Now
$\overline {c} \in \overline {c} = \mathord {-} a$
by Complements; so
$\mathbf{B}a = \mathbf{B}c = \mathbf{B}\overline {c} = \mathbf{B}(\mathord {-} a)$
. The case when
$a \in a$
is similar, defining
$c \notin c = \{v \in \mathbf{B}a : (\exists x \notin a)v = \mathord {-} x\} = \{\mathord {-} x : x \notin a\} = {\mathord {-} a}$
.
Concerning (2). If
$a \in a \leftrightarrow b \in b$
, then
$a = b$
iff
$\mathord {-} a = \mathord {-} b$
by induction assumption (2). Without loss of generality, suppose that
$a \in a$
and
$b \notin b$
; in establishing (1), we found that
$\mathord {-} a \notin \mathord {-} a$
and
$\mathord {-} b \in \mathord {-} b$
; so
$a \neq b$
and
$\mathord {-} a \neq \mathord {-} b$
.
I ended Section 4 by stating some simple facts about extensions of BLT. I will prove the distinctively boolean facts, leaving the remainder to the reader:
Proposition 4.7 Fragment
(2) BLT proves Union, i.e.,
$\forall a(\bigcup a\ \mathrm{exists})$
(5) BLT contradicts Powersets, i.e., it proves
$\exists a \lnot \exists b \forall x(x \in b \leftrightarrow x \subseteq a)$
(6) BLT proves Foundation-restricted-to-high-sets, i.e.,
$(\forall a \in a)(\exists x \in a)a \cap x = \emptyset $
.
(7)
$\mathrm{BLT}_{+}$
contradicts unrestricted Foundation, i.e., it proves
$(\exists a \neq \emptyset )(\forall x \in a)a \cap x \neq \emptyset $
.
Proof
(2) If
$a \in a$
, then
$\bigcup a = \overline {\{x \in \overline {a} : (\forall y \in a)x \notin y\}}$
, which exists by Separation
$_{\notin }$
and Complements. If
$a \notin a$
, then using Separation
$_{\notin }$
let
$a_0 = \{x \in a : x \notin x\}$
and let
$a_1 = \{x \in a : x \in x\}$
. I will show that
$\bigcup a_0$
and
$\bigcup a_1$
exist, so that, using Complements and Lemma A.11:
$$ \begin{align*}\bigcup a = \bigcup a_0 \cup \bigcup a_1 = \overline{\overline{\bigcup a_0} \cap \overline{\bigcup a_1}}.\end{align*} $$
Clearly
$\bigcup a_0$
exists by Separation
$_{\notin }$
on
$\mathbf{B}a$
. If
$a_1 = \emptyset $
then
$\bigcup a_1 = \emptyset $
; otherwise,
$\bigcup a_1 = \overline {\bigcap \{\overline {x} : x \in a_1\}}$
, which exists by Complements and Separation
$_{\notin }$
on
$\mathbf{B}a$
.
(5) If there is only one bevel, then the only sets are
$\emptyset $
and
$V = \{\emptyset , V\}$
, so that
$\wp \emptyset = \{\emptyset \}$
does not exist. Otherwise, we find
$\overline {\{\emptyset \}}$
at the second bevel, and if
$\wp \overline {\{\emptyset \}}$
existed it would be
$\{x : \emptyset \notin x\}$
. So suppose for reductio that
$a = \{x : \emptyset \notin x\}$
. Then
$\emptyset \notin \emptyset $
, so
$\emptyset \in a$
, so
$a \notin a$
. Now
$\overline {a} \in \overline {a} = \{x : \emptyset \in x\}$
by Complements, so that
$\emptyset \in \overline {a}$
, contradicting that
$\emptyset \in a$
.
(6) If
$a \in a$
then
$\overline {a} \in a$
by Complements, and
$a \cap \overline {a} = \emptyset $
.
(7) We find
$\{V\}$
at the second bevel, and
$\{V\} \cap V \neq \emptyset $
.
Appendix B The set-theoretic equivalence of BST and BLT
I now want to prove Theorem 3.3, which states that BLT and BST say exactly the same things about sets. (This mirrors Pt.1 Section 4.)
To show that BST says no more about sets than BLT does, I define a translation
$* : \text {BST} \longrightarrow \mathrm{BLT}$
, whose non-trivial actions are as follows:Footnote
38
$$ \begin{align*} {Lo}(x)&:= x \notin x & {Hi}(x) &\mathrel{\mathord{:}\mathord{=}} x \in x\\ (\mathbf{s} < \mathbf{t})^* &\mathrel{\mathord{:}\mathord{=}} \mathbf{s} \in \mathbf{t} & (x \preceq \mathbf{s})^* &\mathrel{\mathord{:}\mathord{=}} (x \subseteq \mathbf{s} \lor \overline{x} \subseteq \mathbf{s}) & (\forall \mathbf{s} \phi)^* &\mathrel{\mathord{:}\mathord{=}} (\forall \mathbf{s} : \mathit{Bev})(\phi^*). \end{align*} $$
After translation, I treat all first-order variables as being of the same sort. Fairly trivially, for any BLT-sentence
$\phi $
, if
$\text {BST} \vdash \phi $
then
$\text {BST}^* \vdash \phi $
. The left-to-right half of Theorem 3.3 now follows as
$*$
is an interpretation:
Lemma B.1 BLT
$\mathrm{BST}^*$
holds.
Proof Extensionality
$^*$
is Extensionality. Order
$^*$
holds by Lemma A.4; Staging
$^*$
holds by Stratification
$_{\notin }$
and Complements; and Cases
$^*$
is trivial. Next, by Lemma A.4 and Lemma A.8, we can simplify
$(x \prec \mathbf{s})^*$
to
$x \in \mathbf{s}$
. So, using Lemmas A.1 and A.4, we can simplify Priority
${}_{{Lo}}^*$
thus:
$$ \begin{align*} (\forall s \in \mathit{Bev})& (\forall a\notin a)((a \subseteq s \lor \overline{a} \subseteq s) \rightarrow (\forall x \in a)x \in s) \\ \text{i.e., }(\forall s \in \mathit{Bev})&(\forall a \subseteq s )(\forall x \in a) x \in s \end{align*} $$
which is trivial; then Priority
$_{{Hi}}^*$
holds similarly, by Complements. A similar simplification allows us to obtain Specification
$_{{Lo}}^*$
via Separation
$_{\notin }$
; then Specification
$_{{Hi}}^*$
holds similarly, by Complements.Footnote
39
To obtain the right-to-left half of Theorem 3.3, I will work in BST. I start by defining slices, which will go proxy for stages, and will turn out to be bevels, and then stating a few elementary results (for proofs, tweak those of Pt.1 Section 4):
Definition B.2 BST
For each
$\mathbf{s}$
, let
$\check {\mathbf{s}} = \{x : x \prec \mathbf{s}\}$
. Say that a is a slice iff
$a = \check {\mathbf{s}}$
for some stage
$\mathbf{s}$
.
Lemma B.3 BST
$\forall F (\forall a : {Lo})(\exists b : {Lo})\forall x(x \in b \leftrightarrow (F(x) \land x \in a))$
Lemma B.4 BST
$\forall \mathbf{s}(\forall a : {Lo})(a \preceq \mathbf{s} \leftrightarrow (\forall x \in a)x \prec \mathbf{s})$
Lemma B.5 BST
For any s:
(1)
$\check {\mathbf{s}}$
exists and is low
(2)
$\forall \mathbf{r}(\forall a : {Lo})(a \preceq \mathbf{r} \leq \mathbf{s} \rightarrow a \preceq \mathbf{s})$
(3)
$(\forall a : {Lo})(a \subseteq \check {\mathbf{s}} \leftrightarrow a \preceq \mathbf{s})$
We must now part company slightly with the strategy of Pt.1 Section 4, to handle low and high sets, and their relation to (non-)self-membership:
Lemma B.6 BST
If some slice is F, then there is an
$\in $
-minimal slice which is F.
Proof Every slice is low, by Lemma B.5.1. Subsets of low sets are low, by a result like Lemma A.1. From this, and Lemma B.5, it follows that
$\forall \check {\mathbf{s}}\forall x((\exists c : {Lo})x \subseteq c \in \check {\mathbf{s}} \rightarrow x \in \check {\mathbf{s}})$
. The result now follows, reasoning as in Pt.1 Lemma 3.5.
Lemma B.7 BST
a is low iff
$a \notin a$
; and a is high iff
$a \in a$
.
Proof Suppose for reductio that
$a \in a$
is low. Using Staging and Lemma B.6, let
$\check {\mathbf{s}}$
be an
$\in $
-minimal slice such that
$\exists \mathbf{t}(a \preceq \mathbf{t} \land \check {\mathbf{t}}= \check {\mathbf{s}})$
; let
$\mathbf{t}$
witness this. Since
$a \in a \preceq \mathbf{t}$
and a is low,
$a \preceq \mathbf{r} < \mathbf{t}$
for some
$\mathbf{r}$
by Priority
$_{{Lo}}$
; so
$\check {\mathbf{r}} \in \check {\mathbf{t}} = \check {\mathbf{s}}$
by Lemma B.5, contradicting
$\check {\mathbf{s}}$
’s minimality. Discharging the reductio: if a is low, then
$a \notin a$
. Similarly: if a is high, then
$a \in a$
. The biconditionals follow by Cases.
Lemma B.8 BST
$\overline {a}$
exists; and
$a \notin a \leftrightarrow \overline {a} \in \overline {a}$
; and
$\forall \mathbf{s}(a \preceq \mathbf{s} \leftrightarrow \overline {a} \preceq \mathbf{s})$
.
Proof Using Staging, let
$a \preceq \mathbf{s}$
. If
$a \notin a$
, then a is low by Lemma B.7, so
$(\forall x \in a)x \prec \mathbf{s}$
by Priority
$_{{Lo}}$
, so that by Specification
$_{{Hi}}$
and Extensionality
$\{x : x \notin a\} = \overline {a} \preceq \mathbf{s}$
exists and is high, i.e.,
$\overline {a} \in \overline {a}$
by Lemma B.7. If
$a \in a$
, reason similarly using Priority
$_{{Hi}}$
and Specification
$_{{Lo}}$
.
Note that
$\text {BST} \vdash \text {ECS}$
by Lemmas B.3, B.7, and B.8. So Lemmas A.1–A.9 hold verbatim within BST. We can now complete our reasoning about slices, by resuming the proof-strategy of Pt.1 Section 4; at this point, I leave the remaining details to the reader:
Lemma B.9 BST
$\check {\mathbf{s}} \notin \check {\mathbf{s}}$
; and
$\check {\mathbf{s}}$
is transitive
$_{\notin }$
; and
$\check {\mathbf{s}} = \mathbf{P}{\{\check {\mathbf{r}} : \check {\mathbf{r}} \in \check {\mathbf{s}}\}}$
.
Lemma B.10 BST
All slices are comparable, i.e.,
$\kern-1pt\forall \check {\mathbf{s}} \forall \check {\mathbf{t}} (\check {\mathbf{s}} \kern-1pt\in \kern-1pt\check {\mathbf{t}} \kern-0.5pt\lor\kern-0.5pt \check {\mathbf{s}} \kern-0.5pt=\kern-0.5pt \check {\mathbf{t}} \kern-0.5pt\lor\kern-0.5pt \check {\mathbf{t}} \kern-1pt\in \kern-1pt\check {\mathbf{s}})$
.
Lemma B.11 BST
s is a bevel iff s is a slice.
It follows that BST proves Stratification
$_{\notin }$
, delivering Theorem 3.3.
Appendix C Helow sets
In this appendix I prove Theorem 6.2, which shows how to recover ordinary, uncomplemented hierarchies via helow sets (see Definition 6.1). For readability, I refer to non-self-membered sets as low, and self-membered sets as high (cf. Lemma B.7). Note that every helow set is low, since all its members are low (i.e. non-self-membered). Now:
Definition C.1 BLT
If a is low, let
$a_{\triangledown } \mathrel {\mathord {:}\mathord {=}} \{x \in a : x\text { is helow}\}$
; by Separation
$_{\notin }$
,
$a_{\triangledown }$
exists and is low.
Lemma C.2 BLT
a is helow iff every member of a is helow.
Proof
Left-to-right. Where c witnesses that a is helow, if
$x \in a$
, then
$x \in c$
and hence
$x \subseteq c$
, so c also witnesses that x is helow. Right-to-left. Let every member of a be helow. Every member of a is low, so a itself is low; hence
$a \subseteq (\mathbf{B}a)_{\triangledown }$
. Now
$(\mathbf{B}a)_{\triangledown }$
witnesses that a is helow: if
$x \in c \in (\mathbf{B}a)_{\triangledown }$
then c is helow so x is helow (by left-to-right), so
$x \in (\mathbf{B}a)_{\triangledown }$
as
$\mathbf{B}a$
is transitive
$_{\notin }$
.
I can now begin to show that
$\triangledown : \text {LT} \longrightarrow \mathrm{BLT}$
, which simply restricts all quantifiers to helow sets (see Section 6), is an interpretation of LT:
Lemma C.3 BLT
Both Extensionality
$^{\triangledown }$
and Separation
$^{\triangledown }$
hold.
Proof For
$\mathrm{Extensionality}^{\triangledown }$
, fix helow a and b and suppose that
$(\forall x : {Helo})(x \in a \leftrightarrow x \in b)$
; then
$\forall x(x \in a \leftrightarrow x \in b)$
by Lemma C.2, so
$a = b$
by Extensionality. Similarly, repeated use of Lemma C.2 shows that
$\mathrm{Separation}^{\triangledown }$
follows from Separation
$_{\notin }$
.
The next task is to connect bevels with levels
$^{\triangledown }$
. (See Pt.1 Definitions 2.1–3.1 for the definitions of potent,
$\unicode{xb6}$
,
${Hist}$
and
$\mathit{Lev}$
.)
Lemma C.4 BLT
For any bevels
$r, s$
:
(1)
$s_{\triangledown }$
is helow, potent and transitive
(2)
$r \in s $
iff
$r_{\triangledown } \in s_{\triangledown }$
(3)
$s = \mathbf{B}(s_{\triangledown })$
(4)
$s_{\triangledown } = \unicode{xb6}{h} = \unicode{xb6}^{\triangledown }(h)$
, where
$h = \{r_{\triangledown } \in s_{\triangledown } : \mathit{Bev}(r)\}$
.
(5)
$s_{\triangledown }$
is a level
$^{\triangledown }$
Proof
(1) By Lemma C.2,
$s_{\triangledown }$
is helow; then
$s_{\triangledown }$
is potent and transitive as s is potent
$_{\notin }$
and transitive
$_{\notin }$
.
(2) Left-to-right. By (1). Right-to-left. Let
$r_{\triangledown } \in s_{\triangledown }$
. So
$r \neq s$
, since
$r_{\triangledown } \notin r_{\triangledown }$
. Similarly,
$s_{\triangledown } \notin r_{\triangledown }$
, since
$s_{\triangledown }$
is transitive; so
$s \notin r$
by left-to-right. So
$r \in s$
, by Lemma A.9.
(3) Induction on bevels, using (2).
(4) By (1) and Lemma C.2, h is helow. If
$a \in \unicode{xb6}{h}$
, then
$a \in s_{\triangledown }$
as
$s_{\triangledown }$
is potent by (1). Conversely, if
$a \in s_{\triangledown }$
, then
$a \subseteq r \in s$
for some bevel r by Lemma A.8, and
$a \subseteq r_{\triangledown } \in s_{\triangledown }$
by (2) and Lemma C.2, so
$a \in \unicode{xb6}{h}$
. So
$s_{\triangledown } = \unicode{xb6}{h}$
. Repeated use of Lemma C.2, as in Lemma C.3, now yields that
$\unicode{xb6}{h} = \unicode{xb6}^{\triangledown }(h)$
.
(5) With h as in (4), since
$s = \unicode{xb6}^{\triangledown }(h)$
it suffices to show that
${Hist}^{\triangledown }(h)$
. If
$r_{\triangledown } \in h$
, then
$r_{\triangledown } \cap h = \{q_{\triangledown } \in r_{\triangledown } : \mathit{Bev}(q)\}$
, by (1); so
$r_{\triangledown } = \unicode{xb6}^{\triangledown }{(r _{\triangledown } \cap h)}$
by (4).
Lemma C.5 BLT
The levels
$^{\triangledown }$
are the
$\text{bevels}_{\triangledown }$
, i.e.:
$\mathit{Lev}^{\triangledown }(a)$
iff
$(\exists s : \mathit{Bev})a = s_{\triangledown }$
.
Proof By Lemma C.4, if s is a bevel then both
$\mathit{Lev}^{\triangledown }(s_{\triangledown })$
and
$\mathbf{B}(s_{\triangledown }) = s$
. To complete the proof, it suffices to note that if p and q are distinct levels
$^{\triangledown }$
, then
$\mathbf{B}p \neq \mathbf{B}q$
; this follows from Lemma A.10.6 and the fact that the levels
$^{\triangledown }$
are well-ordered by
$\in $
. (The well-ordering of levels
$^{\triangledown }$
is Pt.1 Theorem
$\text {3.10}^{\triangledown }$
, which holds via Lemma C.3.)
Corollary C.6 BLT
$\text{Stratification}^{\triangledown }$
holds; Endless
$_{\notin }$
proves Endless
$^{\triangledown }$
; Infinity
$_{\notin }$
proves
$\text{Infinity}^{\triangledown }$
; and Unbounded
$_{\notin }$
proves Unbounded
$^{\triangledown }$
.
Recalling that
$\text {LT}{+} \mathrm{Infinity}{+} \mathrm{Unbounded}$
is equivalent to ZF (see Section 6), Lemmas C.3 and C.6 yield Theorem 6.2.
Appendix D Definitional equivalence
In this appendix, I prove the definitional equivalence discussed in Section 7.Footnote 40
D.1 Interpreting BLT
$_{\mathbf{ZF}}$
in ZF
I first define an interpretation,
${I}$
, to simulate (extensions of) BLT within (extensions of) LT. The key idea is to use
$\emptyset $
as a flag to indicate whether to treat a set as low or high. To allow
$\emptyset $
to play this role, I define a bijection
$\sigma : V \longrightarrow V \setminus \{\emptyset \}$
:Footnote
41
$$ \begin{align*} \sigma(a) &\mathrel{\mathord{:}\mathord{=}} \begin{cases} \{a\}&\text{if }a\text{ is a Zermelo number,}\\ a&\text{otherwise,} \end{cases} \end{align*} $$
where the Zermelo numbers are
$0 = \emptyset $
and
$n+1 = \{n\}$
. I then interpret membership thus:
$$ \begin{align*} x \mathrel{\in^{{I}}} a &\text{ iff } (\sigma(x) \in a \leftrightarrow \emptyset \notin a). \end{align*} $$
Since
$\sigma (a) \notin a$
for all a, it follows that
$a \mathrel {\notin ^{{I}}} a$
iff
$\emptyset \notin a$
(i.e., a is treated as low), and
$a \mathrel {\in ^{{I}}} a$
iff
$\emptyset \in a$
(i.e. a is treated as high). I will now prove a sequence of results which establish that
${I}$
is an interpretation of BLT. The first few are straightforward:
Lemma D.1
$\text {LT}_{+}$
Where
$a \subseteq ^{{I}} b$
abbreviates
$(\forall x \mathrel {\in ^{{I}}} a)x \mathrel {\in ^{{I}}} b$
:
(1) If
$\emptyset \notin a$
and
$\emptyset \notin b$
, then:
$a \subseteq b$
iff
$a \subseteq ^{{I}} b.$
(2) If
$\emptyset \in a$
and
$\emptyset \in b$
, then:
$a \supseteq b$
iff
$a \subseteq ^{{I}} b$
.
Proof
(1) Since
$\sigma $
is a bijection
$V \longrightarrow V \setminus \{\emptyset \}$
,
$a \subseteq b$
iff
$\forall x(\sigma (x) \in a \rightarrow \sigma (x) \in b)$
iff
$a \subseteq ^{{I}} b$
.
(2) Similarly,
$a \supseteq b$
iff
$\forall x(\sigma (x) \notin a \rightarrow \sigma (x) \notin b)$
iff
$a \subseteq ^{{I}} b$
.
Lemma D.2
$\text {LT}_{+}$
Extensionality
$^{{I}}$
holds.
Proof Suppose
$\forall x(x \mathrel {\in ^{{I}}} a \leftrightarrow x \mathrel {\in ^{{I}}} b)$
. If
$a \mathrel {\notin ^{{I}}} a$
but
$b \mathrel {\in ^{{I}}} b$
, then
$\forall x(\sigma (x) \in a \leftrightarrow \sigma (x) \notin b)$
, so that
$a \cup b = V$
, which is impossible. Generalising,
$a \mathrel {\in ^{{I}}} a$
iff
$b\mathrel {\in ^{{I}}} b$
. Now apply Lemma D.1.
Lemma D.3
$\text {LT}_{+}$
Separation
$_{\!\notin}^{{I}}$
holds.
Proof Fix F and
$a \mathrel {\notin ^{{I}}} a$
, i.e.,
$\emptyset \notin a$
. Using Separation, let
$b = \{\sigma (x) \in a : F(x)\}$
. Since
$\emptyset \notin b$
we have
$\forall x(x \mathrel {\in ^{{I}}} b \leftrightarrow (F(x) \land x \mathrel {\in ^{{I}}} a))$
.
The interpretation of complementation is obvious:
$\overline {a}^{{I}}= a \cup \{\emptyset \}$
if
$a \mathrel {\notin ^{{I}}} a$
, and
$\overline {a}^{{I}} = a \setminus \{\emptyset \}$
if
$a \mathrel {\in ^{{I}}} a$
. The next result follows trivially:
Lemma D.4
$\text {LT}_{+}$
$\forall a\forall x(x \mathrel {\in ^{{I}}} a \leftrightarrow x \mathrel {\notin ^{{I}}} \overline {a}^{{I}})$
, and Complements
$^{{I}}$
holds.
The only intricate part of this interpretation concerns the treatment of bevels. Within
$\text {LT}_{+}$
, we can define the von Neumann ordinals, and recursively define the following:
$$ \begin{align*}W_\gamma = \{\sigma(x) : (\exists \beta < \gamma)x \subseteq W_\beta \cup \{\emptyset\}\}.\end{align*} $$
Now
$\text {LT}_{+}$
proves that
$W_\gamma $
exists for each
$\gamma $
, and that these are the bevels
$^{{I}}$
:
Lemma D.5
$\text {LT}_{+}$
$\mathit{Bev}^{{I}}(s)$
iff
$s = W_\gamma $
for some
$\gamma $
.
Proof Lemmas D.2–D.4 show that
$\text {LT}_{+}$
proves
$\text {ECS}^{{I}}$
. Hence
$\text {LT}_{+}$
proves Theorem 4.1
$^{{I}}$
, i.e., that the bevels
$^{{I}}$
are well-ordered by
$\mathrel {\in ^{{I}}}$
. For induction on
$\gamma $
, suppose that if
$\beta < \gamma $
then
$W_\beta $
is the
$\beta ^{\text {th}}$
bevel
$^{{I}}$
. Let s be the
$\gamma ^{\text {th}}$
bevel
$^{{I}}$
. By Lemma D.1:
$$ \begin{align*} W_\gamma &= \{\sigma(x) : (\exists \beta < \gamma)x \subseteq W_\beta \cup \{\emptyset\}\}\\ &= \{\sigma(x) : (\exists \beta < \gamma)(x \subseteq^{{I}} W_\beta \lor \overline{x}^{{I}} \subseteq^{{I}} W_\beta)\}\\ &= \{\sigma(x) : (\exists W_\beta \mathrel{\notin^{{I}}} W_\beta \mathrel{\in^{{I}}} s)(x \subseteq^{{I}} W_\beta \lor \overline{x}^{{I}} \subseteq^{{I}} W_\beta)\}\\ &=(\mathbf{P}\{w \in s : \mathit{Bev}(w)\})^{{I}}. \end{align*} $$
So
$W_\gamma = s$
by Lemma A.8
$^{{I}}$
. By induction, the bevels
$^{{I}}$
are the
$W_\gamma $
s.
I can now prove the crucial proposition:
Lemma D.6
$\text {LT}_{+}$
Stratification
$_{\notin }^{{I}}$
holds.
Proof By Lemma D.5, it suffices to show that
$(\forall a \mathrel {\notin ^{{I}}} a)\exists \gamma \, \ a \subseteq ^{{I}} W_\gamma $
. Since the levels are well-ordered by
$\in $
(Pt.1 Theorem 3.10), we can write
$V_\gamma $
for the
$\gamma ^{\text {th}}$
level. I claim: if
$a \mathrel {\notin ^{{I}}} a \subseteq V_\gamma $
, then
$a \subseteq W_\gamma $
. For induction, suppose this holds for all ordinals
$\beta < \gamma $
. Fix
$a \mathrel {\notin ^{{I}}} a \subseteq V_\gamma $
. If
$\gamma = 0$
, then
$a = \emptyset \subseteq ^{{I}} W_0 = \emptyset $
. Otherwise, fix
$x \mathrel {\in ^{{I}}} a$
, i.e.,
$\sigma (x) \in a \subseteq V_\gamma $
; now
$x \subseteq V_\beta $
for some
$\beta < \gamma $
, by Pt.1 Lemma 3.12, so that
$x \subseteq W_\beta \cup \{\emptyset \}$
by the induction hypothesis; so
$\sigma (x) \in W_\gamma $
, i.e.,
$x \mathrel {\in ^{{I}}} W_\gamma $
. Generalising,
$a \mathrel {\subseteq ^{{I}}} W_\gamma $
.
Lemma D.7.
$\mathrm{LT}_+ \vdash \mathrm{BLT}_+^{{I}}$
and
$\mathrm{ZF} \vdash \mathrm{BLT}_{\mathrm{ZF}}^{{I}}$
.
Proof Lemmas D.2–D.6 establish that
$\text {LT}_+ \vdash \mathrm{BLT}^{{I}}$
. And
$\text {LT}_+ \vdash \text {Endless}_{\notin }^{{I}}$
, using Endless and our explicitly defined bevels
$^{{I}}$
, the
$W_\gamma $
s. Evidently, Infinity yields Infinity
$_{\notin }^{{I}}$
. For Unbounded
$_{\notin }^{{I}}$
, fix P and
$a \mathrel {\notin ^{{I}}} a$
; by Unbounded, the set
$c = \{\sigma (P(x)) : \sigma (x) \in a\}$
exists; by construction,
$\emptyset \notin c$
and
$(\forall x \mathrel {\in ^{{I}}} a)P(x) \mathrel {\in ^{{I}}} c$
. The result follows, since ZF is equivalent to
$\text {LT}{\,+}\ \mathrm{Infinity}{\,+}\ \mathrm{Unbounded}$
(see Section 6).
D.2 Interpreting ZF in BLT
$_{\mathbf{ZF}}$
I now switch to working in
$\mathrm{BLT}_{+}$
. Using
$\sigma $
—i.e., using verbatim the same definitions of ‘Zermelo number’ and of
$\sigma $
in
$\mathrm{BLT}_{+}$
as we used in
$\text {LT}_{+}$
—consider this function:
$$ \begin{align*} \eta(a) &= \begin{cases} \{\sigma(\eta(x)) : x \in a\}&\text{if }a\notin a, \\ \{\sigma(\eta(x)) : x \notin a\} \cup \{\emptyset\}&\text{if }a \in a. \end{cases} \end{align*} $$
I will prove that
$\eta $
is a bijection
$V \longrightarrow {Helo}$
. I then define a translation,
${J}$
, by stipulating:
$$ \begin{align*}x \mathrel{\in^{{J}}} a\text{ iff }\eta(x) \in \eta(a).\end{align*} $$
It will follow that
${J}$
is an interpretation of
$\text {LT}_{+}$
in
$\mathrm{BLT}_{+}$
.
Lemma D.8
$\mathrm{BLT}_{+}$
If
$\eta (a) = \eta (b)$
, then
$a = b$
.
Proof Let
$\eta (a) = \eta (b)$
, so that
$a \notin a \leftrightarrow b \notin b$
. For induction, suppose that
$\eta (x) = \eta (y) \rightarrow x = y$
for all
$x, y$
with
$\mathbf{B}x, \mathbf{B}y \in \mathbf{B}a \cup \mathbf{B}b$
. If
$a \notin a$
and
$b \notin b$
, then
$\{\sigma (\eta (x)) : x \in a\} = \{\sigma (\eta (x)) : x \in b\}$
, so that
$a = b$
by the induction hypothesis and the injectivity of
$\sigma $
. The case when
$a \in a$
is similar.
Lemma D.9
$\mathrm{BLT}_{+}$
$\eta (a)$
is helow, for any a.
Proof For induction, suppose that
$\eta (x)$
is helow for all x with
$\mathbf{B}x \in \mathbf{B}a$
. Suppose
$a \notin a$
; since
$\sigma (\eta (x))$
is helow iff
$\eta (x)$
is helow, every member of
$\eta (a)$
is helow; so
$\eta (a)$
is helow by Lemma C.2. The case when
$a \in a$
is similar.
Lemma D.10
$\mathrm{BLT}_{+}$
If a is helow, then
$a = \eta (c)$
for some c.
Proof By Lemma D.8,
$\eta ^{-1}$
is functional. For induction, suppose that for all helow
$z \in \mathbf{B}a$
, we have that
$\eta ^{-1}(z)$
is defined and
$\mathbf{B}(\eta ^{-1}(z)) \subseteq \mathbf{B}z$
.
If
$\emptyset \notin a$
, let
$c \notin c = \{\eta ^{-1}(\sigma ^{-1}(x)) \in \mathbf{B}a : x \in a\}$
using Separation
$_{\notin }$
. Fix
$x \in a$
; then
$\sigma ^{-1}(x) \in \mathbf{B}a$
and
$\sigma ^{-1}(x)$
is helow, recalling that a is helow and using Lemma C.2). Now
$\mathbf{B}(\eta ^{-1}(\sigma ^{-1}(x))) \subseteq \mathbf{B}(\sigma ^{-1}(x)) \in \mathbf{B}a$
by the induction hypothesis, i.e.,
$\eta ^{-1}(\sigma ^{-1}(x)) \in \mathbf{B}a$
. So
$c = \{\eta ^{-1}(\sigma ^{-1}(x)) : x \in a\}$
, so that
$a = \eta (c)$
and
$\mathbf{B}c \subseteq \mathbf{B}a$
.
If
$\emptyset \in a$
, then instead let
$c = \{\eta ^{-1}(\sigma ^{-1}(x)) : \emptyset \neq x \in a\}$
; now
$a = \eta (\overline {c})$
.⊣
Lemma D.11.
$\mathrm{BLT}_+ \vdash \mathrm{LT}_+^{{J}}$
and
$\mathrm{BLT}_{\mathrm{ZF}} \vdash \mathrm{ZF}^{{J}}$
.
D.3 The interpretations are inverse
It remains to show that
${I}$
and
${J}$
are mutually inverse, in the sense required for definitional equivalence.Footnote
42
The key lies in their treatments of the Zermelo numbers. Working informally, let
$\text {z}_n$
be the
$n^{\text {th}}$
Zermelo number, and let
$\text {v}_n$
be defined similarly, but starting from V rather than
$\emptyset $
, i.e.:
$$ \begin{align*} \text{z}_n &= \overbrace{\{\ldots \{}^{n\text{ times}}\emptyset\,\}\ldots\} & \text{v}_n= \overbrace{\{\ldots \{}^{n\text{ times}}V\,\}\ldots\} \end{align*} $$
We can now consider two sequences:
$$ \begin{align*} \begin{array}{llllllll} \text{z}_0, & \text{z}_1, & \text{z}_2, & \text{z}_3, & \ldots, & \text{z}_{2n}, & \text{z}_{2n+1}, & \ldots\\ \text{z}_0, & \text{v}_0, & \text{z}_1, & \text{v}_1, & \ldots, & \text{z}_n, & \text{v}_n, & \ldots \end{array} \end{align*} $$
Inutitively,
${I}$
treats the former sequence as the latter, and
${J}$
treats the latter as the former. The proof that
${I}$
and
${J}$
are mutually inverse simply builds on this intuitive thought.
Here are two facts which make the intuitive thought precise:
Lemma D.12
$\text {LT}_{+}$
$\forall x\, \ x \mathrel {\notin ^{{I}}} \emptyset $
, and
$\forall x\, \ x \mathrel {\in ^{{I}}} \{\emptyset \}$
, and
$\forall x(x \mathrel {\in ^{{I}}} \mathrm{z}_{n+2} \leftrightarrow x = \mathrm{z}_n)$
for all n.
Lemma D.13
$\mathrm{BLT}_{+}$
$\eta (\mathrm{z}_n) = \mathrm{z}_{2n}$
and
$\eta (\mathrm{v}_n) = \mathrm{z}_{2n+1}$
, for all n.
The proofs of both facts are trivial. Using the second fact, though, I can build up to the proof in
$\mathrm{BLT}_{+}$
that
$x \in a$
iff
$(x\mathrel {\in ^{{I}}} a)^{{J}}$
:
Lemma D.14
$\mathrm{BLT}_{+}$
The function
$\sigma ^{{J}}$
, i.e., the
${J}$
-interpretation of LT’s definition of
$\sigma $
, maps
$\mathrm{z}_n \mapsto \mathrm{v}_n \mapsto \mathrm{ z}_{n+1}$
, and
$x \mapsto x$
otherwise.
Proof Note that
$\text {z}_{2n} \in \text {z}_{2n+1} \in \text {z}_{2n+2}$
, with these membership facts unique. So
$\eta (\text {z}_{n}) \in \eta (\text {v}_{n}) \in \eta (\text {z}_{n+1})$
, by Lemma D.13, i.e.,
$\text {z}_{n} \mathrel {\in ^{{J}}} \text {v}_{n} \mathrel {\in ^{{J}}} \text {z}_{n+1}$
.
Lemma D.15
$\mathrm{BLT}_{+}$
$\eta (\sigma ^{{J}}(a)) = \sigma (\eta (a))$
, for all a.
Proof By Lemmas D.13–D.14, we have
$\eta (\sigma ^{{J}}(\text {z}_n)) = \eta (\text {v}_n) = \text {z}_{2n+1} = \sigma (\text {z}_{2n}) = \sigma (\eta (\text {z}_n))$
and
$\eta (\sigma ^{{J}}(\text {v}_n)) = \eta (\text {z}_{n+1}) = \text {z}_{2n+2} = \sigma (\text {z}_{2n+1}) = \sigma (\eta (\text {v}_n))$
. Now suppose
$a \neq \text {z}_n$
and
$a \neq \text {v}_n$
for any n, so that
$\sigma ^{{J}}(a) = a$
and hence
$\eta (\sigma ^{{J}}(a)) = \eta (a)$
; moreover,
$\eta (a) \neq \text {z}_n$
for any n by Lemma D.13; so
$\eta (\sigma ^{{J}}(a)) = \eta (a) = \sigma (\eta (a))$
.
Lemma D.16
$\mathrm{BLT}_{+}$
$\eta (\sigma ^{{J}}(x)) \in \eta (a) \leftrightarrow a \notin a$
iff
$x \in a$
Proof If
$a \notin a$
then
$\eta (a) = \{\eta (\sigma ^{{J}}(x)) : x \in a\}$
by Lemma D.15. If
$a \in a$
then
$\eta (a) = \{\eta (\sigma ^{{J}}(x)) : x \notin a\} \cup \{\emptyset \}$
, and note that
$\emptyset \neq \eta (\sigma ^{{J}}(x)) = \sigma (\eta (x))$
for all x.
Lemma D.17
$\mathrm{BLT}_{+}$
$x \in a$
iff
$(x \mathrel {\in ^{{I}}} a)^{{J}}$
Proof Using Lemma D.16 and the fact that
$a \notin a$
iff
$\eta (\emptyset ) = \emptyset \notin \eta (a)$
, note the following chain of equivalent formulas:
(1)
$x \in a$
(2)
$\eta (\sigma ^{{J}}(x)) \in \eta (a) \leftrightarrow \eta (\emptyset ) \notin \eta (a)$
(3)
$(\sigma (x) \in a \leftrightarrow \emptyset \notin a )^{{J}}$
(4)
$(x \mathrel {\in ^{{I}}} a)^{{J}}$
It remains to show in
$\text {LT}_{+}$
that
$x \in a$
iff
$(x \mathrel {\in ^{{J}}} a)^{{I}}$
. Working in
$\mathrm{BLT}_{+}$
, define
$\mu $
as a map sending
$\text {z}_{n+1} \mapsto \text {v}_n \mapsto \text {z}_n$
and
$x \mapsto x$
otherwise; by Lemma D.14, if
$x \neq \emptyset $
then
$\mu ^{-1}(x) = \sigma ^{{J}}(x)$
. We then have two quick results:
Lemma D.18
$\mathrm{BLT}_{+}$
$\eta (x) \in \eta (a)$
iff
$(x = \emptyset \land a \in a) \lor (x \neq \emptyset \land (\mu (x) \in a \leftrightarrow a \notin a))$
Proof If
$x = \emptyset $
, then
$\eta (\emptyset ) = \emptyset \in \eta (a)$
iff
$a \in a$
. If
$x \neq \emptyset $
; use Lemma D.16.
Lemma D.19
$\text {LT}_{+}$
If
$x \neq \emptyset $
, then
$\sigma (\mu ^{{I}}(x)) = x$
.
Proof By Lemma D.12,
$\mu ^{{I}}$
maps
$\text {z}_{n+2} \mapsto \text {z}_{n+1} \mapsto \text {z}_n$
, and
$x \mapsto x$
otherwise.
Lemma D.20
$\text {LT}_{+}$
$x \in a$
iff
$(x \mathrel {\in ^{{J}}} a)^{{I}}$
Proof Using Lemmas D.19 and D.18
$^{{I}}$
, note the following chain of equivalent formulas:
(1)
$x \in a$
(2)
$(\emptyset = x \land x \in a) \lor (\emptyset \neq x \land x \in a)$
(3)
$(\emptyset = x \land x \in a) \lor (\emptyset \neq x \land \sigma (\mu ^{{I}}(x)) \in a)$
(4)
$(\emptyset = x \land a \mathrel {\in ^{{I}}} a) \lor (\emptyset \neq x\land (\mu ^{{I}}(x) \mathrel {\in ^{{I}}} a \leftrightarrow \emptyset \notin a))$
(5)
$(\emptyset = x \land a \mathrel {\in ^{{I}}} a) \lor (\emptyset \neq x \land (\mu ^{{I}}(x) \mathrel {\in ^{{I}}} a \leftrightarrow a \mathrel {\notin ^{{I}}} a)) $
(6)
$((\emptyset = x \land a \in a) \lor (\emptyset \neq x \land (\mu (x) \in a \leftrightarrow a \notin a)))^{{I}}$
(7)
$(\eta (x) \in \eta (a))^{{I}}$
(8)
$(x \mathrel {\in ^{{J}}} a)^{{I}}$
Theorem 7.1 now follows from Lemmas D.7, D.11, D.17, and D.20.
D.4 Finitary cases of definitional equivalences
The base theories, LT and BLT, are not definitionally equivalent. To see this, consider:
$$ \begin{align*} \text{lt}(1) &\mathrel{\mathord{:}\mathord{=}} 1 & \text{blt}(1)&\mathrel{\mathord{:}\mathord{=}} 2\\ \text{lt}(n+1) &\mathrel{\mathord{:}\mathord{=}} 2^{\text{lt}(n)} & \text{blt}(n+1) &\mathrel{\mathord{:}\mathord{=}} 2^{\text{blt}(n)+1}. \end{align*} $$
Any model of LT with n levels has
$\text {lt}(n)$
sets, and any model of BLT with n bevels has
$\text {blt}(n)$
sets. In particular, there is a model of LT with four sets, but no model of BLT has four sets. So LT and BLT are not definitionally equivalent.
There is, though, a nice definitional equivalence when we insist that there are infinitely many sets but that every (low) set is finite. Concretely: let
$\text {LT}_{\textrm {{fin}}}$
be
$\text {LT}_+ + \lnot \mathrm{Infinity}$
, and let
$\mathrm{BLT}_{\textrm {{fin}}}$
be
$\mathrm{BLT}_+ + \lnot \mathrm{Infinity}_{\notin }$
. Our earlier results immediately entail that
$\text {LT}_{\textrm {{fin}}}$
and
$\mathrm{BLT}_{\textrm {{fin}}}$
are definitionally equivalent. Moreover, as noted in Pt.1 Section 7,
$\text {LT}_{\textrm {{fin}}}$
is equivalent to
$\mathrm{ZF}_{\textrm {{fin}}}$
. Finally,
$\mathrm{ZF}_{\textrm {{fin}}}$
and PA are definitionally equivalent.Footnote
43
So:
Lemma D.21.
PA,
$\mathrm{ZF}_{\mathrm{fin}}$
,
$\mathrm{LT}_{\mathrm{fin}}$
, and
$\mathrm{BLT}_{\mathrm{fin}}$
are definitionally equivalent.
Acknowledgments
Special thanks to Thomas Forster, Joel David Hamkins, Randall Holmes, and Brian King, for extensive discussion. Thanks also to Neil Barton, Sharon Berry, Luca Incurvati, Juliette Kennedy, Øystein Linnebo, Michael Potter, Chris Scambler, James Studd, Rob Trueman, Sean Walsh, Will Stafford, audiences at MIT, Oxford, and Paris, and anonymous referees for this journal.
