2 Free choice sequences

The basic idea of a choice sequence can be seen as arising from two components of Brouwer’s thought. The first component was his metaphysical views: Brouwer, of course, thought of mathematical objects as purely mental constructions with no objective or mind-independent existence. Accordingly, one could not truly assert the existence of some mathematical object without a method for constructing that object mentally.

The second component of Brouwer’s thought was his acceptance of the arithmetized account of the continuum that had become widespread in classical mathematics since Dedekind and Cantor.Footnote ⁷ The arithmetized view of the continuum required defining real numbers in terms of infinite sets or sequences of rational numbers (à la Dedekind cuts, Cauchy sequences, or infinite decimal expansions). Brouwer’s constructivism required that any such sets or sequences must be given as possible mental constructions. For simplicity I will simply talk of sequences rather than sequences or sets. If there is a law that can be followed to construct the sequence, such a sequence passes constructivist muster, since the law provides a method for constructing the sequence. But the fullness of the continuum is not exhausted by (to fix ideas) the Cauchy sequences that can be given by a law. One wants to countenance any arbitrary Cauchy sequences. And the idea of an arbitrary Cauchy sequences emerges in intuitionism as a free choice sequence: an infinitely proceeding series of choices of rational numbers determined freely by an agent.

Since mathematical agents are limited, we must regard these sequences as necessarily unfinished. But the intuitionist regards objects that could, at least in principle, be constructed by a mathematician as legitimate objects of study. And since there is no in-principle finite limit to how long of a sequence a mathematician could create, we can regard a choice sequence as indefinitely proceeding, though not as a completed infinite sequence.

Because of this idealization involved, it is common to describe choice sequences as potentially infinite sequences of numbers created by an idealized mathematician subsequently picking each member of the sequence. They are free to pick any number they like; but they are also free to impose constraints on their future choices. Thus we countenance choice sequences that are, after some stage, bound by some laws as well as those that are free from all constraints.

As Brouwer [Reference Brouwer9, p. 140] described the matter:

Brouwer here countenances a wide range of choice sequences that includes sequences of any type of mathematical object that is already available. Most subsequent studies of choice sequences have, however, only considered sequences of natural numbers, and I will do likewise in this project. Lawless sequences are a specific type of free choice sequence wherein the creating mathematician determines from the beginning that they shall never subject their choices to any restriction or law. The choice of each value for the sequence is entirely unconstrained and subject to no law.

These ideas of Brouwer’s express the basic concept of a free choice sequence which I will be trying to capture in a modal framework. At the same time, in giving the modal account I do not take myself to necessarily be bound by any particular statement or idea of Brouwer’s. Given that his own ideas about choice sequences changed a number of times over his lifetime, this is not a feasible or even desirable goal.Footnote ⁸ Similarly, a variety of explicit accounts of choice sequences developed in later intuitionistic literature, and while they all share some central features, they also differ in important respects. This situation led Troelstra to claim in a survey article that “there are a great many notions of choice sequence which have to be regarded as distinct primitive notions” ([Reference Troelstra33, p. 225], emphasis original). This should not be taken to suggest that there is no core intuitive notion of a free choice sequence—in this section I have sketched just such a notion. Troelstra’s point, rather, is that in fleshing out a fully detailed account of choice sequences there are a number of decision points where multiple ways of proceeding are compatible with the core idea of a free choice sequence. (These decision points, however, concern free choice sequences that lie beyond the realm of lawless sequences. Lawless sequences themselves form a shared basis on which different more complicated conceptions of choice sequences can agree. This is a further reason for focusing on lawless sequences in this paper.)

Although this situation precludes a simple appeal to a generally accepted definition of a choice sequence, we can still take it as an ideal for the modal account of choice sequence to cohere with the conception(s) of choice sequence found in Brouwer, Heyting, Troelstra, and other intuitionists. The important thing is that the modal account should allow us to capture the role that choice sequences play in intuitionistic arguments. I aim to make good on this by showing how a modal theory of choice sequences allows us to prove modal analogues of important intuitionistic results.

I turn now from this informal introduction to the idea of a free choice sequence to consider specific formal theories of lawless sequences.

3 Notational preliminaries

I will use a sort of variables for choice sequences $\alpha , \beta , \gamma ,\dots $ ; intuitively these will be partial functions on $\mathbb {N}$ . Individual variables $x, y, z,\dots $ will be taken to range over natural numbers. Numerical variables will always be taken to have denotations. There will also be a sort of variables $f,g,h,\dots $ ranging over classical functions on $\mathbb {N}$ . These functions are extensional objects whose graph does not change over time.

We can assume in the background all the usual coding apparatus for finite sequences of natural numbers as found in, for instance, [Reference Hájek and Pudlák15]. This provides us with a formula $Seq(x)$ which is true of exactly those numbers x which code finite sequences; such numbers x are known as sequence numbers. It is sometimes also convenient to write $x\in Seq$ rather than $Seq(x)$ . We will write $\langle n_0,\dots ,n_k\rangle $ for the (code of) the finite sequence with $i^{th}$ member $n_{i-1}$ .

There are also length, projection, and concatenation functions for sequences. We will use $lh$ for the length function, $(\cdot )_i$ for the projection function, and $^\frown $ for concatenation. So if $x{\kern-1pt}={\kern-1pt}\langle x_0,\dots ,x_k \rangle $ , then $lh(x){\kern-1pt}={\kern-1pt}k+1$ , and for all $i\leq k$ , $(x)_i=x_i$ . And if $x=\langle x_0,\dots ,x_k\rangle $ and $y=\langle y_0,\dots ,y_l\rangle $ , the concatenation $x^\frown y:=\langle x_0,\dots ,x_k,y_0,\dots ,y_l\rangle $ . We will write $x\preceq y$ when $x,y \in Seq$ and there is some $z\in Seq$ such that $y=x^\frown z$ . Finally, if $\vec {x}=\langle x_0,\dots ,x_{k-1}\rangle $ and $\vec {y}=\langle y_0,\dots ,y_{k-1}\rangle $ are both k-tuples of sequence numbers, then we may write $\vec {x}\preceq \vec {y}$ , understood to mean $x_0\preceq y_0 \wedge \dots \wedge x_{k-1} \preceq y_{k-1}$ .

There are two important pieces of notation that are unique to the literature on choice sequences, though widespread within that literature. First, $\overline {\alpha }(x)$ is used to denote the initial segment of $\alpha $ of length x. Thus, $\overline {\alpha }(x)=y$ iff $y\in Seq$ , $lh(y)=x+1$ , and for all $z\leq x$ , $\alpha (z)=(y)_z$ . Second, it is common to use $\alpha \in x$ as an abbreviation for $\overline {\alpha }(lh(x))=x$ . What this means is that x is a sequence number encoding an initial segment of $\alpha $ . I will also use $\overline {f}$ and $f\in n$ analogously when f is a classical function variable.

The initial segment of $\alpha $ , symbolized is $\alpha $ will refer to the largest sequence number n such that $\alpha \in n$ , and $\alpha $ is not (yet) defined on any greater arguments. In other words, $\mathrm {is}\alpha =n$ iff $\forall x< lh(n) \alpha (x)=(n)_x \wedge \forall x\geq lh(n) \alpha (x)\neq \alpha (x)$ .

Finally, one more piece of notation stems from the fact that I will be using a free logic in what follows. Specifically, I will use a negative free logic, so any atom $Pt$ is true only if t denotes. Thus $t=t$ can be used as an existence predicate. Let $t_1 \simeq t_2:\leftrightarrow (t_1=t_2 \vee (t_1 \neq t_1 \wedge t_2 \neq t_2))$ . In other words, $t_1\simeq t_2$ means that either $t_1$ and $t_2$ are both defined and identical or neither is defined.

Since Greek letters are being used for choice sequence variables, I will use $A,B,\dots $ as metavariables ranging over formulas. P will be a metavariable ranging over atomic formulas. I will use both $A^{o_1}_{o_2}$ and $A[o_1 / o_2]$ to denote the result of replacing all free occurrences of $o_1$ in A with $o_2$ .

4 The modal logic

The idea behind the modal theory of choice sequences is that choice sequences are intra-temporal mathematical objects, and we capture their temporal character using modal operators. The main modal operator will be $\square $ , intuitively meaning “at all times henceforth …,” as well as its dual $\lozenge $ , “at some later time ….” By fiat, we can take the later than relation to be reflexive, so that henceforth includes the present moment. Obviously, later than is transitive, and we can take it that the flow of time is not cyclical, so that later than is antisymmetric. Since we cannot assume that the flow of time has any other structure, the appropriate modal logic to use will be S4. In addition to the usual box and diamond, however, we will want to add a further modal operator.

Our choice of S4 reflects the fact that there might be multiple incompatible futures, different branches of time, as it were. Reading the box and diamond as temporal operators, $\square A$ means that A holds at every time henceforth. And $\lozenge A$ means that A holds at some future moment on some branch; in other words, A might hold in the future. To express several concepts in the modal theory of choice sequences, however, we need something further: we need to be able to say that A will eventually be true, no matter how the future evolves; on every future branch of time, there is a moment at which A is true. To express this notion, let us introduce the operator $\mathcal {I}A$ , pronounced “inevitably A”.Footnote ⁹ The logic that results from adding $\mathcal {I}$ to S4 can be called $\mathbf {S4}_{\mathcal {I}}$ .Footnote ¹⁰

The definition of an $\mathbf {S4}_{\mathcal {I}}$ model is exactly the same as that of an S4 model, and the satisfaction clauses are exactly the same for the vocabulary $\rightarrow ,\wedge ,\vee ,\neg ,\forall , \exists , \square ,\lozenge $ . The only thing we need to add is the clause for $\mathcal {I}$ . This requires one more definition:

Now the satisfaction clause for $\mathcal {I}A$ is as follows:

• • $M,w \models \mathcal {I} A$ iff for every maximal chain X above w there is a $u\in X$ such that $M,u\models A$ .

This condition is pictured in the image below: every path above w through the model M eventually intersects the set of A-worlds.

Although conservative over S4, the logic $\mathbf {S4}_{\mathcal {I}}$ is fairly strong, being unaxiomatizable.Footnote ¹¹ Nevertheless, the following list of axiom is sufficient for the purposes of this paper, and as we will see in Section 7.Footnote ¹²

1. M0 The axioms and rules of negative free S4 with CBF. (For concreteness, axioms M0.0–M0.13 are provided in Appendix A.)

2. M1 $\square (A \rightarrow B)\rightarrow (\mathcal {I}A \rightarrow \mathcal {I}B)$ .

3. M2 $A \rightarrow \mathcal {I}A$ .

4. M3 $\square A \rightarrow \neg \mathcal {I}\neg A$ .

5. M4 $\mathcal {I}\mathcal {I}A \rightarrow \mathcal {I}A$ .

6. M5 $\mathcal {I}\square A \rightarrow \square \mathcal {I}A$ .

7. M6 $\mathcal {I}\forall o A \rightarrow \forall o \mathcal {I}A$ .

8. M7 $\exists o \mathcal {I}A \rightarrow \mathcal {I}\exists o A$ .

The reason for using a free logic is that, since choice are meant to grow with time, it might happen that, say, $\alpha (100)$ has not yet been defined. The Converse Barcan Formula, however, ensures that the domain is growing, so that once an object exists it will never disappear. Since we will be working in a many-sorted logic, we include instances of M6 and M7 where o is each sort of variable.

Just as the necessity operator $\square $ has the dual possibility operator $\lozenge $ , definable as $\neg \square \neg $ , so the inevitability operator also has a dual $\neg \mathcal {I}\neg $ . Although I will not introduce a primitive symbol for this dual, it expresses an important concept: $\neg \mathcal {I}\neg A$ means, intuitively, that there is some possible path through the future such that A holds at every time on that path. This could be glossed in English as “it is possible that A holds into perpetuity”. I also want to draw attention to a derivable schema governing $\mathcal {I} $ and $\neg \mathcal {I}\neg $ , which I will appeal to later.

Proof I prove the contrapositive.

With $\mathbf {S4}_{\mathcal {I}}$ as our background logic, we can turn now to developing the modal theory of lawless sequences.

5 The modal theory of lawless sequences

Our language will be that of second-order arithmetic: $\lbrace 0,S,+,\times ,< \rbrace $ . The logical vocabulary is $ \lbrace \forall , \exists , \wedge ,\vee ,\rightarrow ,\neg ,=,\square , \mathcal {I} \rbrace $ . The possibility operator $\lozenge $ can of course be defined as $\lozenge A:\leftrightarrow \neg \square \neg A$ .

There are three sorts of variables: $x,y,z,\dots $ ranging over natural numbers, $f,g,h,\dots $ ranging over classical functions on natural numbers, and $\alpha ,\beta ,\gamma ,\dots $ ranging over choice sequences. The objects in the range of first-order variables $x,y,z,\dots $ are the familiar natural numbers. I assume that the natural numbers form a completed totality rather than themselves being a mere potential infinity. Thus the natural numbers all exist at each moment in time rather than coming to exist at some point in time. Functions $f,g,h,\dots $ are the extensional objects familiar from classical second-order arithmetic, and their graphs are assumed to never change, being fixed for all time. I will occasionally use variables $X,Y,Z$ for sets of natural numbers, though officially such sets are identified with their characteristic functions. The reason for taking functions as primitive and sets as defined, instead of the other way around, is that the intuitionistic theory of lawless sequences is formulated with variables for lawlike functions. These will be translated as classical function variables; so taking function variables to be primitive rather than defined simplifies the translation.

Since choice sequences are supposed to be uncompleted objects, they should be partial functions of natural numbers. This will require our logic to be free, as indicated above.

For some purposes, we will be interested in formulas that contain no occurrences of choice sequence variables or modal operators, that is, formulas in the language of second-order arithmetic. Let this restricted language be denoted by $\mathcal {L}_0$ .

We can separate the axioms of the theory into three categories: logical axioms, arithmetic axioms, and sequence axioms. The logical axioms will be those of $\mathbf {S4}_{\mathcal {I}}$ given above.

5.1 Arithmetical axioms

For arithmetic axioms we include necessitations of universal closures of the following:

1. A0 $0=0 \wedge (S(x)=S(x))\wedge (x+y=x+y) \wedge (x\times y =x\times y)$ .

2. A1 $0\neq S(x)$ .

3. A2 $S(x)=S(y) \rightarrow x=y$ .

4. A3 $x+0=x$ .

5. A4 $x+S(y)=S(x+y)$ .

6. A5 $x\times 0=0$ .

7. A6 $x\times S(y)= (x\times y) +x$ .

8. A7 $x\nless 0$ .

9. A8 $x<S(y)\leftrightarrow (x<y \vee x=y)$ .

10. A9 $\square \forall x \exists y \square f(x)=y$ .

11. IND $\forall f \big ( f(0)=0 \wedge \forall x(f(x)=0 \rightarrow f(S(x))=0 ) \rightarrow \forall x f(x)=0 \big )$ .

In the presence of the full axiom of choice, the induction axiom IND also entails each instance of the induction schema, for A an $\mathcal {L}_0$ formula:

$$ \begin{align*}A(0) \wedge \forall x(A(x) \rightarrow A(S(x))) \rightarrow \forall x A(x) .\end{align*} $$

Conversely, the schema also entails the axiom IND by taking the instance $A(x):= f(x)=0$ . Of course, in various subsystems of second-order arithmetic that we will return to in Section 9, the difference between the induction axiom and the induction schema is important.

A0 is included to ensure that arithmetical terms always have a denotation, and A9 ensures that classical functions are always defined and have their values necessarily. Otherwise these are the standard axioms of PA. We also include every instance of the axiom of choice where A is an $\mathcal {L}_0$ formula:

1. AC $\forall x \exists y A(x,y) \rightarrow \exists f \square \forall x \square A(x,f(x))$ .

This of course entails the comprehension schema for sets of numbers (where, again, A is an $\mathcal {L}_0$ formula):

1. CA $ \exists X \square \forall x(x\in X \leftrightarrow A(x))$ .

The reason for not allowing choice sequence variables to occur in the choice schema is that, per axiom A9, we want our functions to not change with time. If we allowed choice sequences to occur in the choice schema, we could define a function f such that $\forall x (\alpha (x)=f(x) \vee (\alpha (x)\neq \alpha (x) \wedge f(x)=0)$ . But then f would be subject to change as $\alpha $ grew, which we do not want.

(The reason for allowing all instances of AC and the full induction schema will be discussed in Section 8.3. For most purposes in this paper, however, choice for $\Delta ^0_1$ formulas would suffice.)

Given that the goal of this paper is to combine a modal-potentialist construal of lawless sequences with a standard, classical theory of second-order arithmetic, we want the arithmetic portion of the theory to hold constant through all time. This idea of a formula holding constant through time is captured by the notion of stability.

Definition 5.1 (Stability).

Say that a formula A is positively stable when the following holds:

$$ \begin{align*}\square\forall\vec{\alpha} \forall \vec{f}\forall \vec{x} [ A(\vec{\alpha},\vec{f},\vec{x})\rightarrow \square A(\vec{\alpha},\vec{f},\vec{x}) ].\end{align*} $$

And A is negatively stable when:

$$ \begin{align*}\square\forall\vec{\alpha} \forall\vec{f} \forall\vec{x}[ \neg A(\vec{\alpha},\vec{f},\vec{x})\rightarrow \square \neg A(\vec{\alpha},\vec{f},\vec{x})].\end{align*} $$

A formula that is both positively and negatively stable will be called stable simpliciter.

Thus, to say that a formula A is provably stable in a theory T is to say that T proves these two conditionals. Similarly, a model in which those two conditionals are true would be a model in which A is stable.

There are at least three natural ways to ensure that the arithmetic portion of the theory is provably stable. The first way is simply to add as axioms the positive and negative stability of all $\mathcal {L}_0$ formulas. The second option appeals to the full axiom of choice. The third option uses AC restricted to atomic $\mathcal {L}_0$ formulas and the Barcan formula for individual and classical function variables. The Barcan formula, recall, is the schema $ \forall o \square A(o) \rightarrow \square \forall o A(o) $ .

Proposition 5.2. Assume the axioms A0–A9. Then:

1. 1. Assuming full AC, each $\mathcal {L}_0$ formula A is provably stable.

2. 2. Assuming the Barcan Formula for individual variables and classical function variables and AC restricted to atomic formulas, each $\mathcal {L}_0$ formula A is provably stable.

Proof (1) Given any $\mathcal {L}_0$ formula A, AC entails that there is a function:

$$ \begin{align*}f_A(\vec{x})= \begin{cases} 1, & \mathrm{if~} A(\vec{x}), \\ 0, & \mathrm{if~} \neg A(\vec{x}). \end{cases}\end{align*} $$

Now by A9, $f_A$ has its values necessarily. So if A, then $f_A(\vec{x})=1$ , hence $\square f_A(\vec {x})=1$ , hence $\square A(\vec {x})$ . Similarly if $\neg A(\vec {x})$ .

(2) Induction on the complexity of A. For the atomic case, use AC as in the proof of (1). For the induction step, the cases where A is $\neg B$ , $B\vee C$ , $B\wedge C$ , or $B\rightarrow C$ are all straightforward using the i.h. Consider the case where A is $\forall y B$ . By i.h. (suppressing other free variables for readability) we have a proof of $\forall y(B \rightarrow \square B)$ , which gives $\forall y B \rightarrow \forall y \square B$ , which by the Barcan Formula gives $\forall y B\rightarrow \square \forall y B$ . This shows A is positively stable.

For negative stability, by the i.h. we have $\forall y(\neg B \rightarrow \square \neg B)$ , which entails $\exists y \neg B \rightarrow \exists y \square \neg B)$ , which entails $\neg \forall y B \rightarrow \square \neg \forall y B$ .

The cases of $\exists x B$ , $\forall f B$ , and $\exists f B$ are similar.

Each of these three ways of ensuring the stability of $\mathcal {L}_0$ formulas is well-motivated. For instance, because arithmetic stability falls straightforwardly out of the main goal of this paper, it would not be unreasonable to simply stipulate it axiomatically. Likewise, the idea that the realm of numbers and classical functions on them is fixed and unchanging suggests adopting the Barcan Formula.Footnote ¹³

Since I already stipulated that we have the full AC available, we could simply leave the matter there. In Sections 8.3 and 9, however, I will return to the question of whether one could use weaker versions of AC; in that context, we would need to have a different way of proving stability for $\mathcal {L}_0$ formulas.

6 The intuitionistic theory of lawless sequences

In this section I will introduce the intuitionistic theory of lawless sequences; then in the next two sections I will show that this theory can be interpreted in $MC_{LS}$ . Because this theory is not very well known outside intuitionistic circles, I will both present the precise axioms of lawless sequences and also discuss their informal motivation. (The intuitionistic theory $LS$ of lawless sequence results from adding these axioms to a simple base theory of analysis. I will return to that base theory in Section 8.3, but for now the focus will be on the axioms peculiar to lawless sequences.) My exposition here largely follows [Reference Troelstra31, Chapter 2] and [Reference Troelstra and van Dalen34, Chapter 12], and the reader familiar with those references may skim or skip this section.

To reduce clutter, in this section only I will use $n,m$ as variables ranging over sequence numbers, so that if $Seq$ is the set of sequences numbers, $\forall n$ and $\exists n$ should be taken as abbreviating $\forall n\in Seq$ and $\exists n\in Seq$ .

There are four axioms of this theory, which I will discuss in turn. The first axiom says that for every possible initial segment, there is a lawless sequence with that initial segment.

1. LS1 $\forall n \exists \alpha (\alpha \in n)$

Similar to the axiom S6 in my modal theory, $LS1$ serves as a density principle. Troelstra also describes it as corresponding to the informal idea that we can pick any initial segment of a sequence before we let it proceed on its own.

The second axiom says that (extensional) identity is decidable for lawless sequences, where extensional identity $\alpha =\beta $ is understood to mean $\forall x (\alpha (x)=\beta (x))$ .

1. LS2 $\alpha = \beta \vee \alpha \neq \beta $

This axiom is justified by reference to intensional identity: two segments are intensionally identical (written $\alpha \equiv \beta $ ) if they are given as the very same procedure for picking numbers. Intuitively, intensional identity should be decidable. So if we can argue that $\alpha = \beta \leftrightarrow \alpha \equiv \beta $ , then it would follow that extensional identity is decidable. Clearly $\alpha \equiv \beta \rightarrow \alpha =\beta $ . Conversely, since at any stage of picking, one only knows a finite initial segment of a sequence, the only way one could know two sequences are (always) coextensive is if they are given as the very same sequence of choices. Hence $\alpha =\beta \rightarrow \alpha \equiv \beta $ . Note that this is an intuitionistic argument. It asks what it would take to prove $\alpha =\beta $ and concludes that one would have to have proved $\alpha \equiv \beta $ . Moreover, it does not rely on the “unfinished” character of choice sequences, for even if we think of lawless sequences as already completed by the ideal mathematician, our inability to survey the entire sequence, or predict its course via a law, would preclude us from asserting $\alpha =\beta $ unless we had a proof of $\alpha \equiv \beta $ .

The third axiom says that any property A which holds of a lawless sequence $\alpha $ depends only on some finite initial segment of $\alpha $ . Thus, the third axiom justifies a continuity principle for mappings from lawless sequences to numbers.

1. LS3 $A(\alpha ,\beta _1,\dots ,\beta _l) \wedge \bigwedge _i \alpha \neq \beta _i \rightarrow \exists n ( \alpha \in n \wedge \forall \gamma \in n (\bigwedge _i \gamma \neq \beta _i \rightarrow A(\gamma ,\beta _1,\dots ,\beta _l)))$

This is justified by the idea that anything that can be asserted about a lawless sequence is asserted at some finite stage, and hence is asserted on the basis of only a finite segment of the sequence. Thus the assertion should also hold of any sequence with that same initial finite segment. This is often called the axiom of open data.

The reason for requiring that $\alpha $ be distinct from the $\beta $ ’s is to rule out counterexamples that rely on $\alpha $ and $\beta $ being identical. For instance, if A were the simple formula $\alpha =\beta $ , then it would be false that $\exists n \forall \gamma \in n A(\gamma ,\beta )$ . The point is that our initial motivation for $LS3$ relied on the idea that A must hold on the basis of some finite portion of $\alpha $ ’s graph. But $\alpha =\beta $ would provide some information about the entirety of $\alpha $ ’s future graph, namely that it coincides with $\beta $ ’s graph. Thus we want to rule out this extra bit of information.

Now in fact, we can require that the $\beta $ ’s also be pairwise distinct. Since identity is decidable, $A(\alpha ,\beta _1,\beta _2)$ is equivalent to $[A(\alpha ,\beta _1,\beta _2) \wedge \beta _1\neq \beta _2 ] \vee [A(\alpha ,\beta _1,\beta _1)\wedge \beta _1=\beta _2]$ . The generalization to more than two variables $\beta _i$ is obvious. This gives the following alternative formulation of $LS3$ which it will be somewhat more convenient to work with when we interpret $LS$ in $MC_{LS}$ .Footnote ¹⁴

1. LS3^′

Finally, it is easy to observe that this axiom justifies the principle of $\forall \alpha \exists x$ -continuity (also called weak continuity for numbers):

$$ \begin{align*}\forall \alpha \exists x A(\alpha,x)\rightarrow \forall \alpha \exists x \exists y \forall \beta \in \overline{\alpha}(y) A(\beta,x).\end{align*} $$

To obtain this schema from $LS3$ , for each $\alpha $ and x satisfying $ A(\alpha ,x)$ we find an n as in $LS3$ (i.e., $\forall \gamma \in n A(\gamma ,x)$ ). Then trivially there is a y such that $\overline {\alpha }(y)=n$ , so we have

$$ \begin{align*}\forall \alpha \forall x [ A(\alpha,x)\rightarrow \exists y \forall \beta \in \overline{\alpha}(y) A(\beta,x)].\end{align*} $$

Then some easy quantificational logic gives us the principle of $\forall \alpha \exists x$ -continuity.

The fourth and final axiom is also a continuity principle, saying roughly that whenever a lawlike sequence can be chosen from a lawless sequence, then there is a uniform, lawlike way of choosing each such lawlike sequence on the basis of the neighborhood in which each lawless sequence is found.

The precise statement of this fourth axiom is more technical, and requires the notion of a neighborhood function. If $F \subset \mathbb {N}^{\mathbb {N}}$ is a class of mappings on natural numbers, a neighborhood function on F encodes a continuous functional $F\rightarrow \mathbb {N}$ . For instance, F might be the classical functions or, in the case that interests us, F will be the lawless sequences. Intuitively, letting $K_F$ be the class of neighborhood functions on F, a particular function $e\in K_F$ takes initial segments of a sequence $\xi \in F$ , and $e(\overline {\xi }(x))=0$ if the initial segment $\overline {\xi }(x)$ is not long enough to determine the value of the function that e encodes and $e(\overline {\xi }(x))=y+1$ if the function that e codes takes value y on any argument that agrees with $\xi $ on the first x arguments. The class of neighborhood functions on lawless sequences can be defined as the class of e satisfying:

$$ \begin{align*}\forall \alpha \exists x ( e(\overline{\alpha}(x))> 0 ) \wedge \forall n,m (e(n)> 0 \rightarrow e(n^\frown m)= e(n) ).\end{align*} $$

Let $e\in K_0$ abbreviate this formula. For brevity, define $e(\alpha )=x :\leftrightarrow \exists y (e(\overline {\alpha }(y)=x+1)$ . Finally, let $\nu _p (\alpha _1,\dots ,\alpha _p):=\lambda x.\nu _p (\alpha _1(x),\dots ,\alpha _p(x))$ be a pairing function on sequences.

If e is a neighborhood function on lawless sequences, then it is reasonable also to see e as a neighborhood function encoding a continuous functional $F\rightarrow \mathbb {N}$ for any class of functions $F\subseteq \mathbb {N}^{\mathbb {N}}$ . If you simply abstract away from any intensional information you have about $f\in F$ , then you can treat its graph as though it were the graph of a lawless function, and scan through that graph until you find an n such that $e(\overline {f}(n))>0$ . This idea that any neighborhood function on lawless sequences induces a neighborhood function on all functions $\mathbb {N}^{\mathbb {N}}$ is the so-called extension principle.

Now, $\nu _p (\alpha _1,\dots ,\alpha _p)\in \mathbb {N}^{\mathbb {N}}$ , so we should also be able to regard any $e\in K_0$ as a neighborhood function for p-tuples of lawless sequences as well. This leads to the following preliminary version of $LS4$ .

1. LS4₀

The motivation for this is similar to $LS3$ : if for any lawless sequence you can find a lawlike sequence satisfying A, then this must be possible on the basis of some initial data from the lawless sequence. So for some neighborhood there is a lawlike way of finding the lawlike sequence from the value of the neighborhood function on that lawless sequence. Then we can extend this idea to multiple lawless sequences by taking them together via pairing as a single sequence. Since this sequence of p-tuples was formed by pairing sequences that are entirely lawless, the paired sequence should not exhibit any lawlike behavior either. Just as we were able to use a neighborhood function to find a lawlike sequence from a single lawless sequence, we should be able to do similarly with a p-tuple of lawless sequences. Hence Troelstra’s gloss on this axiom is that “with respect to operations of types $\mathbb {N}^{\mathbb {N}}\rightarrow \mathbb {N}$ , p-tuples of independent lawless sequences behave like single lawless sequences” ([Reference Troelstra31, p. 28]).

To get from this preliminary version $LS4_0$ to the final, official axiom $LS4$ , we need to introduce another class of functions, denoted K. K is inductively defined as the least class of functions satisfying the following two conditions:

1. K1 $\exists y>0 \forall x f(x)=y \rightarrow f\in K$ .

2. K2 $[f(0)=0 \wedge \forall x \exists g\in K (\forall n\in Seq \, f(\langle x \rangle ^\frown n)=g(n))] \rightarrow f\in K$ .

It is plausible that $K=K_0$ . It is easy to check that $K_0$ satisfies both K1 and K2, so that $K_0\subseteq K$ . Conversely, let $e\in K_0$ be arbitrary. Then the tree of n such that $e(n)=0$ will be well-founded, and we can argue by transfinite induction that for every node n in this tree, $\lambda m. e(n^\frown m)\in K$ , and hence $\lambda m. e(\langle \rangle ^\frown m):= e\in K$ . This argument can be fleshed out into a formally rigorous argument (as we will see in Theorem 8.19), though the inclusion $K_0\subseteq K$ requires application of the law of excluded middle, and so is non-constructive. Intuitionistically, $K=K_0$ can be proved by (decidable) Bar Induction and in fact is equivalent to decidable Bar Induction in the background theory of elementary analysis ([Reference Troelstra and van Dalen34, p. 4.8.13]).

Adopting the identification $K=K_0$ gives us our final formulation of $LS4$ .

1. LS4

7 The Beth–Kripke translation

The main goal of this paper is to provide an interpretation of the intuitionistic theory $LS$ in the classical modal theory $MC_{LS}$ . In this section, I introduce the translation that will be used for that interpretation. This translation was defined in [Reference Brauer, Linnebo and Shapiro7], where it was also shown to provide a faithful translation of intuitionistic logic in $\mathbf {S4}_{\mathcal {I}}$ . For full details the reader may refer to that paper; I will just sketch the main ideas behind the translation.

The translation is inspired by a variant of the familiar Beth semantics for intuitionistic logic, which allows the domains of worlds in the model to grow. Such models are sometimes called Beth–Kripke models, and hence the translation was called the Beth–Kripke translation. One further tweak that [Reference Brauer, Linnebo and Shapiro7] add is to require that for every term in the relevant language, and every path through the Beth–Kripke model, there is a world where that term has a denotation.

The insight that enables our translation is that a Beth–Kripke model for intuitionistic logic can equally be viewed as a model for $\mathbf {S4}_{\mathcal {I}}$ by using the respective semantic clauses. Moreover, the semantic clauses for intuitionistic forcing can be explicitly mimicked in an $\mathbf {S4}_{\mathcal {I}}$ model by adding some modal operators. This is done according to the following translation.

When we are working in many-sorted logic, all the quantifiers are translated according to this scheme, no matter what type o is.

Now it is easy to see that for any non-modal formula A, $T\Vdash A$ as a Beth–Kripke model just in case $T\models A^{\mathsf {B}}$ as an $\mathbf {S4}_{\mathcal {I}}$ model. The last detail to take care of is that in our variant Beth–Kripke models, it is required that each term eventually have a denotation. For a term t, the following condition asserts that t inevitably exists:

(IE_t ) $$\begin{align} \square \forall \vec{x} \mathcal{I} [t(\vec{x})=t(\vec{x})]. \end{align} $$

For a fixed language $\mathcal {L}$ , let $IE:=\lbrace IE_t : t\in \mathcal {L} \rbrace $ . Then we have the following result, which shows that the deductive system for $\mathbf {S4}_{\mathcal {I}}$ given in Section 4 faithfully interprets intuitionistic logic via the $\mathsf {B}$ translation.

We have already observed that $MC_{LS}$ proves that each term eventually denotes. Thus, in order to prove that $MC_{LS}$ interprets the intuitionistic theory $LS$ it remains to show that $MC_{LS}$ proves the $\mathsf {B}$ translations of the axioms of $LS$ .

8 Interpreting $LS$

In this section I show that $MC_{LS}$ does indeed interpret $LS$ under the $\mathsf {B}$ translation. As just noted, it only remains to show that the translations of axioms of $LS$ are provable in $MC_{LS}$ . In Section 8.1 I do this for $LS1$ and $LS2$ , along with noting a few other simple facts. In Section 8.2 I prove the translations of $LS3$ and $LS4$ . The key tool here is an elimination theorem showing that each formula $A^{\mathsf {B}}$ is equivalent to an arithmetical formula. Then in Section 8.3 I finally note that $MC_{LS}$ interprets the base theory of elementary analysis that $LS$ is built on.

8.2 Continuity principles

In this section I show that $MC_{LS}$ proves $LS3^{\mathsf {B}}$ and $LS4^{\mathsf {B}}$ . To do so, I will establish an elimination theorem showing that every formula A in the range of the $\mathsf {B}$ translation is equivalent to an arithmetical formula with no occurrences of choice sequence variables, either free or bound.Footnote ¹⁵ When A is in the range of the $\mathsf {B}$ translation, we can define the arithmetical translation T of A relative to $\vec {n}$ . If A has k choice sequence parameters, $T(A,\vec {n})$ will be an arithmetical formula with k number parameters $n_1,\dots ,n_k$ . The intention is that when A says something about $\alpha _1,\dots ,\alpha _k$ , $T(A,\vec {n})$ says something about all classical functions $g_1,\dots ,g_k$ that have initial segments $n_1,\dots ,n_k$ . The elimination theorem will then show that these are equivalent, so that any formula $A^{\mathsf {B}}(\alpha )$ amounts to a claim that all classical functions with $\mathrm {is} \alpha $ as an initial segment behave in a certain way.

Definition 8.8 (T-translation).

If A is a formula in the range of the $\mathsf {B}$ translation with at most k choice sequence parameters $\alpha _1,\dots ,\alpha _k$ , define the translation $T(A,\vec {n})$ relative to sequence numbers $n_1,\dots ,n_k$ inductively as follows:

• • When A is the translation of an atom, $\mathcal {I}\square P(\vec {x},\vec {\alpha },\vec {f})$ , define $T(A,\vec {n})$ to be

  $$ \begin{align*}\forall g_1\in n_1 \dots \forall g_k\in n_k \exists y_1\dots\exists y_k \forall h_1\in \overline{g_1}(y_1) \dots \forall h_k \in \overline{g_k}(y_k) P(\vec{x},\vec{h},\vec{f}).\end{align*} $$

• • When A is a conjunction $B \wedge C$ , let $T(A,\vec {n})$ be $T(B,\vec {n})\wedge T(C,\vec {n})$ .

• • When A is $\mathcal {I}(B \vee C)$ , let $T(A,\vec {n})$ be $\forall \vec {g}\in \vec {n}\exists \vec {y} \left ( T\left ( B,\overrightarrow {\overline {g}(y)} \right ) \vee T \left ( C,\overrightarrow {\overline {g}(y)}\right ) \right )$ .

• • When A is $\square \neg B$ , let $T(A,\vec {n})$ be $\forall \vec {m} \succeq \vec {n} \neg T(B,\vec {m})$ .

• • When A is $\square (B \rightarrow C)$ , let $T(A,a)$ be $\forall \vec {m} \succeq \vec {n} \big ( T(B,\vec {m}) \rightarrow T(C,\vec {m}) \big )$ .

• • When A is $\square \forall x B$ , let $T(A,\vec {n})$ be $\forall \vec {m}\succeq \vec {n} \forall x T(B,\vec {m})$ .

• • When A is $\square \forall f B$ , let $T(A,\vec {n})$ be $\forall \vec {m}\succeq \vec {n} \forall f T(B,\vec {m})$ .

• • When A is $\mathcal {I} \exists x B$ , let $T(A,\vec {n})$ be $\forall \vec {g}\in \vec {n} \exists \vec {y} \exists x T\left (B,\overrightarrow {\overline {g}(y)}\right )$ .

• • When A is $\mathcal {I} \exists f B$ , let $T(A,\vec {n})$ be $\forall \vec {g}\in \vec {n} \exists \vec {y} \exists f T\left ( B,\overrightarrow {\overline {g}(y)} \right )$ .

• • When A is $\square \forall \alpha _{k+1} B$ , let $T(A,\vec {n})$ be

  $$ \begin{align*}\forall \vec{m} \succeq \vec{n} \left( \bigwedge_{1\leq i \leq k} T(B^{\alpha_{k+1}}_{\alpha_i},\vec{m}) \wedge \forall m_{k+1}\in Seq \, T(B,\vec{m}, m_{k+1}) \right).\end{align*} $$

• • When A is $\mathcal {I}\exists \alpha _{k+1}B$ , let $T(A,\vec {n})$ be

  $$ \begin{align*}\forall \vec{g}\in \vec{n} \exists \vec{y} \left( \bigvee_{1\leq i \leq k} T\left(B^{\alpha_{k+1}}_{\alpha_i},\overrightarrow{\overline{g}(y)} \right) \vee \exists m \in Seq \, T\left(B,\overrightarrow{\overline{g}(y)},m\right) \right).\end{align*} $$

The goal will be to show that any formula in the range of the $\mathsf {B}$ translation is equivalent to its T translation. I begin with some simple facts that I will often appeal to without mention.

Proposition 8.9. When A is in the range of the $\mathsf {B}$ translation, $T(A,\vec {n})$ is a formula in the language $\mathcal {L}_0$ of second-order arithmetic. Hence $T(A,\vec {n})$ is positively and negatively stable.

Lemma 8.10. Say $\vec {x}$ and $\vec {f}$ are the free variables in $T(A,m,\vec {n})$ . Then $MC_{LS}$ proves:

1. 1. For all $\vec {x}$ and $\vec {f}$ , if $T(A,m,\vec {n})$ and $m\preceq m'$ , then $T(A,m',\vec {n})$ .

2. 2. For all $\vec {x}$ and $\vec {f}$ , if for all $m'\succ m$ , $T(A,m', \vec {n})$ , then $T(A,m,\vec {n})$ .

Proof Both claims can be proved simultaneously by a straightforward induction on A.

I will also define one more notion, which I will call the $\alpha $ -n replacement of an atom P. This notion only plays a supporting role in the proof of the elimination theorem, but it will return in Section 9 as a key part of the conservativity argument there.

Definition 8.11 ( $\alpha $ -n replacement).

Given an atom $P(\vec {\alpha })$ , possibly with other free variables not shown, define the $\vec {\alpha }$ - $\vec {n}$ replacement $\mathcal {R}(P,\vec {\alpha },\vec {n})$ as follows. Let $\alpha _{i_1}(t_1),\dots ,\alpha _{i_k}(t_k)$ be a list of all occurrences of choice sequence variables and their arguments, subject to the constraint that no earlier item on the list itself contains an occurrence of an item later in the list. Let $t_j'$ be the result of successively replacing in $t_j$ any occurrences of $\alpha _{i_l}(t_l)$ , for $l<j$ , with $(n_{i_l})_{t_l'}$ . Let $P'$ be the result of successively replacing each occurrence of $\alpha _{i_j}(t_j)$ with $(n_{i_j})_{t_j'}$ . Then $\mathcal {R}(P,\vec {\alpha },\vec {n})$ is the formula:

$$ \begin{align*}\left( \bigwedge_{1\leq j\leq k} t_j'<lh(n_{i_j}) \wedge P' \right) \vee \left( \bigvee_{1\leq j\leq k} t_j'\geq lh(n_{i_j}) \wedge 0=1 \right).\end{align*} $$

(For classical functions $\vec {g}$ , the $\vec {g}$ - $\vec {n}$ replacement $\mathcal {R}(P,\vec {g},\vec {n})$ can be defined in exactly the same way.)

This definition is quite wordy, but the idea is simple: we replace occurrences of $\alpha (x)$ with $(n)_x$ , and iterate for nested occurrences such as $\alpha _2(\alpha _1(x))$ . The motivation, of course, is that when n is the initial segment of $\alpha $ , this will provide an $\mathcal {L}_0$ formula that is equivalent to the original atom containing choice sequence variables. An example of an $\vec {\alpha }$ - $\vec {n}$ replacement will illustrate the idea.

Example 8.12. Let $P:\leftrightarrow \alpha _1(\alpha _2(4))< \alpha _3(\alpha _3(2))$ . Then $\mathcal {R}(P,\alpha _1,\alpha _2,\alpha _3, n_1,n_2,n_3)$ is the formula:

$$ \begin{align*} \left( 4< lh(n_2) \wedge (n_2)_4 <lh(n_1) \wedge 2< lh(n_3) \wedge (n_3)_2 < lh (n_3) \wedge (n_1)_{(n_2)_4} < (n_3)_{(n_3)_2} \right)& \\ \vee \big( \big( 4\geq lh(n_2) \vee (n_2)_4 \geq lh(n_1) \vee 2 \geq lh(n_3) \vee (n_3)_2 \geq lh (n_3) \big) \wedge 0=1 \big).& \end{align*} $$

It is evident that $P\alpha $ is provably equivalent to its $\alpha $ - $\mathrm {is}\ \alpha $ replacement:

Proposition 8.13. For each atom P, $MC_{LS}\vdash \square \forall \vec {\alpha } \forall \vec {n} \big(\kern-1.5pt \bigwedge _i \mathrm {is} \alpha _i=n_i \rightarrow( P\vec {\alpha } \leftrightarrow \mathcal {R}(P,\vec {\alpha },\vec {n}) ) \big)$ .

And here is the key theorem.

Theorem 8.14 (Elimination theorem).

If A is a formula in the range of the $\mathsf {B}$ translation with free variables among $\vec {x},\vec {f},\vec {\alpha }$ , then $MC_{LS}$ proves

$$ \begin{align*}\square \forall \vec{x} \forall f \forall \vec{\alpha} &\left( \bigwedge_{i,j} \neg \square \forall x \alpha_i(x)\simeq \alpha_j(x)\right.\\& \quad \left.\rightarrow \left( A(\vec{x},\vec{\alpha},\vec{f}) \leftrightarrow \forall \vec{n} \left( \bigwedge_i \mathrm{is} \alpha_i = n_i \rightarrow T(A,\vec{n}) \right) \right) \right).\end{align*} $$

This is proved by a lengthy induction on the complexity of A. Although the proof illustrates some key argument patterns used in $MC_{LS}$ , the details are somewhat tedious, and hence it is relegated to Appendix B. With the elimination theorem in hand, it is straightforward to prove the translation of $LS3'$ .

Theorem 8.15. $ MC_{LS} \vdash LS3{^{\prime {\mathsf {B}}}}$ .

Proof $LS3{^{\prime {\mathsf {B}}}}$ is

$$ \begin{align*} &\square \Bigg( \Bigg. \left( A^{\mathsf{B}}(\alpha,\vec{\beta}) \wedge \bigwedge_i (\alpha \neq \beta_i)^{\mathsf{B}} \wedge \bigwedge_{i,j} (\beta_i \neq \beta_j)^{\mathsf{B}} \right) \rightarrow \\& \quad \rightarrow \mathcal{I} \exists n \square \left( Seq^{\mathsf{B}}(n) \wedge (\alpha\in n)^{\mathsf{B}} \wedge \square \forall \gamma \square \left( (\gamma\in n)^{\mathsf{B}} \wedge \bigwedge_i (\gamma\neq \beta_i)^{\mathsf{B}} \rightarrow A^{\mathsf{B}}(\gamma,\vec{\beta}) \right) \right) \Bigg. \Bigg). \end{align*} $$

We can immediately make some obvious simplifications in light of the fact that $Seq(n)$ and $\alpha \in n$ are equivalent to their $^{\mathsf {B}}$ translations and $(\alpha \neq \beta )^{\mathsf {B}}$ is equivalent to $\neg \square \forall x (\alpha (x)\simeq \beta (x))$ .

Suppose that $A^{\mathsf {B}}(\alpha ,\vec {\beta })$ and that $\alpha $ and the $\beta $ ’s are all pairwise distinct. Let n be $\mathrm {is} \alpha $ and let $\mathrm {is} \beta _i=m_i$ . Then by Theorem 8.14 we have $T(A^{\mathsf {B}},n,\vec {m})$ . Let $\gamma \in n$ be an arbitrary choice sequence distinct from all the $\beta $ ’s. Then necessarily there are some $n'\succeq n$ and $\vec {m'}\succeq \vec {m}$ such that is $\mathrm {\gamma }=n'$ and $\mathrm {is} \beta _i=m_i'$ . But by Lemma 8.10, we know $T(A^{\mathsf {B}},n',\vec {m'})$ , so by Theorem 8.14 we know $A^{\mathsf {B}}(\gamma ,\vec {\beta })$ .

I turn now to the translation of $LS4$ . First, recall the definition of a neighborhood function:

$$ \begin{align*}e\in K_0 :\leftrightarrow \forall \alpha \exists x e(\overline{\alpha}(x))> 0 \wedge \forall n (e(n)> 0 \rightarrow \forall m\succeq n \, e(m)=e(n) ) .\end{align*} $$

This concept has an equivalent arithmetical definition, as the following lemma shows.

Lemma 8.16. $MC_{LS} \vdash (e\in K_0)^{\mathsf {B}} \leftrightarrow \forall g \exists x \, e(\overline {g}(x))> 0 \wedge \forall n (e(n)> 0 \rightarrow \forall m\succeq n \, e(m)=e(n) )$ .

Proof Observe that $(e\in K_0)^{\mathsf {B}}$ is equivalent to $\square \forall \alpha \mathcal {I }\exists x \, e(\overline {\alpha }(x))> 0 \wedge \forall n (e(n)\neq 0 \rightarrow \forall m\succeq n \, e(m)=e(n) )$ . So clearly it will suffice to show within $MC_{LS}$ that $\square \forall \alpha \mathcal {I }\exists x e(\overline {\alpha }(x))> 0 \leftrightarrow \forall g \exists x \, e(\overline {g}(x))>0$ .

First assume $\square \forall \alpha \mathcal {I} \exists x \, e(\overline {\alpha }(x))> 0$ . Then, in particular, for a sequence $\gamma $ such that $\mathrm {is} \gamma =\langle \rangle $ , it is true that $\mathcal {I}\exists x \, e(\overline {\gamma }(x))>0$ . Every function g agrees with the defined segment of $\gamma $ , so for each g it is not inevitable that $\gamma $ and g disagree. Hence for each g it is possible that $\exists x (\overline {\gamma }(x)=\overline {g}(x) \wedge e(\overline {g}(x))>0$ . So for each g there is an x such that $e(\overline {g}(x))>0$ .

Conversely, assume that $\forall g \exists x \, e(\overline {g}(x))>0$ . Let $C(n) :\leftrightarrow n\in Seq \wedge e(n)=0 $ . So C holds of the sequence numbers that a choice sequence $\alpha $ could go through and still have $e(\mathrm {is} \alpha )$ be 0. By the assumption, C is quasi-treelike and well-founded. (In fact, C will define a tree.) So by S5 it is inevitable that $\alpha $ leaves C. That is, it is inevitable that there is some x such that $e(\overline {\alpha }(x))>0$ .

This lemma is interesting for two reasons. First, it is technically useful because it reduces the property $(e\in K_0)^{\mathsf {B}}$ to something arithmetical and hence stable. Second, it is interesting because it shows that the neighborhood functions that encode continuous operations from lawless sequences to natural numbers also encode continuous operations from lawlike sequences (represented as classical functions) to natural numbers. This is a version of what has been called the extension principle in intuitionistic mathematics.Footnote ¹⁶ The extension principle admits of very compelling informal plausibility arguments, but it is nevertheless a substantive claim. That this version of the principle is actually provable in $MC_{LS}$ is of some interest.

We can also observe that neighborhood functions so defined really do encompass k-adic neighborhood functions in the way informally sketched in the discussion of Section 4.

Lemma 8.17. $MC_{LS} \vdash (e \in K_0)^{\mathsf {B}} {\kern-1pt}\rightarrow{\kern-1pt} \forall \alpha _1 \dots \forall \alpha _k \mathcal {I}\exists x \exists n {\kern-1pt}\in{\kern-1pt} Seq ( lh(n)=x \wedge \forall y<x \, (n)_y=\langle \alpha _1(y),\dots ,\alpha _k(y) \rangle \wedge e(n)>0 )$ .

Proof Consider the formula $C(n):\leftrightarrow e(n)=0 \wedge \forall x<lh(n) \exists y_1,\dots ,y_k x=\langle y_1,\dots ,y_k\rangle $ . The $\preceq $ -downward closure $\overline {C}(m):\leftrightarrow \exists n(C(n) \wedge m \preceq n$ is then quasi-treelike, and by Lemma 8.16, $\overline {C}$ will be well-founded. So inevitably $\vec {\alpha }$ will leave $\overline {C}$ . That is, inevitably $\exists x \exists n \in Seq ( lh(n)=x \wedge \forall y<x \, (n)_y=\langle \alpha _1(y),\dots ,\alpha _k(y) \rangle \wedge e(n)>0)$ .

Theorem 8.18. $MC_{LS} \vdash LS4_0^{\mathsf {B}}$ .

Proof Applying some obvious simplifications whose validity we have already established, $LS4_0^{\mathsf {B}}$ is

$$ \begin{align*} &\square \forall \vec{\alpha} \square \left( \bigwedge_{i,j} \neg\square \forall x \alpha_i(x)\simeq \alpha_j(x) \rightarrow \mathcal{I} \exists f A^{\mathsf{B}}(\vec{\alpha},f) \right) \\& \quad \rightarrow \mathcal{I} \exists e\in K_0 \square \forall n \square \left(\vphantom{\left( \bigwedge_{i,j} \neg\square \forall x \alpha_i(x)\simeq\alpha_j(x) \rightarrow A^{\mathsf{B}}(\vec{\alpha},f) \right)} e(n)>0 \rightarrow \mathcal{I} \exists f \square \forall \vec{\alpha}\in n \right.\\& \qquad\qquad\qquad\qquad\quad\qquad \square \left.\left( \bigwedge_{i,j} \neg\square \forall x \alpha_i(x)\simeq\alpha_j(x) \rightarrow A^{\mathsf{B}}(\vec{\alpha},f) \right) \right). \end{align*} $$

Suppose the antecedent of this large conditional holds. Then by Theorem 8.14 we know that for any pairwise distinct $\alpha $ ’s, $\forall \vec {n} [ \bigwedge _i \mathrm {is} \alpha _i=n_i \rightarrow \forall \vec {g}\in \vec {n}\exists \vec {y} \exists f T(A^{\mathsf {B}},\overrightarrow{g(y)})]$ .

Define the function e as follows. If n codes a k-tuple of sequences $\vec {n}$ but $\neg \exists f T(A^{\mathsf {B}},\vec {n})$ , then $e(n)=0$ . If n codes a k-tuple of sequences $\vec {n}$ and $ \exists f T(A^{\mathsf {B}},\vec {n})$ , then $e(n)= 1$ . And, just so e is a well-defined function, if n does not code a k-tuple of sequences, put $e(n)=2$ . To ensure that e is a neighborhood function, we need to show that $\forall \vec {g} \exists x \, e(\overline {g}(x))>0$ . For this, given the suppositions in place, it will suffice to show that for all $\vec {g}$ there is some x such that it is possible to have $\bigwedge \mathrm {is} \alpha _i=\overline {g_i}(x)$ . Using S4 and S9, we can argue that for any functions $g_1,\dots ,g_k$ it is possible for there to exist distinct $\alpha _1,\dots ,\alpha _k$ with respective initial segments $\overline {g_1}(0),\dots ,\overline {g_k}(0)$ . Thus $\forall \vec {g}\exists \vec {y} \exists f T(A^{\mathsf {B}},\overrightarrow{g(y)})$ . This ensures that e is indeed a neighborhood function.

Now suppose $e(n)>0$ . If $e(n)=2$ , let f be arbitrary; since there will not be any $\vec {\alpha }\in n$ in that case, the whole antecedent of our big conditional $LS4_0^{\mathsf {B}}$ will hold trivially. But if $e(n)=1$ , then n must code a k-tuple of sequences $\vec {n}$ and we know that $\exists f T(A^{\mathsf {B}},\vec {n})$ . Let f be any such witness. By Lemma 8.10, we also know that for any $\vec {m}\succeq \vec {n}$ , $T(A^{\mathsf {B}},\vec {m})$ (where f occurs as a parameter). For any k distinct choice sequences $\vec {\alpha }\in n$ , there will be some $\vec {m}\succeq \vec {n}$ such that $\bigwedge _i \mathrm {is}\ \alpha _i=m_i$ ; and hence by Theorem 8.14, $A^{\mathsf {B}}(\vec {\alpha },f)$ will hold.

As a slight digression, note that in this proof we had to appeal to an instance of the axiom of choice for a formula $\exists f T(A^{\mathsf {B}},\vec {n})$ —actually, a boolean combination of this formula with some $\Delta ^0_1$ formulas. The complexity of $T(A^{\mathsf {B}},\vec {n})$ can be bounded in terms of the complexity of A, but there are formulas $T(A^{\mathsf {B}},\vec {n})$ of arbitrarily high quantificational complexity. So, unlike the proofs of $LS1$ , $LS2$ , and $LS3$ , this proof actually requires the strength of $MC_{LS}$ with the full axiom of choice. It is open, however, whether a different proof might use weaker assumptions.

Returning now to our discussion of $LS4$ , recall that the official version of $LS4$ is formulated with the inductively defined class of functions K in place of the explicitly defined class $K_0$ . To directly define an analogous class K in $MC_{LS}$ , I would have to extend $MC_{LS}$ to a stronger theory such as third-order arithmetic. Rather than do that, however, I will simply show that $K_0$ satisfies the inductive closure conditions and then show schematically that $K_0$ is included in any other class that satisfies the inductive conditions. Then it will follow that any theory extending $MC_{LS}$ which is capable of formally defining K will interpret $LS4$ . The limitation of $MC_{LS}$ is merely in what definitions it can formalize, not in its deductive strength.

Make the following two abbreviations, which are schematic in the formula A:

• • $\mathbf {K1}(A):\leftrightarrow \exists y>0 \forall x \, f(x)=y \rightarrow f\in A$ .

• • $\mathbf {K2}(A): \leftrightarrow [f(0)=0 \wedge \forall x \exists g\in A (\forall n\in Seq \, f(\langle x \rangle ^\frown n)=g(n))] \rightarrow f\in A$ .

Then the following theorem is essentially the combination of Propositions 4.8.5 and 4.8.7 in [Reference Troelstra and van Dalen34].

Theorem 8.19. $MC_{LS}$ proves:

1. 1. $\mathbf {K1}(K_0) \wedge \mathbf {K2}(K_0)$ .

2. 2. $\mathbf {K1}(A) \wedge \mathbf {K2}(A) \rightarrow \forall f (f\in K_0 \rightarrow f\in A)$ .

Proof (1) That $\mathbf {K1}(K_0)$ is obvious. To see that $\mathbf {K2}(K_0)$ holds, suppose f satisfies the antecedent of $\mathbf {K2}(K_0)$ , but $f\notin K_0$ . So $\exists h \forall x f(\overline {h}(x))=0 \vee \exists n (f(n)> 0 \wedge \exists m\succeq n \, f(m)\neq f(n) )$ . The possibility that $\exists n (f(n)> 0 \wedge \exists m\succeq n \, f(m)\neq f(n) )$ is ruled out by the fact that $f(0)=0 \wedge \forall x \exists g\in K_0 (\forall n\in Seq \, f(\langle x \rangle ^\frown n)=g(n))$ . So we must have that $\exists h \forall x f(\overline {h}(x))=0$ . Let $h'(x):=h(x+1)$ . But then let $g\in K_0$ be the witness for $f(\langle h(0) \rangle ^\frown n)=g(n)$ . So $\forall x g(\overline {h'}(x))=0$ , which contradicts $g\in K_0$ .

(2) Suppose $\mathbf {K1}(A) \wedge \mathbf {K2}(A)$ but that we have some $f\in K_0$ but $f\notin A$ . We can uniformly define the functions $g_n$ so that $g_n(m)=f(n^\frown m)$ . Now since A satisfies $\mathbf {K2}$ , we know that for every n, if $g_n \notin A$ , then there is an extension $n'\succ n$ with length $lh(n)+1$ such that $g_{n'}\notin A$ . Thus by the axiom of dependent choice there is a function H enumerating these n such that $g_n\notin A$ . Then it is easy to define a function h such that $\overline {h}(x)=H(x+1)$ . Since f is a neighborhood function, there will be some x such that for all $m\succeq \overline {h}(x)$ , $f(m)=f(\overline {h}(x))>0$ . But then $g_m$ is a constant, non-zero function, so $g_m\in A$ , a contradiction.

This theorem shows that $K_0$ is closed under the inductive clauses $\mathbf {K1}$ and $\mathbf {K2}$ and, schematically, for any other class which is also so closed, $K_0$ is included in that class. Since this latter fact is schematic, any extension of $MC_{LS}$ that proved the existence of a least fixed point for the inductive clauses K1 and K2 would prove that $K_0$ was that fixed point. Such an extension might for instance frame $MC_{LS}$ in a background third-order arithmetic, or might extend the language with a new constant K for the fixed point, or might use some other means. More to the point, for present purposes, any proof in $LS$ that appeals to the minimality of K will appeal to a particular instance $A\subseteq K$ ; this can then be interpreted in $MC_{LS}$ as $A \subseteq K_0$ , which we have just seen to be provable. All that matters is that the axiom of dependent choice can be applied to formulas of the form $g_n \notin A$ .

8.3 Elementary analysis and $IDB$

I have shown so far that $MC_{LS}$ proves the $\mathsf {B}$ translations of the axioms $LS1$ – $LS4$ . The theory $LS$ , however, is based on a background theory called $IDB_1$ .Footnote ¹⁷ ( $IDB$ stands for “inductively defined Brouwer-operations”.) Thus, the last thing to do to complete our interpretation of $LS$ is to show that $MC_{LS}$ proves the $\mathsf {B}$ translations of the axioms of $IDB_1$ .

$IDB_1$ itself results from starting with the theory of elementary analysis known as $EL_1$ and adding to the language a constant K and axioms $\mathbf {K1}(K)$ , $\mathbf {K2}(K)$ and the schema $\mathbf {K1}(A) \wedge \mathbf {K2}(A) \rightarrow K\subseteq A$ . This portion of the theory is handled by translating K as $K_0$ and appealing to Theorem 8.19.

The language of $EL_1$ consists of the language of arithmetic plus function symbols $f,g,\dots $ , an abstraction operator $\lambda $ , and a recursor $\mathsf {R}$ . The axioms are those of Heyting Arithmetic $HA$ , with induction extended to the full language of $EL_1$ , the conversion axiom:

(CON) $$ \begin{align} (\lambda x t)s = t^x_s \end{align} $$

and recursion axioms, where $\Phi $ is some unary functor:

(REC-1) $$ \begin{align} \mathsf{R}(t_1,\Phi,0)=t, \end{align} $$

(REC-2) $$ \begin{align} \mathsf{R}(t_1,\Phi,S(t_2))=\Phi(\langle \mathsf{R}(t_1,\Phi,t_2),t_2 \rangle ), \end{align} $$

and finally, the axiom of choice for numbers and functions:

(AC-NF) $$ \begin{align} \forall x \exists f A(x,f) \rightarrow \exists g \forall x A(x,g(x,\cdot)). \end{align} $$

It is clear that we can omit $\lambda $ and $\mathsf {R}$ from the development of $EL_1$ by appeal to the axiom of choice. Given any proof in $EL_1$ that includes instances $\lambda x.t(x)$ , we know $\exists f \forall x f(x)=t(x)$ , and then replace each instance of $\lambda x.t(x)$ with $f(x)$ throughout the proof. (In case there are instances of $\lambda $ -abstracts that themselves contain $\lambda $ -abstracts, we work from the inside out, gradually replacing more and more $\lambda $ -abstracts.) Similarly, the axiom of choice allows us to prove the existence of a function g such that $\forall x g(x)=\mathsf {R}(t_1,\Phi ,x)$ , so we can replace instances of $\mathsf {R}$ by function variables. Then since AC holds in $MC_{LS}$ , we can interpret these modified proofs from which occurrences of $\lambda $ and $\mathsf {R}$ have been removed.

Next, we can observe that AC-NF holds in $MC_{LS}$ . Since $MC_{LS}$ includes second-order arithmetic, this is a standard result.

Proposition 8.20. $MC_{LS}\vdash $ AC-NF.

Proof Suppose $\forall x \exists f A(x,f)$ , and for simplicity suppose f is unary. Define a relation $f_1 \triangleleft f_2 :\leftrightarrow \exists x (f_1(x)< f_2(x) \wedge \forall y<x f_1(y)=f_2(y))$ . Then define $g(x,y)=z :\leftrightarrow \exists f [ A(x,f) \wedge f(y)=z \wedge \forall f' (A(x,f')\rightarrow f\triangleleft f' )]$ . To show that g is well-defined, we need to show that among the functions satisfying $A(x,f)$ there indeed one which is $\triangleleft $ -least among them. Consider the set $X =\lbrace \langle y,z \rangle : \exists f_1 \exists f_2 [A(x,f_1) \wedge A(x,f_2) \wedge f_1(y)=z < f_2(y) \wedge \forall w<y f_1(w)=f_2(w) \rbrace $ . In other words, $\langle y,z\rangle $ is the argument-value pair that witnesses $f_1\triangleleft f_2$ . Now if there were no $\triangleleft $ -least function satisfying A, then (using QF-DC) the lexicographic ordering of X would not be well-founded, which is impossible.

Finally, the axioms of $HA$ —which are, of course, the same as the axioms of $PA$ —will be equivalent to their $\mathsf {B}$ translations by stability. Putting all this together, we have the main theorem:

Theorem 8.21. $MC_{LS}$ interprets the theory $LS$ under the translation $\mathsf {B}$ .

Obviously, this interpretation is not faithful. That is, there are non-theorems of $LS$ whose $\mathsf {B}$ translations will be theorems of $MC_{LS}$ . Indeed, there will be non-theorems A of $EL_1$ such that $MC_{LS}\vdash A^{\mathsf {B}}$ . This is a consequence of the fact that the arithmetic portion of $MC_{LS}$ is both classical and equivalent to its $\mathsf {B}$ -translation.

The fact that $EL_1^{\mathsf {B}}$ is equivalent in $MC_{LS}$ to the result of erasing all modal operators is the reason we have had to include such strong choice principles and the full schema of induction. AC-NF being an axiom of $EL_1$ requires that AC-NF $^{\mathsf {B}}$ , and hence AC-NF itself, be a theorem of $MC_{LS}$ . Likewise, since $EL_1$ includes every instance of the schema of induction, $MC_{LS}$ also needs to include every instance in order to interpret $EL_1$ via $\mathsf {B}$ .

On the other hand, the interpretation of $LS1$ – $LS3$ required no essential use of induction and only $\Delta ^0_1$ -AC. (In inferring that various formulas were quasi-treelike, I often implicitly assumed that function-existence was closed under recursive operations.) On the other hand, as I observed above, the interpretation of $LS4$ seems to require the full axiom of choice. Given that $LS4$ requires the existence of a sufficiently inclusive class of neighborhood functions, it is perhaps not surprising that this requires a commitment to strong function existence principles. With the exception of assuming that there are enough classical functions, however, the principles about choice sequences per se require very little mathematical strength. They are all provable on the basis of our philosophically well-motivated axioms S1–S9. And as we will see in the next section, these axioms have very little mathematical strength on their own.

9 $MC_{LS}$ and classical theories

In this section I study the relation between the modal three-sorted theory $MC_{LS}$ and the standard non-modal two-sorted theories of second-order arithmetic. Given a familiar theory Z of second-order arithmetic, let $MC_{LS}(Z)$ be the theory like $MC_{LS}$ except that the arithmetical axioms are those of Z. For instance, $MC_{LS}(RCA_0)$ is the theory consisting of axioms A0–A9, and the induction schema restricted to $\Sigma ^0_1$ formulas, AC restricted to $\Delta ^0_1$ formulas, arithmetic stability axioms, and the axioms S1–S9. Then the main result of this section will be that if Z is any subsystem of second-order arithmetic extending $RCA_0$ , then $MC_{LS}(Z)$ is conservative over Z. (The choice of $RCA_0$ is so that the basic coding of finite sequences and so forth is possible, as this is necessary for the meaningfulness of several of the sequence axioms.)

To prove this, I will show how, given a countable model M of Z, we can define a partial order $\mathbb {P}$ that can serve as a Kripke model for $MC_{LS}$ . The key to this result is providing a non-standard interpretation of $\mathcal {I}$ in $\mathbb {P}$ .Footnote ¹⁸ To distinguish this non-standard interpretation of the modal vocabulary from the standard, intended interpretation given in Section 4, I will use the expression “forcing” and the symbol $\Vdash $ to refer to the interpretation in $\mathbb {P}$ .Footnote ¹⁹ Then I will show that (1) all arithmetic formulas that are true in M are forced at every $w\in \mathbb {P}$ , (2) all the axioms of $MC_{LS}(Z)$ are also forced at every $w\in \mathbb {P}$ , and (3) that forcing is closed under $\mathbf {S4}_{\mathcal {I}}$ deducibility. Conservativity follows from these three facts.

Let M be a countable model of some subsystem of second-order arithmetic Z extending $RCA_0$ . $|M|$ will denote the first-order domain of Z, and $S_M$ its second-order domain, that is, the functions of M. Let $\langle w_k'\rangle _{k\in \mathbb {N}}$ be an enumeration of the functions that map natural numbers to $Seq^M$ and that are non-zero on a finite set. (Recall that 0 codes the empty sequence $\langle \rangle $ .) Further, let $w_0'$ be the constant 0 function. Let $\langle n_k\rangle _{k\in \mathbb {N}}$ be an enumeration of $Seq^M$ . Since M is countable, both of these enumerations will exist, though not necessarily in M. Now define a new enumeration $\langle w_k\rangle _{k\in \mathbb {N}}$ of functions as follows: $w_0=w_0'$ , and for $k>0$ , if $i_1,\dots ,i_k$ are the least arguments on which $w_k'$ is 0, put $w_k(i_j)=n_j$ for $1\leq j\leq k$ and otherwise let $w_k(x)=w_k'(x)$ .

Let $\mathbb {P}_M$ be the set of functions $w_k$ , and define the relation $w \sqsubseteq u$ to mean that whenever $w(i)=n>0$ we have $u(i)=m$ , for some $m \succeq n$ . Clearly $(\mathbb {P}_M,\sqsubseteq )$ is a partial order with least element the constant zero function $w_0$ . In general I will omit the subscript and just write $\mathbb {P}$ .

Also, define a variable assignment to be a function from choice sequence variables to natural numbers. I will use $\sigma $ , possibly subscripted, to denote a variable assignment; $\sigma [\alpha \mapsto i]$ will denote the variable assignment that agrees with $\sigma $ except possibly on $\alpha $ , which $\sigma $ maps to i. Since the functions $w$ serve as the worlds in our Kripke model, the idea is that, when $\sigma (\alpha )=i$ , $w(i)$ is interpreted as the initial segment of $\alpha $ .

Recall the definition of the $\alpha ,n$ replacement $\mathcal{R}(P,\alpha ,n)$ from Definition 8.11. In particular, note that if $\vec {\alpha }$ are all the choice sequence variables occurring in P, then $\mathcal{R}(P,\vec {\alpha },\vec {n})$ is arithmetic, and if P has no instances of choice sequence variables, then $\mathcal{R}(P,\alpha ,n)$ is just P.

For the interpretation of $\mathcal {I}$ , we will need to define two new notions: the function $w[f_i(x_i)]_I$ , and an $[f_i]_I$ -chain. This can be pronounced “f-I-chain.”

It is not difficult to see that f-I-chains exist:

Now we can define the forcing relation that will provide an interpretation of $MC_{LS}(Z)$ . I will assume that the background metatheory has a name for every $x\in |M|$ and $f\in S_M$ .

The intuitive idea behind the clause for $\mathcal {I}$ is that, fixing some $f_i$ ’s, the extensions $ w[f_i(x_i)]_I$ of $w$ trace out a possible future history of how the choice sequences assigned to members of I evolve. Considering all index sets I that include at least the free variables of A is a way of saying that this happens for every possible future history, which is the intended meaning of $\mathcal {I}$ . The extra complications involving the chain C come from the fact that the function $ w[f_i(x_i)]_I$ may not be in $\mathbb {P}$ . An $[f_i]_I$ -chain is a way of approximating the path of extensions $ w[f_i(x_i)]_I$ within $\mathbb {P}$ .

Note that a formula $w,\sigma \Vdash A$ may have free variables; in fact, the free variables of this formula will be w, $\sigma $ , and the free number and classical function variables of A.

As usual, we can say that $w\Vdash A$ when $w,\sigma \Vdash A$ for all $\sigma $ . And it is easy to see that if A is a sentence, then $w, \sigma \Vdash A$ for some $\sigma $ iff $w, \sigma \Vdash A$ for all $\sigma $ .

As an exercise in applying definitions, one can verify the following simple facts:

It is also easy to see that the forcing definition coincides with truth in M for arithmetical formulas:

Next, we want to observe that the axioms of $MC_{LS}$ are forced.

This proof just consists in checking each axiom. The details are in Appendix C. Then, by checking that each axiom of $\mathbf {S4}_{\mathcal {I}}$ is forced everywhere, and that the inference rules of $\mathbf {S4}_{\mathcal {I}}$ preserve the property of being forced everywhere, we can establish:

The proof, again, is in Appendix C. In summary, the theorems of this section entail our conservativity result.