On Algorithm and Robustness in a Non-standard Sense

Abstract

In this paper, we investigate the invariance properties, i.e. robustness, of phenomena related to the notions of algorithm, finite procedure and explicit construction. First of all, we provide two examples of objects for which small changes completely change their (non)computational behavior. We then isolate robust phenomena in two disciplines related to computability.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The object -or better concept- of study in Computer Science is unsurprisingly computation. The notions of algorithm, finite procedure and explicit computation are central. The present paper investigates the robustness of these notions, i.e. we are interested in phenomena regarding computation which are reasonably stable under variations of parameters. Let us first consider two illuminating examples of non-robust phenomena in Computer Science.

Example 1.

Recently¹ the following remarkable mathematical object was developed: a pair of computable ² random variables (X, Y ) for which the conditional distribution P[Y | X] is non-computable ^??, as it codes the Halting Problem ^??. Let CAM be the statement that such (X, Y ) exists. Before trotting out all sorts of indispensability claims based on CAM, one should bear in mind that the conditional distribution P[Y | X] becomes computable again³, after the addition to Y of some kind of generic noise E. Let CAM _E be the statement that P[Y + E, X] is computable, for computable (X, Y ) and generic noise E. Evidently, we may see CAM _E as a variation of CAM involving an error parameter. However, the (non)computational content of CAM is completely different from that of CAM _E . Indeed, the addition of the noise E dramatically changes the non-computability of P[Y, X], and hence the computational content of CAM _E , compared to CAM. In short, the computational behavior of P[Y | X] is sensitive to minor perturbations and CAM is non-robust with regard to the addition of error parameters.

Example 2.

In Constructive Analysis⁴, the notion of finite procedure is central. An object only exists after it has been constructed (in finitely many steps). The following is a well-known negative result of the constructive school: Given a uniformly continuous function on [0, 1] such that f(1) < 0 and f(0) > 0, we cannot in general construct x ₀ ∈ [0, 1] such that f(x ₀) = 0. In other words, the intermediate value theorem, INT for short, cannot be proved in Constructive Analysis. By contrast, we have the following positive result, called INT _E : Given $\epsilon \in \mathbb{R}$ and given a uniformly continuous function on [0, 1] such that f(1) < 0 and f(0) > 0, we can construct x ₀ such that | f(x ₀) |  < ε. Again, we may see INT _E as a variation of INT involving an error parameter. Analogous to the previous example, the computational behavior of the intermediate value is sensitive to minor perturbations: the addition of an error term makes the former computable (in the sense of Constructive Analysis). In other words, INT also exhibits computational non-robustness with regard to the addition of error parameters.

The previous examples provide phenomena regarding computation that are destroyed by a minor variation. In this paper, we intend to identify phenomena regarding computation that are not affected by certain variations (like perturbation of parameters). In other words, we are looking for robust behavior in topics related to Computer Science. The importance of robustness cannot be overestimated, as our scientific models of reality are only approximations and tend to incorporate imprecise assumptions, often for valid reasons such as workability, elegance or simplicity. Thus, if a phenomenon X occurs in a robust model, we are reasonably certain that X cannot be ascribed to an artifact of the model, but corresponds to a real-world phenomenon X′.

A similar point has been made in the past by Ian Hacking and Wesley Salmon. In particular, the numerous independent ways of deriving Avogadro’s constant (with negligible errors) are taken by Hacking and Salmon to be sufficient evidence for the real-world existence of molecules and atoms.⁵ Another example from Hacking is concerned with the photo-electric effect.

The simple inference argument says it would be an absolute miracle if for example the photoelectric effect went on working while there were no photons. The explanation of the persistence of this phenomenon […] is that photons do exist. As J. J. C. Smart expresses the idea: ‘One would have to suppose that there were innumerable lucky accidents about the behavior mentioned in the observational vocabulary, so that they behaved miraculously as if they were brought about by the non-existent things ostensibly talked about in the theoretical vocabulary.’ The realist then infers that photons are real […] (Hacking 1983, pp. 54-55).

In general, numerous independent derivations of the same phenomenon make it implausible that the latter is an artifact of a particular framework or modeling assumption, i.e. the phenomenon in question is about something real⁶. Hence, by seeking out the robust phenomena involving computation, we may get a better understanding of the real core of computation, while at the same time develop a better theory of what exactly constitutes robustness.

We begin our search in two disciplines related to computability, Reverse Mathematics and Constructive Analysis, both introduced below. First, in Section 2, we study the invariance properties present in Reverse Mathematics, a discipline intimately connected to computability. Secondly, we do the same for Errett Bishop’s constructive notion of algorithm from Constructive Analysis in Section 3.

2 Reverse Mathematics

In this section, we identify certain invariance properties in Reverse Mathematics. The latter is closely related to Recursion Theory, a classical framework for studying (non)computability. A central object in Recursion Theory is the Turing machine ⁷, introduced next.

2.1 Alan Turing’s Machine and Recursion Theory

In 1928, the famous mathematician David Hilbert posed the Entscheidungsproblem. In modern language, the Entscheidungsproblem (or ‘decision problem’) asks for no less than the construction of an algorithm that decides the truth or falsity of a mathematical statement. In other words, such an algorithm takes as input a mathematical statement (in a suitable formal language) and outputs ‘true’ or ‘false’ after a finite period of time.

Before the Entscheidungsproblem could be solved, a formal definition of algorithm was necessary. Both Alonzo Church and Alan Turing provided such a formalism,⁷ being the λ-calculus and the Turing machine, respectively. Church showed that, if the notion algorithm is formalized using the λ-calculus, then the construction required to solve the Entscheidungsproblem is impossible. Independently, Turing showed that the Entscheidungsproblem can be reduced to the Halting Problem, which is known to have no algorithmic solution, assuming ‘algorithm’ is identified with ‘computation on a Turing Machine’. In time, it was shown that both formalisms, though quite different in nature, enable the computation of the same class of functions, now called the recursive functions. The latter class was intended to formalize the notion of recursion, later giving rise to Recursion Theory.

Because of the correspondence between these three formalisms, it is generally accepted that we should identify the (informal and vague) class of algorithmically computable functions with the class of function computable by a Turing machine. This identification hypothesis is called the Church-Turing thesis. However, as suggested by Example 1, not all computability phenomena are robust. In the next section, we identify a phenomenon in Reverse Mathematics which is.

2.2 Reverse Mathematics and Robustness

Reverse Mathematics is a program in the Foundations of Mathematics founded⁸ in the Seventies by Harvey Friedman. Stephen Simpson’s famous monograph Subsystems of Second-order Arithmetic is the standard reference.⁹ The goal of Reverse Mathematics is to determine the minimal axiom system necessary to prove a particular theorem of ordinary mathematics. Classifying theorems according to logical strength reveals the following striking phenomenon.⁹

It turns out that, in many particular cases, if a mathematical theorem is proved from appropriately weak set existence axioms, then the axioms will be logically equivalent to the theorem.

This phenomenon is dubbed the ‘Main theme’ of Reverse Mathematics. A good instance of the latter may be found in the Reverse Mathematics of WKL₀ ¹⁰. An example of the Main Theme is that the logical principle WKL is equivalent to Peano’s existence theorems for ordinary differential equations y′ = f(x, y), the equivalence being provable in RCA₀. Some explanation might be in order: the system RCA₀ may be viewed as the logical formalization of the notion Turing machine, which in turn formalizes the notion of algorithm.¹¹ The principle WKL (or Weak König’s Lemma) states the existence of certain non-computable objects.¹²

We now consider the system¹³ ERNA which has no a priori connection to RCA₀, or Reverse Mathematics, or computability¹⁴. We will show that a version of the Main Theme of Reverse Mathematics is also valid in ERNA, but with the predicate ‘ = ’ replaced by ‘ ≈ ’, i.e. equality up to infinitesimals from Nonstandard Analysis.¹⁵ Indeed, the following theorem contains several statements, translated from (Simpson 2009, IV) into ERNA’s language, while preserving equivalence.

Theorem 3

(Reverse Mathematics for ERNA + ∏ ₁-TRANS) The theory ERNA proves the equivalence between ∏ ₁ -TRANS and each of the following theorems concerning near-standard functions:

• 1. Every S-continuous function on [0, 1] is bounded.

• 2. Every S-continuous function on [0, 1] is continuous there.

• 3. Every S-continuous function on [0, 1] is Riemann integrable ¹⁶.

• 4. Weierstrass’ theorem: every S-continuous function on [0, 1] has, or attains a supremum, up to infinitesimals.

• 5. The strong Brouwer fixed point theorem: every S-continuous function ϕ : [0, 1] → [0, 1] has a fixed point up to infinitesimals of arbitrary depth.

• 6. The first fundamental theorem of calculus: $\left( \int_{0}^{x} f(t)dt\right)^{\prime} \approx f(x)$.

• 7. The Peano existence theorem for differential equations y′ ≈ f(x,y).

• 8. The Cauchy completeness, up to infinitesimals, of ERNA ’s field.

• 9. Every S-continuous function on [0, 1] has a modulus of uniform continuity.

• 10. The Weierstrass approximation theorem.

A common feature of the items in the previous theorem is that strict equality has been replaced with ≈ , i.e. equality up to infinitesimals. This seems the price to be paid for ‘pushing down’ into ERNA the theorems equivalent to Weak König’s lemma. For instance, item (7) from Theorem 3 guarantees the existence of a function $\phi(x)$ such that $\phi^\prime(x) \approx f(x,\phi(x))$, i.e. a solution, up to infinitesimals, of the differential equation y′ = f(x, y). However, in general, there is no function $\psi(x)$ such that $\psi^\prime(x) = f(x, \psi(x))$ in ERNA + ∏ ₁ -TRANS. In this way, we say that the Reverse Mathematics of ERNA + ∏ ₁ -TRANS is a copy up to infinitesimals of the Reverse Mathematics of WKL₀, suggesting the following general principle¹⁷.

Principle 4

Let T(=) be a theorem of ordinary mathematics, involving equality. If RCA ₀ proves T(=) ⇔ WKL, then ERNA proves T(≈) ⇔ ∏ ₁ -TRANS.

Furthermore, there are more results of this nature. In a forthcoming paper, we show examples of the following general principle¹⁸.

Principle 5

Let T(=) be a theorem of ordinary mathematics, involving equality. If RCA ₀ proves T(=) ⇔ WKL, then $\rm ERNA + {\Pi }_{2}\textrm{ -TRANS}$ proves T(≋) ⇔ ∏₃-TRANS.

Here, the predicate ‘≋’ is best described as ‘equality up to arbitrarily small infinitesimals’. At least two more variations¹⁹ are possible and in each instance, we obtain a similar principle concerning equivalences.

We conclude that the equivalences proved in Reverse Mathematics display a certain degree of robust behavior: First of all, we observe similar series of equivalences in different frameworks. In other words, the equivalences observed in classical Reverse Mathematics are not an artifact of the framework, as they occur elsewhere in similar forms. Secondly, the equivalences in classical Reverse Mathematics remain valid when we consider different error predicates, i.e. replace equality by ‘ ≈ ’ or ‘≋’. Thus, small perturbations in the form of error predicates do not destroy the observed equivalences.

3 Reuniting the antipodes

In this section²⁰, we show that the notion of algorithm in Constructive Analysis is endowed with a degree of robustness. This is achieved indirectly by defining a new notion called ‘Ω-invariance’ inside Nonstandard Analysis, and showing that it is close to the constructive notion of algorithm, as it gives rise to the same kind of Reverse Mathematics results. In other words, there are two different notions of finite procedure, i.e. the constructive notion of algorithm and Ω-invariance, which both give rise to the same kind of equivalences in (Constructive) Reverse Mathematics. Again, we observe that the latter are not affected by some change of framework.

3.1 The notion of finite procedure in Nonstandard Analysis

Here, we define Ω-invariance, a central notion, inside (classical) Nonstandard Analysis. We show that Ω-invariance is quite close to the notion of finite procedure.

With regard to notation, we take $\mathbb{N} =\{ 0,1,2,\ldots \,\}$ to denote the set of natural numbers, which is extended to ${}{{^\ast}}\mathbb{N} =\{ 0,1,2,\ldots,\omega,\omega + 1,\ldots \,\}$, the set of hypernatural numbers, with $\omega \not\in \mathbb{N}$. The set $\Omega {= }{^{\ast}}\mathbb{N} \setminus \mathbb{N}$ consists of the infinite numbers, whereas the natural numbers are finite. Finally, a formula is bounded or ‘Δ₀’, if all the quantifiers are bounded by terms and no infinite numbers occur.

Definition 6 (Ω-invariance)

Let ψ(n,m) be Δ ₀ and fix ω ∈ Ω.

The formula ψ(n,ω) is Ω-invariant if

$$(\forall n \in \mathbb{N})(\forall \omega ^\prime \in \Omega )(\psi (n,\omega ) \leftrightarrow \psi (n,\omega ^\prime )).$$

(1)

For $f : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ , the function f(n,ω) is called Ω-invariant, if

$$(\forall n \in \mathbb{N})(\forall \omega ^\prime \in \Omega )(f(n,\omega ) = f(n,\omega ^\prime )).$$

(2)

Now, any object φ(ω) defined using an infinite number ω is potentially non-computable, as infinite numbers can code (non-recursive) sets of natural numbers.²¹ Hence, it is not clear how an Ω-invariant object might be computable or constructive in any sense. However, although an Ω-invariant object clearly involves an infinite number, the object does not depend on the choice of the infinite number, by definition. Furthermore, by the following theorem, the truth value of ψ(n, ω) and the value of f(n, ω) is already determined at some finite number.

Theorem 7 (Modulus lemma)

For every Ω-invariant formula ψ(n,ω),

$$(\forall n \in \mathbb{N})(\exists {m}_{0} \in \mathbb{N})(\forall m,m^\prime {\in }{{^\ast}}\mathbb{N})[m,m^\prime \geq {m}_{ 0} \rightarrow \psi (n,m) \leftrightarrow \psi (n,m^\prime )].$$

For every Ω-invariant function f(n,ω), we have

$$(\forall n \in \mathbb{N})(\exists {m}_{0} \in \mathbb{N})(\forall m,m^\prime {\in }{{^\ast}}\mathbb{N})[m,m^\prime \geq {m}_{ 0} \rightarrow f(n,m) = f(n,m^\prime )].$$

In each case, the number m ₀ is computed by an Ω-invariant function.

Proof.

Although the proof of this lemma is outside of the scope of this paper, it is worth mentioning that it makes essential use of the fact that an Ω-invariant object does not depend on the choice of infinite number.

The previous theorem is called ‘modulus lemma’ as it bears a resemblance to the modulus lemma from Recursion Theory.²² Intuitively, our modulus lemma states that the properties of an Ω-invariant object are already determined at some finite number. This observation suggests that the notion of Ω-invariance models the notion of finite procedure quite well.

Another way of interpreting Ω-invariance is as follows: central to any version of constructivism is that there are basic objects (e.g. the natural numbers) and there are certain basic operations on these objects (e.g. recursive functions or constructive algorithms). All other objects are non-basic (aka ‘non-constructive’ or ‘ideal’), and are to be avoided, as they fall outside the constructive world. It goes without saying that infinite numbers in ${^\ast\mathbb{N}}$ are ideals objects par excellence. Nonetheless, our modulus lemma suggests that if an object does not depend on the choice of ideal element in its definition, it is not ideal, but actually basic. This is the idea behind Ω-invariance: ideal objects can be basic if their definition does not really depend on the choice of any particular ideal element. In this way, Ω-invariance approaches the notion of finite procedure from above, while the usual methods work from the ground up by defining a set of basic constructive operations and a method for combining/iterating these.

We now consider two examples of Ω-invariant objects.

Remark 8

First of all, assume we have $(\exists n \in \mathbb{N})\varphi (n)$, with φ ∈ Δ₀. Then the function²³ (μn ≤ ω)φ(n) is Ω-invariant. Hence, there is an Ω-invariant function providing a witness n ₀ for φ(n ₀) (Compare item (5) in Definition 10).

Secondly, we show that a Δ ₁-formula is Ω-invariant. To this end, assume ψ ∈ Δ ₁, i.e. for some φ> ₁,φ ₂ ∈ Δ ₀, we have that

$$\psi (m) \leftrightarrow (\exists {n}_{1} \in \mathbb{N}){\varphi }_{1}({n}_{1},m) \leftrightarrow (\forall {n}_{2} \in \mathbb{N}){\varphi }_{2}({n}_{2},m),$$

(3)

for all $m \in \mathbb{N}$. Now fix some ω′∈ Ω. Let p _ψ(m) be the least n ₁ ≤ ω′ such that φ ₁(n ₁,m), if such exists and ω′ otherwise. Let q _ψ(m) be the least n ₂ ≤ ω′ such that ¬φ ₂(n ₂,m) if such exists and ω′ otherwise. For $m \in \mathbb{N}$, if ψ(m) holds, then p _ψ(m) is finite and q _ψ(m) is infinite. In particular, we have p _ψ (m) < q _ψ (m). Now suppose there is some ${m}_{0} \in \mathbb{N}$ such that p _ψ (m ₀ ) < q _ψ (m ₀) and ¬ψ(m ₀). By (3), we have $(\forall {n}_{1} \in \mathbb{N})\neg {\varphi }_{1}({n}_{1},{m}_{0})$ and, by definition, the number p _ψ(m) must be infinite. Similarly, the number q _ψ (m ₀) must be finite. However, this implies p _ψ (m ₀ ) ≥ q _ψ (m ₀), which yields a contradiction. Thus, we have ψ(m) ↔ p _ψ (m) < q _ψ (m), for all $m \in \mathbb{N}$. It is clear that we obtain the same result for a different choice of ω′∈ Ω, implying that ψ is Ω-invariant.

Care should be taken to choose the right axiom system to formalize the above informal derivation. Indeed, in certain axiom systems, not all Δ₁-formulas are Ω-invariant.

Finally, we consider the transfer principle from Nonstandard Analysis.

Principle 9

For all φ in Δ ₀ , we have

$$(\forall n \in \mathbb{N})\varphi (n) \rightarrow (\forall n {\in }{{^\ast}}\mathbb{N})\varphi (n).$$

(4)

The previous principle is called ‘∏ ₁ -TRANS’ or ‘∏ ₁-transfer’. Note that ∏ ₁-transfer expresses that $\mathbb{N}$ and ${}{{^\ast}}\mathbb{N}$ have the same properties. In other words, the properties of $\mathbb{N}$ are transferred to ${}{{^\ast}}\mathbb{N}$. In what follows, we do not assume that this principle is given.

3.2 Constructive Analysis and Constructive Reverse Mathematics

In this section, we sketch an overview of the discipline Constructive Reverse Mathematics (CRM). In order to describe CRM, we first need to briefly consider Errett Bishop’s Constructive Analysis.

Inspired by L. E. J. Brouwer’s famous foundational program of intuitionism,²⁴ Bishop initiated the redevelopment of classical mathematics with an emphasis on algorithmic and computational results. In his famous monograph ²⁴ Foundations of Constructive Analysis, he lays the groundwork for this enterprise. In honour of Bishop, the informal system of Constructive Analysis is now called ‘BISH’. In time, it became clear to the practitioners of Constructive Analysis that intuitionistic logic provides a suitable formalization²⁵ for BISH.

Definition 10 (Connectives in BISH)

• 1. The disjunction P ∨ Q: we have an algorithm that outputs either P or Q, together with a proof of the chosen disjunct.

• 2. The conjunction P ∧ Q: we have a proof of P and of Q.

• 3. The implication P → Q: by means of an algorithm we can convert any proof of P into a proof of Q.

• 4. The negation ¬P: assuming P, we can derive a contradiction (such as 0 = 1); equivalently, we can prove P → (0 = 1).

• 5. The formula (∃x)P(x): we have (i) an algorithm that computes a certain object x, and (ii) an algorithm that, using the information supplied by the application of algorithm (i), demonstrates that P(x) holds.

• 6. The formula (∀x ∈ A)P(x): we have an algorithm that, applied to an object x and a proof that x ∈ A, demonstrates that P(x) holds.

Having sketched Bishop’s Constructive Analysis, we now introduce Constructive Reverse Mathematics. In effect, Constructive Reverse Mathematics (CRM) is a spin-off from the Reverse Mathematics program introduced in Section 3.2. In CRM, the base theory is (inspired by) BISH and the aim is to find the minimal axioms that prove a certain non-constructive theorem. As in Friedman-Simpson style Reverse Mathematics, we also observe many equivalences between theorems and the associated minimal axioms.

We now provide two important CRM results.²⁶ First of all, we consider the limited principle of omniscience (LPO).

Theorem 11

In BISH , the following are equivalent.

• 1. LPO: P ∨¬P (P ∈ Σ ₁).

• 2. LPR: $(\forall x \in \mathbb{R})(x > 0 \vee \neg (x > 0))$ .

• 3. MCT: (The monotone convergence theorem) Every monotone bounded sequence of real numbers converges to a limit.

• 4. CIT: (The Cantor intersection theorem).

For MCT (resp. CIT), an algorithm computes the limit (resp. real in the intersection). Next, we list some equivalences of LLPO, the lesser limited principle of omniscience. Note that LLPO is an instance of De Morgan’s law.

Theorem 12

In BISH , the following are equivalent.

• 1. LLPO: ¬(P ∧ Q) →¬P ∨¬Q (P,Q ∈ Σ ₁ ).

• 2. LLPR: $(\forall x \in \mathbb{R})[\neg (x > 0) \vee \neg (x < 0)]$ .

• 3. NIL: $(\forall x,y \in \mathbb{R})(xy = 0 \rightarrow x = 0 \vee y = 0)$ .

• 4. CLO: For all $x,y \in \mathbb{R}$ with ¬(x < y), {x,y} is a closed set.

• 5. IVT: a version of the intermediate value theorem.

• 6. WEI: a version of the Weierstraß extremum theorem.

For IVT (resp. WEI), an algorithm computes the interm. value (resp. max.).

It should be noted that any result proved in BISH is compatible²⁷ with classical, intuitionistic and recursive mathematics.

3.3 Reverse-engineering Reverse Mathematics

In this section, we sketch a translation²⁸ of results from Constructive Reverse Mathematics to Nonstandard Analysis. We translate²⁸ Bishop’s primitive notion of algorithm and finite procedure as the notion of Ω-invariance in Nonstandard Analysis. Following Definition 10, the intuitionistic disjunction translates²⁸ to the following in Nonstandard Analysis.

Definition 13 (Hyperdisjunction)

For formulas φ ₁ and φ₂, the formula ${\varphi }_{1}(n)\mathbb{V}{\varphi }_{2}(n)$ is the statement: There is an Ω-invariant formula ψ such that

$$(\forall n \in \mathbb{N})(\psi (n,\omega ) \rightarrow {\varphi }_{1}(n) \wedge \neg \psi (n,\omega ) \rightarrow {\varphi }_{2}(n).$$

(5)

Note that ${\varphi }_{1}(n)\mathbb{V}{\varphi }_{2}(n)$ indeed implies φ₁(n) ∨ φ₂(n). Furthermore, given the formula ${\varphi }_{1}(n)\mathbb{V}{\varphi }_{2}(n)$, there is an Ω-invariant procedure (provided by ψ(n, ω)) to determine which disjunct of φ ₁(n) ∨ φ₂(n) makes it true. Thus, we observe that the meaning of the hyperdisjunction ‘ $\mathbb{V}$’ is quite close to its intuitionistic counterpart ‘ ∨ ’ from Definition 10.

The other intuitionistic connectives may be translated analogously. The translation of → (resp. ¬) will be denoted ⇛ (resp.  ∼ ). As for disjunction, the meaning of the intuitionistic connectives is quite close to that of the hyperconnectives. Furthermore, as suggested by the following theorems, the equivalences from CRM remain valid after the translation. In particular, we have the following theorems, to be compared to Theorems 11 and 12.

Theorem 14

In Nonstandard Analysis, the following are equivalent.

• 1. ∏ ₁ -TRANS.

• 2. $\mathbb{L}\mathbb{P}\mathbb{O}$: $P\mathbb{V}\sim P$ (P ∈ Σ ₁ ).

• 3. $\mathbb{L}\mathbb{P}\mathbb{R}$ : $(\forall x \in \mathbb{R})(x > 0\mathbb{V}\sim (x > 0))$ .

• 4. $\mathbb{M}\mathbb{C}\mathbb{T}$ : (The monotone convergence theorem) Every monotone bounded sequence of real numbers converges to a limit.

• 5. $\mathbb{C}\mathbb{I}\mathbb{T}$: (The Cantor intersection theorem).

Analogous to the context of CRM, in $\mathbb{M}\mathbb{C}\mathbb{T}$ (resp.  $\mathbb{C}\mathbb{I}\mathbb{T}$), the limit (resp. real in the intersection) is computed by an Ω-invariant function.

Theorem 15

In $\mathbb{N}\mathbb{S}\mathbb{A}$ , the following are equivalent.

• 1. $\mathbb{L}\mathbb{L}\mathbb{P}\mathbb{O}$ : $\sim (P \wedge Q) \Rrightarrow \sim P\mathbb{V}\sim Q$ (P,Q ∈ Σ ₁ ).

• 2. $\mathbb{L}\mathbb{L}\mathbb{P}\mathbb{R}$ : $(\forall x \in \mathbb{R})[\sim (x > 0)\mathbb{V}\sim (x < 0)]$ .

• 3. $\mathbb{N}\mathbb{I}\mathbb{L}$: $(\forall x,y \in \mathbb{R})(xy = 0 \Rrightarrow x = 0\mathbb{V}y = 0)$ .

• 4. $\mathbb{C}\mathbb{L}\mathbb{O}$ : For all $x,y \in \mathbb{R}$ with ∼(x < y), {x,y} is a closed set.

• 5. $\mathbb{I}\mathbb{V}\mathbb{T}$ : a version of the intermediate value theorem.

• 6. $\mathbb{W}\mathbb{E}\mathbb{I}$: a version of the Weierstraß extremum theorem.

Analogous to the context of CRM, in $\mathbb{I}\mathbb{V}\mathbb{T}$ (resp.  $\mathbb{W}\mathbb{E}\mathbb{I}$), the intermediate value (resp. maximum) is computed by an Ω-invariant function.

The previous theorems only constitute an example of a general theme. In particular, it is possible to translate most²⁹ theorems (and corresponding equivalences) from CRM to Nonstandard Analysis in the same way as above. Comparing Theorems 11 and 12 to Theorems 14 and 15, we conclude that the equivalences observed in CRM remain intact after changing the underlying framework (based on algorithm and intuitionistic logic, by Definition 10) to Nonstandard Analysis (based on Ω-invariance and the hyperconnectives, by Definition 13). Hence, we observe the robustness phenomenon described at the beginning of this section.

In conclusion, we discuss just how far the analogy between Constructive Analysis and Nonstandard Analysis takes us. For instance, on the level of intuition, the formula ¬(x ≤ 0) does not imply x > 0, as the former expresses that it is impossible that $x \in \mathbb{R}$ is below zero (but might still be very close to zero), while the latter expresses that x is bounded away from zero by some rational q we may construct. In Nonstandard Analysis, ∼ (x ≤ 0) only states that for some (possible infinite) $k {\in }{{^\ast}}\mathbb{N}$, we have $0 < \frac{1} {k} < x$. Hence, ∼ ( x ≤ 0) is consistent with x ≈ 0, while x > 0 has the same interpretation as in BISH. Thus, we observe a correspondence between the latter and Nonstandard Analysis, even on the level of intuitions. A similar conclusion follows from comparing the meaning of IVT and $\mathbb{I}\mathbb{V}\mathbb{T}$, as is done after Theorem 15.

Secondly, another interesting correspondence is provided by the equivalence between items (1) and (2) in Theorem 12. Indeed, to prove this equivalence, one requires the axiom ¬(x > 0 ∧  x < 0) of the constructive continuum.³⁰ As it turns out, to establish the equivalence between items (1) and (2) in Theorem 15, the formula ∼ (x > 0 ∧  x < 0) is needed in Nonstandard Analysis. Hence, the correspondence between BISH and the latter goes deeper than merely superficial resemblance.

Thirdly, we discuss the above result in the light of the so-called Brouwer-Heyting-Kolmogorov (BHK) interpretation, given by Definition 10. While the equivalences in Theorems 14 and 15 are proved in classical logic, they carry a lot more information. For instance, to show that $\mathbb{L}\mathbb{P}\mathbb{R}$ implies $\mathbb{L}\mathbb{P}\mathbb{O}$, a formula $\psi (\vec{x},n,\omega )$ is defined²⁹ such that $\psi (\vec{x},{\ulcorner\psi }_{1}\urcorner,\omega )$ is an Ω-invariant formula which decides between P and ∼ P ( P ∈ Σ ₁ ), for every Ω-invariant formula ${\psi }_{1}(\vec{x},\omega )$ which decides between x > 0 and ∼ ( x > 0). Hence, we do not only have $\mathbb{L}\mathbb{P}\mathbb{R} \rightarrow \mathbb{L}\mathbb{P}\mathbb{O}$, but also an implication akin to the BHK interpretation, i.e. that an Ω-invariant decision procedure is converted, by an Ω-invariant procedure, to another Ω-invariant decision procedure.

We finish this section with the following remark.

Remark 16 (Reuniting the antipodes)

The title of this section refers to a conference with the same name held in 1999 in Venice. Following Bishop’s strong criticism³¹ of Nonstandard Analysis, this conference was part of a reconciliatory attempts between the communities of Nonstandard Analysis and Constructive Analysis. Little work³² has indeed taken place in the intersection of these disciplines, but Theorems 14 and 15 can be interpreted as an attempt at reuniting the antipodes that are Nonstandard and Constructive Analysis. Nonetheless, it has been noted in the past³³ that Nonstandard Analysis has a constructive dimension.

Acknowledgement: This publication was made possible through the generous support of a grant from the John Templeton Foundation for the project Philosophical Frontiers in Reverse Mathematics. I thank the John Templeton Foundation for its continuing support for the Big Questions in science. Please note that the opinions expressed in this publication are those of the author and do not necessarily reflect the views of the John Templeton Foundation