Reverse formalism 16

Abstract

In his remarkable paper Formalism 64, Robinson defends his eponymous position concerning the foundations of mathematics, as follows:

• (i) Any mention of infinite totalities is literally meaningless.

• (ii) We should act as if infinite totalities really existed.

Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that ‘some infinite totalities are more meaningful than others’, the textbook example being that of infinitesimals (versus less controversial infinite totalities). For instance, Bishop and Connes have made such claims regarding infinitesimals, and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate ‘meaning’ and ‘computational content’, though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the absence of meaning (i.e. computational content). We will debunk the Bishop–Connes critique by establishing the contrary, namely that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content (not involving Nonstandard Analysis), similar to the ‘reversals’ from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation.

Appendices

Appendix 1: The formal systems ${\textsf {P}}$ and ${\textsf {H}}$ in full detail

1.1 Gödel’s system T

In this section, we briefly introduce Gödel’s system T and the associated systems $\textsf {E-PA}^{\omega }$ and $\textsf {E-PA}^{\omega *}$. In his famous Dialectica paper (Gödel (1958)), Gödel defines an interpretation of intuitionistic arithmetic into a quantifier-free calculus of functionals. This calculus is now known as ‘Gödel’s system T’, and is essentially just primitive recursive arithmetic (Buss 1998, §1.2.10) with the schema of recursion expanded to all finite types. The set of all finite types $\pmb {T}$ is:

where 0 is the type of natural numbers, and $\sigma \rightarrow \tau$ is the type of mappings from objects of type $\sigma$ to objects of type $\tau$. Hence, Gödel’s system T includes ‘recursor’ constants $\pmb {R}^{\rho }$ for every finite type $\rho \in \pmb {T}$, defining primitive recursion as follows:

for $f^{\rho }$ and $g^{0\rightarrow ( \rho \rightarrow \rho )}$. The system $\textsf {E-PA}^{\omega }$ is a combination of Peano Arithmetic and system T, and the full axiom of extensionality E. The detailed definition of $\textsf {E-PA}^{\omega }$ may be found in (Kohlenbach 2008, §3.3); We do introduce the notion of equality and extensionality in $\textsf {E-PA}^{\omega }$, as these notions are needed below.

Definition 7.3

[Equality] The system $\textsf {E-PA}^{\omega }$ includes equality between natural numbers ‘$=_{0}$’ as a primitive. Equality ‘$=_{\tau }$’ for type $\tau$-objects x, y is then:

$$\begin{aligned}{}[x=_{\tau }y] \equiv (\forall z_{1}^{\tau _{1}}\dots z_{k}^{\tau _{k}})[xz_{1}\dots z_{k}=_{0}yz_{1}\dots z_{k}] \end{aligned}$$

(7.1)

if the type $\tau$ is composed as $\tau \equiv (\tau _{1}\rightarrow \dots \rightarrow \tau _{k}\rightarrow 0)$. The usual inequality predicate ‘$\le _{0}$’ between numbers has an obvious definition, and the predicate ‘$\le _{\tau }$’ is just ‘$=_{\tau }$’ with ‘$=_{0}$’ replaced by ‘$\le _{0}$’ in (7.1). The axiom of extensionality is the statement that for all $\rho , \tau \in \pmb {T}$, we have:

Next, we introduce $\textsf {E-PA}^{\omega *}$, a definitional extension of $\textsf {E-PA}^{\omega }$ from van den Berg et al. (2012) with a type for finite sequences. In particular, the set $\pmb {T}^{*}$ is defined as:

where $\sigma ^{*}$ is the type of finite sequences of objects of type $\sigma$. The system $\textsf {E-PA}^{\omega *}$ includes PR for all $\rho \in \pmb {T}^{*}$, as well as dedicated ‘list recursors’ to handle finite sequences for any $\rho ^{*}\in \pmb {T}^{*}$. A detailed definition of $\textsf {E-PA}^{\omega *}$ may be found in (van den Berg et al. 2012, §2.1). We now introduce some notations specific to $\textsf {E-PA}^{\omega *}$, as also used in van den Berg et al. (2012).

Notation 1.21 (Finite sequences) The system $\textsf {E-PA}^{\omega *}$ has a dedicated type for ‘finite sequences of objects of type $\rho$’, namely $\rho ^{*}$. Since the usual coding of finite sequences of natural numbers goes through in $\textsf {E-PA}^{\omega *}$, we shall not always distinguish between 0 and $0^{*}$. Similarly, we do not always distinguish between ‘$s^{\rho }$’ and ‘$\langle s^{\rho }\rangle$’, where the former is ‘the object s of type $\rho$’, and the latter is ‘the sequence of type $\rho ^{*}$ with only element $s^{\rho }$’. The empty sequence for the type $\rho ^{*}$ is denoted by ‘$\langle \rangle _{\rho }$’, usually with the typing omitted. Furthermore, we denote by ‘$|s|=n$’ the length of the finite sequence $s^{\rho ^{*}}=\langle s_{0}^{\rho },s_{1}^{\rho },\dots ,s_{n-1}^{\rho }\rangle$, where $|\langle \rangle |=0$, i.e. the empty sequence has length zero. For sequences $s^{\rho ^{*}}, t^{\rho ^{*}}$, we denote by ‘$s*t$’ the concatenation of s and t, i.e. $(s*t)(i)=s(i)$ for $i<|s|$ and $(s*t)(j)=t(|s|-j)$ for $|s|\le j< |s|+|t|$. For a sequence $s^{\rho ^{*}}$, we define $\overline{s}N:{=}\langle s(0), s(1), \dots , s(N)\rangle$ for $N^{0}<|s|$. For a sequence $\alpha ^{0\rightarrow \rho }$, we also write $\overline{\alpha }N=\langle \alpha (0), \alpha (1),\dots , \alpha (N)\rangle$ for any$N^{0}$. By way of shorthand, $q^{\rho }\in Q^{\rho ^{*}}$ abbreviates $(\exists i<|Q|)(Q(i)=_{\rho }q)$. Finally, we shall use $\underline{x}, \underline{y},\underline{t}, \dots$ as short for tuples $x_{0}^{\sigma _{0}}, \dots x_{k}^{\sigma _{k}}$ of possibly different type $\sigma _{i}$.

We have used $\textsf {E-PA}^{\omega }$ and $\textsf {E-PA}^{\omega *}$ interchangeably in this paper. Our motivation is the ‘star morphism’ used in Robinson’s approach to Nonstandard Analysis, and the ensuing potential for confusion.

1.2 The classical system ${\textsf {P}}$

In this section, we introduce the system ${\textsf {P}}$, a conservative extension of $\textsf {E-PA}^{\omega }$ with fragments of Nelson’s ${\textsf {IST}}$.

To this end, we first introduce the base system $\textsf {E-PA}_{\text {st}}^{\omega *}$. We use the same definition as (van den Berg et al. 2012, Def. 6.1), where E-PA$^{\omega *}$ is the definitional extension of E-PA$^{\omega }$ with types for finite sequences as in (van den Berg et al. 2012, §2). The set $\mathcal {T}^{*}$ is defined as the collection of all the terms in the language of $\textsf {E-PA}^{\omega *}$.

Definition 7.4

The system $\textsf {E-PA}^{\omega *}_{\text {st}}$ is defined as $\textsf {E-PA}^{\omega {*}} + \mathcal {T}^{*}_{\text {st}} + \textsf {IA}^{\text {st}}$, where $\mathcal {T}^{*}_{\text {st}}$ consists of the following axiom schemas.

• 1. The schema³⁰$\text {st}(x)\wedge x=y\rightarrow \text {st}(y)$,

• 2. The schema providing for each closed³¹ term $t\in \mathcal {T}^{*}$ the axiom $\text {st}(t)$.

• 3. The schema $\text {st}(f)\wedge \text {st}(x)\rightarrow \text {st}(f(x))$.

The external induction axiom IA$^{\text {st}}$ is as follows.

Secondly, we introduce some essential fragments of ${\textsf {IST}}$ studied in van den Berg et al. (2012).

Definition 7.7

[External axioms of ${\textsf {P}}$]

• 1. ${\textsf {HAC}}_{{\textsf {int}}}$: For any internal formula $\varphi$, we have

  $$\begin{aligned} (\forall ^{\text {st}}x^{\rho })(\exists ^{\text {st}}y^{\tau })\varphi (x, y)\rightarrow \big (\exists ^{\text {st}}F^{\rho \rightarrow \tau ^{*}}\big )(\forall ^{\text {st}}x^{\rho })(\exists y^{\tau }\in F(x))\varphi (x,y), \end{aligned}$$

  (7.2)

• 2. $\textsf {I}$: For any internal formula $\varphi$, we have

  $$\begin{aligned} (\forall ^{\text {st}} x^{\sigma ^{*}})(\exists y^{\tau } )(\forall z^{\sigma }\in x)\varphi (z,y)\rightarrow (\exists y^{\tau })(\forall ^{\text {st}} x^{\sigma })\varphi (x,y), \end{aligned}$$

• 3. The system ${\textsf {P}}$ is $\textsf {E-PA}_{\text {st}}^{\omega *}+\textsf {I}+{\textsf {HAC}}_{{\textsf {int}}}$.

Note that I and ${\textsf {HAC}}_{{\textsf {int}}}$ are fragments of Nelson’s axioms Idealisation and Standard part. By definition, F in (7.2) only provides a finite sequence of witnesses to $(\exists ^{\text {st}}y)$, explaining its name Herbrandized Axiom of Choice.

The system ${\textsf {P}}$ is connected to $\textsf {E-PA}^{\omega }$ by the following theorem. Here, the superscript ‘$S_{\text {st}}$’ is the syntactic translation defined in (van den Berg et al. 2012, Def. 7.1).

Theorem 7.5

Let ${\varPhi }(\underline{a})$ be a formula in the language of E-PA$^{\omega *}_{\text {st}}$ and suppose ${\varPhi }(\underline{a})^{S_{\text {st}{}}}\equiv \forall ^{\text {st}{}}\underline{x} \, \exists ^{\text {st}{}}\underline{y} \, \varphi (\underline{x}, \underline{y}, \underline{a})$. If ${\varDelta }_{{{\textsf {int}}}}$ is a collection of internal formulas and

$$\begin{aligned} \mathrm{\mathsf{P}} + {\varDelta }_{{{\textsf {int}}}} \vdash {\varPhi }(\underline{a}), \end{aligned}$$

(7.3)

then one can extract from the proof a sequence of closed³² terms t in $\mathcal {T}^{*}$ such that

$$\begin{aligned} \mathrm{\mathsf{E}}\hbox {-}\mathrm{\mathsf{PA}}^{\omega *} + {\varDelta }_{{{\textsf {int}}}} \vdash \ \forall \underline{x} \, \exists \underline{y}\in \underline{t}(\underline{x})\ \varphi (\underline{x},\underline{y}, \underline{a}). \end{aligned}$$

(7.4)

Proof

Immediate by (van den Berg et al. 2012, Theorem 7.7). $\square$

The proofs of the soundness theorems in (van den Berg et al. 2012, §5-7) provide an algorithm $\mathcal {A}$ to obtain the term t from the theorem. In particular, these terms can be ‘read off’ from the nonstandard proofs. The translation $S_{\text {st}}$ can be formalised in any reasonable³³ system of constructive mathematics. In fact, the formalisation of the results in van den Berg et al. (2012) in the proof assistant Agda (based on Martin-Löf’s constructive type theory Martin-Löf (1975)) is underway in Xu and Sanders (2015).

In light of the results in Sanders (2016a), the following corollary (which is not present in van den Berg et al. (2012)) is essential to our results. Indeed, the following corollary expresses that we may obtain effective results as in (7.6) from any theorem of Nonstandard Analysis which has the same form as in (7.5). It was shown in Sanders (2016a), Sanders (2015), Sanders (2016c) that the scope of this corollary includes the Big Five systems of Reverse Mathematics and the associated ‘zoo’ ([37]).

Corollary 7.6

If ${\varDelta }_{{{\textsf {int}}}}$ is a collection of internal formulas and $\psi$ is internal, and

$$\begin{aligned} \mathrm{\mathsf{P}} + {\varDelta }_{{{\textsf {int}}}} \vdash (\forall ^{\text {st}}\underline{x})(\exists ^{\text {st}}\underline{y})\psi (\underline{x},\underline{y}, \underline{a}), \end{aligned}$$

(7.5)

then one can extract from the proof a sequence of closed$^{32}$ terms t in $\mathcal {T}^{*}$ such that

$$\begin{aligned} \mathrm{\mathsf{E}}\hbox {-}\mathrm{\mathsf{PA}}^{\omega *} + {\varDelta }_{{{\textsf {int}}}} \vdash (\forall \underline{x})(\exists \underline{y}\in t(\underline{x}))\psi (\underline{x},\underline{y},\underline{a}). \end{aligned}$$

(7.6)

Proof

Clearly, if for internal $\psi$ and ${\varPhi }(\underline{a})\equiv (\forall ^{\text {st}}\underline{x})(\exists ^{\text {st}}\underline{y})\psi (x, y, a)$, we have $[{\varPhi }(\underline{a})]^{S_{\text {st}}}\equiv {\varPhi }(\underline{a})$, then the corollary follows immediately from the theorem. A tedious but straightforward verification using the clauses (i)-(v) in (van den Berg et al. 2012, Def. 7.1) establishes that indeed ${\varPhi }(\underline{a})^{S_{\text {st}}}\equiv {\varPhi }(\underline{a})$. $\square$

For the rest of this paper, the notion ‘normal form’ shall refer to a formula as in (7.5), i.e. of the form $(\forall ^{\text {st}}x)(\exists ^{\text {st}}y)\varphi (x,y)$ for $\varphi$ internal.

Finally, the previous theorems do not really depend on the presence of full Peano arithmetic. We shall study the following subsystems.

Definition 7.9

• 1. Let E-PRA$^{\omega }$ be the system defined in (Kohlenbach 2005, §2) and let E-PRA$^{\omega *}$ be its definitional extension with types for finite sequences as in (van den Berg et al. 2012, §2).

• 2. $({\textsf {QF-AC}}^{\rho , \tau })$ For every quantifier-free internal formula $\varphi (x,y)$, we have

  $$\begin{aligned} (\forall x^{\rho })(\exists y^{\tau })\varphi (x,y) \rightarrow (\exists F^{\rho \rightarrow \tau })(\forall x^{\rho })\varphi (x,F(x)) \end{aligned}$$

  (7.7)

• 3. The system ${\textsf {RCA}}_{0}^{\omega }$ is $\textsf {E-PRA}^{\omega }+{\textsf {QF-AC}}^{1,0}$.

The system ${\textsf {RCA}}_{0}^{\omega }$ is the ‘base theory of higher-order Reverse Mathematics’ as introduced in (Kohlenbach 2005, §2). We permit ourselves a slight abuse of notation by also referring to the system $\textsf {E-PRA}^{\omega *}+{\textsf {QF-AC}}^{1,0}$ as ${\textsf {RCA}}_{0}^{\omega }$.

Corollary 7.8

The previous theorem and corollary go through for ${\textsf {P}}$ and $\textsf {{E-PA}}^{\omega *}$ replaced by ${\textsf {P}}_{0}\equiv \textsf {{E-PRA}}^{\omega *}+\mathcal {T}_{\text {st}}^{*} +{\textsf {HAC}}_{{\textsf {int}}} +\textsf {{I}}+{\textsf {QF-AC}}^{1,0}$ and ${\textsf {RCA}}_{0}^{\omega }$.

Proof

The proof of (van den Berg et al. 2012, Theorem 7.7) goes through for any fragment of E-PA$^{\omega {*}}$ which includes EFA, sometimes also called $\textsf {I}{\varDelta }_{0}+\textsf {EXP}$. In particular, the exponential function is (all what is) required to ‘easily’ manipulate finite sequences. $\square$

1.3 The constructive system ${\textsf {H}}$

In this section, we define the system ${\textsf {H}}$, the constructive counterpart of ${\textsf {P}}$. The system $\textsf {H}$ was first introduced in (van den Berg et al. 2012, §5.2), and constitutes a conservative extension of Heyting arithmetic ${\textsf {E-HA}}^{\omega }$ by (van den Berg et al. 2012, Cor. 5.6). We now study the system ${\textsf {H}}$ in more detail.

Similar to Definition 7.3, we define $\textsf {E-HA}^{\omega *}_{\text {st}}$ as $\textsf {E-HA}^{\omega {*}} + \mathcal {T}^{*}_{\text {st}} + \textsf {IA}^{\text {st}}$, where $\textsf {E-HA}^{\omega *}$ is just $\textsf {E-PA}^{\omega *}$ without the law of excluded middle. Furthermore, we define

$$\begin{aligned} {\textsf {H}}\equiv {\textsf {E-HA}}^{\omega *}_{\text {st}}+{\textsf {HAC}}+ {{\textsf {\text {I}}}}+{\textsf {NCR}}+\textsf {HIP}_{\forall ^{\text {st}}}+\textsf {HGMP}^{\text {st}}, \end{aligned}$$

where ${\textsf {HAC}}$ is ${\textsf {HAC}}_{{\textsf {int}}}$ without any restriction on the formula, and where the remaining axioms are defined in the following definition.

Definition 1.28   [Three axioms of ${\textsf {H}}$]

• 1. $\textsf {HIP}_{\forall ^{\text {st}}}$

  $$\begin{aligned}{}[(\forall ^{\text {st}}x)\phi (x)\rightarrow (\exists ^{\text {st}}y){\varPsi }(y)]\rightarrow (\exists ^{\text {st}}y')[(\forall ^{\text {st}}x)\phi (x)\rightarrow (\exists y\in y'){\varPsi }(y)], \end{aligned}$$

  where ${\varPsi }(y)$ is any formula and $\phi (x)$ is an internal formula of E-HA$^{\omega *}$.

• 2. $\textsf {HGMP}^{\text {st}}$

  $$\begin{aligned}{}[(\forall ^{\text {st}}x)\phi (x)\rightarrow \psi ] \rightarrow (\exists ^{\text {st}}x')[(\forall x\in x')\phi (x)\rightarrow \psi ] \end{aligned}$$

  where $\phi (x)$ and $\psi$ are internal formulas in the language of E-HA$^{\omega *}$.

• 3. NCR

  $$\begin{aligned} (\forall y^{\tau })(\exists ^{\text {st}} x^{\rho } ){\varPhi }(x, y) \rightarrow (\exists ^{\text {st}} x^{\rho ^{*}})(\forall y^{\tau })(\exists x'\in x ){\varPhi }(x', y), \end{aligned}$$

  where ${\varPhi }$ is any formula of E-HA$^{\omega *}.$

Intuitively speaking, the first two axioms of Definition 7.9 allow us to perform a number of non-constructive operations (namely Markov’s principle and independence of premises) on the standard objects of the system ${\textsf {H}}$, provided we introduce a ‘Herbrandisation’ as in the consequent of ${\textsf {HAC}}$, i.e. a finite list of possible witnesses rather than one single witness. Furthermore, while ${\textsf {H}}$ includes idealisation I, one often uses the latter’s classical contraposition, explaining why NCR is useful (and even essential) in the context of intuitionistic logic.

Surprisingly, the axioms from Definition 7.9 are exactly what is needed to convert nonstandard definitions (of continuity, integrability, convergence, et cetera) into the normal form $(\forall ^{\text {st}}x)(\exists ^{\text {st}}y)\varphi (x, y)$ for internal $\varphi$, as is clear from e.g. Sect. 5.3. The latter normal form plays an equally important role in the constructive case as in the classical case by the following theorem.

Theorem 7.10

If ${\varDelta }_{{{\textsf {int}}}}$ is a collection of internal formulas, $\varphi$ is internal, and

$$\begin{aligned} \mathrm{\mathsf{H}} + {\varDelta }_{{{\textsf {int}}}} \vdash \forall ^{\text {st}{}}\underline{x} \, \exists ^{\text {st}{}}\underline{y} \, \varphi (\underline{x}, \underline{y}, \underline{a}), \end{aligned}$$

(7.8)

then one can extract from the proof a sequence of closed terms t in $\mathcal {T}^{*}$ such that

$$\begin{aligned} \mathrm{\mathsf{E}}\hbox {-}\mathrm{\mathsf{HA}}^{\omega *} + {\varDelta }_{{{\textsf {int}}}} \vdash \ \forall \underline{x} \, \exists \underline{y}\in \underline{t}(\underline{x})\ \varphi (\underline{x},\underline{y}, \underline{a}). \end{aligned}$$

(7.9)

Proof

Immediate by (van den Berg et al. 2012, Theorem 5.9). $\square$

The proofs of the soundness theorems in (van den Berg et al. 2012, §5-7) provide an algorithm $\mathcal {B}$ to obtain the term t from the theorem. Finally, we point out one very useful principle to which we have access.

Theorem 7.11

The systems P, H, and P$_{0}$ prove overspill, i.e.

for any internal formula $\varphi$.

Proof

See (van den Berg et al. 2012, Prop. 3.3). $\square$

In conclusion, we have introduced the systems ${\textsf {H}}$, ${\textsf {P}}$, which are conservative extensions of Peano and Heyting arithmetic with fragments of Nelson’s internal set theory. We have observed that central to the conservation results (Corollary 7.6 and Theorem 7.5) is the normal form $(\forall ^{\text {st}}x)(\exists ^{\text {st}}y)\varphi (x, y)$ for internal $\varphi$.

Appendix 2: Nonstandard analysis and qualitative information

We list examples of applications of Nonstandard Analysis in which the latter is explicitly used to model qualitative phenomena.

• 1. Raiman (1986, 1991) introduces a formal language FOG for reasoning with qualitative notions ‘close’, ‘negligible’, and ‘same order of magnitude’. Raiman proves FOG to be validated in Robinson’s Non-standard Analysis Robinson (1966). The system FOG has been used in economics and circuit design (Dague et al. 1987; Bourgine and Raiman 1986).

• 2. Weld studies the perturbation technique exaggeration in Weld (1990) by means of Nonstandard Analysis. In particular, he uses unlimited and infinitesimal values to study the limit behaviour for ‘large’ and ‘small’ parameter values.

• 3. Davis presents a system based on Nonstandard Analysis for reasoning with qualitative notions like ‘small’, ‘large’, and ‘medium’. Results in dynamical systems and differential equations are obtained Davis (1990).

• 4. Suenaga et al. provide deductive verification framework of signals based on Nonstandard Analysis in (Suenaga et al. 2013). Rather than using approximations up to some large finite precision, they use a correct-up-to-infinitesimals approximation using unlimited precision.

• 5. Vopenka (1991) proposes the use of various nonstandard structures (inside his alternative set theoryAST) to model vague phenomena.

• 6. Tzouvaras (1998) proposes the use of Nonstandard Analysis to model vague notions like ‘similarity’ and ‘small’.

In light of the previous list, we hope the reader is convinced that Nonstandard Analysis can be used to model qualitative notions. The usual caveat applies: We do not claim that this modelling is the best or even accurate; we merely point out that people have used Nonstandard Analysis for this purpose in practice.

Appendix 3: Some theorems relating to term extraction

Theorem 9.1

The system P proves that a normal form can be derived from an implication between normal forms.

Proof

Let $\varphi , \psi$ be internal and consider the following implication between normal forms:

$$\begin{aligned} (\forall ^{\text {st}}x)(\exists ^{\text {st}}y)\varphi (x, y)\rightarrow (\forall ^{\text {st}}z)(\exists ^{\text {st}}w)\psi (z, w). \end{aligned}$$

(9.1)

Since standard functionals have standard output for standard input by Definition 7.3, (9.1) implies

$$\begin{aligned} (\forall ^{\text {st}}\zeta )\big [(\forall ^{\text {st}}x)\varphi (x, \zeta (x))\rightarrow (\forall ^{\text {st}}z)(\exists ^{\text {st}}w)\psi (z, w)\big ]. \end{aligned}$$

(9.2)

Bringing all standard quantifiers outside, we obtain the following normal form:

$$\begin{aligned} (\forall ^{\text {st}}\zeta , z)(\exists ^{\text {st}} w, x)\big [\varphi (x, \zeta (x))\rightarrow \psi (z, w)\big ], \end{aligned}$$

(9.3)

as the formula in square brackets is internal. $\square$

It is an interesting exercise to establish the previous theorem for ${\textsf {H}}$ in the stead of ${\textsf {P}}$.

Theorem 9.2

For internal $\varphi$, the system P proves that $(\forall \varepsilon \approx 0)(\forall ^{\text {st}}x)(\exists ^{\text {st}}y^{\tau })\varphi (x, y, \varepsilon )$ is equivalent to a normal form.

Proof

Written out in full, the initial formula from the theorem is:

$$\begin{aligned} \textstyle (\forall \varepsilon )\big [(\forall ^{\text {st}} k^{0})(|\varepsilon |<\frac{1}{k})\rightarrow (\forall ^{\text {st}}x)(\exists ^{\text {st}}y^{\tau })\varphi (x, y, \varepsilon )\big ], \end{aligned}$$

and bringing outside all standard quantifiers as far as possible:

$$\begin{aligned} \textstyle (\forall ^{\text {st}}x)\underline{(\forall \varepsilon )(\exists ^{\text {st}}y^{\tau }, k^{0})\big [|\varepsilon |<\frac{1}{k}\rightarrow \varphi (x, y, \varepsilon )\big ]}, \end{aligned}$$

the underlined formula is suitable for Idealisation. Applying the latter yields

$$\begin{aligned} \textstyle (\forall ^{\text {st}}x)(\exists ^{\text {st}}w^{0^{*}}, z^{\tau ^{*}}){(\forall \varepsilon )(\exists y^{\tau } \in z, k^{0}\in w)\big [|\varepsilon |<\frac{1}{k}\rightarrow \varphi (x, y, \varepsilon )\big ]}, \end{aligned}$$

and let $N^{0}$ be the maximum of all w(i) for $i<|w|$. We obtain:

$$\begin{aligned} \textstyle (\forall ^{\text {st}}x)(\exists ^{\text {st}}z^{\tau ^{*}}, N){(\forall \varepsilon )(\exists y^{\tau }\in z)\big [|\varepsilon |<\frac{1}{N}\rightarrow \varphi (x, y, \varepsilon )\big ]}. \end{aligned}$$

(9.4)

Clearly, (9.4) implies the initial formula from the theorem. $\square$

Appendix 4: Examples in reverse mathematics of the computational content of nonstandard analysis

1.1 Theorems equivalent to ${\textsf {ACA}}_{0}$

In this section, we study the monotone convergence theoremMCT, i.e. the statement that every bounded increasing sequence of reals is convergent, which is equivalent to arithmetical comprehension ${\textsf {ACA}}_{0}$ by (Simpson 2009, III.2.2). We prove an equivalence between a nonstandard version of $\mathrm {\textsf {MCT}}$ and a fragment of Transfer. From this nonstandard equivalence, we obtain an effective RM equivalence involving $\mathrm {\textsf {MCT}}$ and arithmetical comprehension.

Firstly, the nonstandard version of $\mathrm {\textsf {MCT}}$ (involving nonstandard convergence) is:

where ‘$(\forall K\in {\varOmega })(\dots )$’ is short for $(\forall K^{0}))(\lnot \text {st}(K)\rightarrow \dots )$. The effective version MCT$_{\textsf {ef}}(t)$:

$$\begin{aligned} \textstyle (\forall c_{(\cdot )}^{0\rightarrow 1},k^{0})\big [(\forall n^{0})(c_{n}\le c_{n+1}\le 1)\rightarrow (\forall N,M\ge t(c_{(\cdot )})(k))[|c_{M}- c_{N}|\le \frac{1}{k} ] \big ]. \end{aligned}$$

(10.1)

We require two equivalent (Kohlenbach 2005, Prop. 3.9) versions of arithmetical comprehension:

Clearly, $(\exists ^{2})$ (and therefore $(\mu ^{2})$) is the functional version of ${\textsf {ACA}}_{0}$. We also recall the restriction of Nelson’s axiom Transfer as follows:

Denote by $\textsf {MU}(\mu )$ the formula in square brackets in $\mu ^{2}$. We have the following theorem which establishes the explicit equivalence between $(\mu ^{2})$ and uniform $\mathrm {\textsf {MCT}}$.

Theorem 10.1

We have P$\vdash$MCT$_{{\textsf {ns}}}\leftrightarrow {\varPi }_{1}^{0}$-TRANS. From this proof, terms s, u can be extracted such that E-PA$^{\omega *}$ proves:

(10.2)

Proof

See (Sanders 2016a, §4.1). $\square$

We point out (10.2) is the ‘effective’ version of the equivalence ${\textsf {ACA}}_{0}\leftrightarrow \mathrm {\textsf {MCT}}$; the former is obtained from the corresponding ‘nonstandard’ equivalence ${\varPi }_{1}^{0}{-\textsf {TRANS}}\leftrightarrow \mathrm {\textsf {MCT}}_{{\textsf {ns}}}$. Note that the latter proof proceeds by contradiction.

Finally, while we did not emphasise this in Sect. 2, Reverse Mathematics usually studies mathematical theorems formalised in second-order arithmetic. The latter only involves natural numbers and sets thereof, i.e. continuous functions on the real numbers are indirectly present in the form of codes (See Kohlenbach 2002, §4). Now, (10.2) is clearly not part of second-order arithmetic (as it involves objects of type two), but it is possible to obtain results in second-order arithmetic from (10.2), as explored in Sanders (2017).

1.2 Theorems equivalent to ${\textsf {ATR}}_{0}$ and ${\varPi }_{1}^{1}{\hbox {-}\textsf {CA}}_{0}$

In this section, we study equivalences relating to ${\textsf {ATR}}_{0}$ and ${\varPi }_{1}^{1}{\hbox {-}\textsf {CA}}_{0}$, the strongest Big Five systems. We shall work with the Suslin functional$(S^{2})$, the functional version of ${\varPi }_{1}^{1}{\hbox {-}\textsf {CA}}_{0}$.

Feferman has introduced the following version of the Suslin functional (See e.g. Avigad and Feferman (1998)).

where the formula in square brackets is ${\textsf {MUO}}(\mu _{1})$. We require another instance of Transfer:

We first consider ${\textsf {PST}}$, i.e. the statement that every tree with uncountably many paths has a non-empty perfect subtree. As proved in (Simpson (2009), V.5.5), we have ${\textsf {PST}}\leftrightarrow {\textsf {ATR}}_{0}$ and a uniform version of ${\textsf {PST}}$ is equivalent to the Suslin functional by (Sakamoto and Yamazaki 2004, Theorem 4.4). Now, ${\textsf {PST}}$ has the following nonstandard and uniform versions.

Theorem 10.2

(PST$_{{{\mathbf {\mathsf{{ns}}}}}}$) For all standard trees $T^{1}$, there is standard $P^{1}$ such that

$$\begin{aligned} (\forall f_{(\cdot )}^{0\rightarrow 1})(\exists f\in T)(\forall n)(f_{n}\ne _{1} f) \rightarrow P \text {is a non-empty perfect subtree of} T. \end{aligned}$$

Theorem 10.3

(PST$_{{{\mathbf {\mathsf{{ef}}}}}}(t)$) For all trees $T^{1}$, we have

$$\begin{aligned} (\forall f_{(\cdot )}^{0\rightarrow 1})(\exists f\in T)(\forall n)(f_{n}\ne _{1} f) \rightarrow t(T)\text { is a non-empty perfect subtree of} T. \end{aligned}$$

As a technicality, we require that P as in the previous two principles consists of a pair $(P', p')$ such that $P'$ is a perfect subtree of T such that $p'\in P'$.

Theorem 10.4

We have P$\vdash$PST$_{{\textsf {ns}}}\leftrightarrow {\varPi }_{1}^{1}$-TRANS. From the latter, terms s, u can be extracted such that ${\textsf {E-PA}}^{\omega *}$ proves:

(10.3)

Proof

See (Sanders 2016a, §4.5). $\square$

In conclusion, (10.3) is the ‘effective’ version of (Sakamoto and Yamazaki 2004, Theorem 4.4); the former is obtained from the corresponding ‘nonstandard’ equivalence ${\varPi }_{1}^{1}\hbox {-}{\textsf {TRANS}}\leftrightarrow {\varPi }_{1}^{1}$-TRANS. Note that the latter proof proceeds by contradiction.

Another more mathematical statement which can be treated along the same lines is every countable Abelian group is a direct sum of a divisible and a reduced group. The latter is called ${\textsf {DIV}}$ and equivalent to ${\varPi }_{1}^{1}{\hbox {-}\textsf {CA}}_{0}$ by (Simpson 2009, VI.4.1). By the proof of the latter, the reverse implication is straightforward; We shall therefore study ${\textsf {DIV}}\rightarrow {\varPi }_{1}^{1}{\hbox {-}\textsf {CA}}_{0}$.

To this end, let ${\textsf {DIV}}(G, D, E)$ be the statement that the countable Abelian group G satisfies $G=D\oplus E$, where D is a divisible group and E a reduced group. The nonstandard version of ${\textsf {DIV}}$ is as follows:

where we used the same technicality as for PST$_{{\textsf {ns}}}$. The effective version is:

We have the following theorem.

Theorem 10.5

We have have P$\vdash$DIV$_{{\textsf {ns}}}\rightarrow {\varPi }_{1}^{1}$-TRANS. From the latter, a term u can be extracted such that E-PA$^{\omega *}$ proves:

(10.4)

Proof

See (Sanders 2015, §4.5). $\square$