Equality and Equivalence, Intuitionistically

Abstract

We show that the intuitionistic first-order theory of equality has continuum many complete extensions. We also study the Vitali equivalence relation and show there are many intuitionistically precise versions of it.

For Mohammad Ardeshir

Solem enim e mundo tollere videntur qui amicitiam e vita tollunt.

They take away the sun from the world, surely, those who take away friendship from life.

Cicero, de Amicitia, XIII 47

1.1 Introduction

We want to contribute to L. E. J. Brouwer’s program of doing mathematics intuitionistically.

We follow his advice to interpret the logical constants constructively.

A conjunction $A\;\wedge \;B$ is considered proven if and only if one has a proof of A and also a proof of B.

A disjunction $A\vee B$ is considered proven if and only if either A or B is proven.

An implication $A\rightarrow B$ is considered proven if and only if there is a proof of B using the assumption A.

A negation $\lnot A$ is considered proven if and only if there is a proof of $A\rightarrow 0=1$.

An existential statement $\exists x \in V[P(x)]$ is considered proven if and only an element $x_0$ is produced together with a proof of the associated statement $P(x_0)$.

A universal statement $\forall x\in V[P(x)]$ is considered proven if and only if a method is given that produces, given any x in V, a proof of the associated statement P(x).

We also use some axioms proposed by Brouwer: his Continuity Principle, our Axiom 1, a slightly stronger version of it, the First Axiom of Continuous Choice, our Axiom 2, and his Thesis on Bars in $\mathcal {N}$, our Axiom 4.

In some of our proofs, we use an Axiom of Countable Choice, our Axiom 3. Intuitionistic mathematicians, who accept infinite step-by-step constructions not determined by a rule, consider this axiom a reasonable proposal.

Finally, we believe that generalized inductive definitions, like our Definition 25, fall within the compass of intuitionistic mathematics.

Our subject is the (intuitionistic) first-order theory of equality. By considering structures $(\mathcal {X}, =)$ where $\mathcal {X}$ is a subset of Baire space $\mathcal {N}=\omega ^\omega$ and $=$ the usual equality relation on $\mathcal {N}$, we find that the theory has an uncountable and therefore astonishing¹ variety of elementarily different infinite models and, as a consequence, an astonishing variety of complete extensions, see Theorem 15. The key observation²  leading to this result is the recognition that, in a spread,³ an isolated point is the same as a decidable point.⁴ It follows that the set of the non-isolated points of a spread is a definable subset of the spread. In spreads that are transparent,⁵ the set of the non-isolated points of the spread coincides with the coherence of the spread,⁶ and the coherence itself is spread. It may happen that the coherence of a transparent spread is transparent itself and then the coherence of the coherence also is a definable subset of the spread. And so on.

Any structure $(\mathcal {N}, R)$, where R is an equivalence relation on $\mathcal {N}$, is a model of the theory of equality. We study the Vitali equivalence relation, see Sect. 1.9, as an example. This equivalence relation, in contrast to the equality relation on $\mathcal {N}$, is not stable,⁷ see Theorem 16.

There is a host of binary relations on $\mathcal {N}$ that, from a classical point of view, all would be the same as the Vitali equivalence relation, see Sects. 1.10 and 1.11, and especially Definition 25, Corollary 3 and Definition 28. It turned out to be difficult to find differences between them that are first-order expressible. We did find some such differences, however, by studying structures $(\mathcal {N}, =, R)$, where R is an intuitionistic version of the Vitali equivalence relation and $=$ the usual equality, see Sect. 1.12.

The paper is divided into 13 Sections and consists roughly of two parts. Sections 1.2, 1.3, 1.4, 1.5, 1.6, 1.7 and 1.8 lead up to the result that the theory of equality has continuum many complete extensions, see Theorem 15. Sections 1.9, 1.10, 1.11 and 1.12 treat the Vitali equivalence relations. Section 1.13 lists some notations and conventions and may be used by the reader as a reference.

1.2 Intuitionistic Model Theory

Given a relational structure $\mathfrak {A}=(A, R_0, R_1, \ldots , R_{n-1})$, we construct a first-order language $\mathcal {L}$ with basic formulas $\mathsf {R}_i(\mathsf {x}_0, \mathsf {x}_1,\ldots , \mathsf {x}_{l_i-1})$, where $i<n$ and $l_i$ is the arity of $R_i$. The formulas of $\mathcal {L}$ are obtained from the basic formulas by using $\wedge , \vee , \rightarrow , \lnot , \exists , \forall$ in the usual way.

For every formula $\varphi =\varphi (\mathsf {x}_0, \mathsf {x}_1, \ldots , \mathsf {x}_{m-1})$ of $\mathcal {L}$, for all $a_0, a_1, \ldots , a_{m-1}$ in A, we define the statement:

$$\mathfrak {A}\models \varphi [a_0, a_1, \ldots , a_{m-1}]$$

($\mathfrak {A}$ realizes $\varphi$ if $\mathsf {x}_0, \mathsf {x}_1, \ldots , \mathsf {x}_{m-1}$ are interpreted by $a_0, a_1, \ldots , a_{m-1}$, respectively), as Tarski did it, with the proviso that connectives and quantifiers are interpreted intuitionistically.

A formula $\varphi$ of $\mathcal {L}$ without free variables will be called a sentence.

A theory (in $\mathcal {L}$) is a set of sentences of $\mathcal {L}$.

Given a theory $\Gamma$ in $\mathcal {L}$ and a structure $\mathfrak {A}$, we define: $\mathfrak {A}$ realizes $\Gamma$ if and only if, for every $\varphi$ in $\Gamma$, $\mathfrak {A}\models \varphi$.

Given a structure $\mathfrak {B}$ that has the same signature as $\mathfrak {A}$, so that the formulas of $\mathcal {L}$ may be interpreted in $\mathfrak {B}$ as well as in $\mathfrak {A}$, we let $Th(\mathfrak {B})$, the theory of $\mathfrak {B}$, be the set of all sentences $\varphi$ of $\mathcal {L}$ such that $\mathfrak {B}\models \varphi$.

A theory $\Gamma$ in $\mathcal {L}$ will be called a complete theory if and only if there exists a structure $\mathfrak {B}$ such that $\Gamma =Th(\mathfrak {B})$.

This agrees with one of the uses of the expression ‘complete theory’ in classical, that is: usual, non-intuitionistic, model theory, see Hodges (1993, p. 43). Note that one may be unable to decide, for a given sentence $\varphi$ and a given structure $\mathfrak {B}$, whether or not $\mathfrak {B}\models \varphi$. Intuitionistically, it is not true that, for every complete theory $\Gamma$ and every sentence $\varphi$, either $\varphi \in \Gamma$ or $\lnot \varphi \in \Gamma$.

Complete theories $\Gamma , \Delta$ are positively different if one may point out a sentence $\psi$ such that $\psi \in \Gamma$ and $\lnot \psi \in \Delta$.⁸

Structures $\mathfrak {A}, \mathfrak {B}$ are elementarily equivalent if and only if $Th(\mathfrak {A})=Th(\mathfrak {B})$ and (positively) elementarily different if $Th(\mathfrak {A})$ is positively different from $Th(\mathfrak {B})$.

Let $\Gamma$ be a theory in $\mathcal {L}$. A good question is the following:

How many complete theories $\Delta$ can one find extending $\Gamma$?

We will say: $\Gamma$ admits countably many complete extensions if and only if there exists an infinite sequence $\Delta _0, \Delta _1, \ldots$ of complete theories extending $\Gamma$ such that, for all m, n, if $m\ne n$, then $\Delta _m,\Delta _n$ are (positively) different, and

$\Gamma$ admits continuum many complete extensions if and only if there exists a function $\alpha \mapsto \Delta _\alpha$ associating to every element $\alpha$ of $\mathcal {C}=2^\omega$ a complete theory extending $\Gamma$ such that for all $\alpha , \beta$, if⁹ $\alpha \;\#\;\beta$, then $\Delta _\alpha ,\Delta _\beta$ are (positively) different.

A main result of this paper is that the first-order theory of equality admits continuum many complete extensions.

1.3 Equality May Be Undecidable

The first-order theory EQ of equality consists of the following three axioms:

• 1. $\mathsf {\forall x[x=x]}$,

• 2. $\mathsf {\forall x\forall y[x=y\rightarrow y=x]}$ and

• 3. $\mathsf {\forall x\forall y\forall z[(x=y\;\wedge \;y=z)\rightarrow x=z]}$.

A model of EQ is a structure of the form (V, R), where V is a set and R is an equivalence relation on V, possibly, but not necessarily, the equality relation belonging to V.

Classically, every complete extension of EQ is realized in one of the structures from the list: $(\{0\},=)$, $(\{0,1\},=)$, $(\{0,1,2\},=)$, $\dots$ and $(\omega ,=)$. This shows that, classically, EQ admits of (no more than) countably many complete extensions.

Intuitionistically, however, we have to observe that all structures on this list satisfy the sentence

$\mathsf {\forall x\forall y[x=y\;\vee \;\lnot (x=y)]}$,

that is: the equality relation, on each of these sets, is a decidable relation.

Turning to the set $\mathcal {N}$, we note that, if we define an element $\alpha$ of $\mathcal {N}$ by stipulating:

$$\forall n[\alpha (n)\ne 0\leftrightarrow \forall i<99[d(n+i)=9]],$$

where $d:\mathbb {N}\rightarrow \{0,1,\ldots ,9\}$ is the decimal expansion of $\pi$, then, at this moment, we have no proof of:

$\alpha =\underline{0}\;\vee \lnot (\alpha =\underline{0})$.

This is because, if $\alpha =\underline{0}$, then $\lnot \exists n\forall i<99[\alpha (n+i)=9]$, and, if $\lnot (\alpha =\underline{0})$, then $\lnot \lnot \exists n\forall i<99[d(n+i)=9]$, and we have no proof of either alternative.

This example shows us that the statement $\forall \alpha [\alpha =\underline{0}\;\vee \;\lnot (\alpha =\underline{0})]$, for a constructive mathematician, who interprets the disjunction strongly, is a reckless statement.¹⁰

The following axiom, used by Brouwer,¹¹ implies that the statement

$\forall \alpha [\alpha =\underline{0}\;\vee \;\lnot (\alpha =\underline{0})]$ even leads to a contradiction.

Axiom 1

(Brouwer’s Continuity Principle)

For all $R\subseteq \mathcal {N}\times \omega$, if $\forall \alpha \exists n[\alpha Rn]$, then $\forall \alpha \exists m \exists n\forall \beta [\overline{\alpha }m \sqsubset \beta \rightarrow \beta Rn]$.

An immediate consequence is:

Lemma 1

(Brouwer’s Continuity Principle, the case of disjunction)

For all $P_0, P_1\subseteq \mathcal {N}$, if $\forall \alpha [\alpha \in P_0\;\vee \;\alpha \in P_1]$, then

$\forall \alpha \exists m[\forall \beta [\overline{\alpha }m\sqsubset \beta \rightarrow \beta \in P_0]\;\vee \; \forall \beta [\overline{\alpha }m\sqsubset \beta \rightarrow \beta \in P_1]]$.

Proof

Define $R:=\{(\alpha , n)\mid n<2\;\wedge \;\alpha \in P_n\}$ and apply Axiom 1.$\square$

Theorem 1

• (i) $(\mathcal {N}, =)\models \mathsf {\forall x\lnot \forall y[x=y\;\vee \;\lnot (x=y)]}$.

• (ii) $(\mathcal {N}, =)\models \mathsf {\lnot \forall x\forall y[x=y\;\vee \;\lnot (x=y)]}$.

Proof

• (i) Let $\alpha$ be given and assume: $\forall \beta [\alpha =\beta \;\vee \;\lnot (\alpha =\beta )]$.

  Using Lemma 1, find m such that

  either $\forall \beta [\overline{\alpha }m\sqsubset \beta \rightarrow \alpha = \beta ]$ or $\forall \beta [\overline{\alpha }m\sqsubset \beta \rightarrow \lnot (\alpha = \beta )]$.

  Consider $\beta :=\overline{\alpha }m*\langle \alpha (m)+1\rangle *\underline{0}$ (for the first alternative) and $\beta :=\alpha$ (for the second one) and conclude that both alternatives are false.

• (ii) This is an immediate consequence of (i).

$\square$

Definition 1

For each n, we let $\psi _n$ be the sentence

$\mathsf {\exists x_0\exists x_1\ldots \exists x_n}[\bigwedge _{i<j<n}\lnot (\mathsf {x}_i=\mathsf {x}_j)]$.

$T_{inf}:=EQ\cup \{\psi _n\mid n\in \omega \}$.

$\psi _n$ expresses that a set has at least $n+1$ elements.

Note that, in classical mathematics, $T_{inf}$ has only one complete extension.

Intuitionistically, however, $T_{inf}$ has (at least) two positively different complete extensions, $Th\bigl ((\mathcal {N},=)\bigr )$ and $Th\bigl ((\omega , =)\bigr )$.

The next Theorem reflects the fact that, in classical model theory, all models of $T_{inf}$ are elementarily equivalent.

Theorem 2

The theory $T_{inf}\cup \{\forall \mathsf {x\forall y[x=y\;\vee \;\lnot (x=y)]}\}$ has only one complete extension.

Proof

For each n, consider the first n variables of our language: $\mathsf {x}_0, \mathsf {x}_1, \ldots ,\mathsf {x}_{n-1}$. A formula $\varepsilon =\varepsilon (\mathsf {x}_0, \mathsf {x}_1, \ldots ,\mathsf {x}_{n-1})$ is called an equality type if and only if it is of the form $\bigwedge _{i<j<n} \sigma _{ij}$ where each $\sigma _{ij}$ either is the formula $\mathsf {x}_i=\mathsf {x}_j$ or the formula $\lnot (\mathsf {x}_i=\mathsf {x}_j)$.¹² One may prove: for all structures $(V_0, R_0), (V_1, R_1)$, both realizing $T_{inf}\cup \{\forall \mathsf {x\forall y[x=y\;\vee \;\lnot (x=y)]}\}$, for each formula $\varphi =\varphi (\mathsf {x}_0, \mathsf {x}_1, \ldots ,\mathsf {x}_{n-1})$, for each equality type $\varepsilon =\varepsilon (\mathsf {x}_0, \mathsf {x}_1, \ldots ,\mathsf {x}_{n-1})$, $(V_0, R_0)\models \forall \mathsf {x}_0\forall \mathsf {x}_1 \ldots \forall \mathsf {x}_{n-1}[\varepsilon \rightarrow \varphi ]$ if and only if $(V_1, R_1)\models \forall \mathsf {x}_0\forall \mathsf {x}_1 \ldots \forall \mathsf {x}_{n-1}[\varepsilon \rightarrow \varphi ]$. The proof is by induction on the complexity of the formula $\varphi$.

It follows that any two models $(V_0, R_0), (V_1, R_1)$, both realizing

$T_{inf}\cup \{\forall \mathsf {x\forall y[x=y\;\vee \;\lnot (x=y)]}\}$, are elementarily equivalent.$\square$

From here on, we restrict attention to infinite models of EQ, that is, to models of $T_{inf}$. The hackneyed question to make a survey of models that are finite, or at least not infinite, and of models for which one can not decide if they are finite or infinite, is left for another occasion. That the job is not an easy one will be clear to readers of Veldman (1995).

1.4 Spreads

Definition 2

Let $\beta$ be given. $\beta$ is called a spread-law, $Spr(\beta )$, if and only if $\forall s[\beta (s)=0\leftrightarrow \exists n[\beta (s*\langle n \rangle )=0]]$.

For every $\beta$, we define: $\mathcal {F}_\beta :=\{\alpha \mid \forall n[\beta (\overline{\alpha }n)=0]\}$.

$\mathcal {X}\subseteq \mathcal {N}$ is closed if and only if $\exists \beta [\mathcal {X}=\mathcal {F}_\beta ]$.

$\mathcal {X}\subseteq \mathcal {N}$ is a spread if and only if $\exists \beta [Spr(\beta )\;\wedge \;\mathcal {X}=\mathcal {F}_\beta ]$.

If $Spr(\beta )$ and $\beta (\langle \;\rangle )\ne 0$, then $\mathcal {F}_\beta =\emptyset$.

If $Spr(\beta )$ and $\beta (\langle \;\rangle )=0$, then $\mathcal {F}_\beta$ is inhabited.¹³ One may define $\alpha$ such that

$\forall n[\alpha (n)=\mu p[\beta (\overline{\alpha }n*\langle p \rangle )=0]]$ and observe: $\forall n[\beta (\overline{\alpha }n)=0]$, that is: $\alpha \in \mathcal {F}_\beta$.

Is every closed set a spread?

Define $\beta$ such that $\forall s[\beta (s) =0\leftrightarrow \lnot \forall i<99[d(n+i)=9]],$ where

$d:\mathbb {N}\rightarrow \{0,1,\ldots , 9\}$ is the decimal expansion of $\pi$.

If $\mathcal {F}_\beta$ is a spread, that is $\exists \gamma [Spr(\gamma )\;\wedge \;\mathcal {F}_\gamma =\mathcal {F}_\beta ]$, then either $\mathcal {F}_\beta$ is inhabited and $\lnot \exists s\forall i<99[d(s+i)=9]$ or $\mathcal {F}_\beta = \emptyset$ and $\lnot \lnot \exists s\forall i<99[d(s+i)=9]$.

For this $\beta$, the statement ‘$\mathcal {F}_\beta$ is a spread’ thus turns out to be reckless.

Brouwer’s Continuity Principle enables one to obtain a stronger conclusion.

Theorem 3

$\lnot \forall \beta \exists \gamma [Spr(\gamma )\;\wedge \;\mathcal {F}_\gamma =\mathcal {F}_\beta ]$.

Proof

Assume: $\forall \beta \exists \gamma [Spr(\gamma )\,\wedge \,\mathcal {F}_\gamma {=}\mathcal {F}_\beta ]$.

Then $\forall \beta [\exists \alpha [\alpha \in \mathcal {F}_\beta ]\,\vee \,\lnot \exists \alpha [\alpha \in \mathcal {F}_\beta ]]$. Using Lemma 1, find m such that either $\forall \beta [\overline{\underline{0}}m\sqsubset \beta \rightarrow \exists \alpha [\alpha \in \mathcal {F}_\beta ]]$ or $\forall \beta [\overline{\underline{0}}m\sqsubset \beta \rightarrow \lnot \exists \alpha [\alpha \in \mathcal {F}_\beta ]]$.

Both alternatives are false, as we see by considering $\beta = \underline{\overline{0}}m*\underline{1}$ (for the first alternative), and $\beta =\underline{0}$ (for the second one).$\square$

Lemma 2

(Brouwer’s Continuity Principle extends to spreads)

Let $\beta$ be given such that $Spr(\beta )$. Then, for all $R\subseteq \mathcal {N}\times \omega$,

if $\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha Rn]$, then $\forall \alpha \in \mathcal {F}_\beta \exists m \exists n\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m \sqsubset \gamma \rightarrow \gamma Rn]$.

Proof

Assume: $Spr(\beta )$. If $\beta (\langle \;\rangle )\ne 0$, then $\mathcal {F}_\beta =\emptyset$ and there is nothing to prove.

Assume $\beta (\langle \;\rangle )=0$. Define $\sigma$ such that $\sigma (\langle \;\rangle )=\langle \;\rangle$ and, for all s, for all n,

• 1. if $\beta (s*\langle n\rangle )=0$, then $\sigma (s*\langle n\rangle )=s*\langle n\rangle$, and,

• 2. if $\beta (s*\langle n \rangle )\ne 0$, then $\sigma (s*\langle n \rangle )=\sigma (s)*\langle \mu p[\beta \bigl (\sigma (s)*\langle p\rangle \bigr )=0]\rangle$.

Note: $\forall s[\beta \bigl (\sigma (s)\bigr )=0]$ and $\forall s\forall t[s\sqsubset t\rightarrow \sigma (s)\sqsubset \sigma (t)]$.

Define $\rho :\mathcal {N}\rightarrow \mathcal {N}$ such that $\forall \alpha \forall n[ \sigma (\overline{\alpha }n)\sqsubset \rho |\alpha ]$.

Note: $\forall \alpha [\rho |\alpha \in \mathcal {F}_\beta ]\;\wedge \; \forall \alpha \in \mathcal {F}_\beta [\rho |\alpha =\alpha ]$.

The function $\rho$ is called a retraction of $\mathcal {N}$ onto $\mathcal {F}_\beta$.

Now assume: $\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha Rn]$. Conclude: $\forall \alpha \exists n[(\rho |\alpha )R n]$.

Let $\alpha$ in $\mathcal {F}_\beta$ be given. Using Axiom 1, find m, n such that

$\forall \gamma [\overline{\alpha }m\sqsubset \gamma \rightarrow (\rho |\gamma )Rn]$. Conclude: $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \gamma R n]$.

We thus see: $\forall \alpha \in \mathcal {F}_\beta \exists m\exists n\forall \gamma \in \mathcal {F}_\beta [\overline{\gamma }m\sqsubset \alpha \rightarrow \gamma Rn]$.$\square$

Recall that, for all $\alpha , \beta$, $\alpha \;\#\;\beta \leftrightarrow \alpha \perp \beta \leftrightarrow \exists n[\alpha (n)\ne \beta (n)],$ and

$\alpha =\beta \leftrightarrow \forall n[\alpha (n)=\beta (n)]\leftrightarrow \lnot (\alpha \;\#\;\beta )$, and $\alpha \ne \beta \leftrightarrow \lnot \forall n[\alpha (n)=\beta (n)].$

The constructive apartness relation $\#$ is more useful than the negative inequality relation $\ne$.

Markov’s Principle, in the form: $\forall \alpha [\lnot \lnot \exists n[\alpha (n)=0]\rightarrow \exists n[\alpha (n)=0]]$,¹⁴ is equivalent to the statement that the two relations coincide: $\forall \alpha \forall \beta [\alpha \ne \beta \rightarrow \alpha \;\#\;\beta ]$.

The intuitionistic mathematician does not accept Markov’s Principle.

Definition 3

We let $AP=AP(\mathsf {x,y})$ be the formula $\mathsf {\forall z[ \lnot (z=x)\;\vee \;\lnot (z=y)]}$.

The following theorem reformulates a well-known fact.

Theorem 4

(Apartness is definable) For all $\beta$ such that $Spr(\beta )$,

for all $\alpha , \delta$ in $\mathcal {F}_\beta$, $\alpha \;\#\;\delta$ if and only if $(\mathcal {F}_\beta ,=)\models AP[\alpha , \delta ]$.

Proof

First, assume $\alpha \;\#\;\delta$. Find n such that $\overline{\alpha }n \ne \overline{\delta }n$. Note: for every $\gamma$ in $\mathcal {F}_\beta$, either: $\overline{\gamma }n \ne \overline{\alpha }n$ and $\gamma \;\#\;\alpha$, or: $\overline{\gamma }n\ne \delta n$ and $\gamma \;\#\;\delta$. Conclude: $(\mathcal {F}_\beta ,=)\models AP[\alpha , \delta ]$.

Next, assume $(\mathcal {F}_\beta ,=)\models AP[\alpha , \delta ]$, that is $\forall \gamma \in \mathcal {F}_\beta [\gamma \ne \alpha \;\vee \;\gamma \ne \delta ]$.

Applying Lemma 2, find m such that either $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \gamma \ne \alpha ]$ or $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \gamma \ne \delta ]$. The first alternative is clearly wrong (take $\gamma :=\alpha$). The second alternative implies: $\overline{\alpha }m \perp \delta$ (if $\overline{\alpha }m \sqsubset \delta$, one could take $\gamma :=\delta$), and thus: $\alpha \;\#\;\delta$.$\square$

Definition 4

For each n, we let $\psi _n^+$ be the sentence $\mathsf {\exists x_0\exists x_1\ldots \exists x_n}[\bigwedge _{i<j<n}AP(\mathsf {x}_i,\mathsf {x}_j)]$.

$T_{inf}^+:=EQ\cup \{\psi _n^+\mid n\in \omega \}$.

$\psi _n^+$ expresses that a set has at least $n+1$ elements that are mutually apart.

Every model of $T^+_{inf}$ realizes $T_{inf}$. In the second part of the paper we will meet a structure that realizes $T_{inf}$ but not $T^+_{inf}$, see Theorem 17 in Sect. 1.9.

The theory $T^+_{inf}\cup \{\forall \mathsf {x\forall y[x=y\;\vee \;\lnot (x=y)]}\}$ has only one complete extension, the same as the one and only complete extension of $T_{inf}\cup \{\forall \mathsf {x\forall y[x=y\;\vee \;\lnot (x=y)]}\}$, see Theorem 2.

1.5 Spreads with a Decidable Equality

Definition 5

We let $D=D(\mathsf {x})$ be the formula: $\mathsf {\forall y[x=y\;\vee \;\lnot (x=y)]}$.

Definition 6

Assume $Spr(\beta )$ and $\alpha \in \mathcal {F}_\beta$.

$\alpha$ is an isolated point of $\mathcal {F}_\beta$ if and only if $\exists n\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }n \sqsubset \gamma \rightarrow \alpha = \gamma ]$, or, equivalently, $\exists n\forall s[\bigl (\overline{\alpha }n\sqsubset s\;\wedge \;\beta (s)=0\bigr )\rightarrow s\sqsubset \alpha ]$.

$\alpha$ is a decidable point of $\mathcal {F}_\beta$ if and only if $\forall \gamma \in \mathcal {F}_\beta [\alpha =\gamma \;\vee \;\lnot (\alpha =\gamma )]$, or, equivalently, $(\mathcal {F}_\beta ,=)\models D[\alpha ]$.

$\mathcal {I}(\mathcal {F}_\beta )$ is the set of the isolated points of $\mathcal {F}_\beta$.

Cantor called $\mathcal {I}(\mathcal {F}_\beta )$ the adherence of $\mathcal {F}_\beta$.

Lemma 3

Assume $Spr(\beta )$.

• (i) For each $\alpha$ in $\mathcal {F}_\beta$, $\alpha$ is an isolated point of $\mathcal {F}_\beta$ if and only if $\alpha$ is a decidable point of $\mathcal {F}_\beta$.

• (ii) $\mathcal {I}(\mathcal {F}_\beta )$ is a definable subset of $\mathcal {F}_\beta$.

Proof

• (i) Let $\alpha$ be an isolated point of $\mathcal {F}_\beta$.

  Find n such that $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }n \sqsubset \gamma \rightarrow \alpha = \gamma ]$.

  Note: for each $\gamma$ in $\mathcal {F}_\beta$, either $\overline{\alpha }n\sqsubset \gamma$ and $\alpha =\gamma$, or $\overline{\alpha }n\perp \gamma$ and $\alpha \ne \gamma$.

  Conclude: $\forall \gamma \in \mathcal {F}_\beta [\alpha =\gamma \;\vee \;\lnot (\alpha =\gamma )]$, that is: $\alpha$ is a decidable point of $\mathcal {F}_\beta$.

  Now assume: $\alpha$ is a decidable point of $\mathcal {F}_\beta$, that is:

  $\forall \gamma \in \mathcal {F}_\beta [\alpha =\gamma \;\vee \;\lnot (\alpha =\gamma )]$.

  Apply Lemma 2 and find m such that either $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \alpha =\gamma ]$ or $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \lnot ( \alpha =\gamma )]$. As the second alternative does not hold (take $\gamma =\alpha$), conclude: $\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }m\sqsubset \gamma \rightarrow \alpha =\gamma ]$, and: $\alpha$ is an isolated point of $\mathcal {F}_\beta$.

• (ii) Using (i), note: $\mathcal {I}(\mathcal {F}_\beta ) =\{\alpha \in \mathcal {F}_\beta \mid (\mathcal {F}_\beta , =)\models D[\alpha ]\}$.

$\square$

Definition 7

Assume $Spr(\beta )$ and $\alpha \in \mathcal {F}_\beta$.

$\alpha$ is a limit point of $\mathcal {F}_\beta$ if and only if $\forall n\exists \delta \in \mathcal {F}_\beta [ \overline{\alpha }n\sqsubset \delta \;\wedge \;\alpha \perp \delta ]$, or, equivalently, $\forall n\exists s[\overline{\alpha }n \sqsubset s\;\wedge \; \beta (s) =0\;\wedge \;\alpha \perp s]$.

$\mathcal {L}(\mathcal {F}_\beta )$ is the set of the limit points of $\mathcal {F}_\beta$.

Cantor called $\mathcal {L}(\mathcal {F}_\beta )$ the coherence of $\mathcal {F}_\beta$.

Lemma 4

$\forall \beta [Spr(\beta )\rightarrow \mathcal {L}(\mathcal {F}_\beta )\subseteq \mathcal {F}_\beta \setminus \mathcal {I}(\mathcal {F}_\beta ) ]$, that is:

in all spreads, every limit point is a non-isolated point.

Proof

Obvious.$\square$

Theorem 5

The following are equivalent:

• (i) Markov’s Principle: $\forall \alpha [\lnot \lnot \exists n[\alpha (n)=0]\rightarrow \exists n[\alpha (n)=0]]$.

• (ii) $\forall \beta [Spr(\beta )\rightarrow \mathcal {F}_\beta \setminus \mathcal {I}(\mathcal {F}_\beta )\subseteq \mathcal {L}(\mathcal {F}_\beta )]$, that is: in all spreads, every non-isolated point is a limit point.

Proof

(i) $\Rightarrow$ (ii). Let $\beta$ be given such that $Spr(\beta )$. Assume $\alpha$ is not an isolated point of $\mathcal {F}_\beta$, that is: $\lnot \exists n\forall s[\bigl (\overline{\alpha }n\sqsubset s\;\wedge \;\beta (s)=0\bigr )\rightarrow s\sqsubset \alpha ]$.

Let n be given.

Define $\delta$ such that $\forall s[\delta (s)=0 \leftrightarrow (\overline{\alpha }n\sqsubset s\;\wedge \;\beta (s) =0 \;\wedge \; s\perp \alpha )]$.

Then $\lnot \forall s[\delta (s)\ne 0]$ and: $\lnot \lnot \exists s[\delta (s)=0]$.

Using Markov’s Principle, we conclude: $\exists s[\delta (s)=0]$.

We thus see: $\forall n \exists s[\overline{\alpha }s\sqsubset s \;\wedge \;\beta (s)=0 \;\wedge \; s\perp \alpha ]$, and: $\alpha$ is a limit point of $\mathcal {F}_\beta$.

(ii) $\Rightarrow$ (i). Let us assume: $\forall \beta [Spr(\beta )\rightarrow \mathcal {F}_\beta \setminus \mathcal {I}(\mathcal {F}_\beta )\subseteq \mathcal {L}(\mathcal {F}_\beta )]$,

Let $\alpha$ be given such that $\lnot \lnot \exists n[\alpha (n)=0]$.

Define $\beta$ such that

$\forall s[\beta (s)=0\leftrightarrow \forall m<length(s)[s(m)\ne 0\rightarrow \exists n\le m[\alpha (n)=0]]]$.

Note: $Spr(\beta )$ and $\underline{0} \in \mathcal {F}_\beta$, and: if $\exists n[\alpha (n)=0]$, then $\underline{0}$ is a limit point of $\mathcal {F}_\beta$.

Conclude: if $\underline{0}$ is an isolated point of $\mathcal {F}_\beta$, then $\lnot \exists n[\alpha (n)=0]$.

As $\lnot \lnot \exists n[\alpha (n)=0]$, conclude: $\underline{0}$ is not an isolated point of $\mathcal {F}_\beta$.

By our assumption, $\underline{0}$ thus is a limit point of $\mathcal {F}_\beta$.

Find s such that $\beta (s)=0$ and $s \perp \underline{0}$. Conclude: $\exists n\le length(s)[\alpha (n)=0]$.

Conclude: $\forall \alpha [\lnot \lnot \exists n[\alpha (n)=0]\rightarrow \exists n[\alpha (n)=0]]$, that is: Markov’s Principle.$\square$

We thus see that the converse of Lemma 4, being equivalent to Markov’s Principle, is not an intuitionistic theorem.

We could not answer the question if, in general, $\mathcal {L}(\mathcal {F}_\beta )$ is a definable subset of $(\mathcal {F}_\beta , =)$. In some special cases, however, it is, and the following definition is useful.

Definition 8

Assume $Spr(\beta )$. $\mathcal {F}_\beta$ is called transparent if and only if there exists $\gamma$ such that $Spr(\gamma )$ and $\mathcal {F}_\gamma = \mathcal {L}(\mathcal {F}_\beta )$ and $\forall \alpha \in \mathcal {F}_\beta [\exists n[\gamma (\overline{\alpha }n)\ne 0]\rightarrow \alpha \in \mathcal {I}(\mathcal {F}_\beta )]$.

Note that, for each $\beta$ such that $Spr(\beta )$, if $\mathcal {F}_\beta$ is transparent, then

$\mathcal {F}_\beta \setminus \mathcal {I}(\mathcal {F}_\beta )\subseteq \mathcal {L}(\mathcal {F}_\beta )$. The statement that every spread $\mathcal {F}_\beta$ is transparent thus is seen to imply Markov’s Principle.

In Sect. 1.7 we will see many examples of transparent spreads.

The fact that not every spread is a transparent spread is one of the reasons that Brouwer did not succeed in finding a nice intuitionistic version of Cantor’s Main Theorem,¹⁵ see Brouwer (1919).

Definition 9

Let $\beta$ satisfy $Spr(\beta )$ and let $\varphi$ be given.

We define: $\varphi :\mathcal {F}_\beta \rightarrow \omega$ if and only if $\forall \alpha \in \mathcal {F}_\beta \exists p[\varphi (\overline{\alpha }p)\ne 0]$.

If $\varphi :\mathcal {F}_\beta \rightarrow \omega$, then we define, for each $\alpha$ in $\mathcal {F}_\beta$, $\varphi (\alpha )$ as the number z such that $\varphi (\overline{\alpha }q)=z+1$, where $q=\mu p[\varphi (\overline{\alpha }p)\ne 0]$.

We define: $\varphi$ is an injective map from $\mathcal {F}_\beta$ into $\omega$, notation: $\varphi :\mathcal {F}_\beta \hookrightarrow \omega$,

if and only if $\varphi :\mathcal {F}_\alpha \rightarrow \omega$ and $\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [\alpha \;\#\;\delta \rightarrow \varphi (\alpha )\ne \varphi (\delta )]$.

We define: $\varphi : \mathcal {F}_\beta \rightarrow \mathcal {N}$ if and only if $\forall n[\varphi ^n:\mathcal {F}_\beta \rightarrow \omega ]$.

If $\varphi :\mathcal {F}_\beta \rightarrow \mathcal {N}$, then we define, for each $\alpha$ in $\mathcal {F}_\beta$, $\varphi |\alpha$ as the element $\delta$ of $\mathcal {N}$ such that $\forall n[\delta (n)=\varphi ^n(\alpha )]$.

We define: $\varphi$ is an injective map from $\mathcal {F}_\beta$ into $\mathcal {N}$, notation: $\varphi :\mathcal {F}_\beta \hookrightarrow \mathcal {N}$,

if and only if $\varphi :\mathcal {F}_\alpha \rightarrow \mathcal {N}$ and $\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [\alpha \;\#\;\delta \rightarrow \varphi |\alpha \;\#\;\varphi |\delta ]$.

For every $\mathcal {X}\subseteq \mathcal {N}$, $\mathcal {F}_\beta$ embeds into $\mathcal {X}$ if and only if there exists an injective map from $\mathcal {F}_\beta$ into $\mathcal {X}$.

The following axiom is, at least at first sight, a little bit stronger than Brouwer’s Continuity Principle.

Axiom 2

(First Axiom of Continuous Choice) For all $R\subseteq \mathcal {N}\times \omega$,

if $\forall \alpha \exists n[\alpha Rn]$, then $\exists \varphi :\mathcal {N}\rightarrow \omega \forall \alpha [\alpha R\varphi (\alpha )]$.

Lemma 5

(The First Axiom of Continuous Choice extends to spreads) Let $\beta$ be given such that $Spr(\beta )$. Then, for all $R\subseteq \mathcal {F}_\beta \times \omega$,

if $\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha R n]$, then $\exists \varphi : \mathcal {F}_\beta \rightarrow \omega \forall \alpha \in \mathcal {F}_\beta [\alpha R\varphi (\alpha )]$.

Proof

Assume: $Spr(\beta )$ and $\beta (\langle \;\rangle )=0$. As in the proof of Lemma 2, define $\rho :\mathcal {N}\rightarrow \mathcal {F}_\beta$ such that $\forall \alpha [\rho |\alpha \in \mathcal {F}_\beta ]\;\wedge \; \forall \alpha \in \mathcal {F}_\beta [\rho |\alpha =\alpha ]$.

Now assume $\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha Rn]$. Conclude: $\forall \alpha \exists n[(\rho |\alpha )R n]$.

Applying Axiom 2, find $\varphi :\mathcal {N}\rightarrow \omega$ such that $\forall \gamma [ (\rho |\gamma )R\varphi (\gamma )]$.

Conclude: $\varphi :\mathcal {F}_\beta \rightarrow \omega$ and $\forall \gamma \in \mathcal {F}_\beta [\gamma R\varphi (\gamma )]$.$\square$

Theorem 6

Assume $Spr(\beta )$. $(\mathcal {F}_\beta ,=)\models \mathsf {\forall x}[D(\mathsf {x})]$ if and only if $\exists \varphi [\varphi :\mathcal {F}_\beta \hookrightarrow \omega ]$.

Proof

First assume: $(\mathcal {F}_\beta ,=)\models \mathsf {\forall x}[D(\mathsf {x})]$. Then, by Lemma 3,

$\forall \alpha \in \mathcal {F}_\beta \exists n\forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }n\sqsubset \gamma \rightarrow \alpha =\gamma ]$. Using Lemma 5, find $\varphi :\mathcal {F}_\beta \rightarrow \omega$ such that $\forall \alpha \in \mathcal {F}_\beta \forall \gamma \in \mathcal {F}_\beta [\overline{\alpha }\varphi (\alpha )\sqsubset \gamma \rightarrow \alpha =\gamma ]$. Define $\psi :\mathcal {F}_\beta \rightarrow \omega$ such that $\forall \alpha \in \mathcal {F}_\beta [\psi (\alpha )=\overline{\alpha }\varphi (\alpha )]$. Clearly, $\psi :\mathcal {F_\beta }\hookrightarrow \omega$.

Now assume: $\varphi :\mathcal {F}_\beta \hookrightarrow \omega$. Note: $\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [\alpha = \delta \leftrightarrow \varphi (\alpha )=\varphi (\delta )]$.

Also: $\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [\varphi (\alpha )=\varphi (\delta )\;\vee \;\lnot \bigl (\varphi (\alpha )=\varphi (\delta )\bigr )]$.

Therefore: $\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [\alpha = \delta \;\vee \; \lnot (\alpha =\delta )]$. Conclude: $(\mathcal {F}_\beta ,=)\models \mathsf {\forall x}[D(\mathsf {x})]$.$\square$

Definition 10

Assume $Spr(\beta )$. $\mathcal {F}_\beta$ is enumerable if and only if either $\mathcal {F}_\beta =\emptyset$ or $\exists \delta [\forall n[\delta ^n \in \mathcal {F}_\beta ]\;\wedge \;\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha =\delta ^n]]$.

Lemma 6

Assume $Spr(\beta )$. $\mathcal {F}_\beta$ is enumerable if and only if $\exists \varphi [\varphi :\mathcal {F}_\beta \hookrightarrow \omega ]$.

Proof

Assume $\mathcal {F}_\beta$ is enumerable and $\beta (\langle \;\rangle )=0$.

Find $\delta$ such that $\forall n[\delta ^n\in \mathcal {F}_\beta ]$ and $\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha =\delta ^n]$.

Using Lemma 5, find $\varphi :\mathcal {F}_\beta \rightarrow \omega$ such that $\forall \alpha \in \mathcal {F}_\beta [\alpha =\delta ^{\varphi (\alpha )}]$.

Note: $\varphi :\mathcal {F}_\beta \hookrightarrow \omega$.

Now assume: $\varphi :\mathcal {F}_\beta \hookrightarrow \omega$.

We make a preliminary observation.

Let s, n be given such that $\beta (s) =0$ and $\varphi (s)=n+1$ and $\forall t\sqsubset s[\varphi (t)=0]$.

Note: $\forall \alpha \in \mathcal {F}_\beta [s\sqsubset \alpha \rightarrow \varphi (\alpha )=n]$ and, therefore:

$\forall \alpha \in \mathcal {F}_\beta \forall \delta \in \mathcal {F}_\beta [(s\sqsubset \alpha \;\wedge \; s\sqsubset \delta )\rightarrow \alpha =\delta ]$.

Now let $\gamma$ be the element of $\mathcal {F}_\beta$ satisfying $\forall n[\gamma (n):=\mu p[\beta (\overline{\gamma }n*\langle p\rangle )=0]]$.

Define $\delta$ such that, for all s, if $\beta (s) =0$ and $\varphi (s)\ne 0$ and $\forall t\sqsubset s[\varphi (t)=0]$, then $s\sqsubset \delta ^s$ and $\delta ^s \in \mathcal {F}_\beta$, and if not, then $\delta ^s=\gamma$.

Note: $\forall s[\delta ^s \in \mathcal {F}_\beta ]$ and $\forall \alpha \in \mathcal {F}_\beta \exists s[\alpha =\delta ^s]$.$\square$

Corollary 1

Assume $Spr(\beta )$.

$(\mathcal {F}_\beta , =)\models \forall \mathsf {x}[D(\mathsf {x})]$ if and only if $\mathcal {F}_\beta$ is enumerable.

Proof

Use Theorem 6 and Lemma 6.$\square$

1.6 Spreads with Exactly One Undecidable Point

Definition 11

We let $\tau _2$ be the element of $\mathcal {C}$ satisfying: $\forall s[\tau _2(s)=0\leftrightarrow \forall i<length(s)[s(i)<2\;\wedge \; \bigl (i+1<length(s)\rightarrow s(i)\le s(i+1)\bigr )]]$. We define: $\mathcal {T}_2:=\mathcal {F}_{\tau _2}$.

Note: $\tau _2$ is a spread-law and $\mathcal {T}_2$ is a spread.

Let us take a closer look at $\mathcal {T}_2$.

Observe: $\forall \alpha [\alpha \in \mathcal {T}_2\leftrightarrow \forall i[\alpha (i)\le \alpha (i+1)<2]]$.

For each n, we define $n^*:= \underline{\overline{0}}n*\underline{1}$.

The infinite sequence $\underline{0}, 0^*, 1^*, 2^*, \ldots$ is a list of elements of $\mathcal {T}_2$ and a classical mathematician might think it is the list of all elements of $\mathcal {T}_2$. The intuitionistic mathematician knows better. He defines $\alpha$ in $\mathcal {T}_2$ such that

$$\forall n[\alpha (n) =1\leftrightarrow \exists k\le n\forall i<99[d(k+i)=9]],$$

where $d:\mathbb {N}\rightarrow \{0,1,\ldots ,9\}$ is the decimal expansion of $\pi$. As yet, one has no proof of the statement ‘$\alpha =\underline{0}$’, as this statement implies: $\forall k\exists i<99]d(k+i)=9]$. As yet, one also has no proof of the statement: ‘$\exists n[\alpha = n^*]$’ as this statement implies: $\exists n\forall i<99[d(n+i)=9]$. The statement that $\alpha$ occurs in the above list is a reckless one.

For each n, $n^*$ is an isolated and a decidable point of $\mathcal {T}_2$, and $\underline{0}$ is a non-isolated and an undecidable point of $\mathcal {T}_2$. It follows, by Lemma 3 and Corollary 1, that $\mathcal {T}_2$ is not an enumerable spread. In particular, the statement that the list $\underline{0}, 0^*, 1^*, 2^*, \ldots$ is a complete list of the elements of $\mathcal {T}_2$, leads to a contradiction, as appears again from the following Theorem.

Theorem 7

• (i) $\lnot \forall \alpha \in \mathcal {T}_2[\alpha =\underline{0}\;\vee \;\exists n[\alpha = n^*]]$.

• (ii) $\forall \alpha \in \mathcal {T}_2[\alpha \;\#\;\underline{0}\rightarrow \exists n[\alpha = n^*]]$.

Proof

• (i) Assume $\forall \alpha \in \mathcal {T}_2[\alpha =\underline{0}\;\vee \;\exists n[\alpha = n^*]]$. Using Lemma 2, find m, n such that either $\forall \alpha \in \mathcal {T}_2[\underline{\overline{0}}m\sqsubset \alpha \rightarrow \alpha =\underline{0}]$ or $\forall \alpha \in \mathcal {T}_2[\underline{\overline{0}}m\sqsubset \alpha \rightarrow \alpha =n^*]$. Note that both alternatives are false.

  Conclude: $\lnot \forall \alpha \in \mathcal {T}_2[\alpha =\underline{0}\;\vee \;\exists n[\alpha = n^*]]$.

• (ii) Let $\alpha$ in $\mathcal {T}_2$ be given such that $\alpha \;\#\;\underline{0}$. Define $n:=\mu m[\overline{\alpha }(m+1)\perp \underline{0}]$. Note: $\overline{\alpha }(n+1)=\overline{\underline{0}}n*\langle 1 \rangle$ and $\alpha =n^*$.

Definition 12

Assume $Spr(\beta )$. $\mathcal {F}_\beta$ is almost-enumerable if and only if either $\mathcal {F}_\beta =\emptyset$ or $\exists \delta [\forall n[\delta ^n\in \mathcal {F}_\beta ]\;\wedge \;\forall \alpha \in \mathcal {F}_\beta \forall \varepsilon \exists n[\overline{\alpha }\varepsilon (n) = \overline{\delta ^n}\varepsilon (n)]]$.

This definition deserves some explanation. If $\mathcal {F}_\beta$ is almost-enumerable and inhabited, we are able to come forward with an infinite sequence $\delta ^0, \delta ^1, \ldots$ of elements of $\mathcal {F}_\beta$ such that, for every $\alpha$ in $\mathcal {F}_\beta$, every attempt $\varepsilon$ to prove that $\alpha$ is apart from all elements of the infinite sequence $\delta ^0, \delta ^1, \ldots$, ($\varepsilon$ expresses the guess: $\forall n[\overline{\alpha }\varepsilon (n)\perp \overline{\delta ^n}\varepsilon (n)]$), will positively fail.

Almost-enumerable spreads are studied in Veldman (2018, Sect. 9), where they are called almost-countable located and closed subsets of $\mathcal {N}$.

Theorem 8

$\mathcal {T}_2$ is almost-enumerable.

Proof

Define $\delta$ such that $\delta ^0=\underline{0}$ and, for each n, $\delta ^{n+1}=n^*=\underline{\overline{0}}n*\underline{1}$. Note: $\forall n[\delta ^n \in \mathcal {T}_2]$. Let $\varepsilon$ be given. If $\overline{\alpha }\varepsilon (0)=\overline{\delta ^0}\varepsilon (0)$, we are done. If not, then $\alpha \perp \underline{0}$ and we may determine n such that $\alpha =\delta ^{n+1}$ and $\overline{\alpha }\varepsilon (n+1)=\overline{\delta ^{n+1}}\varepsilon (n+1)$.$\square$

Axiom 3

(Second Axiom of Countable Choice)

For every $R\subseteq \mathbb {N}\times \mathcal {N}$, if $\forall n\exists \alpha [nR\alpha ]$, then $\exists \alpha \forall n[n R \alpha ^n]$.

Theorem 9

• (i) $(\mathcal {T}_2,=)\models \exists \mathsf {x}[\lnot D(\mathsf {x})\;\wedge \;\forall \mathsf {y}[AP(\mathsf {x, y})\rightarrow D(\mathsf {y})]]$.

• (ii) For all $\beta$ such that $Spr(\beta )$,

  if $(\mathcal {F}_\beta ,=)\models \exists \mathsf {x}[\lnot D(\mathsf {x})\;\wedge \;\forall \mathsf {y}[AP(\mathsf {x, y})\rightarrow D(\mathsf {y})]]$, then $\mathcal {F}_\beta$ embeds into $\mathcal {T}_2$.

Proof

• (i) $\underline{0}$ is not an isolated point of $\mathcal {T}_2$, and, therefore, not a decidable point of $\mathcal {T}_2$. Also, by Theorem 7 (ii), $\forall \alpha \in \mathcal {T}_2[\alpha \;\#\;\underline{0}\rightarrow \exists n[\alpha = n^*]]$, and, for each n, for each $\alpha$ in $\mathcal {T}_2$, $\alpha = n^*\leftrightarrow \overline{\underline{0}}n*\langle 1\rangle \sqsubset \alpha$, so one may decide: $\alpha = n^*$ or $\lnot (\alpha = n^*)$, and: $n^*$ is a decidable point of $\mathcal {T}_2$.

  We thus see: $(\mathcal {T}_2,=)\models \lnot D(\mathsf {x})\;\wedge \;\forall \mathsf {y}[AP(\mathsf {x, y})\rightarrow D(\mathsf {y})][\underline{0}]$, and are done.

• (ii) Assume: $Spr(\beta )$ and $(\mathcal {F}_\beta ,=)\models \exists \mathsf {x}[\lnot D(\mathsf {x})\;\wedge \;\forall \mathsf {y}[AP(\mathsf {x, y})\rightarrow D(\mathsf {y})]]$.

  Find $\alpha$ in $\mathcal {F}_\beta$ such that $\alpha$ is not an isolated point of $\mathcal {F}_\beta$.

  Note: for each s such that $\beta (s)=0$, the set $\mathcal {F}_\beta \cap s:=\{\delta \in \mathcal {F}_\beta \mid s\sqsubset \delta \}$ is a spread, and, if $s\perp \alpha$, then $\mathcal {F}_\beta \cap s$ consists of isolated points of $\mathcal {F}_\beta \cap s$ only, and thus, by Theorem 6, embeds into $\omega$.

  Using Axiom 3, we find $\varphi$ such that, for each s, if $\beta (s)=0$ and there exist n, i such that $s=\overline{\alpha }n*\langle i\rangle$ and $i\ne \alpha (n)$, then $\varphi ^s:\mathcal {F}_\beta \cap s\hookrightarrow \omega$.

  We now define $\psi :\mathcal {F}_\beta \rightarrow \mathcal {T}_2$ such that $\psi |\alpha =\underline{0}$ and, for each $\delta$ in $\mathcal {F}_\beta$, if $\delta \;\#\;\alpha$, then $\psi |\delta =\overline{\underline{0}}\bigl (\overline{\delta }n, \varphi ^{\overline{\delta }n}(\delta )\bigr )*\underline{1}$ where $n:=\mu i[\overline{\delta }i \perp \alpha ]$. $\square$

1.7 More and More Undecidable Points: The Toy Spreads

Definition 13

For each n, we let $\tau _n$ be the element of $\mathcal {C}$ satisfying: $\forall s[\tau _n(s)=0\leftrightarrow \forall i<length(s)[s(i)<n\;\wedge \; \bigl (i+1<length(s)\rightarrow s(i)\le s(i+1)\bigr )]]$.

We also define: $\mathcal {T}_n:=\mathcal {F}_{\tau _n}$.

For each n, $\tau _n$ is a spread-law and $\mathcal {T}_n$ and $\mathcal {T}_n=\{\alpha \mid \forall i[\alpha (i)\le \alpha (i+1)<n]\}$ is a spread.

In this paper, the spreads $\mathcal {T}_0, \mathcal {T}_1, \ldots$ will be called the toy spreads.

Note: $\mathcal {T}_0=\emptyset$ and $\mathcal {T}_1=\{\underline{0}\}$.

Definition 14

For each $s\ne \langle \;\rangle$, we let $s^\dag$ be the element of $\mathcal {N}$ satisfying $s\sqsubset s^\dag$ and $\forall i\ge length(s)[s^\dag (i)=s^\dag (i-1)]$.

Note that, for each n, for each s, if $s\ne \langle \;\rangle$ and $\tau _n(s)=0$, then $s^\dag \in \mathcal {T}_n$.

Theorem 10

For each $n>0$, $\mathcal {T}_n$ is almost-enumerable.

Proof

Let $n>0$ be given. Define $\delta$ such that, for each s, if $s\ne \langle \;\rangle$ and $\tau _n(s)=0$, then $\delta ^s=s^\dag$, and if not, then $\delta ^s = \underline{0}$.

We claim: $\forall \alpha \in \mathcal {T}_n\forall \varepsilon \exists s[\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)]$.

We establish this claim by proving, for each $k<n$,

$\forall \alpha \in \mathcal {T}_n[\exists i[\alpha (i)\ge k]\rightarrow \forall \varepsilon \exists s[\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)]]$, and we do so by backwards induction, starting with the case $k=n-1$.

The case $k=n-1$ is treated as follows. If $\exists i[\alpha (i)=n-1]$, find

$i_0:=\mu i[\alpha (i)=n-1]$ and consider $s:=\overline{\alpha }(i_0+1)$.

Note: $\alpha =s^\dag =\delta ^s$ and, therefore, for every $\varepsilon$: $\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)$.

Now assume $k<n-1$ is given such that

$\forall \alpha \in \mathcal {T}_n[\exists i[\alpha (i)\ge k+1]\rightarrow \forall \varepsilon \exists s[\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)]]$.

We have to prove: $\forall \alpha \in \mathcal {T}_n[\exists i[\alpha (i)=k]\rightarrow \forall \varepsilon \exists s[\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)]]$.

Let $\alpha$ be given such that $\exists i[\alpha (i)=k]$. Let also $\varepsilon$ be given.

Define $i_0:=\mu i[\alpha (i)=k]$ and define $s:=\overline{\alpha }(i_0+1)$.

There are two cases to consider.

Case (i): $\overline{\alpha }\varepsilon (s)=\overline{s^\dag }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)$. We are done.

Case (ii): $\overline{\alpha }\varepsilon (s)\perp \overline{s^\dag }\varepsilon (s)$. Then $\exists i<\varepsilon (s) [\alpha (i)\ge k+1]$.

Using the induction hypothesis, we conclude: $\exists s[\overline{\alpha }\varepsilon (s)=\overline{\delta ^s}\varepsilon (s)]$.$\square$

Theorem 11

• (i) For each n, for all $\alpha$ in $\mathcal {T}_n$, $\alpha \in \mathcal {I}(\mathcal {T}_n)$ if and only if $\exists m[\alpha (m)+1=n]$.

• (ii) For each n, $\mathcal {T}_{n+1}\setminus \mathcal {I}(\mathcal {T}_{n+1}) = \mathcal {T}_n=\mathcal {L}(\mathcal {T}_{n+1})$.

• (iii) For each n, $\mathcal {T}_n=\{\alpha \in \mathcal {T}_{n+1}\mid (\mathcal {T}_{n+1},=)\models \lnot D[\alpha ]\}$.

Proof

The proof uses Lemma 3 and is left to the reader.$\square$

Definition 15

We define an infinite sequence $D_0, D_1, \ldots$ of formulas, as follows.

$D_0:= \mathsf {\forall y[x=y\;\vee \;\lnot (x=y)}]$,

$D_1:=\lnot D_0(\mathsf {x}) \;\wedge \; \forall \mathsf {y}[\lnot D_0(\mathsf {y})\rightarrow \bigl (\mathsf {x=y\;\vee \;\lnot (x=y)\bigr )}]$,

$D_2:=\lnot D_0(\mathsf {x})\;\wedge \; \lnot D_1(\mathsf {x})\;\wedge \; \forall \mathsf {y}[\bigl (\lnot D_0(\mathsf {y})\;\wedge \;\lnot D_1(\mathsf {y})\bigr )\rightarrow \bigl (\mathsf {x=y\;\vee \;\lnot (x=y)\bigr )}]$,

and, more generally for each $m>0$,

$D_{m}:=\bigwedge _{i<m}\lnot D_i(\mathsf {x}) \;\wedge \; \forall \mathsf {y}[\bigl (\bigwedge _{i<m}\lnot D_i(\mathsf {y})\bigr )\rightarrow \bigl (\mathsf {x=y\;\vee \;\lnot (x=y)\bigr )}]$.

We also define, for each $m>0$, sentences $\psi _m$ and $\rho _m$, as follows:

$\psi _{m}:=\exists \mathsf {x}[ D_{m}(\mathsf {x})]$ and $\rho _m:=\exists \mathsf {x}[D_m(\mathsf {x})\;\wedge \;\forall \mathsf {y}[D_m(\mathsf {y})\rightarrow \mathsf {y=x}]]$.

Definition 16

Assume $Spr(\beta )$.

$\alpha$ in $\mathcal {F}_\beta$ is a limit point of order 0 of $\mathcal {F}_\beta$ if and only if $\alpha$ is an isolated point of $\mathcal {F}_\beta$.

For each m, $\alpha$ is a limit point of order $m+1$ of $\mathcal {F}_\beta$ if and only if, for each p, there exists a limit point $\gamma$ of order m such that $\overline{\alpha }p\sqsubset \gamma$ and $\alpha \perp \gamma$.

Assume $n>0$ and $\alpha \in \mathcal {T}_n$. Note the following:

• 1. $(\mathcal {T}_n, =)\models D_0[\alpha ]$ if and only if $\alpha$ is an isolated point of $\mathcal {T}_n$ if and only if either: $n=1$ or: $n>1$ and $\exists p[\alpha (p) = n-1]$.

• 2. $(\mathcal {T}_n, =)\models \lnot D_0[\alpha ]$ if and only if $\alpha$ is a limit point (of order 1) of $\mathcal {T}_n$ if and only if $n>1$ and $\alpha \in \mathcal {T}_{n-1}$.

• 3. $(\mathcal {T}_n, =)\models D_1[\alpha ]$ if and only if $\alpha$ is an isolated point among the limit points (of order 1) of $\mathcal {T}_n$ if and only if $n>1$ and $\alpha \in \mathcal {T}_{n-1}$ and $\exists p[\alpha (p) =n-2]$.

• 4. $(\mathcal {T}_n, =)\models \lnot D_0\;\wedge \;\lnot D_1[\alpha ]$, if and only if $\alpha$ is a limit point of order 2 of $\mathcal {T}_n$ if and only if $n>2$ and $\alpha \in \mathcal {T}_{n-2}$.

• 5. For each $m>0$, $(\mathcal {T}_n, =)\models D_{2}[\alpha ]$ if and only if $\alpha$ is an isolated point among the limit points of order 2 if and only if $n>2$ and $\alpha \in \mathcal {T}_{n-2}$ and $\exists p[\alpha (p)= n-3]$.

• 6. For each $m>0$, $(\mathcal {T}_n, =)\models \bigwedge _{i<m} \lnot D_i[\alpha ]$ if and only if $\alpha$ is a limit point of order m of $\mathcal {T}_n$ if and only if $n>m$ and $\alpha \in \mathcal {T}_{n-m}$.

• 7. For each $m>0$, $(\mathcal {T}_n, =)\models D_{m}[\alpha ]$ if and only if $\alpha$ is an isolated point among the limit points of order m if and only if $n>m$ and $\alpha \in \mathcal {T}_{n-m}$ and $\exists p[\alpha (p)= n-m-1]$.

• 8. For each $m>0$, $\mathcal {T}_n\models \psi _m$ if and only if $\mathcal {T}_n$ contains an isolated point of $\mathcal {T}_{n-m}$ if and only if $n>m$.

• 9. For each $m>0$, $\mathcal {T}_n\models \rho _m$ if and only if $\mathcal {T}_n$ contains exactly one isolated point of $\mathcal {T}_{n-m}$ if and only if $\mathcal {T}_{n-m}=\{\underline{0}\}$ if and only if $n=m+1$.

After these preliminary observations, the following Theorem is easy to understand:

Theorem 12

• (i) For each n, $\mathcal {T}_n$ is a transparent¹⁶ spread and,

  if $n>0$, then $\mathcal {I}(\mathcal {T}_n)= \{\alpha \in \mathcal {T}_n\mid \exists p[\alpha (p)+1=n]\}$ and $\mathcal {L}(\mathcal {T}_n)=\mathcal {T}_{n-1}$.

• (ii) For all n, for all $m>0$, $\mathcal {T}_n=\{\alpha \in \mathcal {T}_{n+m}\mid (\mathcal {T}_{n+m},=)\models \bigwedge _{i<m} \lnot D_i[\alpha ]\}$.

• (iii) For all m, $\{\underline{0}\}=\mathcal {T}_1=\{\alpha \in \mathcal {T}_{m+1}\mid (\mathcal {T}_{m+1},=)\models \bigwedge _{i<m} \lnot D_i[\alpha ]\}$.

• (iv) For all $n>0$, for all $m>0$, $(\mathcal {T}_n, =)\models \psi _m$ if and only if $m+1\le n$.

• (v) For all $n>0$, for all $m>0$, $(\mathcal {T}_n, =)\models \rho _m$ if and only if $m+1=n$.

Proof

Use the preliminary observations preceding this Theorem.$\square$

Corollary 2

For all n, m, if $n\ne m$, then there exists a sentence $\psi$ such that $(\mathcal {T}_m,=)\models \psi$ and $(\mathcal {T}_n, =)\models \lnot \psi$.

1.8 Finite and Infinite Sums of Toy Spreads

1.8.1 A Main Result

Definition 17

Assume $Spr(\beta ), Spr(\gamma )$.

We define: $\mathcal {F}_\beta \uplus \mathcal {F}_\gamma :=\{\langle 0\rangle *\delta \mid \delta \in \mathcal {F}_\beta \}\cup \{\langle 1\rangle *\delta \mid \delta \in \mathcal {F}_\gamma \}$.

For each m, we define: $m\otimes \mathcal {F}_\beta :=\{\langle i\rangle *\delta \mid i<m, \delta \in \mathcal {F}_\beta \}$.

We also define: $\omega \otimes \mathcal {F}_\beta :=\{\langle i\rangle *\delta \mid i\in \omega , \delta \in \mathcal {F}_\beta \}$.

Note that $\mathcal {F}_\beta \uplus \mathcal {F}_\gamma$, $m\otimes \mathcal {F}_\beta$ and $\omega \otimes \mathcal {F}_\beta$ are spreads again.

We also define, for all $m,n>0$, sentences $\psi _m^n$ and $\rho _m^n$, as follows:

$\psi ^n_{m}:=\exists \mathsf {x}_0\exists \mathsf {x_1}\ldots \exists \mathsf {x}_{n-1}[\bigwedge _{i<j<n}[AP(\mathsf {x}_i, \mathsf {x}_j) \;\wedge \;\bigwedge _{i<n}\bigwedge _{j<m}\lnot D_j(\mathsf {x}_i)]$.

and $\rho ^n_m:=\exists \mathsf {x}_0\exists \mathsf {x_1}\ldots \exists \mathsf {x}_{n-1}[\bigwedge _{i<j<n}[AP(\mathsf {x}_i, \mathsf {x}_j) \;\wedge \;\bigwedge _{i<n}\bigwedge _{j<m}\lnot D_j(\mathsf {x}_i)\;\wedge \forall \mathsf {z}[\bigwedge _{j<m} \lnot D_j(\mathsf {z})\rightarrow \bigvee _{i<n} \mathsf {z}=\mathsf {x}_i] ]$.

The sentence $\psi ^n_m$ expresses: ‘there exist (at least) n limit points of order m that are mutually apart’.

The sentence $\rho ^n_m$ expresses: ‘there exist exactly n limit points of order m that are mutually apart’.

Theorem 13

• (i) For all $m,n,p,q>0$,

  $(n\otimes \mathcal {T}_m,=)\models \psi ^q_p$ if and only if either: $p+1< m$ or: $p+1=m$ and $q\le n$.

• (ii) For all $m,n,p,q>0$, $(n\otimes \mathcal {T}_m,=)\models \rho _p^q$ if and only if $p+1=m$ and $n=q$.

• (iii) For all $m,p,q>0$, $(\omega \otimes \mathcal {T}_m,=)\models \psi ^q_p$ if and only if $p< m$.

Proof

(i) Note the following:

If $p+1<m$ and $n>0$, then $\mathcal {T}_m$ and also $n\otimes \mathcal {T}_m$ contain infinitely many limit points of order p that are mutually apart.

If $p+1=m$ and $n>0$, then $n \otimes \mathcal {T}_m$ contains exactly n limit points of order p that are mutually apart: the points $\langle i\rangle *\underline{0}$, where $i<n$, so $(n\otimes \mathcal {T}_m,=)\models \psi ^q_p$ if and only if $q\le n$.

If $p< m$, then $\omega \times \mathcal {T}_m$ contains infinitely many limit points of order p that are mutually apart.

The proofs of (i), (ii) and (iii) follow easily from these observations.$\square$

Definition 18

For each k, for each s in $\omega ^k$, we define: $\mathcal {V}_s=\bigcup _{i<k}\{\langle i\rangle *\delta \mid \delta \in \mathcal {T}_{s(i)}\}$.

Definition 19

Let $\mathcal {F}_0, \mathcal {F}_1\subseteq \mathcal {N}$ and assume $\varphi :\mathcal {F}_0\rightarrow \mathcal {F}_1$.

$\varphi$ is a (surjective) map from $\mathcal {F}_0$ onto $\mathcal {F}_1$ if and only if $\forall \beta \in \mathcal {F}_1\exists \alpha \in \mathcal {F}_0[\varphi |\alpha =\beta ]$.

$\mathcal {F}_0$ is equivalent to $\mathcal {F}_1$, notation: $\mathcal {F}_0\sim \mathcal {F}_1$, if and only if there exists $\varphi :\mathcal {F}_0\rightarrow \mathcal {F}_1$ that is both injective¹⁷ and surjective.

Theorem 14

• (i) For each m, $\mathcal {T}_m\oplus \mathcal {T}_{m+1}\sim \mathcal {T}_{m+1}$.

• (ii) For all m, n, if $m<n$, then $\mathcal {T}_m\oplus \mathcal {T}_n\sim \mathcal {T}_{n}$.

• (iii) For all k, for all s in $\omega ^k$, there exist m, n such that $\mathcal {V}_s\sim n\otimes \mathcal {T}_m$.

Proof

• (i) Let m be given. Define $\varphi :\mathcal {T}_m\oplus \mathcal {T}_{m+1}\rightarrow \mathcal {T}_{m+1}$ such that, for all $\delta$ in $\mathcal {T}_m$, $\varphi |\langle 0\rangle *\delta = \langle 1\rangle *S\circ \delta$, and, for each $\delta$ in $\mathcal {T}_{m+1}$, $\varphi |\langle 1\rangle *\delta = \langle 0 \rangle *\delta$. Clearly, $\varphi$ is a one-to-one function mapping $\mathcal {T}_m\oplus \mathcal {T}_{m+1}$ onto $\mathcal {T}_{m+1}$.

• (ii) Let m be given. We use induction on n. The case $n=m+1$ has been treated in (i). Now let n be given such that $m<n$ and $\mathcal {T}_m\oplus \mathcal {T}_n\sim \mathcal {T}_n$.

  Then $\mathcal {T}_m\oplus \mathcal {T}_{n+1}\sim \mathcal {T}_m\oplus (\mathcal {T}_n\oplus \mathcal {T}_{n+1})\sim (\mathcal {T}_m\oplus \mathcal {T}_n)\oplus \mathcal {T}_{n+1} \sim \mathcal {T}_n\oplus \mathcal {T}_{n+1}\sim \mathcal {T}_{n+1}$.

• (iii) We use induction on k. If $s\in \omega ^0$, then $s=\langle \;\rangle$ and $\emptyset =\mathcal {V}_s = 0\otimes \mathcal {T}_1$.

  Now let k be given such that,

  for all s in $\omega ^k$, there exist m, n such that $\mathcal {V}_s= n \otimes \mathcal {T}_m$.

  Let $s=t*\langle p\rangle$ in $\omega ^{k+1}$ be given. Find m, n such that $\mathcal {V}_t=n\otimes \mathcal {T}_m$.

  Note: $\mathcal {V}_s\sim \mathcal {V}_t\oplus \mathcal {T}_{p}$ and consider several cases.

  Case (1): $t=\langle \;\rangle$. Then $\mathcal {V}_s=1\otimes \mathcal {T}_{p}$.

  Case (2): $t \ne \langle \;\rangle$ and $p<m$. Then, by (ii): $\mathcal {V}_s \sim \mathcal {V}_t\sim n\otimes \mathcal {T}_m$.

  Case (3): $t \ne \langle \;\rangle$ and $p=m$. Then: $\mathcal {V}_s \sim \mathcal {V}_t\oplus \mathcal {T}_m\sim (n+1)\otimes \mathcal {T}_m$.

  Case (4): $t \ne \langle \;\rangle$ and $p>m$. Then, by (ii):

  $$\mathcal {V}_s \sim \mathcal {V}_t\oplus \mathcal {T}_{p }\sim \underbrace{\mathcal {T}_m\oplus \ldots \oplus \mathcal {T}_m}_{n}\oplus \mathcal {T}_{p }\sim \mathcal {T}_p\sim 1\otimes \mathcal {T}_{p}.$$

$\square$

Definition 20

For each $\alpha$, we define: $\mathcal {V}_\alpha :=\bigcup _i \{\langle i \rangle *\delta \mid \delta \in \mathcal {T}_{\alpha (i)}\}$.

Theorem 15

(EQ has continuum many complete extensions¹⁸)

• (i) For each $\alpha$, $\mathcal {I}(\mathcal {V}_\alpha )=\bigcup _i\{\langle i\rangle *\delta \mid \delta \in \mathcal {T}_{\alpha (i)}\;\wedge \;\exists p[\delta (p)+1=\alpha (i)]\}$.

• (ii) For all $\alpha$, for all n, $(\mathcal {V}_\alpha ,=)\models \psi _n$ if and only if $\exists i[\alpha (i)>n]$.

• (iii) For all $\alpha$, for all n, $(\mathcal {V}_\alpha ,=)\models \rho _n$ if and only if

  $\exists i[\alpha (i)=n+1\;\wedge \;\forall j[\alpha (j)=n+1\rightarrow i=j]]$.

• (iv) For all $\zeta , \eta$ in $[\omega ]^\omega$, if $\zeta \perp \eta$ and $\zeta (0)=\eta (0)=2$,

  then there exists a sentence $\psi$ such that $(\mathcal {V}_\zeta ,=)\models \psi$ and $(\mathcal {V}_\eta ,=)\models \lnot \psi$.

Proof

• (i) Use Theorem 12 (i).

• (ii) Note that, for each $\alpha$, for each n, $(\mathcal {V}_\alpha ,=)\models \psi _n$ if and only if $\mathcal {V}_\alpha$ contains a limit point of order n if and only if $\exists i[\alpha (i)>n]$.

• (iii) Note that, for each $\alpha$, for each n, $(\mathcal {V}_\alpha ,=)\models \rho _n$ if and only if $\mathcal {V}_\alpha$ contains exactly one limit point of order n if and only if

  $\exists i[\alpha (i)=n+1\;\wedge \;\forall j[\alpha (j)=n+1\rightarrow i=j]]$.

• (iv) Using (iii), note that, for all $\zeta$ in $[\omega ]^\omega$, if $\zeta (0)>1$, then $\forall n[(\mathcal {V}_\zeta ,=) \models \rho _n$ if and only if $\exists p[\zeta (p)= n+1]$.

  Conclude that, for all $\zeta ,\eta$ in $[\omega ]^\omega$, for all p, if $\zeta (0)=\eta (0)=2$ and $\zeta \perp \eta$ and $p:=\mu i[\zeta (i)\ne \eta (i)]$ and $\zeta (p)<\eta (p)$, then $\lnot \exists i[\eta (i)=\zeta (p)]$, and, therefore, $(\mathcal {V}_\zeta ,=)\models \psi _{\zeta (p)-1}$ and $(\mathcal {V}_\eta ,=)\models \lnot \psi _{\zeta (p)-1}$.

$\square$

1.8.2 Finitary Spreads Suffice

Definition 21

Assume $Spr(\beta )$. $\beta$ is called a finitary spread-law or a fan-law if and only if $\exists \gamma \forall s[\beta (s)=0\rightarrow \forall n[\beta (s*\langle n \rangle )=0\rightarrow n\le \gamma (s)]]$.

$\mathcal {X}\subseteq \mathcal {N}$ is a fan if and only if there exists a fan-law $\beta$ such that $\mathcal {X}=\mathcal {F}_\beta$.

Note that the toy spreads $\mathcal {T}_0, \mathcal {T}_1, \ldots$ are fans.

The set $\mathcal {V}_\alpha$, however, is a spread but, in general, not a fan.

Define, for each $\alpha$, $\mathcal {V}^*_\alpha := \overline{\bigcup _n \underline{\overline{0}} n*\langle 1\rangle *\mathcal {T}_{\alpha (n)}}$.¹⁹

Note that, for each $\alpha$, $\mathcal {V}_\alpha ^*$ is a fan.

One may prove a statement very similar to Theorem 15 (iv):

For all $\zeta , \eta$ in $[\omega ]^\omega$, if $\zeta \perp \eta$ and $\zeta (0)=\eta (0)=2$, then there exists a sentence $\psi$ such that $(\mathcal {V}^*_\zeta , =)\models \psi$ and $(\mathcal {V}^*_\eta , =)\models \lnot \psi$.

1.8.3 Comparison with an Older Theorem

The first-order theory DLO of dense linear orderings without endpoints is formulated in a first-order language with binary predicate symbols $=$ and $\sqsubset$ and consists of the following axioms:

• 1. $\mathsf {\forall x[x\sqsubset x]}$,

• 2. $\mathsf {\forall x\forall y\forall z[(x\sqsubset y\;\wedge \;y\sqsubset z)\rightarrow x\sqsubset z]}$,

• 3. $\mathsf {\forall x\forall y[ \bigl (\lnot (x\sqsubset y)\;\wedge \;\lnot (y\sqsubset x)\bigr )\rightarrow x=y]}$.

• 4. $\mathsf {\forall x\forall y[x\sqsubset y\rightarrow \forall z[x\sqsubset z\;\vee \;z\sqsubset y]]}$,

• 5. $\mathsf {\forall x\exists y[x\sqsubset y]\;\wedge \;\forall x\exists y[y\sqsubset x]}$,

• 6. $\mathsf {\forall x\forall y[x\sqsubset y\rightarrow \exists z[x\sqsubset z\;\wedge \;z\sqsubset y]]}$, and

• 7. axioms of equality.

$(\mathcal {R}, =_\mathcal {R}, <_\mathcal {R})$ realizes DLO.

Let $DLO^-$ be the theory one obtains from DLO by leaving out axiom (4). If one defines a relation $<'_\mathcal {R}$ on $\mathcal {R}$ by: $\forall x\forall y[x<'_\mathcal {R} y\leftrightarrow \lnot \lnot (x<_\mathcal {R}y)]$, then $(\mathcal {R}, =_\mathcal {R}, <'_\mathcal {R})$ realizes $DLO^-$ but not DLO.

In Veldman and Janssen (1990, Theorem 2.4) one constructs a function $\alpha \mapsto A_\alpha$ associating to each element $\alpha$ of $2^\omega =\mathcal {C}$ a subset $A_\alpha$ of the set $\mathcal {R}$ of the real numbers such that, for each $\alpha$ in $\mathcal {C}$, $A_\alpha$ is dense in $(\mathcal {R}, <_\mathcal {R})$, and, for all $\alpha , \beta$ in $\mathcal {C}$, if $\alpha \perp \beta$, then there exists a sentence $\psi$ such that $(A_\alpha , <_\mathcal {R})\models \psi$ and $(A_\beta , <_\mathcal {R})\models \lnot \psi$.

Note: each structure $(A_\alpha , <_\mathcal {R})$ realizes DLO. The (intuitionistic) theory DLO thus has continuum many complete extensions.²⁰

One may obtain the result of Theorem 15 (iv) for subsets of $\mathcal {R}$ as well as for subsets of $\mathcal {N}$. Define an infinite sequence $\mathcal {U}_0, \mathcal {U}_1, \ldots$ of subsets of $\mathcal {R}$ by:

$\mathcal {U}_0:=\emptyset$ and $\mathcal {U}_1:=\{0_\mathcal {R}\}$, and for each $m>0$, $\mathcal {U}_{m+1}= \overline{\bigcup _n \frac{1}{2^{n+1}}+\frac{1}{2^{n+2}}\cdot _\mathcal {R} \mathcal {U}_m}.$²¹

For each m, one may define $\varphi :\mathcal {T}_m\rightarrow \mathcal {U}_m$ such that $\varphi$ is surjective and satisfies: $\forall \delta \in \mathcal {T}_m\forall \zeta \in \mathcal {T}_m[\delta \perp \zeta \leftrightarrow \varphi |\delta \;\#_\mathcal {R}\;\varphi |\zeta ]$.

It follows that, for each m, the structures $(\mathcal {T}_m,=)$ and $(\mathcal {U}_m, =_\mathcal {R})$ are elementarily equivalent.

Define, for each $\alpha$ in $[\omega ]^\omega$, $A_\alpha :=\bigcup _n n+_\mathcal {R}\mathcal {U}_{\alpha (n)}$.

Note: for all $\alpha ,\beta$ in $[\omega ]^\omega$, if $\alpha \perp \beta$, then there exists a sentence $\psi$ such that $(A_\alpha , =_\mathcal {R})\models \psi$ and $(A_\beta , =_\mathcal {R})\models \lnot \psi$.

We thus obtain a result similar to Veldman and Janssen (1990, Theorem 2.4), this time using not the ordering relation $<_\mathcal {R}$ but only the equality relation $=_\mathcal {R}$.

Note that, for all $\alpha ,\beta$ in $\mathcal {R}$, $\alpha =_\mathcal {R} \beta \leftrightarrow \bigl (\lnot (\alpha<_\mathcal {R} \beta )\;\wedge \;\lnot (\beta <_\mathcal {R}\alpha )\bigr )$.

Conclude: the relation $=_\mathcal {R}$ is definable in the structure $(\mathcal {R}, <_\mathcal {R})$.

Conclude: for all subsets $\mathcal {T}, \mathcal {U}$ of $\mathcal {R}$, if there exists a sentence $\psi$ such that

$(\mathcal {T}, =_\mathcal {R})\models \psi$ and $(\mathcal {U}, =_\mathcal {R})\models \lnot \psi$, then there also exists a sentence $\psi ^*$ such that

$(\mathcal {T}, <_\mathcal {R})\models \psi ^*$ and $(\mathcal {U}, <_\mathcal {R})\models \lnot \psi ^*$.

The conclusion of Veldman and Janssen (1990, Theorem 2.4) might have been obtained as a corollary of Theorem 15 (iv).

1.9 The Vitali Equivalence Relation

For all $\alpha , \beta$, we define

$$\alpha \sim _V\beta \leftrightarrow \exists n\forall m>n[\alpha (m)=\beta (m)].$$

The relation $\sim _V$ will be called the Vitali equivalence relation.

This is because the relation $\sim _V$ on $\mathcal {N}$ resembles the relation $\sim _\mathbb {Q}$ on the set $\mathcal {R}$ of the real numbers defined by:

$$x\sim _\mathbb {Q}y\leftrightarrow \exists q\in \mathbb {Q}[x-_\mathcal {R}y=q].$$

The relation $\sim _\mathbb {Q}$ has played an important rôle in classical set theory.

If one constructs, using the axiom of choice, within the interval [0, 1], a transversal for this equivalence relation, that is: a complete set of mutually inequivalent representatives, one obtains a set that is not Lebesgue measurable. This discovery is due to G. Vitali.

Note: $(\mathcal {N}, \sim _V)\models EQ$.

The following theorem brings to light an important difference between $(\mathcal {N},=)$ and $(\mathcal {N}, \sim _V)$.

Definition 22

A proposition P is stable if and only if $\lnot \lnot P\rightarrow P$.

A binary relation $\sim$ on $\mathcal {N}$ is stable if and and only if

$\forall \alpha \forall \beta [\lnot \lnot (\alpha \sim \beta )\rightarrow \alpha \sim \beta ]$.²²

Theorem 16

(Equality is stable but the Vitali equivalence relation is not stable)

• (i) $(\mathcal {N}, =)\models \mathsf {\forall x \forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

• (ii) $(\mathcal {N}, \sim _V)\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

Proof

• (i) Note: for all $\alpha , \beta$, $\alpha =\beta \leftrightarrow \lnot (\alpha \;\#\;\beta )$, and, therefore:

  $\lnot \lnot (\alpha =\beta )\leftrightarrow \lnot \lnot \lnot (\alpha \;\#\;\beta )\leftrightarrow \lnot (\alpha \;\#\; \beta )\leftrightarrow \alpha =\beta$.

• (ii) Let $\gamma$ be given.

  Consider $\mathcal {F}^\gamma :=\{\alpha \mid \forall m\forall n[\bigl (\alpha (m)\ne \gamma (m)\;\wedge \;\alpha (n)\ne \gamma (n)\bigr )\rightarrow m=n]$.

  $\mathcal {F}^\gamma$ is the set of all $\alpha$ that differ at at most one place from $\gamma$.

  Note that $\mathcal {F}^\gamma$ is a spread.

  We have two claims.

  First claim: $\forall \alpha \in \mathcal {F}^\gamma [\lnot \lnot (\alpha \sim _V \gamma )]$.

  The proof is as follows. Let $\alpha$ in $\mathcal {F}^\gamma$ be given. Distinguish two cases.

  Case (1). $\exists n[\alpha (n)\ne \gamma (n)]$. Find n such that $\alpha (n)\ne \gamma (n)$ and conclude:

  $\forall m>n[\alpha (m)=\gamma (m)]$ and $\alpha \sim _V\gamma$.

  Case (2). $\lnot \exists n[\alpha (n)\ne \gamma (n)]$. Conclude: $\forall n[\alpha (n)=\gamma (n)]$ and $\alpha \sim _V\gamma$.

  We thus see: if $\exists n[\alpha (n)\ne \gamma (n)]\;\vee \;\lnot \exists n[\alpha (n)\ne \gamma (n)]$, then $\alpha \sim _V\underline{\gamma }$.

  As $\lnot \lnot (\exists n[\alpha (n)\ne \gamma (n)]\;\vee \;\lnot \exists n[\alpha (n)\ne \gamma (n)])$, also $\lnot \lnot (\alpha \sim _V\gamma )$.

  Second claim: $\lnot \forall \alpha \in \mathcal {F}^\gamma [\alpha \sim \gamma ]$.

  In order to see this, assume: $\forall \alpha \in \mathcal {F}^\gamma [\alpha \sim \gamma ]$, that is:

  $\forall \alpha \in \mathcal {F}\exists n\forall m>n[\alpha (m)=\gamma (m)]$. Using Lemma 2, find p, n such that

  $\forall \alpha \in \mathcal {F}^\gamma [\overline{\gamma }p\sqsubset \alpha \rightarrow \forall m>n[\alpha (m)=\gamma (m)]]$. Define $m:=\max (p,n+1)$ and define $\alpha$ such that $\forall n[\alpha (n)\ne \gamma (n)\leftrightarrow n=m]$. Note: $\overline{\gamma } p\sqsubset \alpha$ and $m>n$ and $\alpha (m)\ne \gamma (m)$. Contradiction.

  Combining our two claims, we see:

  not: for all $\alpha$, if $\lnot \lnot (\alpha \sim _V \gamma )$ then $\alpha \sim _V \gamma$.

  Conclude: $(\mathcal {N}, \sim _V)\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

$\square$

It follows from Theorem 16 that there is no relation $\#_V$ on $\mathcal {N}$ satisfying the requirements of an apartness relation²³  with respect to $\sim _V$:

• (i) $\forall \alpha \forall \beta [\lnot (\alpha \;\#_V\;\beta )\leftrightarrow \alpha \sim _V\beta ]$

• (ii) $\forall \alpha \forall \beta [\alpha \;\#_V\;\beta \rightarrow \beta \;\#_V\;\alpha ]$

• (iii) $\forall \alpha \forall \beta [\alpha \;\#_V\;\beta \rightarrow \forall \gamma [\alpha \;\#_V\;\gamma \;\vee \;\gamma \;\#_V\;\beta ]]$.

The existence of an apartness $\#_V$ would imply, by the first one of these requirements, that $\sim _V$ is a stable relation, as, for any proposition P, $\lnot \lnot \lnot P\leftrightarrow \lnot P$.

The next Theorem now is no surprise:

Theorem 17

$(\mathcal {N}, \sim _V)\models \mathsf {\forall x \forall y[\lnot }AP(\mathsf {x,y})]$.

Proof

Let $\alpha , \beta$ be given.

Assume $(\mathcal {N},\sim _V)\models AP[\alpha , \beta ]$, that is, $\forall \gamma [\gamma \not \sim _V \alpha \;\vee \;\gamma \not \sim _V \beta ]$.

Applying Lemma 1, find p such that

either $\forall \gamma [\overline{\alpha }p\sqsubset \gamma \rightarrow \gamma \not \sim _V \alpha ]$ or $\forall \gamma [\overline{\alpha }p\sqsubset \gamma \rightarrow \gamma \not \sim _V \beta ]$.

The first of these two alternatives is wrong, as $\overline{\alpha }p\sqsubset \alpha \;\wedge \; \alpha \sim _V \alpha$.

Conclude: $\forall \gamma [\overline{\alpha }p\sqsubset \gamma \rightarrow \gamma \not \sim _V \beta ]$.

Define $\gamma$ such that $\overline{\alpha }p\sqsubset \gamma$ and $\forall i>p[\gamma (i)=\beta (i)]$.

Note: $\overline{\alpha }p\sqsubset \gamma \;\wedge \; \gamma \sim _V \beta$.

Contradiction.

Conclude: $(\mathcal {N}, =_V)\models \lnot AP[\alpha , \beta ]$.

We thus see: $(\mathcal {N}, =_V)\models \mathsf {\forall x \forall y[\lnot }AP(\mathsf {x,y})]$.$\square$

Clearly, the relation defined by the formula AP in the structure $(\mathcal {N}, \sim _V)$ fails to satisfy the first requirement for an apartness relation with respect to $\sim _V$.

It follows from Theorem 17 that $(\mathcal {N}, \sim _V)$, while realizing $T_{inf}$, does not realize $T^+_{inf}$, see Definitions 1 and 4.

1.10 A First Vitali Variation

There are many intuitionistic versions of the classical Vitali equivalence relation. This is obvious to someone who knows that there are many variations upon the notion of a finite and decidable subset of $\mathbb {N}$, see Veldman (1995) and Veldman (2005, Sect. 3).

Definition 23

We define an infinite sequence $\sim ^0_V, \sim ^1_V, \ldots$ of relations on $\mathcal {N}$ such that $\sim ^0_V\;=\;\sim _V$ and, for each i,

$$ \alpha \sim _V^{i+1}\beta \leftrightarrow \exists n\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim ^i_V\beta ]. $$

We also define:

$$\alpha \sim ^\omega _V\beta \leftrightarrow \exists i[\alpha \sim ^i_V\beta ].$$

Theorem 18

• (i) $\forall i \forall n\forall s \in \omega ^n\forall t \in \omega ^n\forall \alpha \forall \beta [s*\alpha \sim ^i_V t*\beta \leftrightarrow \alpha \sim _V^i \beta ]$.

• (ii) $\forall i\forall \alpha \forall \beta [\alpha \sim _V^{i}\beta \rightarrow \alpha \sim _V^{i+1}\beta ]$.

• (iii) $\forall i\forall \gamma \lnot \forall \alpha [\alpha \sim _V^{i+1}\gamma \rightarrow \alpha \sim _V^i\gamma ]$.

• (iv) $\forall i\forall j\forall \alpha \forall \beta \forall \gamma [(\alpha \sim _V^i \beta \;\wedge \;\beta \sim _V^j \gamma )\rightarrow \alpha \sim _V^{i+j}\gamma ]$.

• (v) $\sim _V^\omega$ is an equivalence relation on $\mathcal {N}$.

Proof

• (i) One proves this easily by induction.

• (ii) Obvious.

• (iii) Let $\gamma$ be given.

  For each i, define $\mathcal {F}^\gamma _i:=\{\alpha \mid \forall s \in [\omega ]^{i+1}\exists j<i+1[\alpha \circ s(j)=\gamma \circ s(j)]\}$.

  Note: for each i, $\mathcal {F}^\gamma _i$ is a spread, and $\mathcal {F}^\gamma _i \subsetneq \mathcal {F}^\gamma _{i+1}$.

  For each i, $\mathcal {F}^\gamma _i$ consists of all $\alpha$ that assume at most i times a value different from the value assumed by $\gamma$. In particular, $\mathcal {F}^0_\gamma =\{\gamma \}$.

  Note: for all $i, m, \alpha , \beta$,

  if $m=\mu n[\alpha (n)\ne \gamma (n)]$ and $\alpha =\overline{\alpha }(m+1)*\beta$, then $\alpha \in \mathcal {F}^\gamma _{i+1}\leftrightarrow \beta \in \mathcal {F}^\gamma _i$.

  We have two claims.

  First claim: $\forall i\forall \alpha \in \mathcal {F}^\gamma _i[\alpha \sim _V^i\gamma ]$.

  We prove this claim by induction.

  The starting point of the induction is the observation:

  $\forall \alpha \in \mathcal {F}_0^\gamma [\alpha =\gamma ]$, so $\forall \alpha \in \mathcal {F}^\gamma _0[\alpha \sim _V^0\gamma ]$.

  Now assume i is given such that $\forall \alpha \in \mathcal {F}_i^\gamma [\alpha \sim ^i_V\gamma ]$.

  Assume $\alpha \in \mathcal {F}^\gamma _{i+1}$ and $\exists n[\alpha (n)\ne \gamma (n)]$. Find n such that $\alpha (n)\ne \gamma (n)$. Find $\beta$ such that $\alpha =\overline{\alpha }(n+1)*\beta$, and note: $\beta \in \mathcal {F}^\gamma _i$ and thus, by the induction hypothesis, $\beta \sim _V^i \gamma$. Conclude, using (i): $\alpha \sim _V^i \gamma$.

  We thus see:

  $\forall \alpha \in \mathcal {F}^\gamma _{i+1}[\exists n[\alpha (n)\ne \gamma (n)]\rightarrow \alpha \sim ^i_V\gamma ]$, that is: $\forall \alpha \in \mathcal {F}^\gamma _{i+1}[\alpha \sim ^{i+1}_V \gamma ]$. This completes the proof of the induction step.

  Second claim: $\forall i \lnot \forall \alpha \in \mathcal {F}^\gamma _{i+1}[\alpha \sim ^i_V \gamma ]$.

  We again use induction.

  We first prove: $\lnot \forall \alpha \in \mathcal {F}^\gamma _1[\alpha \sim _V \gamma ]$.

  Assume $\forall \alpha \in \mathcal {F}^\gamma _1[\alpha \sim _V \gamma ]$, that is: $\forall \alpha \in \mathcal {F}_1\exists n\forall m>n[\alpha (m) =\gamma (m)]$.

  Note: $\gamma \in \mathcal {F}_1^\gamma$ and $\mathcal {F}^1_\gamma$ is a spread.

  Using Lemma 2, find p, n such that

  $\forall \alpha \in \mathcal {F}_1[\overline{\gamma }p\sqsubset \alpha \rightarrow \forall m>n[\alpha (m)=\gamma (m)]$.

  Define $m:=\max (n+1,p)$ and define $\alpha$ such that $\forall n[\alpha (n)=\gamma (n)\leftrightarrow n\ne m]$.

  Note: $\alpha \in \mathcal {F}_1$ and $\overline{\gamma }p\sqsubset \alpha$ and $\alpha (m)\ne \gamma (m)$ and $m>n$. Contradiction.

  Conclude: $\lnot \forall \alpha \in \mathcal {F}^\gamma _1[\alpha \sim _V \gamma ]$.

  Now let i be given such that $\lnot \forall \alpha \in \mathcal {F}^\gamma _{i+1}[\alpha \sim _V^i \gamma ]$.

  We want to prove: $\lnot \forall \alpha \in \mathcal {F}^\gamma _{i+2}[\alpha \sim _V^{i+1} \gamma ]$.

  Assume: $\forall \alpha \in \mathcal {F}^\gamma _{i+2}[\alpha \sim _V^{i+1} \gamma ]$, that is:

  $\forall \alpha \in \mathcal {F}^\gamma _{i+2}\exists n\forall m>n[\alpha (m)\ne \gamma (m)\rightarrow \alpha \sim ^{i+1}_V\gamma ]$. Using Lemma 2, find p, n such that $\forall \alpha \in \mathcal {F}^\gamma _{i+2}[(\overline{\gamma }p\sqsubset \alpha \;\wedge \;m>n\;\wedge \;\alpha (m)\ne \gamma (m))\rightarrow \alpha \sim ^i_V\gamma ]$.

  Define $m:=\max (n+1, p)$. Let $\beta$ in $\mathcal {F}^\gamma _{i+1}$ be given. Define $\alpha$ such that $m=\mu n[\alpha (n)\ne \gamma (n)]$ and $\forall n> m[\alpha (n)=\beta (n)]$. Note: $\alpha \in \mathcal {F}^\gamma _{i+2}$ and $\alpha (m)\ne \gamma (m)$ and $m>n$, so $\alpha \sim _V^{i}\gamma$, and, therefore, by (i), $\beta \sim _V^{i}\gamma$. We thus see: $\forall \beta \in \mathcal {F}^\gamma _{i+1}[\beta \sim _V^i\gamma ]$ and, by the induction hypothesis, obtain a contradiction.

  This completes the proof of the induction step.

  Taking our first and second claim together, we obtain the conclusion:

  $\forall \gamma \forall i\lnot \forall \alpha [\alpha \sim ^{i+1}_V \gamma \rightarrow \alpha \sim ^{i}_V \gamma ]$.

• (iv) We have to prove:

  for all i, for all j, $\forall \alpha \forall \beta \forall \gamma [(\alpha \sim _V^i \beta \;\wedge \;\beta \sim _V^j \gamma )\rightarrow \alpha \sim _V^{i+j}\gamma ]$.

  We use induction on $i+j$ and distinguish four cases.

  Case (1): $i=j=0$. Assume $\alpha \sim ^0_V\beta$ and $\beta \sim ^0_V\gamma$. Find n, p such that $\forall m>n[\alpha (m)=\beta (m)]$ and $\forall m>p[\beta (m)=\gamma (m)]$. Define $q:=\max (n, p)$ and note: $\forall m>q[\alpha (m)=\gamma (m)]$. Conclude: $\alpha \sim ^0_V\gamma$.

  Case (2): $i=0$ and $j>0$. Assume $\alpha \sim ^0_V\beta$ and $\beta \sim ^j_V\gamma$. Find n, p such that $\forall m>n[\alpha (m)=\beta (m)]$ and $\forall m>p[\beta (m)\ne \gamma (m)\rightarrow \beta \sim ^{j-1}_V\gamma ]$. Define $q:=\max (n,p)$.

  Assume $m>q$ and note: if $\alpha (m)\ne \gamma (m)$, then $\beta (m) \ne \gamma (m)$ and $\beta \sim ^{j-1}_V\gamma$. Using the induction hypothesis, conclude: $\alpha \sim ^{j-1}_V \gamma$.

  We thus see: $\forall m>q[\alpha (m)\ne \gamma (m)\rightarrow \alpha \sim ^{j-1}_V\gamma ]$, that is: $\alpha \sim ^j_V\gamma$.

  Case (3): $i>0$ and $j=0$. Assume $\alpha \sim ^i_V\beta$ and $\beta \sim ^0_V\gamma$. Find n, p such that $\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim ^{i-1}_V \beta ]$ and $\forall m>p[\beta (m)=\gamma (m)]$. Define $q:=\max (n,p)$.

  Assume $m>q$ and note: if $\alpha (m)\ne \gamma (m)$, then $\alpha (m) \ne \beta (m)$ and $\alpha \sim ^{i-1}_V\beta$. Using the induction hypothesis, conclude: $\alpha \sim ^{i-1}_V \gamma$.

  We thus see: $\forall m>q[\alpha (m)\ne \gamma (m)\rightarrow \alpha \sim ^{i-1}_V\gamma ]$, that is: $\alpha \sim ^i_V\gamma$.

  Case (4): $i>0$ and $j>0$. Assume $\alpha \sim ^i_V\beta$ and $\beta \sim ^j_V\gamma$. Find n, p such that $\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim ^{i-1}_V \beta ]$ and $\forall m>p[\beta (m)\ne \gamma (m)\rightarrow \beta \sim ^{j-1}_V\gamma ]$. Define $q:=\max (n,p)$.

  Assume $m>q$ and $\alpha (m)\ne \gamma (m)$. Then either: $\alpha (m)\ne \beta (m)$ and $\alpha \sim ^{i-1}\beta$, and, by the induction hypothesis, $\alpha \sim ^{i+j-1}_V\gamma$, or: $\beta (m)\ne \gamma (m)$ and $\beta \sim ^{j-1}\gamma$ and, by the induction hypothesis, $\alpha \sim ^{i+j-1}\gamma$.

  We thus see: $\forall m>q[\alpha (m)\ne \gamma (m)\rightarrow \alpha \sim ^{i+j-1}\gamma ]$. Conclude: $\alpha \sim ^{i+j}\gamma$.

• (v) is an easy consequence of (iv).

The next Theorem shows that the structures $(\mathcal {N}, \sim _V)$ and $(\mathcal {N}, \sim ^\omega _V)$ have a property in common.

Theorem 19

($\sim ^\omega _V$ is not stable)

$(\mathcal {N}, \sim _V^\omega )\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x =y]}$.

Proof

Let $\gamma$ be given.

We repeat a definition we gave in the proof of Theorem 18 (iii).

For each i, $\mathcal {F}^\gamma _i:=\{\alpha \mid \forall s \in [\omega ]^{i+1}\exists j<i+1[\alpha \circ s(j)=\gamma \circ s(j)]\}$.

In the proof of Theorem 18 (iii), we saw: $\forall i\forall \alpha \in \mathcal {F}^\gamma _i[\alpha \sim ^i_V \gamma ]$.

Conclude: $\forall i\forall \alpha \in \mathcal {F}^\gamma _i[\alpha \sim ^\omega _V \gamma ]$.

We now define: $\mathcal {F}^\gamma _\omega :=\{\alpha \mid \forall i[i=\mu n[\alpha (n)\ne \gamma (n)]\rightarrow \alpha \in \mathcal {F}_{i+1}]\}$.

Like each $\mathcal {F}^\gamma _i$, $\mathcal {F}^\gamma _\omega$ is a spread, and $\gamma \in \mathcal {F}^\gamma _\omega$.

We have two claims.

First claim: $\forall \alpha \in \mathcal {F}^\gamma _\omega [\lnot \lnot (\alpha \sim _V^\omega \gamma )]$.

The argument is as follows. Let $\alpha$ in $\mathcal {F}^\gamma _\omega$ be given and distinguish two cases.

Case (1): $\lnot \exists n[\alpha (n)\ne \gamma (n)]$. Then $\alpha =\gamma$ and $\alpha \sim _V^\omega \gamma$.

Case (2): $\exists n[\alpha (n)\ne \gamma (n)]$. Find $i:=\mu n[\alpha (n)\ne \gamma (n)]$. Note: $\alpha \in \mathcal {F}_{i+1}^\gamma$ and $\alpha \sim ^\omega _V \gamma$.

As $\lnot \lnot (\exists n[\alpha (n)\ne \gamma (n)]\;\vee \;\lnot \exists n[\alpha (n)\ne \gamma (n)])$, also $\lnot \lnot (\alpha \sim _V^\omega \gamma )$.

Second claim: $\lnot \forall \alpha \in \mathcal {F}^\gamma _\omega [\alpha \sim _V^\omega \gamma ]$.

In order to see this, assume: $\forall \alpha \in \mathcal {F}^\gamma _\omega [\alpha \sim _V^\omega \gamma ]$, that is: $\forall \alpha \in \mathcal {F}_\omega \exists i[\alpha \sim ^i_V \gamma ]$.

Using Lemma 2, find p, i such that $\forall \alpha \in \mathcal {F}^\gamma _\omega [\overline{\gamma }p\sqsubset \alpha \rightarrow \alpha \sim ^i_V \gamma ]$.

Define $q:=\max (p, i+1)$. Let $\alpha$ in $\mathcal {F}^\gamma _q$ be given. Define $\beta$ such that

$\forall n<q[\beta (n)=\gamma (n)]$ and $\beta (q)\ne \gamma (q)$ and $\forall n>q[\beta (n)=\alpha (n)]$.

Note: $\beta \in \mathcal {F}_{q+1}$ and $q=\mu n[\beta (n)\ne \gamma (n)]$, and, therefore, $\beta \in \mathcal {F}_\omega ^\gamma$.

As $\overline{\gamma }q\sqsubset \beta$, we conclude: $\beta \sim _V^i\gamma$.

As $\beta \sim ^0_V\alpha$, also $\alpha \sim _V^i\gamma$.

We thus see: $\forall \alpha \in \mathcal {F}_q[\alpha \sim _V^i \gamma ]$.

As $q>i$, this contradicts the Second claim in the proof of Theorem 18 (iii).

Taking our two claims together, we conclude:

$\forall \gamma \lnot \forall \alpha \in \mathcal {F}^\gamma _\omega [\lnot \lnot (\alpha \sim ^\omega _V\gamma )\rightarrow \alpha \sim ^\omega _V\gamma ]$.

Conclude: $(\mathcal {N}, \sim ^\omega _V)\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x =y]}$.$\square$

We did not succeed in finding a sentence $\psi$ such that $(\mathcal {N}, \sim _V)\models \psi$ and

$(\mathcal {N}, \sim ^\omega _V)\models \lnot \psi$.

1.11 More and More Vitali Relations

In Veldman (1995), Veldman (1999) and Veldman (2005, Sect. 3), one studies the set

$$\mathbf {Fin}:=\{\alpha \mid \alpha \sim _V\underline{0}\}=\{\alpha \mid \exists n \forall m>n[\alpha (m)=0]\}.$$

For each $\alpha$, $\alpha \in \mathbf {Fin}$ if and only if $D_\alpha :=\{m\mid \alpha (m)\ne 0\}$ is a finite subset of $\mathbb {N}$.

For each i, the set $\{\alpha \mid \alpha \sim _V^i \underline{0}\}$ is called, in Veldman (1999) and Veldman (2005), the i-th perhapsive extension of the set $\mathbf {Fin}$. It is shown, in Veldman (1995), Veldman (1999) and Veldman (2005), that the process of building perhapsive extensions of $\mathbf {Fin}$ can be carried on into the transfinite.

In a similar way, the Vitali equivalence relation  $\sim _V$ admits of transfinitely many extensions.

The relation $\sim _V^\omega$ is only a first extension of $\sim _V$. Let us consider a second one.

Recall: $\forall \alpha \forall \beta [\alpha \sim _V^\omega \leftrightarrow i[\alpha \sim _V^ i\beta ]]$.

Definition 24

We define an infinite sequence $\sim _V^{\omega +0}=\sim _V^\omega , \sim ^{\omega +1}_V, \sim ^{\omega +2}_V, \ldots$ of relations on $\mathcal {N}$, such that, for each $i>0$,

$$ \alpha \sim _V^{\omega +i+1}\beta \leftrightarrow \exists n\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim ^{\omega +i}_V\beta ]. $$

We also define:

$$\alpha \sim ^{\omega +\omega }_V\beta \leftrightarrow \exists i[\alpha \sim ^{\omega +i}_V\beta ].$$

One may prove analogues of Theorems 18 and 19 and conclude:

$\sim _V^{\omega +\omega }$ is an equivalence relation on $\mathcal {N}$, properly extending $\sim _V^\omega$, that, like $\sim _V$ and $\sim _V^\omega$, is not stable in the sense of Theorem 19.

One may continue and define $\sim _V^{\omega +\omega +\omega }$, and $\sim _V^{\omega +\omega +\omega +\omega }$ and so on.

The process of building such extensions leads further into the transfinite, as follows.

Definition 25

Let R be a binary relation on $\mathcal {N}$.

We define a binary relation $R^+$ on $\mathcal {N}$ by:

$$\alpha R^+\beta \leftrightarrow \exists n\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha R \beta ].$$

We let $\mathcal {E}$ be the least class of binary relations on $\mathcal {N}$ such that

• (i) the Vitali equivalence relation$\sim _V$ belongs to $\mathcal {E}$, and,

• (ii) for every R in $\mathcal {E}$, also $R^+ \in \mathcal {E}$, and,

• (iii) for every infinite sequence $R_0, R_1, \ldots$ of elements of $\mathcal {E}$, also $\bigcup _i R_i \in \mathcal {E}$.

The elements of $\mathcal {E}$ are the extensions of the Vitali equivalence relation.

Note that $<_V^\omega$ and $<_V^{\omega +\omega }$ are in $\mathcal {E}$.

In general, a relation R in $\mathcal {E}$ is not transitive. One may prove, for instance, that the relation $<_V^1$, while belonging to $\mathcal {E}$, is not transitive.

The next Theorem shows that $\mathcal {E}$ contains many transitive relations.

Theorem 20

($\mathcal {E}$ contains many transitive relations)

• (i) $\sim _V$ is transitive.

• (ii) Given any transitive R in $\mathcal {E}$, there exists a transitive T in $\mathcal {E}$ such that $R^+\subseteq T$.

• (iii) Given any infinite and increasing sequence $R_0\subseteq R_1\subseteq \ldots$ of transitive relations in $\mathcal {E}$, also $\bigcup _i R_i$ is a transitive relation in $\mathcal {E}$.

Proof

• (i) Obvious.

• (ii) We take our inspiration from Theorem 18 (iv) and (v).

  Let a transitive R in $\mathcal {E}$ be given.

  Define an infinite sequence $R^0, R^1, \ldots$ of elements of $\mathcal {E}$ such that $R^0=R$ and, for each i, $R^{i+1}= (R^ i)^+$.

  One may prove: for all i, for all j, $\forall \alpha \forall \beta \forall \gamma [(\alpha R^i\beta \;\wedge \;\beta R^i\gamma )\rightarrow \alpha R^{i+j} \gamma ]$, as it is done for the special case $R=\sim _V$ in the proof of Theorem 18 (iv).

  Define $T:=\bigcup _i R^i$ and note: $T\in \mathcal {E}$, $R^+\subseteq T$ and T is transitive.

• (iii) Note: for every increasing sequence $R_0\subseteq R_1\subseteq \ldots$ of transitive relations on $\mathcal {N}$, also $\bigcup _i R_i$ is transitive.

Theorem 20 will gain significance after Corollary 3, which shows that, for every R in $\mathcal {E}$, $R\subseteq R^+$ and $\lnot (R^+\subseteq R)$.

We did not succeed in proving that every R in $\mathcal {E}$ extends to a transitive T in $\mathcal {E}$.

Definition 26

A binary relation R on $\mathcal {N}$ is shift-invariant if and only if

$\forall \alpha \forall \beta [\alpha R \beta \leftrightarrow (\alpha \circ S) R (\beta \circ S)]$.

Lemma 7

Every R in $\mathcal {E}$ is shift-invariant.

Proof

The proof is a straightforward exercise in induction on $\mathcal {E}$. Note:

• (I) $\sim _V$ is shift-invariant.

• (II) For every binary relation R on $\mathcal {N}$, if R is shift-invariant, then $R^+$ is shift-invariant.

• (III) For every infinite sequence $R_0, R_1, \ldots$ of binary relations on $\mathcal {N}$, if each $R_n$ is shift-invariant, then $\bigcup _iR_i$ is shift-invariant.

  Conclude: every R in $\mathcal {E}$ is shift-invariant.$\square$

Definition 27

We let $\mathcal {E}^*$ be the least class of binary relations on $\mathcal {N}$ such that

• (i) the Vitali equivalence relation$\sim _V$ belongs to $\mathcal {E}^*$, and

• (ii) for every infinite sequence $R_0, R_1, \ldots$ of elements of $\mathcal {E}^*$, also $(\bigcup _i R_i)^+\in \mathcal {E}^*.$

Lemma 8

$\mathcal {E}^*\subseteq \mathcal {E}$ and, for all R in $\mathcal {E}$, there exists T in $\mathcal {E}^*$ such that $R\subseteq T$.

Proof

The proofs of the two statements are straightforward, by induction on $\mathcal {E}^*$ and $\mathcal {E}$, respectively.$\square$

Theorem 21

For each R in $\mathcal {E}^*$, $R\subseteq R^+$ and $\lnot (R^+\subseteq R)$.

Proof

For each R in $\mathcal {E}$, we define $Fin_R:=\{\alpha \mid \alpha R\underline{0}\}$.²⁴

We prove for each R in $\mathcal {E}^*$ there exists a fan $\mathcal {F}$ such that $\mathcal {F}\subseteq Fin_{R^+}$ and $\lnot (\mathcal {F}\subseteq Fin_R)$.

We do so by induction on $\mathcal {E}^*$.

(I) Define $\mathcal {F}:=\{\alpha \mid \forall m\forall n[(\alpha (m)\ne 0 \;\wedge \;\alpha (n)\ne 0)\rightarrow m=n]\}$.

Note that $\mathcal {F}$ is a fan.

For each $\alpha$ in $\mathcal {F}$, for each n, if $\alpha (n)\ne 0$ then: $\forall m>n[\alpha (m)=0]$ and $\alpha \in Fin_{\sim _V}$. Conclude: for each $\alpha \in \mathcal {F}$, if $\exists n[\alpha (n)\ne 0]$, then $\alpha \in Fin_{\sim _V}$, that is: $\alpha \in Fin_{(\sim _V)^+}$. Conclude: $\mathcal {F}\subseteq Fin_{(\sim _V)^+}$.

Now assume $\mathcal {F}\subseteq Fin_{\sim _V}$, that is: $\forall \alpha \in \mathcal {F}\exists n\forall m>n[\alpha (m)=0]$. Using Lemma 2, find p, n such that $\forall \alpha \in \mathcal {F}[\underline{\overline{0}}p\sqsubset \alpha \rightarrow \forall m>n[\alpha (m)=0]]$.

Define $q:=\max (p, n+1)$ and consider $\alpha :=\underline{\overline{0}}q*\langle 1 \rangle *\underline{0}$. Contradiction.

Conclude: $\lnot (\mathcal {F}\subseteq Fin_{\sim _V})$.

(II) Let $R_0, R_1, \ldots$ be an infinite sequence of elements of $\mathcal {E}$.

Let $\mathcal {F}_0, \mathcal {F}_1,\ldots$ be an infinite sequence of fans such that,

for each n, $\mathcal {F}_n\subseteq Fin_{(R_n)^+}$ and $\lnot (\mathcal {F}_n\subseteq Fin_{ R_n})$.

Consider $R:=(\bigcup _i R_i)^+$.

Define $\mathcal {F}:=\{\alpha \mid \forall n[n=\mu i[\alpha (i)\ne 0]\rightarrow \exists \beta \in \mathcal {F}_{n'}[\alpha =\overline{\alpha }(n+1)*\beta ]\}$.²⁵

Note that $\mathcal {F}$ is a fan.

We now prove: $\mathcal {F}\subseteq Fin_{R^+}$ and $\lnot (\mathcal {F}\subseteq Fin_R)$.

Note that, for each $\alpha \in \mathcal {F}$, for each n, if $n=\mu i[\alpha (i)\ne 0]$, then there exists $\beta$ in $\mathcal {F}_{n'}$ such that $\alpha =\overline{\alpha }(n+1)*\beta$.

As, for each n, $\mathcal {F}_n\subseteq Fin_{(R_n)^+}\subseteq Fin_{\bigcup _i (R_i)^+}$, and $\bigcup _i(R_i)^+\subseteq \bigl (\bigcup _i R_i\bigr )^+=R$ and R is shift-invariant, conclude: $\forall \alpha \in \mathcal {F}[\exists n[\alpha (n)\ne 0]\rightarrow \alpha \in Fin_R]$, that is: $\mathcal {F}\subseteq Fin_{R^+}$.

Now assume $\mathcal {F}\subseteq Fin_R$, that is: $\forall \alpha \in \mathcal {F}\exists n\forall m>n[\alpha (m)\ne 0]\rightarrow \exists i[\alpha \in Fin_{R_i}]]$. Using Lemma 2, find p, n such that

$\forall \alpha \in \mathcal {F}[\overline{\underline{0}} p\sqsubset \alpha \rightarrow \forall m >n[\alpha (m)\ne 0\rightarrow \exists i[\alpha \in Fin_{R_i}]]$.

Define $q:=\max (p, n+1)$ and note: $\forall \alpha \in \mathcal {F}[\overline{\underline{0}}q*\langle 1\rangle \sqsubset \alpha \rightarrow \exists i[\alpha \in \mathcal {F}_i]]$.

Using Lemma 2 again, find r, i such that $\forall \alpha \in \mathcal {F}[\overline{\underline{0}}q*\langle 1 \rangle *\overline{\underline{0}}r\sqsubset \alpha \rightarrow \alpha \in \mathcal {F}_i]$.

Find $n\ge q+r+1$ such that $n' =i$ and define $t:=n-(q+1)$.

Note: $t\ge r$ and conclude: $\forall \beta \in \mathcal {F}_i[\overline{\underline{0}}q *\langle 1\rangle *\overline{\underline{0}}t*\langle 1 \rangle *\beta \in Fin_{R_i}]$.

As $R_i$ is shift-invariant, conclude: $\mathcal {F}_i\subseteq Fin_{R_i}$.

Contradiction, as $\lnot (\mathcal {F}_i\subseteq Fin_{R_i})$.

Conclude: $\lnot (\mathcal {F} \subseteq Fin_{R})$.$\square$

Corollary 3

For each R in $\mathcal {E}$, $R\subseteq R^+$ and $\lnot (R^+\subseteq R)$.

Proof

Assume we find R in $\mathcal {E}$ such that $R=R^+$.

Conclude, by induction on $\mathcal {E}$: for all U in $\mathcal {E}$, $U\subseteq R$.

Using Lemma 8, find T in $\mathcal {E}^*$ such that $R\subseteq T$.

By Theorem 21, $T\subseteq T^+$ and $\lnot (T^+\subseteq T)$.

On the other hand, $T^+\subseteq R\subseteq T$.

Contradiction. $\square$

Definition 28

We define binary relations $\sim _V^{\lnot \lnot }$ and $\sim _V^{almost}$ on $\mathcal {N}$, as follows.

For all $\alpha , \beta$, $\alpha \sim _V^{\lnot \lnot }\beta \leftrightarrow \lnot \lnot \exists n\forall m>n[\alpha (n)=\beta (n)]\leftrightarrow \lnot \lnot (\alpha \sim _V\beta )$, and

$\alpha \sim ^{almost}_V\beta \leftrightarrow \forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$.

$\alpha \sim _V^{almost}\beta$ if and only if the set $\{n\mid \alpha (n)\ne \beta (n)\}$ is almost$^*$-finite in the sense used in Veldman (2005, Section 0.8.2).

The following axiom is a form of Brouwer’s famous Thesis on bars in $\mathcal {N}$, see Veldman (2006).

Axiom 4

(The Principle of Bar Induction)

For all $B,C\subseteq \mathbb {N}$, if $\forall \alpha \exists n[\overline{\alpha }n \in B]$ and $B\subseteq C$ and $\forall s[s\in C\leftrightarrow \forall n[s*\langle n\rangle \in C]]$, then $\langle \; \rangle \in C$,

or, equivalently,

for all $B,C\subseteq [\omega ]^{<\omega }$, if $\forall \zeta \in [\omega ]^\omega \exists n[\overline{\zeta }n \in B]$ and $B\subseteq C$ and

$\forall s\in [\omega ]^{<\omega }[s\in C\leftrightarrow \forall n[s*\langle n\rangle \in [\omega ]^{<\omega }\rightarrow s*\langle n\rangle \in C]]$, then $\langle \; \rangle \in C$.

Theorem 22

• (i) $\sim _V^{\lnot \lnot }$ and $\sim _V^{almost}$ are equivalence relations on $\mathcal {N}$.

• (ii) For all R in $\mathcal {E}$, $\sim _V\;\subseteq R\subseteq \;\sim _V^{\lnot \lnot }$.

• (iii) For all R in $\mathcal {E}$, $R\;\subseteq \; \sim ^{almost}_V$.

• (iv) $\forall \alpha \forall \beta [ \alpha \sim _V^{almost}\beta \rightarrow \exists R\in \mathcal {E}[\alpha R\; \beta ]$.

• (v) $\forall \alpha \forall \beta [\alpha \sim _V^{almost}\beta \rightarrow \alpha \sim _V^{\lnot \lnot }\beta ]$.

Proof

(i) One easily proves that $\sim _V^{\lnot \lnot }$ is an equivalence relation. One needs the fact that, for all propositions P, Q, $(\lnot \lnot P\;\wedge \;\lnot \lnot Q)\rightarrow \lnot \lnot (P\;\wedge \; Q)$.

We prove that $\sim _V^{almost}$ is a transitive relation.

Let $\alpha , \beta , \gamma$ be given such that $\alpha \sim _V^{almost}\beta$ and $\beta \sim _V^{almost} \gamma$.

Let $\zeta$ in $[\omega ]^\omega$ be given. Find $\eta$ in $[\omega ]^\omega$ such that $\forall n[\alpha \circ \zeta \circ \eta (n)=\beta \circ \zeta \circ \eta (n)]$. Find p such that $\beta \circ \zeta \circ \eta (p)=\gamma \circ \zeta \circ \eta (p)$. Define $n:=\eta (p)$ and note: $\alpha \circ \zeta (n)=\gamma \circ \zeta (n)$.

We thus see: $\forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\gamma \circ \zeta (n)]$, that is: $\alpha \sim ^{almost}_V\gamma$.

(ii) The proof is by (transfinite) induction on $\mathcal {E}$. We only prove: for all R in $\mathcal {E}$, $R\subseteq \;\sim _V^{\lnot \lnot }$ as the statement: for all R in $\mathcal {E}$, $\sim _V\;\subseteq R$ is very easy to prove.

(I) Our starting point is the trivial observation: $\forall \alpha \forall \beta [\alpha \sim _V\beta \rightarrow \lnot \lnot (\alpha \sim _V \beta )]$.

(II) Now let R in $\mathcal {E}$ be given such that $\forall \alpha \forall \beta [\alpha R\beta \rightarrow \lnot \lnot (\alpha \sim _V \beta )]$.

We have to prove: $\forall \alpha \forall \beta [\alpha R^+\beta \rightarrow \lnot \lnot (\alpha \sim _V \beta )]$.

We do so as follows.

Let $\alpha , \beta$ be given such that $\alpha R^+\beta$.

Find n such that $\forall m>n[\alpha (m)\ne \beta (m) \rightarrow \alpha R\beta ]$ and consider two special cases.

Case (1): $\exists m>n[\alpha (m)\ne \beta (m)$. Then $\alpha R\;\beta$, and, therefore: $\lnot \lnot (\alpha \sim _V\beta )$.

Case (2): $\lnot \exists m>n[\alpha (m) \ne \beta (m)$. Then $\forall m>n[\alpha (m)=\beta (m)]$ and $\alpha \sim _V\beta$.

In both cases, we find: $\lnot \lnot (\alpha \sim _V\beta )$.

Conclude²⁶: $\lnot \lnot (\alpha \sim _V\beta )$.

(III) Now let $R_0, R_1, \ldots$ be an infinite sequence of elements of $\mathcal {E}$ such that, for all n, $\forall \alpha \forall \beta [\alpha R_n\beta \rightarrow \lnot \lnot (\alpha \sim _V\beta )]$.

Define $R:=\bigcup _n R_n$ and note: $\forall \alpha \forall \beta [\alpha R\beta \rightarrow \lnot \lnot (\alpha \sim _V\beta )]$.

(iii) The proof is by (transfinite) induction on $\mathcal {E}$.

(I) Our starting point is the observation: $\forall \alpha \forall \beta [a\sim ^0_V\beta \rightarrow \alpha \sim ^{almost}_V \beta ]$.

We prove this as follows:

Let $\alpha ,\beta$ be given such that $\alpha \sim ^0_V \beta$. Find n such that $\forall m>n[\alpha (m)=\beta (m)]$. Note: $\forall \zeta \in [\omega ]^\omega ][\zeta (n+1)>n \;\wedge \;\alpha \circ \zeta (n+1)=\beta \circ \zeta (n+1)]$.

Conclude: $\alpha \sim _V^{almost}\beta$.

(II) Now let R in $\mathcal {E}$ be given such that $\forall \alpha \forall \beta [\alpha R\beta \rightarrow \alpha \sim ^{almost}_V \beta ]$.

We have to prove: $\forall \alpha \forall \beta [aR^+\beta \rightarrow \alpha \sim ^{almost}_V \beta ]$.

We do so as follows.

Let $\alpha , \beta$ be given such that $\alpha R^+\beta$.

Find n such that $\forall m>n[\alpha (m)\ne \beta (m) \rightarrow \alpha R\beta ]$. Let $\zeta$ in $[\omega ]^\omega$ be given. Consider $\zeta (n+1)$ and note $\zeta (n+1)>n$. There now are two cases.

Either $\alpha \circ \zeta (n+1)=\beta \circ \zeta (n+1)$ or $\alpha \circ \zeta (n+1)\ne \beta \circ \zeta (n+1)$.

In the first case we are done, and in the second case we conclude $\alpha R \beta$, and, using the induction hypothesis, find p such that $\alpha \circ \zeta (p)=\beta \circ \zeta (p)$.

In both cases we conclude: $\exists q[\alpha \circ \zeta (q)=\beta \circ \zeta (q)]$.

We thus see: $\forall \zeta \in [\omega ]^\omega \exists q[\alpha \circ \zeta (q)=\beta \circ \zeta (q)]$, that is $\alpha \sim ^{almost}_V\beta$.

Clearly then: $\forall \alpha \forall \beta [[\alpha R^+\beta \rightarrow \alpha \sim ^{almost}_V \beta ]$.

(III) Now let $R_0, R_1, \ldots$ be an infinite sequence of elements of $\mathcal {E}$ such that, for all n, $\forall \alpha \forall \beta [\alpha R_n\beta \rightarrow \alpha \sim _V^{almost}\beta ]$.

Define $R:=\bigcup _n R_n$ and note: $\forall \alpha \forall \beta [\alpha R\beta \rightarrow \alpha \sim _V^{almost}\beta ]$.

(iv) Let $\alpha ,\beta$ be given such that $\alpha \sim ^{almost}\beta$, that is:

$\forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$.

Using Axiom 4, we shall prove: there exists R in $\mathcal {E}$ such that $\alpha R\beta$.

Define $B:=\bigcup _k\{s\in [\omega ]^{k+1}\mid \alpha \circ s(k)=\beta \circ s(k)\}$ and note: B is a bar in $[\omega ]^\omega$, that is: $\forall \zeta \in [\omega ]^\omega \exists n[\overline{\zeta }n \in B]$.

Define $C:= \bigcup _k\{ s \in [\omega ]^{k}\mid \exists n<k[\alpha \circ s(n)=\beta \circ s(n)] \;\vee \;\exists R \in \mathcal {E}[\alpha R \beta ]\}$.

Note: $C= \bigcup _k\{ s \in [\omega ]^{k}\mid \forall n<k[\alpha \circ s(n)\ne \beta \circ s(n)] \rightarrow \exists R \in \mathcal {E}[\alpha R \beta ]\}$.

Note: $B\subseteq C$ and: C is monotone, that is:

$\forall s\in [\omega ]^{<\omega }[s \in C \rightarrow \forall n[s*\langle n \rangle \in [\omega ]^{<\omega }\rightarrow s*\langle n \rangle \in C]]$.

We still have to prove that C is what one calls inductive or hereditary.

Let s in $[\omega ]^{< \omega }$ be given such that $\forall n[s*\langle n \rangle \in [\omega ]^{<\omega }\rightarrow s*\langle n \rangle \in C]$.

We want to prove: $s\in C$.

Find k such that $s\in [\omega ]^k$. In case $\exists n<k[\alpha \circ s(n) =\beta \circ s(n)]$, $s \in C$ and we are done, so we assume: $\forall n<k[\alpha \circ s(n)\ne \beta \circ s(n)]$.

Find a sequence²⁷ $R_0, R_1, \ldots$ of elements of $\mathcal {E}$ such that, for each n, if $s*\langle n \rangle \in [\omega ]^\omega$ and $\alpha (n)\ne \beta (n)$, then $\alpha R_n \beta$.

Define $R:=(\bigcup _i R_i)^+$ and note: $R\in \mathcal {E}$.

We claim: $\alpha R\beta$.

We establish this claim as follows.

Define p such that, if $k=0$, then $p:=0$ and, if $k>0$, then $p:=s(k-1)+1$.

Assume we find $n\ge p$ such that $\alpha (n)\ne \beta (n)$.

Note: $s*\langle n \rangle \in [\omega ]^{k+1}$ and $\forall i<k+1[\alpha \circ (s*\langle n \rangle )(i)\ne \beta \circ (s*\langle n \rangle )(i)]$ and $s*\langle n \rangle \in C$. Conclude: $\alpha R_n\beta$ and $\alpha ( \bigcup _i R_i )\beta$.

We thus see: $\forall n\ge p[\alpha (n)\ne \beta (n)\rightarrow \alpha ( \bigcup _i R_i )\beta ]$.

Conclude: $\alpha ( \bigcup _i R_i )^+ \beta$, that is: $\alpha R \beta$, and, therefore: $s\in C$.

We thus see that C is inductive.

Using Axiom 4, we conclude: $\langle \;\rangle \in C$, that is: $\exists R\in \mathcal {E}[\alpha R \beta ]$.

(v) Let $\alpha ,\beta$ be given such that $\alpha \sim ^{almost}\beta$, that is:

$\forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$.

Using Axiom 4, we prove: $\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]$.

Define $B:=\bigcup _{k}\{s\in [\omega ]^{k+1}\mid \alpha \circ s(k)=\beta \circ s(k)\}$ and note: B is a bar in $[\omega ]^\omega$, that is: $\forall \zeta \in [\omega ]^\omega \exists n[\overline{\zeta }n \in B]$. Define

$C:=\bigcup _k \{ s \in [\omega ]^k\mid \exists n<k[\alpha \circ s(n)=\beta \circ s(n)]\;\vee \;\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]\}$. Note: $C=\bigcup _k \{ s \in [\omega ]^k\mid \forall n<k[\alpha \circ s(n)\ne \beta \circ s(n)]\rightarrow \lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]\}$.

Note: $B\subseteq C$ and C is monotone, that is:

$\forall s\in [\omega ]^{<\omega }[s \in C \rightarrow \forall n[s*\langle n \rangle \in [\omega ]^{<\omega }\rightarrow s*\langle n \rangle \in C]]$.

We still have to prove that C is inductive.

Let s in $[\omega ]^{< \omega }$ be given such that $\forall n[s*\langle n \rangle \in [\omega ]^{<\omega }\rightarrow s*\langle n \rangle \in C]]$.

We want to prove: $s\in C$.

Find k such that $s\in [\omega ]^k$. In case $\exists n<k[\alpha \circ s(n)=\beta \circ s(n)]$, $s\in C$, and we are done, so we assume $\forall n<k[\alpha \circ s(n)\ne \beta \circ s(n)]$.

Define q such that $q:=0$ if $k=0$ and $q:=s(k-1)$ if $k>0$.

Consider two special cases:

Case (1): $\exists n>q[\alpha (n) \ne \beta (n)]$.

Find such n, note: $s*\langle n \rangle \in [\omega ]^\omega$ and $\forall i<k+1[\alpha \circ (s*\langle n \rangle )(i)\ne \beta \circ (s*\langle n \rangle )(i)]$ and $s*\langle n \rangle \in C$, and conclude: $\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]$.

Case (2): $\lnot \exists n>q[\alpha (n) \ne \beta (n)]$, and, therefore, $\forall n>q[\alpha (n)=\beta (n)]$.

In both cases, we find: $\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]$.

Conclude²⁸: $\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]$, and: $s\in C$.

We thus see that C is inductive.

Using Axiom 4, we conclude: $\langle \;\rangle \in C$, and, therefore,

$\lnot \lnot \exists p\forall n>p[\alpha (n)=\beta (n)]$, that is: $\lnot \lnot (\alpha \sim _V \beta )$.$\square$

Corollary 4

• (i) $(\mathcal {N}, \sim _V^{\lnot \lnot })\models \mathsf {\forall x\forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

• (ii) For each R in $\mathcal {E}$, $(\mathcal {N}, R)\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

Proof

• (i) Obvious, as, for any proposition P, $\lnot \lnot \lnot \lnot P\leftrightarrow \lnot \lnot P$.

• (ii) Assume $R\in \mathcal {E}$.

  We first prove: $(\mathcal {N}, R)\models \mathsf {\lnot \forall x\forall y[\lnot \lnot (x=y)\rightarrow x=y]}$.

  Assume $\forall \alpha \forall \beta [\lnot \lnot (\alpha R \beta )\rightarrow \alpha R \beta ]$.

  Note: $\forall \alpha \forall \beta [\alpha \sim _V\beta \rightarrow \alpha R\beta ]$ and, therefore: $\forall \alpha \forall \beta [\lnot \lnot (\alpha \sim _V\beta )\rightarrow \lnot \lnot (\alpha R\beta )]$.

  Conclude: $\sim _V^{\lnot \lnot }\; \subseteq R$.

  By Theorem 22 (ii), $R^+\subseteq \sim _V^{\lnot \lnot }$, so $R^+\subseteq R$. This contradicts Corollary 3.

  The stronger statement announced in the Theorem may be proven in a similar way. Inspection of he proof of Theorem 22 enables one to conclude:

  $(\mathcal {N}, R)\models \mathsf {\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}[\underline{0}]$.

  One easily generalizes this conclusion to:

  for each $\alpha$, $(\mathcal {N}, R)\models \mathsf {\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}[\alpha ]$.

  Conclude: $(\mathcal {N}, R)\models \mathsf {\forall x\lnot \forall y[\lnot \lnot (x=y)\rightarrow x=y]}$. $\square$

Markov’s Principle has been mentioned in Sect. 1.4. Markov’s Principle is not accepted in intuitionistic mathematics, but the following observation still is of interest.

Corollary 5

The following are equivalent.

• (i) Markov’s Principle: $\forall \alpha [\lnot \lnot \exists n[\alpha (n)=0]\rightarrow \exists n[\alpha (n)=0]]$.

• (ii) $\sim _V^{\lnot \lnot }\;\subseteq \;\sim _V^{almost}$.

• (iii) $\sim _V^{almost}$ is stable.

Proof

(i) $\Rightarrow$ (ii). Assume $\lnot \lnot (\alpha \sim _V\beta )$, that is $\lnot \lnot \exists n\forall m>n[\alpha (m)=\beta (m)]$.

Let $\zeta \in [\omega ]^\omega$ be given.

Assume: $\lnot \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$.

Then $\forall n[\zeta (n+1)>n\;\wedge \;\alpha \circ \zeta (n)\ne \beta \circ \zeta (n)]$, so $\forall n\exists m>n[\alpha (m)\ne \beta (m)]$. Contradiction.

Conclude: $\lnot \lnot \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$ and, by Markov’s Principle,

$\exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$.

We thus see $\forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$, that is: $\alpha \sim _V^{almost} \beta$.

(ii) $\Rightarrow$ (iii). By Theorem 22 (v), $\sim _V^{almost}\;\subseteq \; \sim _V^{\lnot \lnot }$. Therefore: $(\sim _V^{almost})^{\lnot \lnot }\;\subseteq \; \sim _V^{\lnot \lnot }$.

Using (ii), we conclude: $(\sim _V^{almost})^{\lnot \lnot }\;\subseteq \;\sim _V^{almost}$, that is: $\sim _V^{almost}$ is stable.

(iii) $\Rightarrow$ (i). Let $\alpha$ be given such that $\lnot \lnot \exists n[\alpha (n)\ne 0]$.

Define $\beta$ such that $\forall m[\beta (m)=0\leftrightarrow \exists n\le m[\alpha (n)=0]]$.

Note: $\lnot \lnot (\beta \sim _V\;\underline{0})$ and, therefore: $\lnot \lnot (\beta \sim _V^{almost}\underline{0})$.

Conclude, using (iii), $\beta \sim _V^{almost} \underline{0}$.

Define $\zeta$ such that $\forall n[\zeta (n)=n]$.

Find m such that $\beta \circ \zeta (m)=\beta (m)=0$ and, therefore, $\exists n\le m[\alpha (n) =0]$.

We thus see: $\forall \alpha [\lnot \lnot \exists n[\alpha (n)=0]\rightarrow \exists n[\alpha (n)=0]]$, that is: Markov’s Principle.$\square$

1.12 Equality and Equivalence

We did not succeed in finding a sentence $\psi$ such that $(\mathcal {N}, \sim _V)\models \psi$ and

$(\mathcal {N}, \sim ^\omega _V)\models \lnot \psi$. We now want to compare the structures $(\mathcal {N}, =, \sim _V)$ and

$(\mathcal {N}, =, \sim _V^\omega )$. We need a first order language with two binary relation symbols: $=$ and $\sim$. The symbol $=$ will denote the equality relation and the symbol $\sim$ will denote, in the first structure, the relation $\sim _V$ and, in the second structure, the relation $\sim _V^\omega$. The reader hopefully will not be confused by the fact that, in the earlier sections, where we used the first order language with a single binary relation symbol, $=$, the symbol $=$ denoted the relations $\sim _V$ and $\sim _V^\omega$.

The next Theorem makes us see that equality is decidable on each equivalence class of $\sim _V$ whereas, on each equivalence class of $\sim _V^\omega$, it is not decidable.

Theorem 23

• (i) $(\mathcal {N}, =, \sim _V)\models \mathsf {\forall x\forall y[x\sim y\rightarrow (x=y\;\vee \;\lnot (x=y))]}$.

• (ii) $(\mathcal {N}, =, \sim _V^\omega )\models \mathsf {\forall x\lnot \forall y[x\sim y\rightarrow (x=y\;\vee \;\lnot (x=y))]}$.

Proof

• (i) Let $\gamma , \alpha$ be given such that $\gamma \sim _V\alpha$.

  Find n such that $\forall m>n[\gamma (m)=\alpha (m)]$ and distinguish two cases.

  Either $\overline{\gamma }(m+1)=\overline{\alpha }(m+1)$ and $\gamma =\alpha$, or $\overline{\gamma }(m+1)\ne \overline{\alpha }(m+1)$ and $\lnot (\gamma =\alpha )$.

  Conclude: $\forall \gamma \forall \alpha [\gamma \sim _V\alpha \rightarrow (\gamma =\alpha \;\vee \;\lnot (\gamma =\alpha ))]$.

• (ii) Let $\gamma$ be given.

  Consider $\mathcal {F}_1^\gamma := \{\alpha \mid \forall m\forall n[(\alpha (m)\ne \gamma (m)\;\wedge \;\alpha (n)\ne \gamma (n))\rightarrow m=n]\}$.

  Note: $\mathcal {F}_1^\gamma$ is a spread.

  Also: $\forall \alpha \in \mathcal {F}_1^\gamma [\gamma \sim _V^1\alpha ]$²⁹ and, therefore, $\forall \alpha \in \mathcal {F}_1^\gamma [\gamma \sim _V^\omega \alpha ]$.

  Assume $\forall \alpha \in \mathcal {F}_1^\gamma [\gamma =\alpha \;\vee \;\lnot (\gamma =\alpha )]$. Applying Lemma 1, find p such that either $\forall \alpha \in \mathcal {F}_1^\gamma [ \overline{\gamma }p\sqsubset \alpha \rightarrow \gamma =\alpha ]$ or $\forall \alpha [ \overline{\gamma }p\sqsubset \alpha \rightarrow \lnot (\gamma =\alpha )]$, and note that both alternatives are false.

  Conclude: $\forall \gamma \lnot \forall \alpha [\gamma \sim _V^\omega \alpha \;\vee \lnot (\gamma =\alpha )]$.

$\square$

Lemma 9

$(\sim _V^{\lnot \lnot })^+\;\subseteq \;\;\sim _V^{\lnot \lnot }$ and $(\sim _V^{almost})^+\;\subseteq \;\;\sim _V^{almost}$.³⁰

Proof

Assume $\alpha (\sim _V^{\lnot \lnot })^+ \beta$.

Find n such that $\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim _V^{\lnot \lnot }\beta ]$.

Note: if $\exists m>n[\alpha (m)\ne \beta (m)]$, then $\alpha \sim _V^{\lnot \lnot } \beta$, and if $\lnot \exists m>n[\alpha (m)\ne \beta (m)]$, then $\forall m>n[\alpha (m)=\beta (m)]$ and $\alpha \sim _V\beta$ and also $\alpha \sim _V^{\lnot \lnot }\beta$.

Conclude: $\lnot \lnot (\alpha \sim _V^{\lnot \lnot }\beta )$, and, therefore, $\alpha \sim _V^{\lnot \lnot }\beta$.

Assume $\alpha (\sim _V^{almost})^+ \beta$.

Find n such that $\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha \sim _V^{almost}\beta ]$.

Let $\zeta$ in $[\omega ]^\omega$ be given. Note: $\zeta (n+1)>n$.

Either: $\alpha \circ \zeta (n+1)=\beta \circ \zeta (n+1)$

or: $\alpha \sim _V^{almost}\beta$ and $\exists p[\alpha \circ \zeta (p)=\beta \circ \zeta (p)]$.

We thus see: $\forall \zeta \in [\omega ]^\omega \exists n[\alpha \circ \zeta (n)=\beta \circ \zeta (n)]$, that is: $\alpha \sim _V^{almost}\beta$. $\square$

Lemma 10

For every shift-invariant binary relation R on $\mathcal {N}$,

$R^+\subseteq R$ if and only if $(\mathcal {N},=,R)\models \mathsf {\forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

Proof

First assume $R^+\subseteq R$.

Assume $\alpha \;\#\;\beta \rightarrow \alpha R \beta$.

Then: $\forall m>0[\alpha (m)\ne \beta (m)\rightarrow \alpha R\beta ]$, so: $\alpha R^+\beta$, and, therefore: $\alpha R\beta$.

We thus see: $(\mathcal {N},=,R)\models \mathsf {\forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

Now assume $(\mathcal {N},=,R)\models \mathsf {\forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

Assume $\alpha R^+\beta$. Find n such that $\forall m>n[\alpha (m)\ne \beta (m)\rightarrow \alpha R \beta ]$.

Define $\gamma , \delta$ such that $\forall m[\gamma (m)=\alpha (n+1+m)\;\wedge \;\delta (m) =\beta (n+1+m)]$.

Note: $\gamma \;\#\;\delta \rightarrow \alpha R \beta$, and, as R is shift-invariant, also: $\gamma \;\#\;\delta \rightarrow \gamma R \delta$, and, therefore: $\gamma R \delta$, and also: $\alpha R\beta$.

We thus see: $R^+\subseteq R$.$\square$

Corollary 6

• (i) $(\mathcal {N},=, \sim _V^{\lnot \lnot })\models \mathsf {\forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

• (ii) $(\mathcal {N},=, \sim _V^{almost})\models \mathsf {\forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

• (iii) For each R in $\mathcal {E}$, $(\mathcal {N},=,R)\models \mathsf {\lnot \forall x \forall y[}\bigl (AP(\mathsf {x,y)\rightarrow x\sim y\bigr )\rightarrow x\sim y]}$.

Proof

Use Lemmas 9 and 10 and Corollary 3. $\square$

1.13 Notations and Conventions

We use $m,n, \ldots$ as variables over the set $\omega =\mathbb {N}$ of the natural numbers.

For every $P\subseteq \mathbb {N}$ such that $\forall n[P(n)\;\vee \;\lnot P(n)]$, for all m,

$m=\mu n[P(n)]\leftrightarrow \bigl (P(m)\;\wedge \;\forall n<m[\lnot P(n)]\bigr )$.

$(m,n)\mapsto J(m,n)$ is a one-to-one surjective mapping from $\omega \times \omega$ onto $\omega$.

$K,L:\omega \rightarrow \omega$ are its inverse functions, so $\forall n[J\bigl (K(n), L(n)\bigr )=n]$.

For each n, $n':=K(n)$ and $n'':=L(n)$.

$(n_0, n_1, \ldots , n_{k-1})\mapsto \langle n_0, n_1, \ldots , n_{k-1}\rangle$ is a one-to-one surjective mapping from the set of finite sequences of natural numbers to the set of the natural numbers.

$\langle n_0, n_1, \ldots , n_{k-1}\rangle$ is the code of the finite sequence $(n_0, n_1, \ldots , n_{k-1})$.

$s\mapsto length(s)$ is is the function that, for each s, gives the length of the finite sequence coded by s.

$s,n\mapsto s(n)$ is the function that, for all s, n, gives the value of the finite sequence coded by s at n. If $n\ge length(s)$, then $s(n)=0$.

For all s, k, if $length(s)=k$, then $s=\langle s(0), s(1), \ldots s(k-1)\rangle$.

$0=\langle \;\rangle$ codes the empty sequence of natural numbers,

the unique finite sequence s such that $length(s)=0$.

$\omega ^k:=\{s\mid length(s)=k\}$.

$[\omega ]^k:=\{s\in \omega ^k\mid \forall i[i+1<k\rightarrow s(i)<s(i+1)]\}$.

$[\omega ]^{<\omega }:=\bigcup _k[\omega ]^k$.

For all s, k, t, l, if $s\in \omega ^k$ and $t\in \omega ^l$, then $s*t$ is the element u of $\omega ^{k+l}$ such that $\forall i<k[u(i)=s(i)]$ and $\forall j<l[u(k+j)=t(j)]$.

$s\sqsubseteq t\leftrightarrow \exists u[s*u =t]$.

$s\sqsubset t\leftrightarrow (s\sqsubseteq t \;\wedge \;s\ne t)$.

We use $\alpha , \beta , \ldots$ as variables over Baire space, the set $\omega ^\omega :=\mathcal {N}$ of functions from $\mathbb {N}$ to $\mathbb {N}$.

$(\alpha , n)\mapsto \alpha (n)$ is the function that associates to all $\alpha , n$, the value of $\alpha$ at n.

For all $\alpha , \beta$, $\alpha \circ \beta$ is the element $\gamma$ of $\mathcal {N}$ such that $\forall n[\gamma (n)=\alpha \bigl (\beta (n)\bigr )]$.

$2^\omega :=\mathcal {C}:=\{\alpha \mid \forall n[\alpha (n)<2]\}$ is Cantor space.

For all $\alpha$, for all k, for all s in $\omega ^k$, $\alpha \circ s$ is the element t of $\omega ^k$ satisfying

$\forall n<k[t(k)=\alpha \bigl (s(k)\bigr )]$.

For each s, k, if $s \in \omega ^k$, then, for each $\alpha$, $s*\alpha$ is the element $\beta$ of $\mathcal {N}$ such that $\forall i <k[\beta (i)=s(i)]$ and $\forall i[\beta (k+i)=\alpha (i)]$.

For each s, for each $\mathcal {X}\subseteq \mathcal {N}$, $s*\mathcal {X}:=\{s*\alpha \mid \alpha \in \mathcal {X}\}$.

For each $\alpha$, for each n, $\alpha ^n$ is the element of $\mathcal {N}$ satisfying $\forall m[\alpha ^n(m)=\alpha \bigl (J(n,m)\bigr )]$.

For each m, $\underline{m} \in \mathcal {N}$ is the element of $\mathcal {N}$ satisfying $\forall n[\underline{m}(n)=m]$.

S is the element of $\mathcal {N}$ satisfying $\forall n[S(n)=n+1]$.

$\forall n[\alpha '(n)=\bigl (\alpha (n)\bigr )'\;\wedge \;\alpha ''(n)=\bigl (\alpha (n)\bigr )'']$.

$\overline{\alpha }n :=\langle \alpha (0),\alpha (1), \ldots \alpha (n-1)\rangle$.

$s\sqsubset \alpha \leftrightarrow \exists n[\overline{\alpha }n =s]$.

$\alpha \perp \beta \leftrightarrow \alpha \;\#\;\beta \leftrightarrow \exists n[\alpha (n)\ne \beta (n)]$.

$[\omega ]^\omega :=\{\zeta \in \mathcal {N}\mid \forall i[\zeta (i)<\zeta (i+1)]\}$.

$\mathbb {Q}$, the set of the rationals, may be defined   as a subset of $\omega$, with accompanying relations $=_\mathbb {Q}$, $<_\mathbb {Q}$, $\le _\mathbb {Q}$ and operations $+_\mathbb {Q}, -_\mathbb {Q}, \cdot _\mathbb {Q}$.

$\mathcal {R}:=\{\alpha \mid \forall n[\alpha ' (n)\in \mathbb {Q}\;\wedge \; \alpha ''(n)\in \mathbb {Q}]\;\wedge \forall n[\alpha '(n)\le _\mathbb {Q}\alpha ' (n+1)\le _\mathbb {Q} \alpha ''(n+1)\le _\mathbb {Q}\alpha ''(n)]\;\wedge \;\forall m\exists n[\alpha ''(n)-_\mathbb {Q} \alpha '(n)<_\mathbb {Q} \frac{1}{2^m}]\}$.

For all $\alpha , \beta$ in $\mathcal {R}$,

$\alpha<_\mathcal {R}\beta \leftrightarrow \exists n[\alpha ''(n)<_\mathbb {Q}\beta '(n)]$ and $\alpha =_\mathcal {R}\beta \leftrightarrow \bigl (\lnot (\alpha<_\mathcal {R} \beta )\;\wedge \;\lnot (\beta <_\mathcal {R}\alpha )\bigr )$.

Operations $+_\mathcal {R}, -_\mathcal {R}$ are defined straightforwardly.