{'fraction_non_alphanumeric': 0.06415643559707974, 'fraction_numerical': 0.01988309584732036, 'mean_word_length': 4.114045618247299, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Nonstandard Analysis and Constructivism!

Almost two decades ago, Wattenberg published a paper with the title 'Nonstandard Analysis and Constructivism?' in which he speculates on a possible connection between Nonstandard Analysis and constructive mathematics. We study Wattenberg's work in light of recent research on the aforementioned connection. On one hand, with only slight modification, some of Wattenberg's theorems in Nonstandard Analysis are seen to yield effective and constructive theorems (not involving Nonstandard Analysis). On the other hand, we establish the incorrectness of some of Wattenberg's (explicit and implicit) claims regarding the constructive status of the axioms Transfer and Standard Part of Nonstandard Analysis.


Introduction
The introduction of Wattenberg's paper [37] includes the following statement: This is a speculative paper. For some time the author has been struck by an apparent affinity between two rather unlikely areas of mathematics -nonstandard analysis and constructivism. [. . . ] The purpose of this paper is to investigate these ideas by examining several examples. ( [37, p. 303]) In a nutshell, the aim of this paper is to study Wattenberg's results in light of recent results on the computational content of Nonstandard Analysis as in [28][29][30][31].
First of all, similar observations concerning the constructive content of Nonstandard Analysis have been made before, e.g. as follows: It has often been held that nonstandard analysis is highly nonconstructive, thus somewhat suspect, depending as it does upon the ultrapower construction to produce a model [. . . ] On the other hand, nonstandard praxis is remarkably constructive; having the extended number set we can proceed with explicit calculations.
However, Wattenberg goes further than most of the aforementioned authors by making the following important observation.
Despite an essential nonconstructive kernel, many nonstandard arguments are constructive until the final step, a step that frequently involves the standard part map. ( [37, p. 303]) This observation is similar to Osswald's local constructivity. In particular, Osswald has qualified the observation from the above quotes as Nonstandard Analysis is locally constructive, to be understood as the fact that the mathematics performed in the nonstandard world is highly constructive 1 . By contrast, the nonstandard axioms (Transfer and Standard Part ) needed to 'jump between' the nonstandard world and usual mathematics, are highly non-constructive in general. Osswald discusses local constructivity in [38, §7], [21, §1-2], or [22, §17.5].
The results in [28][29][30][31] vindicate the Wattenberg and Osswald view in that computational content is extracted from theorems of 'pure' Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, Riemann integration, compactness, et cetera) rather than the 'ε-δ' definitions. With this choice, one only works in the nonstandard universe, avoiding the non-constructive step from and to the standard/usual universe (requiring Transfer and Standard Part ).
In this paper, we show that Wattenberg's results from [37] yield effective and constructive results with only slight modification. However, we also establish the incorrectness of Wattenberg's claims regarding the constructive status of the nonstandard axioms Transfer and Standard Part. In contrast to Wattenberg, we shall work in Nelson's axiomatic approach to Nonstandard Analysis (See Section 2), but this change of framework will have no real impact on our results or Wattenberg's.

Internal set theory and its fragments
In this section, we discuss Nelson's internal set theory, first introduced in [18], and its fragments P and H from [3]. The latter fragments are essential to our enterprise, especially Theorem 2.4 below.
where ϕ(x, t) is internal, and only has free variables t, x. The system IST is (the internal system) ZFC extended with the aforementioned external axioms; The former is a conservative extension of ZFC for the internal language, as proved in [18]. Clearly, the extension from ZFC to IST can be done for other systems, and we are interested in the formalisations of (classical and intuitionistic) arithmetic, namely Peano and Heyting arithmetic. In this regard, the systems H and P from [3], also sketched in the next sections, are nonstandard extensions of the (internal) logical systems E-HA ω and E-PA ω , respectively Heyting and Peano arithmetic in all finite types and the axiom of extensionality. We refer to [12, §3.3] for the exact definitions of the (mainstream in mathematical logic) systems E-HA ω and E-PA ω .
2.2. The classical system P. In this section, we introduce the system P, a conservative extension of Peano arithmetic with fragments of Nelson's IST.
To this end, recall that E-PA ω * and E-HA ω * are the definitional extensions of E-PA ω and E-HA ω with types for finite sequences, as in [3, §2]. For the former systems, we require some notation. Notation 2.1 (Finite sequences). The systems E-PA ω * and E-HA ω * have a dedicated type for 'finite sequences of objects of type ρ', namely ρ * . Since the usual coding of pairs of numbers goes through in both, we shall not always distinguish between 0 and 0 * . Similarly, we do not always distinguish between 's ρ ' and ' s ρ ', where the former is 'the object s of type ρ', and the latter is 'the sequence of type ρ * with only element s ρ '. The empty sequence for the type ρ * is denoted by ' ρ ', usually with the typing omitted. Furthermore, we denote by '|s| = n' the length of the finite sequence s ρ * = s ρ 0 , s ρ 1 , . . . , s ρ n−1 , where | | = 0, i.e. the empty sequence has length zero. For sequences s ρ * , t ρ * , 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| ≤ j < |s| + |t|. For a sequence s ρ * , we define sN := s(0), s(1), . . . , s(N ) for N 0 < |s|. For a sequence α 0→ρ , we also write αN = α(0), α(1), . . . , α(N ) for any N 0 . By way of shorthand, q ρ ∈ Q ρ * abbreviates (∃i < |Q|)(Q(i) = ρ q). Finally, we shall use x, y, t, . . . as short for tuples x σ0 0 , . . . x σ k k of possibly different type σ i . We can now introduce E-PA ω * st . We use the same definition as [3, Def. 6.1], where E-PA ω * is the definitional extension of E-PA ω with types for finite sequences from [3, §2]. The set T * is the collection of all the terms in the language of E-PA ω * .
consists of the following basic axiom schemas.
The schema providing for each closed 4 term t ∈ T * the axiom st(t).
). The external induction axiom IA st is as follows.
Secondly, we introduce some essential fragments of IST studied in [3].

Definition 2.3. [External axioms of P]
3 The language of E-PA ω * st contains a symbol stσ for each finite type σ, but the subscript is essentially always omitted. Hence T * st is an axiom schema and not an axiom. 4 A term is called closed in [3] (and in this paper) if all variables are bound via lambda abstraction. Thus, if x, y are the only variables occurring in the term t, the term (λx)(λy)t(x, y) is closed while (λx)t(x, y) is not. The second axiom in Definition 2.2 thus expresses that stτ (λx)(λy)t(x, y) if (λx)(λy)t(x, y) is of type τ . We usually omit lambda abstraction for brevity.
(1) HAC int : For any internal formula ϕ, we have (2) I: For any internal formula ϕ, we have The system P is E-PA ω * st + I + HAC int . Note that I and HAC int are fragments of Nelson's axioms Idealisation and Standard part. By definition, F in (2.1) only provides a finite sequence of witnesses to (∃ st y), explaining its name Herbrandized Axiom of Choice.
The system P is connected to E-PA ω by Theorem 2.4. The latter (which is not present in [3]) expresses that we may obtain effective results as in (2.3) from any theorem of Nonstandard Analysis which has the same form as in (2.2).
Theorem 2.4. If ∆ int is a collection of internal formulas and ψ is internal, and

2)
then one can extract from the proof a sequence of closed 4 terms t in T * such that Proof. See e.g. [30, §2] or [29, §2].
For the rest of this paper, the notion 'normal form' shall refer to a formula as in (2.2), i.e. of the form (∀ st x)(∃ st y)ϕ(x, y) for ϕ internal. It is shown in [29][30][31] that the scope of Theorem 2.4 includes the 'Big Five' systems of Reverse Mathematics and the associated 'zoo' from [7].
Finally, the previous theorems do not really depend on the presence of full Peano arithmetic. We shall study the following subsystems. (1) Let E-PRA ω be the system defined in [13, §2] and let E-PRA ω * be its definitional extension with types for finite sequences as in [3, §2]. (2) (QF-AC ρ,τ ) For every quantifier-free internal formula ϕ(x, y), we have (3) The system RCA ω 0 is E-PRA ω + QF-AC 1,0 . The system RCA ω 0 is the 'base theory of higher-order Reverse Mathematics' as introduced in [13, §2]. We permit ourselves a slight abuse of notation by also referring to the system E-PRA ω * + QF-AC 1,0 as RCA ω 0 . Corollary 2.6. The previous theorem and corollary go through for P and E-PA ω * replaced by P 0 ≡ E-PRA ω * + T * st + HAC int + I + QF-AC 1,0 and RCA ω 0 . Proof. The proof of [3,Theorem 7.7] goes through for any fragment of E-PA ω * which includes EFA, sometimes also called I∆ 0 +EXP. In particular, the exponential function is (all what is) required to 'easily' manipulate finite sequences.
We now discuss the Standard Part principle Ω-CA, a very practical consequence of the axiom HAC int . Intuitively speaking, Ω-CA expresses that we can obtain the standard part (in casu G) of Ω-invariant nonstandard objects (in casu F (·, M )). Note that we write 'N ∈ Ω' as short for ¬st(N 0 ).

Definition 2.7.
[Ω-invariance] Let F (σ×0)→0 be standard and fix M 0 ∈ Ω. Then (2.5) Principle 2.8 (Ω-CA). Let F (σ×0)→0 be standard and fix M 0 ∈ Ω. For every Ω-invariant F (·, M ), there is a standard G σ→0 such that The axiom Ω-CA provides the standard part of a nonstandard object, if the latter is independent of the choice of nonstandard number used in its definition. The following theorem is not new, but highly instructive in light of Remark 2.10.
Finally, we consider the following remark on how HAC int and I are used.
Remark 2.10 (Using HAC int and I). By definition, HAC int produces a functional F σ→τ * which outputs a finite sequence of witnesses. However, HAC int provides an actual witnessing functional assuming (i) τ = 0 in HAC int and (ii) the formula ϕ from HAC int is 'sufficiently monotone' as in: (∀ st x σ , n 0 , m 0 ) [n ≤ 0 m ∧ ϕ(x, n)] → ϕ(x, m) . Indeed, in this case one simply defines G σ→0 by G(x σ ) := max i<|F (x)| F (x)(i) which satisfies (∀ st x σ )ϕ(x, G(x)), as was done in the proof of Theorem 2.9. To save space in proofs, we will sometimes skip the (obvious) step involving the maximum of finite sequences, when applying HAC int . We assume the same convention for terms obtained from Theorem 2.4, and applications of the contraposition of Idealisation I.
2.3. The constructive system H. In this section, we define the system H, the constructive counterpart of P.
where Ψ(y) is any formula and φ(x) is an internal formula of E-HA ω * .
where φ(x) and ψ are internal formulas in the language of E-HA ω * .
where Φ is any formula of E-HA ω * Intuitively speaking, the first two axioms of Definition 2.11 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 H, provided we introduce a 'Herbrandisation' as in the consequent of HAC, i.e. a finite list of possible witnesses rather than one single witness. Furthermore, while 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 2.11 are exactly what is needed to convert nonstandard definitions (of continuity, integrability, convergence, et cetera) into the normal form (∀ st x)(∃ st y)ϕ(x, y) for internal ϕ, as done in [29, §3.1]. The latter normal form plays an equally important role in the constructive case as in the classical case by the following theorem.
Theorem 2.12. If ∆ int is a collection of internal formulas, ϕ is internal, and H + ∆ int ⊢ ∀ st x ∃ st y ϕ(x, y, a), (2.8) then one can extract from the proof a sequence of closed terms t in T * such that E-HA ω * + ∆ int ⊢ ∀x ∃y ∈ t(x) ϕ(x, y, a). (2.9) Proof. Immediate by [3,Theorem 5.9]. Note that in the latter, just like in the proof of Corollary 2.4, ∀ st x ∃ st y ϕ(x, y, a) is proved to be 'invariant' under a suitable syntactic translation.
Finally, we point out some very useful principles to which we have access.
for any internal formula ϕ.
In conclusion, we have introduced the systems H, 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 result in Theorem 2.4 is the normal form (∀ st x)(∃ st y)ϕ(x, y) for internal ϕ.

Notations.
In this section, we introduce notations relating to H and P.
First of all, we mostly use the same notations as in [3].
if it does not involve st, and 'external' otherwise. The formula A st is defined from A by appending 'st' to all quantifiers (except bounded number quantifiers).
Secondly, we will use the usual notations for natural, rational and real numbers and functions as introduced in [13, p. 288-289]. We only list the definition of real number and related notions in P and related systems.

Definition 2.15 (Real numbers and related notions in P).
(1) A (standard) real number x is a (standard) fast-converging Cauchy sequence We use Kohlenbach's 'hat function' from [13, p. 289] to guarantee that every sequence f 1 is a real.
Functions F : R → R mapping reals to reals are represented by functionals Φ 1→1 mapping equal reals to equal reals, i.e.
Sets of objects of type ρ are denoted X ρ→0 , Y ρ→ , Z ρ→0 , . . . and are given by their characteristic functions f ρ→0 is assumed to output zero or one.
Thirdly, we use the usual extensional notion of equality.
Remark 2.16 (Equality). All the above systems include equality between natural numbers '= 0 ' as a primitive. Equality '= τ ' for type τ -objects x, y is defined as: In the spirit of Nonstandard Analysis, we define 'approximate equality ≈ τ ' as follows: with the type τ as above. All the above systems include the axiom of extensionality: However, as noted in [3, p. 1973], the so-called axiom of standard extensionality (E) st is problematic and cannot be included in our systems. We use (E) n+2 to refer to (E) restricted to type n + 2 functionals ϕ.

2.5.
Preliminaries. In this section, we introduce the usual defintions of continuity, as well as some fragments of Transfer and Standard Part, their normal forms, and the functionals arising from term extraction as in Theorem 2.4.
As will become clear in Section 3.2, there is an intimate connection between nonstandard continuity (2.13) and a 'modulus-of-continuity functional' Ξ as in MPC(Ξ).
) and also the restriction of Nelson's axiom Transfer as follows: (Π 0 1 -TRANS) Denote by MU(µ) the formula in square brackets in (µ 2 ). By the following theorems, Π 0 1 -TRANS is fundamentally non-constructive and closely related to arithmetical comprehension as given by (µ 2 ).
The first implication is immediate as standard functionals produce standard output on standard input by the third basic axiom in Definition 2.2. In particular, µ(f ) is standard for standard f 1 if µ 2 is standard. For the second implication, note that Π 0 1 -TRANS implies by contraposition that: Applying HAC int while bearing in mind Remark 2.10, we obtain standard Φ s.t. ( which immediately yields (µ 2 ) st , and we are done.
Proof. See the proof of Corollary 3.10.
By the previous theorem, term extraction as in Theorem 2.4 converts Π 0 1 -TRANS into (µ 2 ), i.e. the former fragment of Transfer is rather non-constructive.
Finally, we should point out that it is possible to obtain (some) computational information from (non-constructive) proofs in classical mathematics, even involving comprehension. This is the domain of proof mining, to which Kohlenbach's monograph [12] provides an excellent introduction. Thus, our use of 'X is nonconstructive' should be interpreted as the observation that X is rejected in (parts of) constructive mathematics, while X may have implicit constructive content, which can be brought out using proof mining. In fact, we will use a technique from proof theory to obtain computational content from Standard Part in Section 4.2.
2.5.3. Standard Part and related functionals. We shall make use of the following fragments of the Standard Part axiom: These fragments are both equivalent to the following by Theorem 4.4 below: where 'T ≤ 1 1' denotes that T is a binary tree. Clearly, (2.18) is a nonstandard version of weak König's lemma, and the latter is a compactness principle by [33,IV].
As it happens, STP and STP R express the nonstandard compactness of Cantor space and the unit interval by Robinson's theorem in [10, p. 43]. Furthermore, (2.18) is equivalent to the following normal form: Any functional Θ 2→(1 * ×0) satisfying SCF(Θ) is called a special fan functional and the latter object was first introduced in [28]. Note that there is no unique such Θ, i.e. it is in principle incorrect to talk about 'the' special fan functional.
With regard to first order-strength, RCA ω 0 +(∃Θ)SCF(Θ) is a conservative extension of RCA 2 0 + WKL by [13,Prop. 3.15]. All these results may be found in [20]. In conclusion, the special fan functional has rather weak first-order strength, while it is extremely hard to compute (compared to e.g. the computational strength of the Big Five systems of Reverse Mathematics). As will become clear in Section 4.2, the special fan functional still provides plenty of computational content after applying an extra (algorithmic) step.

The intermediate value theorem
We discuss Wattenberg's treatment from [37,II] As is well-known, IVT implies a non-trivial fragment of the law of excluded middle (See e.g. [2, I.7] or [17]) and is therefore rejected in constructive mathematics. The following 'approximate' IVT is described as 'constructive' by Wattenberg ([37, II.2]).
On one hand, a slight modification of Wattenberg's nonstandard proof of IVT will be shown to yield the following effective version of IVT in Section 3.2.
Note that this version no longer involves Nonstandard Analysis. Furthermore, the term s is 'read off' from the (modified) Wattenberg proof. Thus, Wattenberg's claims about the effective content of Nonstandard Analysis do seem to hold water.
One the other hand, some of Wattenberg's (explicit and implicit) claims regarding the constructive status of the nonstandard axioms Transfer and Standard Part will be shown to be incorrect. In particular, Wattenberg suggests that Standard Part is fundamentally non-constructive (See [37, p. 303] and Section 1), but freely (either explicitly or implicitly) makes use of Transfer. We show that Transfer as used by Wattenberg is fundamentally non-constructive in Section 3.3, while the constructive status of Standard Part is discussed in Section 3.4.
Note that item (iii) makes use of uniform nonstandard continuity, while item (iv) makes use of STP to obtain t 0 . According to Wattenberg ([37, p. 303]), the final step of the proof is non-constructive (as it involves STP) and should therefore be omitted. Following this approach, the previous steps immediately yield Theorem 3.4 where t ((1→1)×0)→0 is defined as follows (with the real h := b−a N ): Theorem 3.4 (IVT wat ). For nonstandard N 0 and nonstandard uniformly continu- Note that t does not implement item (ii), but only an approximation up to nonstandard precision. This is however equally good in light of nonstandard (uniform) continuity from item (iii). It should be noted that Wattenberg observes this problem with item (ii) as well in [37, p. 304]. He proposes to replace '≤ R ' by ' ' in [37,II.6], which is however not a decidable 5 predicate either.
We have the following theorem where it should be noted that IVT wat does not have an obvious normal form (to apply Theorem 2.4).
Theorem 3.5. From the proof of IVT wat in P 0 , a term u can be extracted such that RCA ω 0 proves IVT ef (u). Proof. The proof of IVT wat in P 0 follows immediately from the definition of t in (4.11) and steps (i)-(iii) above. We now convert IVT wat into a normal form so that we can apply Theorem 2.4; we assume a = 0 and b = 1 for simplicity. Thus, let A(f, k, N ) be the conjunction of f (0) < R 0 < R f (1) and the formula in square brackets in (2.14), and note that (∀ st k 0 )(∃ st N 0 )A(f, k, N ) implies that f is continuous as in (2.15). In this way, IVT wat implies that for f : [0, 1] → R we have which immediately yields by resolving '≈' that and, since standard functionals yield standard output on standard input, we have for all f : [0, 1] → R that By strengthening the antecedent, the previous formula yields: It should be noted that the constructive system H proves the 'lesser limited principle of omniscience' LLPO relative to 'st' ([3, §3.1]) which implies (∀ st x ∈ R)(x 0 ∨ x 0), i.e. an instance of the law of excluded middle relative to 'st'. However, the decision procedure for the latter follows easily from the constructive fact that (∀x ∈ R)(x ≥ R 0 ∨ x ≤ R a) for 0 < R a ≈ 0. Now bring outside all standard quantifiers as far as possible to obtain: Let C(g, l, f, n) be the formula in square brackets in the previous formula. Apply Idealisation I, while bearing in mind Remark 2.10, to push the standard quantifier involving n to the front as follows: (3.6) Now apply Theorem 2.4 to 'P ⊢ (3.6)' to obtain a term s such that E-PA ω * proves Define u(f, g, k) := t(f, max i<|s(g,k)| s(g, k)(i)) and note that IVT ef (u).
The previous proof serves as a template for obtaining computational content from Nonstandard Analysis as follows. The below proofs follow this template and we will therefore not always go in as much detail as in the previous proof.  As it turns out, the proof of the theorem also goes through constructively, as follows. This is far from obvious as the proof seems to involve non-constructive steps like the independence of premise principle to go from (3.4) to (3.5).
Corollary 3.8. From the proof of IVT wat in H, a term u can be extracted such that E-HA ω * proves IVT ef (u).
Proof. Clearly, the above proof of IVT wat goes through in H. Furthermore, one easily derives (3.7) from IVT wat in H. Indeed, the steps leading up to (3.4) clearly go through in H. For the step from (3.4) to (3.5), the '(∀ st l)' quantifier can be brought to the front in intuitionistic logic, and the same can then be done for the quantifier '(∃ st n)' using the axiom HIP ∀ st from Definition 2.11, while bearing in mind Remark 2.10 as usual. Having obtained (3.5), one applies NCR to obtain (3.6), again bearing in mind Remark 2.10. Finally, one applies Theorem 2.12 to 'H ⊢ (3.6)' to obtain the required term.
In conclusion, Wattenberg's claim that Nonstandard Analysis has effective (even constructive) content seems correct in light of Theorem 3.5 and its corollary.

3.3.
Non-constructivity arising from continuity. In this section, we deal with the exact connection between nonstandard and ε-δ-continuity. We are motivated by the observation that Wattenberg uses the (provable using Transfer ) equivalence between nonstandard and ε-δ-continuity without a second thought in [37,III.3].
By the following theorem and Theorem 2.19, any step from ε-δ-continuity to nonstandard continuity, i.e. NSC 1 and NSC 2 in Definition 2.18, implies a non-trivial fragment of Transfer and is therefore fundamentally non-constructive.
. We may bring out the '(∀ st k)' and '(∀ st N )' quantifiers as follows: Applying Idealisation I to the underlined formula, we obtain a standard z 0 * such that (∀y ∈ [0, 1])(∃N ∈ z) in the previous formula. Now let N 0 be the maximum of all numbers in z, and note that for N = N 0 , we have the following: which implies (since standard functionals have standard output for standard input): and dropping the 'st' in the antecedent, we obtain: and bringing the standard quantifiers up front, we finally have Applying Theorem 2.4 to 'P 0 ⊢ (3.8)', we obtain a term t such that which is exactly as required in light of the definition of A, B and Remark 2.10.
By the previous theorem and corollary, NSC 1 translates to the existence of a modulus-of-continuity-functional when applying Theorem 2.4. Such a functional is fundamentally non-constructive by the corollary, and this non-constructiveness 'trickles down' to any nonstandard theorem of P 0 + NSC 1 as follows.
Proof. Analogous to the proof of the previous corollary following Template 3.6 The previous theorem and corollaries imply that the step from ε-δ continuity (relative to 'st' or not) to the nonstandard variety always involves a non-trivial instance of Transfer, which is fundamentally non-constructive. In particular, by Corollary 3.11, any result proved using NSC 1 only provides computational information involving a non-constructive modulus-of-continuity-functional. In general, moving from the standard into the nonstandard world is highly non-constructive (requiring Transfer ), as was sketched in Section 1 in the form of Osswald's local constructivity. Nonetheless, Wattenberg freely uses Transfer and the equivalence between 'ε-δ' and nonstandard continuity in [37,. This aspect of his investigation into the computational content of Nonstandard Analysis thus seems incorrect. Furthermore, as suggested by its proof, Theorem 3.9 goes through for other notions besides continuity. We now show, for differentiability and Riemann integration, that the step from the ε-δ definition to the nonstandard one yields Π 0 1 -TRANS. First of all, we have the usual definition of differentiability.
(3.10) A 'modulus of differentiability at a' is a function g 1 such that g(k) is N 0 in (3.10).
Let NSD be the statement any standard f : R → R differentiable at zero is also nonstandard differentiable there. Now, NSD is a theorem of IST but we also have the following implication. is well-defined and differentiable in the usual internal 'epsilon-delta' sense. However, which implies that f 0 is not nonstandard differentiable at zero. This contradiction yields Π 0 1 -TRANS, and we are done.
Let DIF(Ξ) be the statement that Ξ(f ) is a modulus for differentiability at zero for every f differentiable at zero. Corollary 3.14. From the proof that P ⊢ NSD → Π 0 1 -TRANS, a term t can be extracted such that E-PA ω ⊢ (∀Ξ 3 ) DIF(Ξ) → MU(t(Ξ))) Proof. A normal form for differentiability as in (3.9) is easy to obtain and as follows: The proof is straightforward and analogous to the proof of Corollary 3.10.
Let NSR be the statement a standard f : R → R integrable on the unit interval is also nonstandard integrable there. As above, NSR is a theorem of IST but we also have the following implication. is larger than any standard real, replacing 0 by √ x 0 in a partition causes the associated Riemann sums to be apart by more than an infinitesimal.
Let RIE(κ) be the statement that κ(f ) is a modulus of Riemann integration for every f : R → R integrable on the unit interval.
Proof. The proof is straightforward and analogous to that of Corollary 3.10.
Hence, switching from epsilon-delta integrability to the nonstandard variety as in NSR is at least as non-constructive as (µ 2 ) and NSC 1 . One readily obtains a version of NSC 2 → Π 0 1 -TRANS for NSR, i.e. for ε-δ-integrability relative to 'st'. In conclusion, Wattenberg's claim that Nonstandard Analysis has effective (even constructive) content is correct in light of Theorem 3.5; his implementation using ε-δ continuity and Transfer is problematic in light of Theorem 3.9, but easily salvageable: By Theorem 3.5 it suffices to just adopt nonstandard (rather than ε-δ) continuity, in line with Osswald's local constructivity. We next investigate Wattenberg's claims regarding the constructive status of Standard Part in Section 3.4.

3.4.
The non-constructive status of Standard Part. We investigate the constructive status of Standard Part in light of Wattenberg's claims that it be fundamentally non-constructive.
First of all, we have the following theorem regarding the use of STP, which is the only fragment of Standard Part used by Wattenberg in [37].
In light of the previous theorem, the use of STP in the proof of a nonstandard theorem translates to the presence of the special fan functional Θ after applying Theorem 2.4. Given the computational hardness of Θ, Wattenberg's claims regarding the non-constructive nature of Standard Part seem justified. However, as will be established in Section 4.2, the fragment of Standard Part used by Wattenberg (namely STP from Section 2.5.3) does have plenty of effective content, though extra technical machinery is needed for this.
Secondly, we show that the generalisation of STP to type two functionals is nonconstructive as it implies (∃ 2 ). In particular, the following rather weak fragment of Standard part is established to be non-constructive by Theorem 3.19.
Note that (E) st n+2 results in a conservative extension of P 0 as shown in [4].
Let f 1 , f 2 be standard binary sequences and fix nonstandard N 0 . Let K(n, f 1 , f 2 ) be the largest k 0 ≤ N such that (∀n 1 , n 2 ≤ k)(f 1 (n 1 , n) = 0 ∨ f 2 (n 2 , n) = 0), if such number exists, and zero otherwise. Define Y 2 as follows: . By overspill, K(n, f 1 , f 2 ) is nonstandard for all standard n 0 . By definition, we have Then Z(f 1 , f 2 , n) is standard and provides the separating set from Σ 0 1 -separation for standard inputs and relative to 'st'.
We provide an alternative proof for Theorem 3.19 as follows.
In conclusion, the previous theorem suggests that the axiom Standard Part is in general fundamentally non-constructive, as claimed by Wattenberg. Moreover, since (E) st n+2 readily follows from Transfer, Theorem 3.19 is especially relevant when a proof utilises both Transfer and Standard Part.

Compactness
We discuss Wattenberg's treatment from [37,III] of compactness (Sections 4.1 and 4.2) and the associated extreme value theorem (Section 4.3).

4.1.
Constructive compactness and Nonstandard Analysis. Wattenberg describes the following form of compactness as 'acceptable' in [37,III.4]. As we will see, his choice of compactness is indeed most suitable for obtaining constructive or effective results.
Note that inside P (and extensions), the unit interval and Cantor space are Fcompact, but not necessarily nonstandard compact (as P+Π 0 1 -TRANS ⊢ STP by [20, §4]). In particular, nonstandard compactness guarantees the infinitesimal proximity of a standard point, while F -compactness states the presence of an 'infinitesimal grid' of nonstandard points. Thus, F -compactness expresses the intuitive notion that a compact space 'can be divided into infinitesimal pieces', a mainstay of the infinitesimal calculus used in physics and engineering. The notion of F -compactness for special cases has been studied in [29].
We first prove a basic result regarding F -compactness. Note that the latter provides a kind of 'discretisation' of the space X as used in an essential way for the unit interval in the steps (i)-(iv) at the beginning of Section 3.2.
Theorem 4.2 (FC R ). An F -compact X ⊂ R has a supremum, i.e. for all standard x (·) and any X ⊂ R, we have Note that Ω-CA converts t(x (·) , N ) from the theorem into a standard supremum.
The constructive version of the previous theorem is [5,Theorem 3,p. 34]. The latter version involves the notion of 'totally boundedness' as in the antecedent of (4.1), which 'falls out' of the notion of F -compactness by the following theorem. Theorem 4.3. From a proof P 0 ⊢ FC R , a term s can be extracted such RCA ω 0 proves that for any x (·) and X ⊂ R and g 1 , we have where the real in the consequent is defined by sup X (x (·) )(k) := t(x (·) , s(x (·) , 2 k )).
Proof. The nonstandard proof is trivial. For the remaining part, one readily proves using underspill that (∀x ∈ X)(∀N 0 ∈ Ω)(∃k ≤ N )(x k ≈ x) has the normal form . Similarly, a normal form for (∀x ∈ X)(∀N ∈ Ω)(x t(x (·) , N ))) is as follows: . Given these normal forms, Theorem 2.4 now readily yields the theorem.
The function g in the antecedent of (4.1) is a modulus of totally boundedness.
Admittedly, the previous result is rather basic but our aim was to show that (a) F -compactness is converted to totally boundedness, the preferred constructive component of compactness, as in the antecedent of (4.1), and (b) that Wattenberg correctly identifies F -compactness as having 'constructive potential' in [37,III].
With regard to (b), we now show that F -compactness cannot be (immediately) replaced with nonstandard compactness as in STP or STP R . To this end, we first prove that STP and STP R have equivalent normal forms as noted in Section 2.5. Note that a version of this theorem not involving STP R may be found in [20].
Theorem 4.4. In P, STP is equivalent to STP R and to the normal forms Proof. We first prove that STP and STP R are equivalent. Now, Hirst establishes in [8] that RCA 0 proves that every real x ∈ [0, 1] has a binary expansion, i.e.
Since P 0 proves the latter (both the internal version and the version relative to 'st'), it is clear that STP ↔ STP R .
Thirdly, assume STP and note that the contraposition of (4.4) yields: Since standard functionals have standard output for standard input, (4.5) implies: Pushing all standard quantifiers outside as far as possible, we obtain that Applying Idealisation I, we pull the standard quantifiers to the front as follows: Now assume (4.8) and note that since w is standard, all of its elements are, implying (4.7). Bringing all standard quantifiers inside again (as far as possible), we obtain (4.6). We now immediately obtain (4.5) by noting that ( )(αn ∈ T ) by applying HAC int and defining g(α) := max i<|Φ(α)| Φ(α)(i) as in Remark 2.10.
In conclusion, STP is equivalent to the normal form (4.2), and term extraction as in Theorem 2.4 converts the latter to the special fan functional introduced in Section 2.5. Since the latter boasts extreme computational hardness, it indeed seems better to avoid nonstandard compactness STP in favour of F -compactness. In the next section, we will show how computational content can still be obtained from STP and the special fan functional.

4.2.
The constructive status of nonstandard compactness. We investigate Standard Part in light of Wattenberg's claims that it be fundamentally non-constructive. By Theorem 3.19, a rather small fragment of Standard part is indeed fundamentally non-constructive. By contrast, we show in this section that STP, which is the particular fragment Wattenberg uses in [37, II-III], still yields constructive content, after some extra technical steps. This section is somewhat more technical in nature as we assume familiarity with the ECF-translation from [35, §2.6.5].
First of all, nonstandard continuity (2.13) clearly yields uniform nonstandard continuity (2.15) for the unit interval inside P 0 + STP by Theorem 4.4. Thus, the following version of IVT is immediate where the term t is as in (4.11).
. For nonstandard N 0 and nonstandard continuous f : We now show that this nonstandard version yields the following effective version.
Proof. Since P 0 proves IVT wat by Theorem 3.19, P 0 + STP proves IVT ′ wat , as in the latter system every nonstandard continuous function is automatically uniform nonstandard continuous on the unit interval by STP R and Theorem 4.4. To obtain the effective results from the theorem, one just proceeds as in Theorem 3.5 using the normal form (4.2) of STP.
Secondly, Theorem 4.7 is not very satisfactory as the special fan functional is not computable (in the sense of Kleene's S1-S9) in e.g. (∃ 2 ), or even the Suslin functional (See [20, §3] for these results). However, the following observation ( [13, §2]) by Kohlenbach will be seen to solve this problem in Theorem 4.9: Here, RCA 2 0 is essentially the base theory RCA 0 of Reverse Mathematics ([33, II]) formulated with function rather than set variables; the syntactical interpretation [ · ] ECF is defined in [35, §2.6.5] and is based on the Kleene-Kreisel model of continuous functionals. In the latter, higher-type objects are represented by so-called associates which is equivalent to the representation used in Reverse Mathematics by [14,Prop. 4.4] of continuous functionals on Baire space.
One often writes α(β), to be understood as α(βm) − 1 for large enough m as in the first item. Given an associate α 1 for Φ 2 , an associate γ 1 for Ψ 3 is now defined such that Ψ(Φ) is γ(α) where the latter is again γ(αk) − 1 for large enough k.
By way of an example, consider the intuitionistic fan functional as in MUC(Ω) from Section 2.5.3. Following the heuristic that all objects of type two or higher are replaced by associates by ECF, it is straightforward to see that [MUC(Ω)] ECF is: The underlined formula expresses that α 1 is an associate representing a (continuous) functional Y 2 , while TOF(γ) expresses that γ 1 is an associate for the intuitionistic fan functional, i.e. Ω(Y ) as in MUC(Ω) is given by γ(α), and the rest of TOF(γ) ensures that γ(α) makes sense.
Note that if a functional Φ 2 has an associate as in Definition 4.8, it is automatically continuous on Baire space. Thus, since µ 2 as in (µ 2 ) is discontinuous (e.g. at 00 . . . ), [(µ 2 )] ECF is equivalent to 0 = 1. In particular, we observe that the ECFtranslation replaces any type two variable with a type one variable over associates, i.e. the new variable ranges over (representations of) continuous functionals.
As a result of the aforementioned 'continuous replacement', WKL is equivalent (∃γ 1 )TOF(γ), and the latter is of course [(∃Ω 3 )MUC(Ω)] ECF . As it turns out, the intuitionistic fan functional even has a primitive recursive associate FAN which may be found in [19, p. 102]. We thus also have WKL ↔ TOF( FAN) (See [16, §7.3.4]). The following theorem shows that the special fan functional becomes 'more computable' thanks to ECF. We shall make use of the nonstandard axiom Note that NUC expresses that every type two functional is nonstandard uniformly continuous on Cantor space, akin to Brouwer's continuity theorem ( [6]).
Note that parts of Theorem 4.9 may be found in [20,28]. We have the following corollary pertaining to Theorem 4.7.
Corollary 4.10. From the proof of IVT ′ wat in P 0 + STP, a term v 1 can be extracted such that RCA 2 0 + WKL proves [IVT ′ ef ] ECF (v ( FAN)) . Proof. Apply the ECF-translation to the conclusion of Theorem 4.7.
Note that WKL is non-constructive, but the term v( FAN) is computable. Furthermore, the only real modification the ECF-translation bestows upong the intermediate value theorem from Theorem 4.7 is the replacement of continuous functions by associates (which can always be done given WKL by [14,Theorem 4.6]).
In conclusion, we have observed that STP is indeed non-constructive in nature in that it gives rise to the special fan functional as in Theorem 4.7. However, a somewhat technical detour (using the ECF-interpretation) still yields computational information as in Corollary 4.10.
4.3. Extreme value theorem. We briefly discuss Wattenberg's treatment from [37,III] of Weierstraß' extreme value theorem inside Nonstandard Analysis. 4.3.1. Preliminaries. The extreme value theorem (WMX) is a basic result from calculus and can be formulated as follows.
Theorem 4.11 (WMX). Suppose that X is compact and that f : X → R is continuous. Then there is x ∈ X such that (∀y ∈ X)(f (y) ≤ R f (x)).
As is well-known, WMX implies a non-trivial fragment of the law of excluded middle (See e.g. [2, I.6] or [17]) and is therefore rejected in constructive mathematics. A slight modification of Wattenberg's nonstandard version of WMX will be shown to yield the following effective version in Section 4.3.2, similar to [5, p. 89].
Theorem 4.12 (WMX ef (s)). For k 0 and f : X → R uniformly continuous with modulus g on the compact space X with modulus of totally boundedness h, we have (∀x ∈ X)(f (x) ≤ R f (s(f, g, h, k)) + 1 k ). Note that this version no longer involves Nonstandard Analysis. Furthermore, the term s is 'read off' from the (modified) Wattenberg proof. Thus, Wattenberg's claims about the effective content of Nonstandard Analysis are again at least partially correct. One the other hand, Wattenberg explicitly uses Transfer in the proof of [37,III.6], which is problematic if one is interested in computational content, as was established above.

4.3.2.
Constructive extreme value theorem and Nonstandard Analysis. Wattenberg proves various nonstandard versions of WMX inside Nonstandard Analysis in [37,III.7]. He refers to (a trivial reformulation of) the Theorem 4.13 below as a completely "constructive" version of the Extreme Value Theorem in [37, p. 308]. Note that Wattenberg uses the notion of an 'implementation' (See [37, Def. III.8]) rather than nonstandard uniform continuity, although both essentially amount to the same thing in this context. Theorem 4.13 (WMX wat ). For nonstandard N 0 , F -compact X with standard sequence x (·) , and nonstandard uniformly continuous f : X → R, we have (∀x ∈ X)(f (x) f (t(x (·) , N ))). Wattenberg proves WMX wat in [37,III.7] using (what amounts to) the following: (i) Fix a standard sequence x (·) and nonstandard N 0 as provided by the Fcompactness of X. (ii) Define t 0 := x 0 and t n+1 := t n if f (x n+1 ) f (t n ) and t n+1 = x n+1 if f (x n+1 ) f (t n ). Note that for n ≤ N , we have f (x n ) f (t N ). (iii) Since for every x ∈ X there is j ≤ N such that x j ≈ x, we have (∀x ∈ X)(f (x) f (t N )) by continuity. Note that item (iii) makes use of uniform nonstandard continuity. When working in IST, one would apply STP to t N to obtain a standard maximum for f . Note that a similar remark regarding Ω-CA as in Remark 3.7 applies to WMX wat .
Finally, we have the following theorem.
Theorem 4.14. From the proof of WMX wat in P 0 , a term u can be extracted such that RCA ω 0 proves WMX ef (u). Proof. The proof of WMX wat inside P 0 follows from the above steps (i)-(iii), assuming we use approximations (say up to precision 2 N for N from item (i)) to f (x i ) and f (t i ). One then applies Theorem 2.4 to P 0 ⊢ WMX wat to obtain the term u from the theorem, following Template 3.6.