What we need to do is to replace the language of time and activity by the more bloodless language of potentiality and actuality. Parsons (Reference Parsons1977, p. 293)
Potentialists, such as Charles Parsons, Øystein Linnebo, and James Studd, think that the concept of set is importantly modal. Put thus, potentialism is a broad church; different potentialists will disagree on the precise details of the relevant modality.Footnote 1 My aim is shed light on potentialism, in general, using Level Theory, LT, as introduced in Part 1.
I start by formulating Potentialist Set Theory, PST. This uses a tensed logic to formalize the bare idea of a ‘potential hierarchy of sets’.Footnote 2 Though PST is extremely minimal, it packs a surprising punch (see Sections 1–4).
In the vanilla version of PST, we need not assume that time is linear. However, if we make that assumption, then the resulting theory is almost definitionally equivalent to LT, its non-modal counterpart (see Sections 5–8). This equivalence allows me to clarify Hilary Putnam’s famous claim, that modal and non-modal set theories express the same facts (see Section 9). Putting my cards on the table: I am not a potentialist, in part because I am so sympathetic with Putnam’s claim.
This paper presupposes familiarity with Part 1. My notation conventions are as in Pt.1 Section 0, with the addition that I use
$\vec {x}$
for an arbitrary sequence, writing things like
$F(\vec {x})$
rather than
$F(x_1, \ldots , x_n)$
. For readability, all proofs are relegated to the appendices.
1 Tense and possibility
Many potentialists hold that temporal language serves as a useful heuristic for their favoured mathematical modality. To illustrate the idea, consider what Studd calls the Maximality Thesis: ‘any sets can form a set’.Footnote 3 This Thesis is given a modal formulation. But, as Studd notes, it can be glossed temporally: ‘any sets will form a set’. Of course, no potentialist will take this temporal gloss literally. Nobody, after all, wants to countenance absurd questions like ‘which pure sets existed at noon today?’, or ‘which pure sets will exist by teatime?’Footnote 4 The idea, to repeat, is just that temporal language is a useful heuristic for the potentialist’s preferred modality.
To elaborate on this heuristic, consider the bare-bones story of (pure) sets, which I told and explored in Part 1, and which I will repeat here:
The Basic Story. Sets are arranged in stages. Every set is found at some stage. At any stage
$\textbf {s}$
: for any sets found before
$\textbf {s}$
, we find a set whose members are exactly those sets. We find nothing else at
$\textbf {s}$
.
We can regard the stages of this Story as moments of time. Regarded thus, the Basic Story adopts the tenseless view of time, according to which moments are just a special kind of object. But this tenseless approach serves potentialists poorly. At no stage is there a set of all the sets which are found at any stage, so this tenseless Story falsifies the claim ‘any sets will form a set’.
Familiarly, though, time can also be thought of in a tensed fashion. On the tensed approach, we do not quantify over moments or stages; rather, we use primitive temporal operators, like ‘it was the case that…’ or ‘previously: …’. And we can retell the Basic Story in tensed terms:
The Tensed Story. Always: for any sets that existed, there is a set whose members are exactly those sets; there are no other sets.
Unlike the Basic Story, this Tensed Story is compatible with the claim ‘(always:) any sets will form a set’.
Note, though, that I say ‘is compatible with’, rather than ‘entails’. If time abruptly ends, then some things will never form a set. And, by design, the Tensed Story is compatible both with the claim that time abruptly ends, and that time is endless. Otherwise put: it says nothing at all about the ‘height’ of any potential hierarchy. This silence is deliberate, for potentialists might disagree about questions of ‘height’.
Still, once potentialists have agreed to use tense as a heuristic for their preferred modality, I do not see how they could doubt that the Tensed Story holds of every potential hierarchy of sets. In what follows, then, I take it for granted that the Tensed Story presents us with the bare idea of a potential hierarchy.
2 Temporal logic for past-directedness
My first goal is to axiomatize the Tensed Story. For this, I will employ a temporal logic. In particular, I use a negative free second-order logic which assumes that time is past-directed. Here is a brief sketch of this past-directed-logic, with fuller explanations in footnotes. (Let me take this opportunity to flag that I am wholly indebted to Studd for the idea of investigating potentialism via temporal logic; see Section 10.2.)
We use ‘
$\mathrm{E}(x)$
’ as an existence predicate; it abbreviates ‘
$x = x$
’. We prohibit consideration of never-existent entities, and we insist that quantification and atomic truth require existence.Footnote
5
We have three temporal operators (with their obvious duals):Footnote
6
-
: A past-tense operator; gloss ‘
’ as ‘previously:
$\phi $
’ or ‘it was the case that
$\phi $
’. -
: A future-tense operator; gloss ‘
’ as ‘eventually:
$\phi $
’ or ‘it will be the case that
$\phi $
’.
-
${{\mathord {\Diamond }}}$
: An unlimited temporal operator; gloss ‘
${{\mathord {\Diamond }}}\phi $
’ as ‘sometimes:
$\phi $
’.
We have Necessitation rules: if
$\phi $
is a theorem, then so are both
and
. We then lay down schemes as follows:Footnote 7
The first two schemes are familiar distribution principles. The second two schemes ensure appropriate past/future interaction. The fifth scheme ensures that before is transitive. The last scheme characterizes past-directedness.Footnote
8
Given past-directedness, ‘sometimes:
$\phi $
’ amounts to ‘it was, is, will be, or was going to be the case that
$\phi $
’. So we adopt this scheme:
It follows that
${\mathord {\Diamond }}$
obeys S5. This completes my sketch of past-directed-logic.
In what follows, I will assume that potentialists are happy to use this temporal logic.Footnote
9
However, it is worth repeating that our potentialist only regards time as a heuristic. Ultimately, they want
${\mathord {\Diamond }}$
to express their favoured mathematical modality. So they will need to explain how (and why) their favoured modality decomposes into other operators,
and
, which obey past-directed-logic. This is a non-trivial demand; but, for the purposes of this paper, I assume it can be met.
3 Potentialist Stage Theory
Armed with past-directed-logic, the Tensed Story is easy to axiomatize. Let PST, for Potentialist Set Theory, be the result of adding these four axioms to past-directed-logic:
-
Mem
$_{{\mathord {\Diamond }}}$
$ \forall a {\mathord {\square }} \forall x({{\mathord {\Diamond }}} x \in a \rightarrow {\mathord {\square }}(\mathrm{E}(a) \rightarrow x \in a)),$
-
Ext
$_{{\mathord {\Diamond }}}$
$\forall a {\mathord {\square }} \forall b({\mathord {\square }} \forall x({{\mathord {\Diamond }}} x \in a \leftrightarrow {{\mathord {\Diamond }}} x \in b) \rightarrow {{\mathord {\Diamond }}} a = b),$
-
Priority
-
Spec
The first two axioms are not explicit in the Tensed Story, but I take it they are supposed to be something like analytic: roughly, Mem
${}_{{\mathord {\Diamond }}}$
says that each set a has its members essentially, and Ext
${}_{{\mathord {\Diamond }}}$
says that if everything which could (ever) be in a could be in b, and vice versa, then
$a = b$
(when they exist).Footnote
10
The next two axioms are explicit in the Story: Priority
says that a set’s members existed before the set itself, and Spec
says that, if every F existed earlier, then the set of Fs exists. So all of PST’s axioms are obviously true of the Tensed Story.
It is worth comparing PST with Stage Theory, ST (see Pt.1 Section 1). Indeed, we could equally think of PST as Potentialised Stage Theory, since it is little more than the most obvious reworking of ST using temporal logic.Footnote 11
4 The inevitability of well-foundedness and persistence
I have just shown that PST is a good formalization of the Tensed Story. As explained in Section 1, though, this Story articulates the bare idea of a potential hierarchy of sets. It follows that any potential hierarchy satisfies PST. This is significant, since PST is surprisingly rich.
To gauge PST’s depths, I will explain how it relates to Level Theory, LT, the non-modal theory which axiomatizes the (tenseless) Basic Story (see Pt.1 Sections 1–5). According to LT, the sets are arranged into well-ordered levels, where levels are sets which goes proxy for the stages of the Basic Story. Now, PST proves the following result (see Appendix A):
Theorem 4.1 PST
Where
$\textit{Max}(s)$
abbreviates
$(\mathrm{E}(s) \land \forall x\ x \subseteq s)$
:
-
(1)
$\mathrm{LT}$
holds, -
(2)
, -
(3)
$(\exists s : \textit{Lev})\textit{Max}(s)$
, -
(4)
$(\forall s : \textit{Lev}){\mathord {\Diamond }}\textit{Max}(s)$
.
If we consider a Kripke model of PST: (1) says that every possible world comprises a hierarchy of sets, arranged into well-ordered levels. Among other things, this yields well-foundedness, i.e.,
$\forall F(\exists x F(x) \rightarrow (\exists x : F) (\forall z : F)z \notin x)$
.Footnote
12
Then (2) is a statement of persistence; it says that, once a set exists, it exists forever after. Last, (3) says that every world has a maximal level, and (4) says that every level is some world’s maximal level. So, the worlds in a Kripke model of PST are, in effect, just arbitrary, persistent, initial segments of an (actualist) LT-hierarchy of pure sets.
I will develop the link between PST and LT over the next few sections. First, I want to highlight the significance of Theorem 4.1. The Tensed Story does not involve an explicit statement of well-foundedness or persistence. So one might try to entertain versions of the Tensed Story wherein well-foundedness or persistence fail: that is, one might try to entertain a potential hierarchy wherein time had no beginning, or wherein sets fade in and out of existence. But the foregoing remarks show that all such speculation is incoherent: every potentialist hierarchy must obey well-foundedness and persistence, since every potentialist hierarchy obeys PST, and PST proves Theorem 4.1. Echoing Scott, then, we see ‘how little choice there is in setting up’ a potential hierarchy of sets.Footnote 13
5 Linear Potentialist Stage Theory
So far, our potentialist has assumed that time is past-directed (to use the tensed-heuristic). If we also assume that time is linear, then we can obtain even deeper connections between PST and LT. I will spell out these connections in Sections 6–8; first, I must say a bit about linearity.
Formally, we can insist on linearity by adding these schemes to past-directed-logic:Footnote 14
As in Section 2, potentialists who want to use this linear-logic must explain why their favoured notion of mathematical possibility vindicates such linearity; this is a non-trivial challenge, but again I will not push it.Footnote 15 When using PST with this linear logic, I write LPST, for linear-PST.
By combining Theorem 4.1 with the assumption of linearity, we can simplify our ideology considerably. Intuitively, linearity allows us to gloss ‘previously’ as ‘when there are fewer things’, and to gloss ‘eventually’ as ‘when there are more things’. More precisely, we recursively define a translation,
$\bullet $
, whose only non-trivial clauses are as follows:Footnote
16
It is then easy to prove:
Lemma 5.1 LPST
$\phi \leftrightarrow \phi ^{\bullet }$
for any
$\mathrm{LPST}$
-formula
$\phi $
.
We can therefore rewrite LPST, without loss, as a modal theory which uses a single primitive modal operator,
${\mathord {\Diamond }}$
, which obeys S5 (for more, see Appendix B).
We can go even further, though, and eliminate all modal notions from LPST. The rough idea is straightforward. Theorem 4.1 says that levels simulate possible worlds, and vice versa. By assuming linearity, we can obtain results which say: actual hierarchies simulate potential hierarchies, and vice versa.
That way of putting things is, however, rather rough. The details of the simulation are in fact quite fiddly. I will therefore divide my discussion into three sections. In Section 6, I consider a deductive version of this simulation. This is suitable for first-order versions of LT and LPST, which I call
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
.Footnote
17
In Section 7, I consider a semantic version of this first-order simulation. Finally, in Section 8, I consider deductive and semantic versions of this simulation for (various) second-order versions of LT and LPST.
6 Near-synonymy: first order, deductive
To interpret
${\mathrm{LT}}_1$
in
${\mathrm{LPST}}_{1}$
, we will simply replace what happens with what could happen. More precisely, we consider the following translation; following Studd, I call
$\phi ^{{\mathord {\Diamond }}}$
the modalization of
$\phi $
:Footnote
18
$$ \begin{align*} \alpha^{{\mathord{\Diamond}}} & \mathrel{\mathord{:}\mathord{=}} {\mathord{\Diamond}} \alpha, \text{for atomic }\alpha, \quad (\phi \land \psi)^{{\mathord{\Diamond}}} \mathrel{\mathord{:}\mathord{=}} (\phi^{{\mathord{\Diamond}}} \land \psi^{{\mathord{\Diamond}}}), \\ (\lnot \phi)^{{\mathord{\Diamond}}} &\mathrel{\mathord{:}\mathord{=}} \lnot\phi^{{\mathord{\Diamond}}}, \qquad\qquad\qquad \ \ \ (\exists x \phi)^{{\mathord{\Diamond}}} \mathrel{\mathord{:}\mathord{=}} {\mathord{\Diamond}} \exists x \phi^{{\mathord{\Diamond}}}. \end{align*} $$
Conversely, to interpret
${\mathrm{LPST}}_{1}$
in
${\mathrm{LT}}_1$
, we take the hint suggested by Theorem 4.1, and simply regard possible worlds as levels. More precisely, we consider the following translation; I call
$\phi ^s$
the levelling of
$\phi $
:Footnote
19
Note that levelling is defined using variables; to illustrate:
$(x \in y)^s$
is
$(x \in y \subseteq s)$
, but
$({{\mathord {\Diamond }}} x \in y)^s$
is
$(\exists t : \textit{Lev})x \in y \subseteq t$
. We now have a deep result about modalization and levelling (see Section B.1 in Appendix B):Footnote
20
Theorem 6.1. For any
${\mathrm{LT}}_1$
-formula
$\phi{:}$
-
(1) If
${\mathrm{LT}}_1 \vdash \phi $
, then
${\mathrm{LPST}}_{1} \vdash \phi ^{{\mathord {\Diamond }}}$
, -
(2)
${\mathrm{LT}}_1 \vdash \phi \leftrightarrow (\phi ^{{\mathord {\Diamond }}})^s$
.
For any
${\mathrm{LPST}}_{1}$
-formula
$\phi{:}$
-
(3) If
${\mathrm{LPST}}_{1} \vdash \phi $
, then
${\mathrm{LT}}_1 \vdash \textit{Lev}(s) \rightarrow \phi ^s$
, -
(4)
${\mathrm{LPST}}_{1} \vdash \textit{Max}(s) \rightarrow (\phi \leftrightarrow (\phi ^s)^{{\mathord {\Diamond }}})$
.
This result entails that modalization and levelling are faithful (see Corollary B.1). But Theorem 6.1 is much stronger than a statement of mutual faithful interpretability; it is almost a definitional equivalence between
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
. This claim, though, requires some explanation.Footnote
21
Roughly speaking, to say that two theories are definitionally equivalent is to say that each interprets the other, and that combining the interpretations gets us back exactly where we began. To make this rough idea precise for the case of first-order theories, we say that S and T are definitionally equivalent iff there are interpretations I and J such that for any
$\textrm {S}$
-formula
$\phi $
: (1) if
$\textrm {S} \vdash \phi $
then
$\textrm {T} \vdash \phi ^I$
; and (2)
$\textrm {S} \vdash \phi \leftrightarrow (\phi ^I)^J$
; and for any
$\textrm {T}$
-formula
$\phi $
: (3) if
$\textrm {T} \vdash \phi $
then
$\textrm {S} \vdash \phi ^J$
; and (4)
$\textrm {T} \vdash \phi \leftrightarrow (\phi ^J)^I$
. Clauses (1) and (3) tell us we have interpretations; clauses (2) and (4) make precise the idea that ‘combining the interpretations gets us back exactly where we began’.
The clauses of Theorem 6.1 are extremely similar to those of a paradigm definitional equivalence. So, Theorem 6.1 is almost a statement of definitional equivalence. Almost; but not quite. We must say something about s in clauses (3) and (4) of Theorem 6.1, thereby disrupting the similarity. So: we do not have a definitional equivalence; but we almost do.
Since ‘almost-definitional-equivalence’ is quite long-winded, and definitional equivalence is sometimes known as ‘synonymy’, I call this a (deductive) near-synonymy between
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
.
7 Near-synonymy: first-order, semantic
Theorem 6.1 is deductive, but we can extract semantic content from it. (In what follows, my discussion of modal semantics should be understood in terms of connected Kripke structures, i.e., variable domain Kripke structures where all worlds are path-connected.)Footnote 22
Modalization is defined syntactically, but it has obvious semantic import: as noted, it tells us to replace what happens with what could happen. This motivates a definition:Footnote 23
Definition 7.1. Let
$\mathcal {P}$
be any connected Kripke structure. Its flattening,
$\flat \mathcal {P}$
, is the following non-modal structure:
$\flat \mathcal {P}$
’s domain is
$\mathcal {P}$
’s global domain
$;$
and
$\flat \mathcal {P} \vDash a \in b$
iff
$\mathcal {P} \vDash {\mathord {\Diamond }} a \in b$
.
Levelling has similar semantic import: it tells us to regard possible worlds as levels. So:
Definition 7.2. Let
$\mathcal {A}$
be any non-modal structure. Its potentialization,
$\sharp \mathcal {A}$
, is the following connected Kripke structure:
$\sharp \mathcal {A}$
’s worlds are those s such that
$\mathcal {A}\vDash \textit{Lev}(s);$
accessibility is given by
$r < s$
iff
$\mathcal {A} \vDash r \in s; \sharp \mathcal {A}$
’s global domain is just
$\mathcal {A}$
’s domain;
$\sharp \mathcal {A} \vDash _{s} {a \in b}$
iff
$\mathcal {A} \vDash a \in b \subseteq s;$
and
$\sharp \mathcal {A} \vDash _{s} a = b$
iff
$\mathcal {A} \vDash a = b \subseteq s$
.
By considering flattening and potentialization, we can move between models of
${\mathrm{LT}}_1$
and connected Kripke models of
${\mathrm{LPST}}_{1}$
. To make this movement almost seamless (but only almost; see below), we need one last general construction; intuitively, this construction will allow us to take a Kripke structure,
$\mathcal {P}$
, and create a new structure,
$\mathcal {P}_{f}$
, by disrupting the ‘identities’ of
$\mathcal {P}$
’s worlds (and perhaps duplicating some worlds):
Definition 7.3. Let
$\mathcal {P}$
be any connected Kripke structure. Let f be any surjection whose range is
$\mathcal {P}$
’s set of worlds. Then
$\mathcal {P}_{f}$
is the following connected Kripke structure:
$\mathcal {P}_{f}$
’s set of worlds is
$\mathrm{dom}(f);$
accessibility is given by
$\textbf {v} < \textbf {w}$
in
$\mathcal {P}_{f}$
iff
$f(\textbf {v}) < f(\textbf {w})$
in
$\mathcal {P};$
$\mathcal {P}_{f}$
has the same global domain as
$\mathcal {P};$
and
$\mathcal {P}_{f} \vDash _{\textbf {w}} R(\vec {a})$
iff
$\mathcal {P} \vDash _{f(\textbf {w})} R(\vec {a})$
for all R
$($
including identity
$)$
.
We now have the following result (see Section B.2 in Appendix B):Footnote 24
-
(1) If
$\mathcal {P} \vDash {\mathrm{LPST}}_{1}$
, then
$\flat \mathcal {P} \vDash {\mathrm{LT}}_1$
. -
(2) If
$\mathcal {P} \vDash {\mathrm{LPST}}_{1}$
, then there is a surjection f such that
$\mathcal {P} = ({\sharp \flat \mathcal {P}})_{f}$
. -
(3) If
$\mathcal {A} \vDash {\mathrm{LT}}_1$
, then
$\sharp \mathcal {A} \vDash {\mathrm{LPST}}_{1}$
. -
(4) If
$\mathcal {A} \vDash {\mathrm{LT}}_1$
, then
$\mathcal {A} = {\flat \sharp \mathcal {A}}$
.
This is a semantic reworking of Theorem 6.1. Consequently, it is almost a statement of (semantic) definitional equivalence. Recall that, roughly speaking, two theories are definitionally equivalent iff each interprets the other, and that combining the interpretations gets us back exactly where we began. In Section 6, I precisely defined this idea for (non-modal) first-order theories in deductive terms. The same idea can be defined in semantic terms. To say that
$\textrm {S}$
and
$\textrm {T}$
are definitionally equivalent is to say that they (respectively, and uniformly from interpretations) define operations, g and h, such that: if
$\mathcal {B} \vDash \textrm {T}$
, then both (1)
$g\mathcal {B} \vDash \textrm {S}$
and (2)
$\mathcal {B} = hg\mathcal {B}$
; and if
$\mathcal {A} \vDash \textrm {S}$
, then both (3)
$h\mathcal {A} \vDash \textrm {T}$
and (4)
$\mathcal {A} = gh\mathcal {A}$
. Clauses (1) and (3) tell us that we have interpretations; clauses (2) and (4) make precise the idea that ‘combining the interpretations gets us back exactly where we began’.
Theorem 7.4 has a very similar shape. So it is almost a (semantic) statement of definitional equivalence between
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
. Again, though: almost, but not quite. Clause (2) of Theorem 7.4 does not tell us that
$\mathcal {P} = {\sharp \flat \mathcal {P}}$
, as a definitional equivalence would require, but introduces a slight wrinkle. So I will say that we have a semantic near-synonymy.
The wrinkle I just mentioned is unavoidable. Fix some
$\mathcal {O} \vDash {\mathrm{LPST}}_{1}$
and f so that
$\mathcal {O} \neq {\mathcal {O}}_{f}$
. Clearly
$\flat \mathcal {O} = \flat ({\mathcal {O}}_{f})$
, so that
${\sharp \flat \mathcal {O}} = {\sharp \flat ({\mathcal {O}}_{f})}$
; so we cannot in general have that
$\mathcal {P} = {\sharp \flat \mathcal {P}}$
. Moreover, this scarcely depends upon the specific definitions of flattening and potentialization; it is an inevitable consequence of the fact that modal semantics has an extra degree of freedom compared with non-modal semantics (the ‘identities’ of worlds, which f can disrupt).
8 Near-synonymy: second-order
I have outlined near-synonymies for the first-order theories
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
. I now want to consider near-synonymies for the second-order theories.
In what follows, I assume that LT’s (non-modal) background logic treats second-order identity as co-extensionality, i.e.,
$\forall F \forall G(\forall \vec {x}(F(\vec {x}) \leftrightarrow G(\vec {x})) \rightarrow F = G)$
. Similarly, I assume that all potentialists treat second-order identity as co-intensionality, i.e.:
-
Coint
$\forall F {\mathord {\square }} \forall G({\mathord {\square }} \forall x_1 \ldots {\mathord {\square }} \forall x_n({\mathord {\Diamond }} F(\vec {x}) \leftrightarrow {\mathord {\Diamond }} G(\vec {x})) \rightarrow {\mathord {\Diamond }} F = G)$
.
To take things further, though, I must separately consider two different approaches to second-order entities: necessitism and contingentism.Footnote 25
8.1 Second-order necessitism
Second-order necessitism treats second-order entities as necessary existents. We can implement this formally via these axioms:
-
Ex
${}_{\textrm {n}}$
$\mathrm{E}(F)$
, for any second-order variable ‘F’, -
Comp
$_{\mathrm{{n}}}$
$\exists F {\mathord {\square }} \forall x_1 \ldots {\mathord {\square }} \forall x_n({\mathord {\Diamond }} F(\vec {x}) \leftrightarrow {\mathord {\Diamond }}\phi)$
, for any formula
$\phi $
not containing ‘F’, -
Inst
$_{\mathrm{{n}}}$
$\forall F {\mathord {\square }} \forall x_1 \ldots {\mathord {\square }} \forall x_n({\mathord {\Diamond }} F(\vec {x}) \rightarrow {\mathord {\square }} ((\mathrm{E}(x_1) \land \cdots \land \mathrm{E}(x_n)) \rightarrow F(\vec {x})))$
.
The scheme Ex
${}_{\textrm {n}}$
guarantees that every second-order entity is a necessary existent. Comp
${}_{\textrm {n}}$
is a kind of potentialized Comprehension principle. Then Inst
${}_{\textrm {n}}$
guarantees that second-order entities have their instances essentially (cf. Mem
${}_{{\mathord {\Diamond }}}$
).
Let
${\mathrm{LPST}}_{{\textrm {n}}}$
, for necessitist-LPST, add these axioms and Coint to LPST.Footnote
26
Unsurprisingly, our earlier results are easily extended, to show that LT and
${\mathrm{LPST}}_{{\textrm {n}}}$
are deductively and semantically near-synonymous (see Theorems B.2 and B.6).
8.2 Second-order contingentism
In contrast with necessitism, second-order contingentism holds that a second-order entity exists iff all its (possible) instances do. Contingentists will therefore spurn Ex
${}_{\textrm {n}}$
, Inst
${}_{\textrm {n}}$
, and Comp
${}_{\textrm {n}}$
, and instead adopt:
-
Ex
$_{\mathrm{{c}}}$
${\mathord {\Diamond }} \mathrm{E}(F)$
, for any second-order variable ‘F’, -
Inst
$_{\mathrm{{c}}}$
$\forall F {\mathord {\square }} \forall x_1 \ldots {\mathord {\square }} \forall x_n({\mathord {\Diamond }} F(\vec {x}) \rightarrow {\mathord {\square }}(\mathrm{E}(F) \rightarrow F(\vec {x})))$
,
retaining plain-vanilla Comprehension. Call the result
${\mathrm{LPST}}_{{\textrm {c}}}$
, for contingentist-LPST.
Potentialists who treat (monadic) second-order quantification as plural quantification are likely to be contingentists.Footnote
27
After all, necessitism proves
$\exists F \lnot {\mathord {\Diamond }} \exists a {\mathord {\square }} \forall x({\mathord {\Diamond }} F(a) \leftrightarrow {\mathord {\Diamond }} x \in a)$
; read plurally, this contradicts the Maximality Thesis, that any sets can form a set (see Section 1). Moreover, the same example establishes that LT and
${\mathrm{LPST}}_{{\textrm {c}}}$
are not deductively near-synonymous. After all, LT proves
$\exists F \lnot \exists a \forall x(F(a) \leftrightarrow x \in a)$
, whose modalization will contradict the Maximality Thesis.
Instead,
${\mathrm{LPST}}_{{\textrm {c}}}$
is deductively and semantically near-synonymous with a weakened version of LT. To obtain this weakening, note that contingentists, in effect, restrict second-order entities to the worlds at which their instances occur. Since worlds go proxy for levels, the non-modal equivalent should restrict second-order entities to those which are bounded by levels. Specifically, let
$\vec {x}\subseteq s$
abbreviate
$(x_1 \subseteq s \land \cdots \land x_n \subseteq s)$
, and let
$F \sqsubseteq s$
abbreviate
$\forall \vec {x}(F(\vec {x}) \rightarrow \vec {x} \subseteq s)$
. Then bounded Level Theory,
${\mathrm{LT}}_{{\textrm {b}}}$
, is the theory whose axioms are Extensionality, Separation, Stratification, and:
-
Strat
$_{\mathrm{{b}}}$
$\forall F(\exists s : \textit{Lev})F \sqsubseteq s$
, -
Comp
$_{\mathrm{{b}}}$
$(\forall s : \textit{Lev})(\exists F \sqsubseteq s)(\forall \vec {x} \subseteq s)(F(\vec {x}) \leftrightarrow \phi)$
, for any
$\phi $
not containing ‘F’,
with Comp
${}_{\textrm {b}}$
replacing the usual Comprehension scheme. Our earlier results can then be extended, to show that
${\mathrm{LPST}}_{{\textrm {c}}}$
and
${\mathrm{LT}}_{{\textrm {b}}}$
are near-synonymous, both deductively and for a Henkin semantics (see Theorems B.3 and B.7).
So far, deductive and semantic results have gone hand-in-hand. However, they can be prised apart, by considering full semantics for second-order logic. For non-modal structures, full (actualist) semantics treats the (monadic) second-order domain as the powerset of the first-order domain. For connected Kripke structures, full contingentist semantics treats a world’s (monadic) second-order domain as the powerset of that world’s first-order domain. This full semantics is sufficiently rich, that
${\mathrm{LPST}}_{{\textrm {c}}}$
is not merely near-synonymous with
${\mathrm{LT}}_{{\textrm {b}}}$
, but with LT itself (see Theorem B.8).
9 The significance of the near-synomies
This table summarises the near-synonymies of Sections 6–8:
To appreciate the significance of these results, consider Paula, a potentialist who uses linear time as a heuristic for her favourite mathematical modality. Paula admires the mathematical work undertaken within
$\mathrm{ZF}_1$
. However, she regards
$\mathrm{ZF}_1$
as lamentably actualist, since it lacks modal operators. Fortunately, there is an extension of
${\mathrm{LPST}}_{1}$
—call it
$\textrm {LPZF}_1$
— which is near-synonymous with
$\mathrm{ZF}_1$
.Footnote
28
Leaning on this near-synonymy, Paula can regard (worryingly actualist)
$\mathrm{ZF}_1$
as a notational-variant of (reassuringly potentialist)
$\textrm {LPZF}_1$
. Indeed, by modalization and levelling, Paula can move fluidly between
$\mathrm{ZF}_1$
and
$\textrm {LPZF}_1$
.
The same idea cuts the other way. Actualist Alan may initially be somewhat perplexed by the boxes and diamonds which pepper Paula’s work. But Alan need not remain confused for long: modalization and levelling allow him to make perfect sense of Paula, as using a notational-variant of
$\mathrm{ZF}_1$
.
9.1 Outlining an Equivalence Thesis
The ease with which Paula and Alan can communicate with each other, despite their philosophical differences, suggests a further thought:
The Potentialist/Actualist Equivalence Thesis. Actualism and potentialism do not disagree; they are different but equivalent ways to express the same facts.
Putnam was the foremost proponent of such a Thesis.Footnote 29 I will say more about Putnam in Section 9.4; first, I want to assess the Equivalence Thesis directly. Specifically, I want to consider the following, concrete argument for the Equivalence Thesis:
-
(a) LT correctly axiomatizes the idea of an actual hierarchy of sets.
-
(b) LPST correctly axiomatizes the idea of a (linear) potential hierarchy of sets.
-
(c) Theories like LT and LPST are near-synonymous.
-
So: the Equivalence Thesis obtains.
I am very sympathetic to this argument. However, I am not yet certain of its soundness. In the remainder of this section, I will explain how the argument is best resisted, but also suggest that the Equivalence Thesis remains plausible in the face of such resistance.
The first two premises of the argument are perfectly secure: I established (a) in Pt.1 Sections 1–5, and (b) in Sections 1–4 of this paper. But I should emphasise the caveat in (b). Whilst every potentialist should accept PST, embracing linearity requires a further step. So: this argument for the Equivalence Thesis can be resisted, straightforwardly, by denying that potentialists can/should assume linearity.
Premise (c), however, contains a sneaky weasel-clause, ‘theories like…’. I will criticise this weaseling in Section 9.3. My more pressing concern, though, is whether we could even hope to infer the Equivalence Thesis from (a)–(c).Footnote 30
9.2 On drawing philosophical conclusions from formal equivalences
Near-synomy is an extremely tight, formal, equivalence between modal and non-modal theories. Still, theories can be an equivalent in some purely formal sense, whilst being non-equivalent in other important senses.
To illustrate, suppose Noddy systematically calls red things ‘green’ and green things ‘red’. Defining interpretations by swapping colour-predicates, Noddy’s theory of the empirical world may be definitionally equivalent with my own. Still, if we hold fixed the interpretation of colour-predicates, then we will say that Noddy’s theory is simply mistaken; Noddy says ‘grass is red’, but grass is green.
This noddy example illustrates a simple moral: whether formally equivalent theories ‘express the same facts’ depends upon how firmly we have pinned down the interpretation of the theories’ expressions. In the case of Noddy, the relevant expressions are colour-predicates. In discussing the Potentialist/Actualist Equivalence Thesis, the relevant expressions are quantifiers and modal operators. And this indicates how discussions of the Equivalence Thesis are likely to play out.
Suppose you think that we have a firm grasp on the concepts used within the metaphysics of mathematics. In particular, suppose you are convinced that there is a clear difference in meaning between ‘there is’ and ‘there could be’ (as used by potentialists), which does not depend upon their use in any particular formal theories. The near-synonymies essentially ask you to move between what ‘there is’ and what ‘there could be’. Given your prior conviction, you will regard this as a change in subject matter. So you will insist that actualism and potentialism make different claims, and reject the Equivalence Thesis.
Suppose instead, though, that you embrace a rather different attitude. You think that, in advance of any particular formal theorising, it is not entirely clear how one might go about distinguishing between the meanings of ‘there is’ and ‘there could be’ (in mathematical contexts). Indeed, you think that any differences in their meaning would have to be revealed by differences in their use. In that case, you will likely find the argument of Section 9.1 extremely compelling. After all, the near-synonymies establish that there is no significant difference between ‘
$\exists $
’ in
${\mathrm{LT}}_1$
and ‘
${\mathord {\Diamond }}\exists $
’ in
${\mathrm{LPST}}_{1}$
.Footnote
31
9.3 Equivalence and contingentist-potentialism
The case of
${\mathrm{LT}}_1$
and
${\mathrm{LPST}}_{1}$
is, though, the very simplest case. The situation concerning second-order theories is more complicated, and this merits scrutiny.
Consider Edna, a potentialist who (i) embraces contingentism and (ii) thinks that time is endless, who also (iii) uses second-order logic, whilst (iv) eschewing the full semantics. So Edna embraces an extension of
${\mathrm{LPST}}_{{\textrm {c}}}$
.Footnote
32
As we saw in Section 8.2, though, this theory is not near-synonymous (whether deductively or using Henkin semantics) with an extension of LT; we must retreat to
${\mathrm{LT}}_{{\textrm {b}}}$
. Edna therefore takes issue with the weasel-clause in premise (c) of the argument for the Equivalence Thesis. Indeed, she goes further, rebutting the argument as follows: actualists will insist that
$\exists F \lnot \exists a \forall x (F(x) \leftrightarrow x \in a)$
; the modalization of this claim is
${\mathord {\Diamond }} \exists F \lnot {\mathord {\Diamond }} \exists a {\mathord {\square }} \forall x({\mathord {\Diamond }} F(x) \leftrightarrow {\mathord {\Diamond }} x \in a)$
; this is inconsistent with her favourite potentialist set theory; so potentialism and actualism genuinely disagree.Footnote
33
This rebuttal of the Equivalence Thesis is exactly as strong as our grasp on the relevant ideology. If we have a firm grasp of Edna’s intended potentialist modality (independently of the formalism), and how that modality contrasts with actuality, and of the sense of (higher-order) quantification, and why contingentism (but not the use of full second-order semantics) is suitable, then Edna’s rebuttal will succeed. For, in that case, attempts to move between discussing what ‘there is’ and what ‘there could be’ will amount to a change in truth-value, and therefore also a change in subject matter. But if our grasp of the relevant ideology is insufficiently firm, then Edna’s worry will melt away. Edna, then, presents us with an interesting way to resist the Equivalence Thesis, which dovetails with the line of resistance offered in Section 9.2.
The upshot is that the failure or success of the Equivalence Thesis turns on whether potentialists can supply us with a sufficiently firm grasp of their favoured metaphysical-mathematical-modal concepts. I am genuinely unsure whether they can, but I cheerfully present this as a challenge.
9.4 Putnam on the equivalence of modal and non-modal theories
To conclude my discussion of the Equivalence Thesis, I want to revisit Putnam. As mentioned in Section 9.1, the Thesis is hugely indebted to Putnam, who claimed in Reference Putnam1967 that modal and non-modal theories are ‘equivalent’. However, it is worth emphasizing a few of the differences between Putnam’s Reference Putnam1967 claim and my Equivalence Thesis.
First. Putnam did not say much about the modality he had in mind, except to connect ‘
${\mathord {\Diamond }}$
’ with possible ‘standard concrete models for Zermelo set theory’.Footnote
34
My discussion is restricted to a potentialist modality, though I have deliberately left room for various different versions of potentialism.Footnote
35
Second. Putnam did not precisely define the formal notion of ‘equivalence’ he had in mind. He sometimes considers the mutual interpretability of modal and non-modal theories;Footnote 36 but mutual interpretability is far too weak to sustain anything like the Equivalence Thesis.Footnote 37 By contrast, my formal notion of ‘equivalence’ is near-synonymy.
Third. Putnam ultimately retracted his version of the Equivalence Thesis.Footnote 38 He claimed that mathematics is ‘about proofs, ways of conceiving of mathematical problems, mathematical approaches, and much more’, and worried that his interpretation would not preserve such things. Now, these considerations might tell against Putnam’s Reference Putnam1967 claim; but they only highlight the plausibility of my Equivalence Thesis. My near-synonymies simply formalize the intuitive and obvious point that LT’s levels simulate LPST’s possible worlds, and vice versa (see Section 5); this simulation straightforwardly preserves proofs; and this is precisely why it is so plausible that LT and LPST do not really differ over ‘ways of conceiving mathematical problems, mathematical approaches’, or anything else that matters.
Fourth. Having decided that modal and non-modal formulations of set theory genuinely disagree, Putnam came to favour the former, on the grounds that non-modal set theories face ‘a generalization of a problem first pointed out by Paul Benacerraf…, e.g., are sets a kind of function or are functions a sort of set’?Footnote 39 Again, this might detract from Putnam’s Reference Putnam1967 claim, but it has no force against my Equivalence Thesis. If LT and LPST are equally good in all other regards—as I think they might be—then choosing potentialism (with its distinctive modality) over actualism (with its distinctive ontology) is exactly as arbitrary as saying that functions are a kind of set (rather than vice versa).
10 Conclusion, and predecessors
The Tensed Story articulates the bare idea of a potential hierarchy of sets. PST axiomatizes that bare idea. Whilst it takes no stance on the height of any potential hierarchy, it ensures persistence and well-foundedness. Moreover, versions of PST are near-synonymous with versions of the non-modal theory LT. And these near-synonymies both sharpen and leave plausible the idea that there is no deep difference between actualism and potentialism.
I will close this paper by comparing PST with some alternative potentialist set theories.
10.1 Parsons and Linnebo
In formulating their modal set theories, Parsons and Linnebo do not use a temporal logic.Footnote
40
Instead, they use a single modal operator,
${\mathord {\Diamond }}$
, whose background logic is S4.2, and which can be glossed as ‘now and henceforth’.
The asymmetry of this operator generates a deep expressive problem.Footnote
41
Stated non-modally: there is a stage (the initial stage) at which nothing has any members. Potentialists should therefore want to be able to prove: possibly, nothing has any members, i.e.,
${\mathord {\Diamond }} \forall x \forall y\, \ x \notin y$
. But this cannot be a theorem for Parsons or Linnebo. To see why, suppose otherwise; then
${\mathord {\square }} {\mathord {\Diamond }} \forall x \forall y\, \ x \notin y$
is also a theorem, by Necessitation; but this is catastrophic, for it catastrophically entails that there is always a later moment at which nothing has any members.
This problem does not arise in PST. There,
${\mathord {\Diamond }}$
obeys S5, and PST proves
${\mathord {\Diamond }} \forall x \forall y\, x \notin y$
.
10.2 Studd
In using a tensed logic to formulate PST, I am entirely indebted to Studd. Moreover, Studd proves a result like Theorem 6.1 for his modal set theory, MST. So my PST is similar to Studd’s MST, and owes a great deal to it. However, it is worth noting two differences.
The minor difference concerns our versions of Priority
. Studd’s MST has: all of a’s members are found together before a is found.Footnote
42
My PST has: each of a’s members is found before a is found. The slight difference emerges only at limit worlds:Footnote
43
in Studd’s MST, a exists at a limit world iff a existed earlier; in my PST, a exists at a limit world iff all of a’s members existed earlier.
The major difference concerns the richness of Studd’s modal schemes. Studd’s MST explicitly adopts modal axioms which guarantee linearity, persistence, well-ordering, and that time is endless.Footnote 44 My PST only assumes past-directedness, and instead proves persistence and well-foundedness (see Section 4). Proof has three virtues over explicit assumption. First: my PST is considerably leaner than Studd’s MST. Second: it will be strictly easier for potentialists to try to explain why they are entitled to assume past-directedness, than to try to justify Studd’s richer assumptions.Footnote 45 Third: as in Section 4, the proofs of persistence and well-foundedness show ‘how little choice there is in setting up’ a potential hierarchy.
Appendix A Elementary results concerning PST
The time has come to prove the results stated in Part 2. I will start with some elementary results within PST, building up to Theorem 4.1 of Section 4. My proofs are semantic, relying on standard soundness and completeness results for (connected) Kripke frames. I use bold letters,
$\textbf {w}, \textbf {v}, \textbf {u}, \ldots $
, for arbitrary worlds (note that this differs from my use of bold letters in Pt.1 and Pt.3).
In what follows, we must not assume that expressions like ‘
$\{x : \phi (x)\}$
’ are rigid designators; we should read ‘
$a = \{x : \phi (x)\}$
’ as abbreviating ‘
$\forall x(x \in a \leftrightarrow \phi (x))$
’, which may be true in one world and false in another. Similarly, recall that ‘
’ abbreviates ‘
$\forall x(x \in a \leftrightarrow \exists c(x \subseteq c \in b))$
’.
I start with two very elementary results:
Lemma A.1 PST
Extensionality holds.
Proof Fix a and b at
$\textbf {w}$
, and assume
$\vDash _{\textbf {w}} \forall x(x \in a \leftrightarrow x \in b)$
. Fix x at world
$\textbf {u}$
, now
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in a$
iff
$\vDash _{\textbf {w}} x \in a$
(by Mem
${}_{{\mathord {\Diamond }}}$
) iff
$\vDash _{\textbf {w}} x \in b$
iff
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in b$
; so
$\vDash _{\textbf {u}} {\mathord {\Diamond }} a = b$
by Ext
${}_{{\mathord {\Diamond }}}$
. Hence
$\vDash _{\textbf {w}} a = b$
.
Lemma A.2 PST
Separation holds.
Proof Using Comprehension, let G be given by
$\forall x(G(x) \leftrightarrow (F(x) \land x \in a))$
. If
$G(x)$
, then
by Priority
; so some
$b = \{x : G(x)\} = \{x \in a : F(x)\}$
exists by Spec
.
Since PST proves Extensionality and Separation, it proves the key results of Pt.1 Section 3, concerning the well-ordering of levels, in the sense of Pt.1 Definition 2.2. This next result establishes that all of the key notions of that Definition are (weakly) rigid:
Lemma A.3 PST
-
(1)
$\forall a(\forall b \subseteq a){\mathord {\square }}(\mathrm{E}(a) \rightarrow (\mathrm{E}(b) \land b \subseteq a))$
, -
(2)
, -
(3)
, -
(4)
$(\forall h : {Hist}){\mathord {\square }}(\mathrm{E}(h) \rightarrow {Hist}(h))$
, -
(5)
$(\forall s : \textit{Lev}){\mathord {\square }}(\mathrm{E}(s) \rightarrow \textit{Lev}(s))$
.
Proof
(1) Fix a and b at
$\textbf {w}$
such that
$\vDash _{\textbf {w}} b \subseteq a$
. Let a exist at
$\textbf {v}$
; by Separation at
$\textbf {v}$
there is c at
$\textbf {v}$
such that
$\vDash _{\textbf {v}} c = \{x \in a : {\mathord {\Diamond }} x \in b\}$
; I claim that
$\vDash _{\textbf {v}} c = b$
. Fix x at
$\textbf {u}$
: if
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in c$
, then
$\vDash _{\textbf {v}} x \in c$
by Mem
${}_{{\mathord {\Diamond }}}$
, so
$\vDash _{\textbf {v}} {\mathord {\Diamond }} x \in b$
and
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in b$
; if
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in b$
, then
$\vDash _{\textbf {w}} x \in b \subseteq a$
by Mem
${}_{{\mathord {\Diamond }}}$
, so that
$\vDash _{\textbf {v}} x \in a$
and
$\vDash _{\textbf {v}} {\mathord {\Diamond }} x \in b$
, i.e.,
$\vDash _{\textbf {v}} x \in c$
, so that
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in c$
. Hence
$\vDash _{\textbf {v}} c = b$
by Ext
${}_{{\mathord {\Diamond }}}$
.
(2) Fix a. If
$\exists z(x \subseteq z \in a)$
, then
by Priority
and (1). So using Spec
we have some b such that
.
(3) Fix a and b at
$\textbf {w}$
with
. Let a exist at
$\textbf {v}$
, and using (2) fix c such that
. Now
$\vDash _{\textbf {v}} b = c$
, by Ext
${}_{{\mathord {\Diamond }}}$
and (1).
(4)–(5) By (1) and (3).
We can now show that levels persist, and also that every world has a maximal level:
Lemma A.4 PST
.
Proof Let s be a level in
$\textbf {w}$
. For induction on levels (i.e., Pt.1 Theorem 3.10), suppose that
. Fix
$\textbf {v}> \textbf {w}$
; using Spec
fix t such that
. I claim that
$\vDash _{\textbf {v}} s = t$
; the result will then follow by induction on levels in
$\textbf {w}$
and Lemma A.3.5.
If
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in s$
, then
$\vDash _{\textbf {w}} x \in s$
; so by Pt.1 Lemma 3.8 there is some r such that
$\vDash _{\textbf {w}} x \subseteq r \in s \land \textit{Lev}(r)$
; now
$\vDash _{\textbf {v}} \mathrm{E}(r) \land \textit{Lev}(r)$
by the induction hypothesis and Lemma A.3.5, and
$\vDash _{\textbf {v}} x \subseteq r$
by Lemma A.3.1; so
$\vDash _{\textbf {v}} x \in t$
and hence
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in t$
. The converse is similar. So
$\vDash _{\textbf {u}} {\mathord {\Diamond }} s = t$
, and
$\vDash _{\textbf {v}} s = t$
by Ext
${}_{{\mathord {\Diamond }}}$
.
Lemma A.5 PST
.
Proof Using Spec
, let
. I claim that h is a history. Fix
$r \in h$
. Clearly
as levels are potent. Conversely, if
$a \in r$
then there is some level q such that
$a \subseteq q \in r$
by Pt.1 Lemma 3.8, and since
we have
; so
$q \in r \cap h$
and hence
. Generalising,
. So h is a history. Using Lemma A.3.2, let
. By construction, s is a level. I claim that s has the required properties.
For reductio, suppose that
; then
$s \in h \subseteq s$
, contradicting the well-ordering of levels; so
.
Suppose
$r \neq s$
. Then either
$r \in s$
or
$s \in r$
by the well-ordering of levels; but if
$s \in r$
then
by Priority
, a reductio. So
$r \in s$
. Hence
by Priority
, and also
$r \subseteq s$
as s is transitive.
From here, we can prove a Löb-like scheme for PST:
Lemma A.6 PST
, for all
$\phi $
.
Proof For reductio, suppose this is false at
$\textbf {w}$
, i.e.,
but
$\vDash _{\textbf {w}} {\mathord {\Diamond }} \lnot \phi $
. So
$\vDash _{\textbf {v}} \lnot \phi $
for some
$\textbf {v}$
. Since
, there is
$\textbf {u} < \textbf {v}$
such that
$\vDash _{\textbf {u}} \lnot \phi $
. For brevity, let:
Now
, by Lemmas A.4 and A.5. Using induction on levels, let s be the
$\in $
-minimal level in
$\textbf {v}$
such that
. So there is
$\textbf {t} < \textbf {v}$
with
$\vDash _{\textbf {t}} \psi (s)$
. Since
$\vDash _{\textbf {t}} \lnot \phi $
and
by assumption, there is
$\textbf {t}_0 < \textbf {t}$
with
$\vDash _{\textbf {t}_0} \lnot \phi $
. Using Lemma A.5, fix r such that
$\vDash _{\textbf {t}_0} \psi (r)$
. Now
by Lemma A.4, so
$\vDash _{\textbf {t}} r \in s$
by Lemma A.5 and choice of s. So
by Lemma A.4, contradicting the choice of s.
This effectively licenses schematic induction on worlds, enabling us to prove the main result of Section 4:
Theorem 4.1 PST
Where
$\textit{Max}(s)$
abbreviates
$(\mathrm{E}(s) \land \forall x\ x \subseteq s):$
-
(1)
$\mathrm{LT}$
holds, -
(2)
, -
(3)
$(\exists s : \textit{Lev})\textit{Max}(s)$
, -
(4)
$(\forall s : \textit{Lev}){\mathord {\Diamond }}\textit{Max}(s)$
.
Proof
(1) It suffices to prove Stratification, i.e., that
$\forall a (\exists s : \textit{Lev})a \subseteq s$
. Fix
$\textbf {w}$
, and suppose for induction on worlds that
$\vDash _{\textbf {v}} \forall a(\exists s : \textit{Lev})a \subseteq s$
for all
$\textbf {v} < \textbf {w}$
. Using Lemma A.5, fix s such that
. Suppose
$\vDash _{\textbf {w}} x \in a$
; by Priority
there is some
$\textbf {u} < \textbf {w}$
such that
$\vDash _{\textbf {u}} \mathrm{E}(x)$
; by assumption there is r such that
$\vDash _{\textbf {u}} \textit{Lev}(r) \land x \subseteq r$
; now
$\vDash _{\textbf {w}} x \subseteq r \in s$
by Lemmas A.3 and A.4, so that
$x \in s$
as s is potent. Hence
$\vDash _{\textbf {w}} a \subseteq s$
. The result follows by Lemma A.6.
(2)–(3) Combine Stratification with Lemmas A.3–A.6.
(4) Fix
$\textbf {w}$
, and suppose for induction on worlds that
$\vDash _{\textbf {v}} (\forall s : \textit{Lev}){\mathord {\Diamond }}\textit{Max}(s)$
for all
$\textbf {v} < \textbf {w}$
. Let s be such that
$\vDash _{\textbf {w}} \textit{Lev}(s)$
. If
then
$\vDash _{\textbf {w}} {\mathord {\Diamond }} \textit{Max}(s)$
by our supposition and Lemma A.3. Otherwise,
$\vDash _{\textbf {w}} (\forall r : \textit{Lev})r \subseteq s$
by the well-ordering of levels and Lemma A.5, so that
$\vDash _{\textbf {w}} \textit{Max}(s)$
by Stratification. The result follows by Lemma A.6.
To round things off, note that LT’s key notions are robust under modalization:
Lemma A.7 PST
-
(1)
$\phi ^{{\mathord {\Diamond }}}(\vec {x})$
iff
${\mathord {\square }}\phi ^{{\mathord {\Diamond }}}(\vec {x})$
, for any LT-formula
$\phi (\vec {x})$
. -
(2) if
$\mathrm{E}(b) \land b \subseteq a$
, then
$(b \subseteq a)^{{\mathord {\Diamond }}}$
. -
(3) if
$(b \subseteq a)^{{\mathord {\Diamond }}}$
, then
${\mathord {\square }}(\mathrm{E}(a) \rightarrow b \subseteq a)$
. -
(4) if
$\mathrm{E}(b)$
and
, then
$\mathrm{E}(a)$
and
. -
(5) if
$\mathrm{E}(b)$
and
, then
$\mathrm{E}(a)$
and
. -
(6) if
$\mathrm{E}(h)$
, then
${Hist}(h) \leftrightarrow {Hist}^{{\mathord {\Diamond }}}(h)$
. -
(7) if
$\mathrm{E}(s)$
, then
$\textit{Lev}(s) \leftrightarrow \textit{Lev}^{{\mathord {\Diamond }}}(s)$
.
Proof
(1) A routine induction on complexity, using the fact that
${\mathord {\Diamond }}$
obeys S5.
(2)–(3) Straightforward.
(4) Suppose
$\vDash _{\textbf {w}} \mathrm{E}(b)$
and
, i.e.,
$\vDash _{\textbf {w}} {\mathord {\square }} \forall x({\mathord {\Diamond }} x \in b \leftrightarrow (\exists z(x \subseteq z \in a))^{{\mathord {\Diamond }}})$
.
I first show that
$\vDash _{\textbf {w}} \mathrm{E}(a)$
. By Separation there is c at
$\textbf {w}$
such that
$\vDash _{\textbf {w}} c = \{x \in b : {\mathord {\Diamond }} x \in a\}$
; I claim
$a = c$
using Ext
${}_{{\mathord {\Diamond }}}$
. Fix x at
$\textbf {u}$
. If
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in c$
then clearly
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in a$
. Conversely, if
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in a$
, then letting
$x= z$
we have
$\vDash _{\textbf {u}} (\exists z(x \subseteq z \in a))^{{\mathord {\Diamond }}}$
by (2), hence
$\vDash _{\textbf {w}} {\mathord {\Diamond }} x \in b$
so that
$\vDash _{\textbf {w}} x \in b$
and hence
$\vDash _{\textbf {w}} x \in c$
i.e.,
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in c$
.
I now show that
. If
$\vDash _{\textbf {w}} x \in b$
, then
$\vDash _{\textbf {w}} (\exists z(x \subseteq z \in a))^{{\mathord {\Diamond }}}$
, i.e., there is
$\textbf {u}$
and z such that
$\vDash _{\textbf {u}} (x \subseteq z \in a)^{{\mathord {\Diamond }}}$
; now
$\vDash _{\textbf {w}} x \subseteq z \in a$
by (3) and as
$\vDash _{\textbf {w}} \mathrm{E}(a)$
. Conversely, if
$\vDash _{\textbf {w}} x \subseteq z \in a$
for some z, then
$\vDash _{\textbf {w}} (\exists z(x \subseteq z \in a))^{{\mathord {\Diamond }}}$
by (2), so
$\vDash _{\textbf {w}} {\mathord {\Diamond }} x \in b$
and so
$\vDash _{\textbf {w}} x \in b$
.
(5) Similar to (4).
(6)–(7) By (1), (4), and (5).
All the results of this appendix can be first-orderized straightforwardly. Keen readers will also notice that the proofs of this appendix have made no apparent use of the assumption of past-directedness. Indeed: the only role for past-directedness is to supply us with a possibility operator,
${\mathord {\Diamond }}$
, which is unrestricted and obeys S5.
Appendix B Results concerning LPST
I will now turn from PST to LPST. As mentioned in Section 5, linearity allows us to define away
and
via the map
$\phi \mapsto \phi ^{\bullet }$
. To guarantee that this is so, we use the results of Appendix A to prove Lemma 5.1 by a simple induction on complexity; I leave this to the reader.
Evidently,
$\mathrm{LPST}^{\bullet }$
is a unimodal S5 theory. However, it may be worth noting that it can be given a simpler presentation. Let MLT be a unimodal S5 theory whose set-theoretic axioms are Mem
${}_{{\mathord {\Diamond }}}$
, Ext
${}_{{\mathord {\Diamond }}}$
, Separation, and clauses (3) and (4) of Theorem 4.1. The proofs of Lemmas A.1–A.3 go through in MLT with only tiny adjustments, and it is easy to show that
for each LPST-formula
$\phi $
. It follows that
$\mathrm{LPST}^{\bullet } \dashv \vdash \mathrm{MLT}$
. By Lemma 5.1, then, LPST and MLT are (strictly) definitionally equivalent.
B.1 Deductive near-synonymy
The key results concerning LPST, though, are the near-synonymies. I will start with the first-order deductive near-synonymy:
Theorem 6.1. For any
${\mathrm{LT}}_1$
-formula
$\phi $
not containing s:
-
(1) If
${\mathrm{LT}}_1 \vdash \phi $
, then
${\mathrm{LPST}}_{1} \vdash \phi ^{{\mathord {\Diamond }}}$
. -
(2)
${\mathrm{LT}}_1 \vdash \phi \leftrightarrow (\phi ^{{\mathord {\Diamond }}})^s$
.
For any
${\mathrm{LPST}}_{1}$
-formula
$\phi $
not containing s:
-
(3) If
${\mathrm{LPST}}_{1} \vdash \phi $
, then
${\mathrm{LT}}_1 \vdash \textit{Lev}(s) \rightarrow \phi ^s$
. -
(4)
${\mathrm{LPST}}_{1} \vdash \textit{Max}(s) \rightarrow (\phi \leftrightarrow (\phi ^s)^{{\mathord {\Diamond }}})$
.
Proof
(1)
$\mathrm{Extensionality}^{{\mathord {\Diamond }}}$
is Ext
${}_{{\mathord {\Diamond }}}$
. For
$\mathrm{Stratification}^{{\mathord {\Diamond }}}$
, use Theorem 4.1.3 and Lemma A.7. For the
$\mathrm{Separation}^{{\mathord {\Diamond }}}_1$
-instances, fix suitable
$\phi $
; fix a at
$\textbf {w}$
; by Separation we have some b in
$\textbf {w}$
such that
$\vDash _{\textbf {w}} b = \{x \in a : \phi ^{{\mathord {\Diamond }}}\}$
. Fix x at
$\textbf {u}$
; now
$\vDash _{\textbf {u}} {\mathord {\Diamond }} x \in b$
iff
$\vDash _{\textbf {w}} x \in b$
iff
$\vDash _{\textbf {w}} \phi ^{{\mathord {\Diamond }}} \land x \in a$
iff
$\vDash _{\textbf {u}} \phi ^{{\mathord {\Diamond }}} \land {\mathord {\Diamond }} x \in a$
by Lemma A.7.
(2) A routine induction on complexity.
(3) The well-ordering and potency of levels yields the levelling of each underlying logical principle. It is then straightforward to obtain the levelling of each
${\mathrm{LPST}}_{1}$
axiom.
(4) An induction on complexity. The cases of atomic formulas, conjunctions, and quantifiers are easy, relying on Mem
${}_{{\mathord {\Diamond }}}$
and Lemma A.7.2 and A.7.3.
For quantifiers: using the induction hypothesis, LPST proves that, if
$\textit{Max}(s)$
then:
$(\exists x \phi)$
iff
$(\exists x \subseteq s)(\phi ^{s})$
iff
${\mathord {\Diamond }}(\exists x \subseteq {s})(\phi ^{s})^{{\mathord {\Diamond }}}$
iff
$((\exists x\phi)^{s})^{{\mathord {\Diamond }}}$
.
For modal operators, I will prove the case for
(the others are similar). Fix
$\textbf {w}$
and, using Theorem 4.1.3, let
$\vDash _{\textbf {w}} \textit{Max}(s)$
; I claim that
.
Suppose
, i.e., there is
$\textbf {v} < \textbf {w}$
such that
$\vDash _{\textbf {v}} \phi $
. Using Theorem 4.1.3, let
$\vDash _{\textbf {v}} \textit{Max}(r)$
. By the induction hypothesis,
$\vDash _{\textbf {v}} \phi \leftrightarrow (\phi ^r)^{{\mathord {\Diamond }}}$
; so
$\vDash _{\textbf {w}} (\phi ^r)^{{\mathord {\Diamond }}}$
. Hence
$\vDash _{\textbf {w}} \textit{Lev}(r) \land {\mathord {\Diamond }} r \in s \land (\phi ^r)^{{\mathord {\Diamond }}}$
; now by Lemma A.7 we have
$\vDash _{\textbf {w}} {\mathord {\Diamond }} \exists r(\textit{Lev}^{{\mathord {\Diamond }}}(r) \land {\mathord {\Diamond }} r \in s \land (\phi ^r)^{{\mathord {\Diamond }}})$
, i.e.,
.
Suppose
, i.e., for some
$\textbf {v}$
and some r at
$\textbf {v}$
we have
$\vDash _{\textbf {v}} \textit{Lev}^{{\mathord {\Diamond }}}(r) \land {\mathord {\Diamond }} r \in s \land (\phi ^r)^{{\mathord {\Diamond }}}$
. Using Theorem 4.1.4 and Lemma A.7, fix
$\textbf {u}$
such that
$\vDash _{\textbf {u}} \textit{Max}(r)$
; note that
$\vDash _{\textbf {u}} (\phi ^r) ^{{\mathord {\Diamond }}}$
, so that
$\vDash _{\textbf {u}} \phi $
by the induction hypothesis. Moreover,
$\textbf {u} < \textbf {w}$
, as
$\vDash _{\textbf {v}} {\mathord {\Diamond }} r \in s$
and we have assumed linearity. So
.
Theorem 6.1 straightforwardly entails that modalization and levelling are faithful:
-
(1)
${\mathrm{LPST}}_{1} \vdash \phi ^{{\mathord {\Diamond }}}$
iff
${\mathrm{LT}}_1 \vdash \phi $
, for any
${\mathrm{LT}}_1$
-formula
$\phi $
. -
(2)
${\mathrm{LT}}_1 \vdash \textit{Lev}(s) \rightarrow \phi ^s$
iff
${\mathrm{LPST}}_{1} \vdash \phi $
, for any
${\mathrm{LPST}}_{1}$
-formula
$\phi $
not containing s.
I leave the proof to the reader. The reader can also prove these two second-order versions of Theorem 6.1, mentioned in Section 8:
Theorem B.2. Theorem 6.1 holds for LT and
${\mathrm{LPST}}_{{\textrm {n}}}$
, where we enrich modalization and levelling with these clauses:
$$ \begin{align*} \alpha ^{{\mathord{\Diamond}}} &\mathrel{\mathord{:}\mathord{=}} {\mathord{\Diamond}}\alpha\text{, for atomic }\alpha, & (\exists F \phi)^{{\mathord{\Diamond}}} &\mathrel{\mathord{:}\mathord{=}} {\mathord{\Diamond}} \exists F \phi^{{\mathord{\Diamond}}},\\ (F = G)^s &\mathrel{\mathord{:}\mathord{=}} F = G, & F(\vec{x})^s\! &\mathrel{\mathord{:}\mathord{=}}\! (F(\vec{x})\hspace{-0.5pt} \land\hspace{-0.5pt} \vec{x} \subseteq s)& \!\!\!\!\!\!(\exists F \phi)^s\! &\mathrel{\mathord{:}\mathord{=}}\! \exists F \phi^s. \end{align*} $$
Theorem B.3. Theorem 6.1 holds for
${\mathrm{LT}}_{{\textrm {b}}}$
and
${\mathrm{LPST}}_{{\textrm {c}}}$
, where we enrich modalization as above, but instead enrich levelling as follows:
$$ \begin{align*} (F = G)^s\! &\mathrel{\mathord{:}\mathord{=}}\! (F = G \sqsubseteq s), &\!\!\!\! F(\vec{x})^s\! &\mathrel{\mathord{:}\mathord{=}}\! (F(\vec{x}) \land F \sqsubseteq s), & \!\!\!\!(\exists F \phi)^s\!& \mathrel{\mathord{:}\mathord{=}}\! (\exists F \sqsubseteq s)\phi^s. \end{align*} $$
B.2 Semantic near-synonymy
I now consider the semantic near-synonymies. The first-order result follows from two lemmas, which are proved by a routine induction on complexity:
Lemma B.4. If
$\mathcal {P} \vDash {\mathrm{LPST}}_{1}$
, then
$\mathcal {P} \vDash \phi ^{{\mathord {\Diamond }}}(\vec {a})$
iff
$\flat \mathcal {P} \vDash \phi (\vec {a})$
, for any
$\vec {a}$
in
$\flat \mathcal {P}$
’s domain and any
${\mathrm{LT}}_1$
-formula
$\phi (\vec {x})$
with free variables displayed.
Lemma B.5. If
$\mathcal {A} \vDash {\mathrm{LT}}_1$
, then
$\mathcal {A} \vDash \phi ^r(\vec {a})$
iff
$\sharp \mathcal {A} \vDash _{r} \phi (\vec {a})$
, for any
$\vec {a}$
from
$\mathcal {A}$
’s domain, any r such that
$\mathcal {A} \vDash \textit{Lev}(r)$
, and any
${\mathrm{LPST}}_{1}$
-formula
$\phi (\vec {x})$
with free variables displayed.
-
(1) If
$\mathcal {P} \vDash {\mathrm{LPST}}_{1}$
, then
$\flat \mathcal {P} \vDash {\mathrm{LT}}_1$
. -
(2) If
$\mathcal {P} \vDash {\mathrm{LPST}}_{1}$
, then there is a surjection f such that
$\mathcal {P} = ({\sharp \flat \mathcal {P}})_{f}$
. -
(3) If
$\mathcal {A} \vDash {\mathrm{LT}}_1$
, then
$\sharp \mathcal {A} \vDash {\mathrm{LPST}}_{1}$
. -
(4) If
$\mathcal {A} \vDash {\mathrm{LT}}_1$
, then
$\mathcal {A} = {\flat \sharp \mathcal {A}}$
.
Proof (1) By Theorem 6.1.1 and Lemma B.4.
(2) Let W be the set of
$\mathcal {P}$
’s worlds; let
$L = \{s : \flat \mathcal {P} \vDash \textit{Lev}(s)\}$
be the set of
${\sharp \flat \mathcal {P}}$
’s worlds. Using Theorem 4.1.3, for each
$\textbf {w} \in W$
, let
$f(\textbf {w})$
be the maximal level in
$\textbf {w}$
.
I claim that
$f : W \longrightarrow L$
is a surjection. To show that
$L \subseteq \mathrm{ran}(f)$
, fix
$s \in L$
, i.e.,
$\flat \mathcal {P} \vDash \textit{Lev}(s)$
. Let
$\textbf {w}$
be such that
$\mathcal {P} \vDash _{\textbf {w}} \mathrm{E}(s)$
; now
$\mathcal {P} \vDash _{\textbf {w}} \textit{Lev}(s)$
by Lemmas B.4 and A.7, and there is
$\textbf {v}$
such that
$\mathcal {P} \vDash _{\textbf {v}} \textit{Max}(s)$
by Theorem 4.1.4; so
$f(\textbf {v}) = s $
. The proof that
$\mathrm{ran}(f) \subseteq L$
is similar but simpler.
Now
$\mathcal {P}$
and
${\sharp \flat \mathcal {P}}$
share a global domain, since
${\mathord {\Diamond }}\mathrm{E}(x)$
is a schema of our logic (see footnote 5). They agree on membership and identity by construction. So
$\mathcal {P} = ({\sharp \flat \mathcal {P}})_{f}$
.
(3) By Theorem 6.1.1 and Lemma B.5.
(4) By Stratification,
$\mathcal {A}$
and
${\flat \sharp \mathcal {A}}$
have the same domain, and they agree on membership by construction.
As discussed in Section 8, we also have two second-order versions of Theorem 7.4 which hold for full or Henkin semantics.
Theorem B.6. Theorem 7.4 holds for LT and
${\mathrm{LPST}}_{{\mathrm {n}}}$
, where we extend flattening and potentialization with these clauses:
Flattening:
$\flat \mathcal {P}$
’s second-order domain is
$\mathcal {P}$
’s global second-order domain
$;$
and
$\flat \mathcal {P} \vDash F(\vec {a})$
iff
$\mathcal {P} \vDash {\mathord {\Diamond }} F(\vec {a})$
.
Potentialization:
$\sharp \mathcal {A}$
’s global second-order domain is
$\mathcal {A}$
’s second-order domain
$;$
and
$\sharp \mathcal {A} \vDash _{s} F(\vec {a})$
iff
$\mathcal {A} \vDash F(\vec {a}) \land \vec {a} \subseteq s$
.
Theorem B.7. Theorem 7.4 holds for
${\mathrm{LT}}_{{\mathrm {b}}}$
and
${\mathrm{LPST}}_{{\mathrm {c}}}$
, where we extend flattening and potentialization as above, and add a further clause for potentialization, to allow variable second-order domains:
$\sharp \mathcal {A} \vDash _{s} \mathrm{E}(F)$
iff
$\mathcal {A} \vDash F \sqsubseteq s$
.
As mentioned in Section 8.2, if we invoke full semantics, we can obtain a final semantic result. Recall that, with full semantics, first-order domains determine second-order domains. (In the modal setting: full contingentist semantics specifies that a world’s monadic second-order domain is the powerset of that world’s first-order domain.) So, when we are using full semantics, we can forget about second-order entities, allowing them to ‘take care of themselves’, and simply use the definitions of flattening and potentialization that were given for first-order theories. We then have a near-synonymy as follows:
Theorem B.8. Using full semantics, Theorem 7.4 holds for LT and
${\mathrm{LPST}}_{{\mathrm {c}}}$
, with flattening and potentialization exactly as defined in Section 7.
Proof Clauses (2)–(4) are left to the reader. To establish (1), suppose
$\mathcal {P} \vDash {\mathrm{LPST}}_{{\textrm {c}}}$
. So
$\mathcal {P} \vDash _{\textbf {w}} \mathrm{LT}$
for each world
$\textbf {w}$
, by Theorem 4.1. Now LT is externally quasi-categorical by Pt.1 Theorem 6.1, and membership is modally robust by Mem
${}_{{\mathord {\Diamond }}}$
and Ext
${}_{{\mathord {\Diamond }}}$
. So, given any two worlds of
$\mathcal {P}$
, one is an initial segment of the other. Hence
$\flat \mathcal {P} \vDash \mathrm{LT}$
.
Appendix C Equivalences concerning LT
${}_{\textbf {b}}$
In Section 9.3, I considered Edna, a contingentist who holds that time is endless. To formalize the claim ‘time is endless’, we have the modal axiom
. Let
${\mathrm{LPST}}_{{\textrm {c}}\mathord {+}}$
be the result of adding this axiom to
${\mathrm{LPST}}_{{\textrm {c}}}$
. So, Edna’s theory is
${\mathrm{LPST}}_{{\textrm {c}}\mathord {+}}$
.
By contrast, consider the principle
. Over
${\mathrm{LPST}}_{{\textrm {c}}}$
, this amounts to the statement ‘time has an end’. Call this theory
${\mathrm{LPST}}_{{\textrm {c}}\mathord {-}}$
.
Actualists can mirror such talk about the ‘end of time’. The sentence Endless, from Pt.1 Section 7, states that the (actualist) hierarchy has no last level. For brevity, let
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
be
${\mathrm{LT}}_{{\textrm {b}}}$
+ Endless, and let
${\mathrm{LT}}_{{\textrm {b}}\mathord {-}}$
be
${\mathrm{LT}}_{{\textrm {b}}}$
+
$\lnot $
Endless. It is easy to confirm that
${\mathrm{LPST}}_{{\textrm {c}}\mathord {+}}$
is near-synonymous with
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
, and that
${\mathrm{LPST}}_{{\textrm {c}}\mathord {-}}$
is near-synonymous with
${\mathrm{LT}}_{{\textrm {b}}\mathord {-}}$
.
However,
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
and
${\mathrm{LT}}_{{\textrm {b}}\mathord {-}}$
merit discussion in their own right. Fairly trivially,
${\mathrm{LT}}_{{\textrm {b}}\mathord {-}}$
is identical to LT +
$\lnot $
Endless. More interestingly,
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
can be regarded as a notational variant of the first-order theory
${\mathrm{LT}}_1$
+ Endless, i.e.,
${\mathrm{LT}}_{1\mathord {+}}$
. Specifically: there is an interpretation which is identity over the first-order entities and bi-interpretability over the second-order entities.Footnote
46
Here is the point in detail. We interpret
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
in
${\mathrm{LT}}_{1\mathord {+}}$
using a translation,
$\Downarrow $
, which tells us to regard n-place second-order variables as an odd way to talk about sets of n-tuples. Formally, its only non-trivial clauses are:
$$ \begin{align*} (Y^n(x_1, \ldots, x_n))^{\Downarrow} &\mathrel{\mathord{:}\mathord{=}} \langle x_1, \ldots, x_n\rangle \in Y^n,\\ (\forall Y^n\phi)^{\Downarrow} &\mathrel{\mathord{:}\mathord{=}} \forall Y^n((\forall z \in Y^n)(z\text{ is an }n\text{-tuple}) \rightarrow \phi^{\Downarrow}), \end{align*} $$
where we treat n-tuples via Wiener–Kuratowski,Footnote
47
and regard each capital, superscripted, variable as just a new first-order variable. This yields a very tight connection between
${\mathrm{LT}}_{1\mathord {+}}$
and
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
:
-
(1)
${\mathrm{LT}}_{1\mathord {+}} \vdash \phi $
iff
${\mathrm{LT}}_{{\mathrm {b}}\mathord {+}} \vdash \phi $
, for first-order
$\phi $
. -
(2)
${\mathrm{LT}}_{{\mathrm {b}}\mathord {+}} \vdash \phi $
iff
${\mathrm{LT}}_{1\mathord {+}} \vdash \phi ^{\Downarrow }$
, for second-order
$\phi $
.
Moreover,
${\mathrm{LT}}_{{\mathrm {b}}\mathord {+}}$
proves that
$\Downarrow $
is identity over the first-order entities and an isomorphism (which blurs types) over the second-order entities.
Proof (1) It suffices to show that
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
proves the Separation scheme. Fix a formula
$\phi $
. Fix a. By Stratification, there is some level
$s \supseteq a$
. Using Comp
${}_{\textrm {b}}$
, there is
$F \sqsubseteq s$
such that
$(\forall x \subseteq s)(F(x) \leftrightarrow \phi)$
. By Extensionality and the Separation axiom, we have
$b = \{x \in a : F(x)\}$
; now
$b = \{x \in a : \phi \}$
, as required, since levels are transitive.
(2) To establish Comp
${}_{\textrm {b}}^{\Downarrow }$
: fix a level s; using Endless, let t be the (
$2n\mathord {+}1){\mathrm{th}}$
level after s; then use the Separation scheme to obtain
$F^n = \{\langle x_1, \ldots , x_n\rangle \in t : \phi ^{\Downarrow }\}$
, noting that
$\langle x_1, \ldots , x_n\rangle \in t$
iff
$x_{i} \subseteq s$
for all
$1 \leq i \leq n$
. Strat
${}_{\textrm {b}}^{\Downarrow }$
follows from Stratification.
To establish the ‘moreover’ clause in
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
, define an isomorphism (which blurs types) via
$\tau (F^n) = \{\langle x_1, \ldots , x_n\rangle : F^n(\vec {x})\}$
.
Note that Theorem C.1 is not a definitional equivalence: definitional equivalence is unavailable, since
${\mathrm{LT}}_{1\mathord {+}}$
and
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
have different grammars. This difference aside,
${\mathrm{LT}}_{1\mathord {+}}$
and
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
are as tightly linked as we could want. Moreover, since
${\mathrm{LPST}}_{{\textrm {c}}\mathord {+}}$
and
${\mathrm{LT}}_{{\textrm {b}}\mathord {+}}$
are near-synonymous, Theorem C.1 allows us to regard
${\mathrm{LPST}}_{{\textrm {c}}\mathord {+}}$
, which is a modal second-order theory, as a notational variant of
${\mathrm{LT}}_{1\mathord {+}}$
, which is a non-modal first-order theory.Footnote
48
Acknowledgments
Special thanks to Øystein Linnebo and James Studd, for extensive discussion. Thanks also to Sharon Berry, Geoffrey Hellman, Luca Incurvati, Will Stafford, Rob Trueman, Albert Visser, Sean Walsh, and anonymous referees for this journal.
