# Effective infinitesimals in $\mathbb{R}$

Karel Hrbacek  K. Hrbacek, Department of Mathematics, City College of CUNY,
New York, NY 10031<EMAIL_ADDRESS>and  Mikhail G. Katz  M. Katz,
Department of Mathematics, Bar Ilan University, Ramat Gan 5290002 Israel
<EMAIL_ADDRESS>
###### Abstract.

We survey the effective foundations for analysis with infinitesimals developed
by Hrbacek and Katz in 2021, and detail some applications. Theories SPOT and
SCOT are conservative over respectively ZF and ZF+ADC. The range of
applications of these theories illustrates the fact that analysis with
infinitesimals requires no more choice than traditional analysis. The theory
SCOT incorporates in particular all the axioms of Nelson’s Radically
Elementary Probability Theory, which is therefore conservative over ZF+ADC.

###### Key words and phrases:

effective analysis; infinitesimals; nonstandard analysis

###### 2020 Mathematics Subject Classification:

Primary 26E35, Secondary 03A05, 03C25, 03C62, 03E70, 03H05

###### Contents

  1. 1 Introduction
  2. 2 Compactness in the extension view
  3. 3 Internal set theories
  4. 4 The axioms of SPOT and SCOT
    1. 4.1 Axioms of the theory SPOT
    2. 4.2 Additional principles
  5. 5 Compactness in internal set theories
  6. 6 Continuity
  7. 7 Continuous image of compacts
  8. 8 Characterisation of uniform continuity
  9. 9 Continuity implies uniform continuity
  10. 10 Heine–Borel theorem
  11. 11 Radically Elementary Probability Theory

##  1\. Introduction

Let ZF be the Zermelo–Fraenkel set theory. Let ZFC be the Zermelo–Fraenkel set
theory with the axiom of choice. Let ACC be the axiom of countable choice, and
ADC the axiom of (countable) dependent choice. The theories ZF, ZF+ACC, and
ZF+ADC have the advantage (over ZFC) of not entailing set-theoretic paradoxes
such as Banach–Tarski. Similarly, ZF, ZF+ACC, and ZF+ADC do not prove the
existence of nonprincipal ultrafilters.

The theories SPOT and SCOT developed in [7] provide frameworks for analysis
with infinitesimals that are conservative respectively over ZF and ZF+ADC, and
therefore share the same advantage (the axioms of SPOT and SCOT appear in
Section 4). Mathematicians generally consider theorems provable in ZF as more
effective than results that require the full ZFC for their proof, and many
feel this way not only about ZF but about ZF+ADC, as well. In this sense, the
theories SPOT and SCOT enable an effective development of analysis based on
infinitesimals. Some applications were already presented in [7], such as
(local) Peano’s existence theorem for first-order differential equations [7,
Example 3.5] and infinitesimal construction of Lebesgue measure via counting
measures [7, Example 3.6].

We first consider the case of compactness. In Section 2, we present the
traditional extension view. Following an outline of SPOT and SCOT in Sections
3 and 4, we deal with compactness in internal set theories in Section 5. After
preliminaries on continuity in Section 6, we present an effective proof using
infinitesimals of the compactness of a continuous image of a compact set in
Section 7. After preliminaries on uniform continuity in Sections 8 and 9, we
present an effective proof using infinitesimals of the Heine–Borel theorem in
Section 10. In Section 11, we show that Nelson’s _Radically Elementary
Probability Theory_ is a subtheory of SCOT.

##  2\. Compactness in the extension view

In this section, we analyze compactness from the viewpoint of traditional
extensions ${\mathbb{R}}\hookrightarrow{{}^{\ast}{\mathbb{R}}}$ to hyperreals.
These cannot be constructed in ZF+ADC and cannot be described as effective in
the sense of Section 1. In Section 5, we will present an effective treatment
of compactness in axiomatic frameworks for analysis with infinitesimals.

For ${\mathbb{N}}$, ${\mathbb{R}}$, $\mathbb{P}=\mathcal{P}({\mathbb{R}})$, or
any set $X$, the corresponding nonstandard extensions ${}^{\ast}X$, etc.
satisfying the transfer principle can be formed either via the compactness
theorem of first-order logic, or via ultrapowers $X^{\mathbb{N}}/\mathcal{F}$,
etc., in terms of a fixed nonprincipal ultrafilter $\mathcal{F}$.

######  Lemma 2.1.

For a finite union, the star of the union is the union of stars.

###### Proof.

Given sets $A,B\subseteq X$, we have

$(\forall{}y\in{}X)\big{[}y\in{}A\cup{}B\longleftrightarrow(y\in{}A)\vee(y\in{}B)\big{]}.$
(2.1)

Applying upward transfer to (2.1), we obtain

$(\forall{}y\in{}{}^{\ast}X)\big{[}y\in{}^{\ast}\\!(A\cup
B)\longleftrightarrow(y\in{{}^{\ast}A})\vee(y\in{}^{\ast}B)\big{]},$

and the claim follows by induction. ∎

######  Theorem 2.2.

If $\langle A_{n}\colon n\in{\mathbb{N}}\rangle$ is a nested sequence of
nonempty subsets of ${\mathbb{R}}$ then the sequence
$\langle{{}^{\ast}A}_{n}\colon n\in{\mathbb{N}}\rangle$ (standard $n$) has a
common point.

###### Proof.

Let $\mathbb{P}=\mathcal{P}({\mathbb{R}})$ be the set of all subsets of
${\mathbb{R}}$. Consider a sequence $\langle A_{n}\in\mathbb{P}\colon
n\in{\mathbb{N}}\rangle$ viewed as a function
$f\colon{\mathbb{N}}\to\mathbb{P},\;n\mapsto A_{n}$. By the extension
principle we have a function
${{}^{\ast}f}\colon{{}^{\ast}{\mathbb{N}}}\to{{}^{\ast}\mathbb{P}}$. Let
$B_{n}={{}^{\ast}f}(n)$. For each standard $n$, we have
$B_{n}={{}^{\ast}A}_{n}\in{{}^{\ast}\mathbb{P}}$.111The injective map
$\ast\colon\mathbb{P}\to{{}^{\ast}\mathbb{P}}$ sends $A_{n}$ to
${{}^{\ast}A}_{n}$. For each standard natural $n$ we have a symbol $a_{n}$ in
the appropriate language (including at least the names for all subsets of
${\mathbb{R}}$), whose standard interpretation is $A_{n}\in\mathbb{P}$.
Meanwhile the nonstandard interpretation of $a_{n}$ is the entity
${{}^{\ast}A}_{n}\in{{}^{\ast}\mathbb{P}}$. The sequence $\langle A_{n}\colon
n\in{\mathbb{N}}\rangle$ in $\mathbb{P}$ is the standard interpretation of the
symbol $a=\langle a_{n}\rangle$. Meanwhile, the nonstandard interpretation of
the symbol $a$ is $\langle B_{n}\colon n\in{{}^{\ast}{\mathbb{N}}}\rangle$ in
${{}^{\ast}\mathbb{P}}$. In particular, one has $B_{n}={{}^{\ast}A}_{n}$ for
standard $n$. For a nonstandard value of the index $n=H$, the entity
$B_{H}\in{{}^{\ast}\mathbb{P}}$ is by definition internal but is in general
not the natural extension of any subset of ${\mathbb{R}}$.

If $\langle A_{n}\rangle$ is a _nested_ decreasing sequence in
$\mathbb{P}\setminus\\{\varnothing\\}$ then by transfer $\langle
B_{n}:n\in{{}^{\ast}{\mathbb{N}}}\rangle$ is nested in
${{}^{\ast}\mathbb{P}}\setminus\\{\varnothing\\}$. Let $H$ be a fixed
nonstandard index. Since $n<H$ for each standard $n$, the set
${{}^{\ast}A}_{n}\subseteq{{}^{\ast}{\mathbb{R}}}$ includes $B_{H}$. Choose
any element $c\in B_{H}$. Then $c$ is contained in ${{}^{\ast}A}_{n}$ for each
standard $n$:

$c\in\bigcap_{n\in{\mathbb{N}}}{{}^{\ast}A}_{n}$

as required.222The conclusion of non-empty intersection remains valid for any
nested sequence of nonempty _internal_ sets, i.e., members of
${{}^{\ast}\mathbb{P}}$; see e.g., [5, Theorem 11.10.1, p. 138] (the proof is
more involved). ∎

######  Definition 2.3.

Let $I$ be a set. A collection $\mathcal{H}\subseteq\mathcal{P}(I)$ has the
_finite intersection property_ if the intersection of every nonempty finite
subcollection of $\mathcal{H}$ is nonempty, i.e.,

$B_{1}\cap\cdots\cap B_{n}\not=\varnothing\text{ for all
}n\in{\mathbb{N}}\text{ and all }B_{1},\ldots,B_{n}\in\mathcal{H}.$

Then Theorem 2.2 has the following equivalent formulation.

######  Corollary 2.4 (Countable Saturation).

If a family of subsets $\\{A_{n}\\}_{n\in{\mathbb{N}}}$ has the finite
intersection property (see Definition 2.3) then the intersection
$\bigcap_{n\in{\mathbb{N}}}{{}^{\ast}A}_{n}$ is nonempty.

Recall that a topological space $T$ is second-countable if its topology admits
a countable base. Recall that a space is Lindelöf if every open cover includes
a countable subcover. A second countable space is necessarily Lindelöf (over
ZF+ACC). If $T$ is a separable metric space then $T$ is second countable and
hence Lindelöf.

A point $y\in{}^{\ast}T$ is called _nearstandard in $T$_ if $y$ is infinitely
close to a standard point $p\in T$, i.e., such that $y$ is contained in the
star ${}^{\ast}U$ of every open neighborhood $U$ of $p$. The intersection of
all such ${}^{\ast}U$ is called the _halo_ of $p$. The relation $x\simeq y$
holds if and only if for all open sets $O$, $x\in{{}^{\ast}O}$ if and only if
$y\in{{}^{\ast}O}$.

######  Theorem 2.5.

Assume $T$ is Lindelöf. Then the following two conditions are equivalent:

  1. (1)

$T$ is compact (i.e., every open cover admits a finite subcover);

  2. (2)

every $y\in{}^{\ast}T$ is nearstandard in $T$.

###### Proof of $(1)\Rightarrow(2)$.

Assume $T$ is compact, and let $y\in{}^{\ast}T$. Let us show that $y$ is
nearstandard in $T$ (this direction does not require saturation).

Suppose on the contrary that $y$ is not nearstandard in $T$, i.e., $y$ is not
in the halo of any (standard) point $p\in T$. Then we can form the open cover
$\mathcal{U}$ of $T$ containing all open sets $U$ such that

$y\notin{}^{\ast}U.$ (2.2)

Since $T$ is compact, $\mathcal{U}$ includes a finite subcover
$U_{1},\ldots,U_{n}$. Applying Lemma 2.1 to the finite union
$T=U_{1}\cup\cdots\cup{}U_{n}$, we obtain

${}^{\ast}T={}^{\ast}U_{1}\cup\cdots\cup{}{}^{\ast}U_{n}.$

Hence $y$ is in one of the ${}^{\ast}U_{i}$, $i=1,\ldots,n$, contradicting
(2.2). The contradiction establishes that $y$ is necessarily nearstandard in
$T$. ∎

###### Proof of $(2)\Rightarrow(1)$.

This direction exploits saturation. Assume each $y\in{}^{\ast}T$ is
nearstandard in $T$. Given an open cover $\\{U_{a}\\}$ of $T$, we need to find
a finite subcover. Since $T$ is Lindelöf, we can assume that the cover is
countable.

Suppose on the contrary that no finite subcollection of $\\{U_{a}\\}$ covers
$T$. Then the complements $S_{a}$ of $U_{a}$ form a countable collection of
(closed) sets $\\{S_{a}\\}$ with the finite intersection property. Applying
countable saturation (Corollary 2.4) to this countable family, we conclude
that the intersection of all ${}^{\ast}S_{a}$ is non-empty. Let
$y\in\bigcap_{a}{}^{\ast}S_{a}$. By assumption, there is a point $p\in T$ such
that

$y\simeq p.$ (2.3)

Since $\\{U_{a}\\}$ is a cover of $T$, it contains a set $U_{b}$ such that
$p\in{}U_{b}$, and hence $y\in{}^{\ast}U_{b}$ since $U$ is open. But
$y\in{}^{\ast}S_{a}$ for all $a$, in particular $y\in{}^{\ast}S_{b}$, so
$y\not\in{}^{\ast}U_{b}$ by Lemma 2.1, contradicting (2.3). The contradiction
establishes the existence of a finite subcover. ∎

##  3\. Internal set theories

In this section we explain in what sense analysis with infinitesimals does not
require the axiom of choice any more than traditional non-infinitesimal
analysis, following [7]. There are two popular approaches to Robinson’s
nonstandard mathematics (including analysis with infinitesimals):

  1. (1)

model-theoretic, and

  2. (2)

axiomatic/syntactic.

For a survey of the various approaches see [3].

The model-theoretic approach (including the construction of the ultrapower)
typically relies on strong forms of the axiom of choice. The
axiomatic/syntactic approach turns out to be more economical in the use of
foundational material, and exploits a richer st-$\in$-language, as explained
below.

The traditional set-theoretic foundation for mathematics is Zermelo–Fraenkel
set theory (ZF). The theory ZF is a set theory formulated in the
$\in$-language. Here “$\in$” is the two-place membership relation. In ZF, all
mathematical objects are built up step-by-step starting from $\emptyset$ and
exploiting the one and only relation $\in$.

For instance, the inequality $0<1$ is formalized as the membership relation
$\emptyset\in\\{\emptyset\\}$, the inequality $1<2$ is formalized as the
membership relation $\\{\emptyset\\}\in\\{\emptyset,\\{\emptyset\\}\\}$, etc.
Eventually ZF enables the construction of the set of natural numbers
${\mathbb{N}}$, the ring of integers ${\mathbb{Z}}$, the field of real numbers
${\mathbb{R}}$, etc.

For the purposes of mathematical analysis, a set theory SPOT has been
developed in the more versatile st-$\in$-language (its axioms are given in
Section 4). Such a language exploits a predicate st in addition to the
relation $\in$. Here “st” is the one-place predicate standard so that st($x$)
is read “$x$ is standard”.

######  Theorem 3.1 ([7]).

The theory SPOT is a conservative extension of ZF.

This means that every statement in the $\in$-language provable in SPOT is
provable already in ZF. In particular, the axiom of choice and the existence
of non-principal ultrafilters are not provable is SPOT, because they are not
provable in ZF. Thus SPOT does not require any additional foundational
commitments beyond ZF.

######  Remark 3.2.

The Separation Axiom of ZF asserts, roughly, that for any $\in$-formula $\phi$
and any set $A$, there exists a set $S$ such that $x\in S$ if and only if
$x\in A\,\wedge\,\phi(x)$ is true. This remains valid in SPOT which is a
conservative extension of ZF. But Separation does not apply to formulas
involving the new predicate st. Specifically, Separation does not apply to the
predicate st itself.

######  Example 3.3.

The collection of standard natural numbers is not a set that could be
described as “$\\{x\in{\mathbb{N}}:{\rm st}(x)\\}$.” Such external collections
can be viewed informally as classes defined by the corresponding predicate.
Thus, in [7] one uses the _dashed curly brace_ notation $\raisebox{-6.0pt}{
\leavevmode\hbox to5.4pt{\vbox to17.47pt{\pgfpicture\makeatletter\hbox{\hskip
5.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@curveto{-1.50002pt}{0.64015pt}{-2.5pt}{2.13397pt}{-2.5pt}{4.26794pt}\pgfsys@lineto{-2.5pt}{4.26796pt}\pgfsys@curveto{-2.5pt}{6.40193pt}{-3.49998pt}{7.89575pt}{-5.0pt}{8.5359pt}\pgfsys@curveto{-3.49998pt}{9.17607pt}{-2.5pt}{10.66988pt}{-2.5pt}{12.80386pt}\pgfsys@lineto{-2.5pt}{12.80386pt}\pgfsys@curveto{-2.5pt}{14.93785pt}{-1.50002pt}{16.43166pt}{0.0pt}{17.07182pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to5.4pt{\vbox to17.47pt{\pgfpicture\makeatletter\hbox{\hskip
5.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@curveto{-1.50002pt}{0.64015pt}{-2.5pt}{2.13397pt}{-2.5pt}{4.26794pt}\pgfsys@lineto{-2.5pt}{4.26796pt}\pgfsys@curveto{-2.5pt}{6.40193pt}{-3.49998pt}{7.89575pt}{-5.0pt}{8.5359pt}\pgfsys@curveto{-3.49998pt}{9.17607pt}{-2.5pt}{10.66988pt}{-2.5pt}{12.80386pt}\pgfsys@lineto{-2.5pt}{12.80386pt}\pgfsys@curveto{-2.5pt}{14.93785pt}{-1.50002pt}{16.43166pt}{0.0pt}{17.07182pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}n\in{\mathbb{N}}:{\rm
st}(n)\raisebox{-6.0pt}{ \leavevmode\hbox to5.4pt{\vbox
to17.47pt{\pgfpicture\makeatletter\hbox{\hskip-16.87183pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@curveto{18.57184pt}{16.43167pt}{19.57182pt}{14.93785pt}{19.57182pt}{12.80388pt}\pgfsys@lineto{19.57182pt}{12.80386pt}\pgfsys@curveto{19.57182pt}{10.66989pt}{20.57181pt}{9.17607pt}{22.07182pt}{8.53592pt}\pgfsys@curveto{20.57181pt}{7.89575pt}{19.57182pt}{6.40195pt}{19.57182pt}{4.26796pt}\pgfsys@lineto{19.57182pt}{4.26796pt}\pgfsys@curveto{19.57182pt}{2.13397pt}{18.57184pt}{0.64017pt}{17.07182pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to5.4pt{\vbox
to17.47pt{\pgfpicture\makeatletter\hbox{\hskip-16.87183pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@curveto{18.57184pt}{16.43167pt}{19.57182pt}{14.93785pt}{19.57182pt}{12.80388pt}\pgfsys@lineto{19.57182pt}{12.80386pt}\pgfsys@curveto{19.57182pt}{10.66989pt}{20.57181pt}{9.17607pt}{22.07182pt}{8.53592pt}\pgfsys@curveto{20.57181pt}{7.89575pt}{19.57182pt}{6.40195pt}{19.57182pt}{4.26796pt}\pgfsys@lineto{19.57182pt}{4.26796pt}\pgfsys@curveto{19.57182pt}{2.13397pt}{18.57184pt}{0.64017pt}{17.07182pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ for such a class,
when convenient. Writing $k\in\raisebox{-6.0pt}{ \leavevmode\hbox
to5.4pt{\vbox to17.47pt{\pgfpicture\makeatletter\hbox{\hskip
5.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@curveto{-1.50002pt}{0.64015pt}{-2.5pt}{2.13397pt}{-2.5pt}{4.26794pt}\pgfsys@lineto{-2.5pt}{4.26796pt}\pgfsys@curveto{-2.5pt}{6.40193pt}{-3.49998pt}{7.89575pt}{-5.0pt}{8.5359pt}\pgfsys@curveto{-3.49998pt}{9.17607pt}{-2.5pt}{10.66988pt}{-2.5pt}{12.80386pt}\pgfsys@lineto{-2.5pt}{12.80386pt}\pgfsys@curveto{-2.5pt}{14.93785pt}{-1.50002pt}{16.43166pt}{0.0pt}{17.07182pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to5.4pt{\vbox to17.47pt{\pgfpicture\makeatletter\hbox{\hskip
5.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@curveto{-1.50002pt}{0.64015pt}{-2.5pt}{2.13397pt}{-2.5pt}{4.26794pt}\pgfsys@lineto{-2.5pt}{4.26796pt}\pgfsys@curveto{-2.5pt}{6.40193pt}{-3.49998pt}{7.89575pt}{-5.0pt}{8.5359pt}\pgfsys@curveto{-3.49998pt}{9.17607pt}{-2.5pt}{10.66988pt}{-2.5pt}{12.80386pt}\pgfsys@lineto{-2.5pt}{12.80386pt}\pgfsys@curveto{-2.5pt}{14.93785pt}{-1.50002pt}{16.43166pt}{0.0pt}{17.07182pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}n\in{\mathbb{N}}:{\rm
st}(n)\raisebox{-6.0pt}{ \leavevmode\hbox to5.4pt{\vbox
to17.47pt{\pgfpicture\makeatletter\hbox{\hskip-16.87183pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@curveto{18.57184pt}{16.43167pt}{19.57182pt}{14.93785pt}{19.57182pt}{12.80388pt}\pgfsys@lineto{19.57182pt}{12.80386pt}\pgfsys@curveto{19.57182pt}{10.66989pt}{20.57181pt}{9.17607pt}{22.07182pt}{8.53592pt}\pgfsys@curveto{20.57181pt}{7.89575pt}{19.57182pt}{6.40195pt}{19.57182pt}{4.26796pt}\pgfsys@lineto{19.57182pt}{4.26796pt}\pgfsys@curveto{19.57182pt}{2.13397pt}{18.57184pt}{0.64017pt}{17.07182pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to5.4pt{\vbox
to17.47pt{\pgfpicture\makeatletter\hbox{\hskip-16.87183pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} {}{}{} { {{}} {}
{}{}{} {}{}{} } { {{}} {} {}{}{} } }{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@moveto{17.07182pt}{17.07182pt}\pgfsys@curveto{18.57184pt}{16.43167pt}{19.57182pt}{14.93785pt}{19.57182pt}{12.80388pt}\pgfsys@lineto{19.57182pt}{12.80386pt}\pgfsys@curveto{19.57182pt}{10.66989pt}{20.57181pt}{9.17607pt}{22.07182pt}{8.53592pt}\pgfsys@curveto{20.57181pt}{7.89575pt}{19.57182pt}{6.40195pt}{19.57182pt}{4.26796pt}\pgfsys@lineto{19.57182pt}{4.26796pt}\pgfsys@curveto{19.57182pt}{2.13397pt}{18.57184pt}{0.64017pt}{17.07182pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ is equivalent to
writing “${\rm st}(k)$ (is true)”. In many cases the passage from a predicate
to a set turns out to be unnecessary: as mentioned in the introduction, in
SCOT (conservative over ZF+ADC) one can give an infinitesimal construction of
the Lebesgue measure; in BST (a modification of Nelson’s IST, possessing
better meta-mathematical properties), the Loeb measure can be handled, as
well; see [8].

######  Remark 3.4 (Sources in Leibniz).

The predicate st formalizes the distinction already found in Leibniz between
assignable and inassignable numbers. An inassignable (nonstandard) natural
number $\mu$ is greater than every assignable (standard) natural number. One
of the formulations of Leibniz’s _Law of Continuity_ posits that “the rules of
the finite are found to succeed in the infinite and vice versa” (cf. Robinson
[14, p. 266]), formalized by Robinson’s transfer principle. See further in
[1], [2], and [11].

If $\mu\in{\mathbb{N}}$ is a nonstandard integer, then its reciprocal
$\varepsilon=\frac{1}{\mu}\in{\mathbb{R}}$ is a positive infinitesimal
(smaller than every positive standard real). Such an $\varepsilon$ is a
nonstandard real number.

A real number smaller in absolute value than some standard real number is
called _limited_ , and otherwise _unlimited_. SPOT proves that every
nonstandard natural number is unlimited [7, Lemma 2.1].

The theory SPOT enables one to take the standard part, or shadow, of every
limited real number $r$, denoted $\operatorname{sh}(r)$. This means that the
difference $r-\operatorname{sh}(r)$ is infinitesimal.

The derivative of the standard function $f(x)$ is then
$\operatorname{sh}\big{(}\frac{f(x+\varepsilon)-f(x)}{\varepsilon}\big{)}$ for
nonzero infinitesimal $\varepsilon$. In more detail, we have the following.

######  Definition 3.5.

Let $f$ be a standard function, and $x$ a standard point. A standard number
$L$ is the _slope_ of $f$ at $x$ if

$(\forall^{in}\varepsilon)(\exists^{in}\lambda)\,f(x+\varepsilon)-f(x)=(L+\lambda)\varepsilon.$
(3.1)

where $\forall^{in}$ and $\exists^{in}$ denote quantification over
infinitesimals.333For further details, see note 4.

The Riemann integral of $f$ over $[a,b]$ (with $f,a,b$ standard), when it
exists, is the shadow of the sum $\sum_{i=1}^{\mu}f(x_{i})\varepsilon$ as $i$
runs from 1 to $\mu$, where the $x_{i}$ are the partition points of an equal
partition of $[a,b]$ into $\mu$ subintervals. For a fuller treatment see [7,
Example 2.8].

The (external) relation of infinite proximity $x\simeq y$ for
$x,y\in{\mathbb{R}}$ is defined by requiring $x-y$ to be infinitesimal.

##  4\. The axioms of SPOT and SCOT

We will now present the axioms that enable this effective approach
(conservative over ZF) to analysis with infinitesimals.

###  4.1. Axioms of the theory SPOT

SPOT is a subtheory of axiomatic (syntactic) theories developed in the 1970s
independently by Hrbacek [6] and Nelson [12]. In addition to the axioms of ZF,
SPOT has three axioms: Standard Part, Nontriviality, and Transfer (for the
historical origins of the latter see Remark 3.4):

> T (Transfer) Let $\phi$ be an $\in$-formula with standard parameters. Then
> $\forall^{\rm st}x\,\phi(x)\to\forall x\,\phi(x)$.

> O (Nontriviality) $\exists\nu\in{\mathbb{N}}\,\forall^{\rm
> st}n\in{\mathbb{N}}\,(n\not=\nu)$.

> SP (Standard Part) Every limited real is infinitely close to a standard
> real.

An equivalent existential version of the Transfer axiom is $\exists
x\;\phi(x)\implies\exists^{{\rm st}}x\;\phi(x)$, for $\in$-formulas $\phi~{}$
with standard parameters.

Nontriviality asserts simply that there exists a nonstandard integer.

An equivalent version of Standard Part is the following.

> SP′ (Standard Part)

$\forall A\subseteq{\mathbb{N}}\,\exists^{\rm
st}B\subseteq{\mathbb{N}}\,\forall^{\rm st}n\in{\mathbb{N}}\,(n\in
B\leftrightarrow n\in A).$

######  Remark 4.1.

The latter formulation can be motivated intuitively as follows. Given a real
number $0<r<1$, consider its base-2 decimal expansion. Let $A$ be the set of
ranks where digit $1$ appears. The set $A$ is not standard if $r$ is not
standard. The corresponding standard set $B$ (whose existence is postulated by
SP′) can be thought of as the set of nonzero digits of the shadow
$\operatorname{sh}(r)$ of $r$. The fact that $r$ and $\operatorname{sh}(r)$
are infinitely close reflects the fact that $A$ and $B$ agree at all limited
ranks. The detailed argument is a bit more technical because binary
representation (like decimal representation) is not unique; see [7, Lemma
2.4].

In the model-theoretic frameworks one has three categories of sets: sets that
are natural extensions of, say, subsets of ${\mathbb{R}}$, more general
internal sets, as well as external sets. In the axiomatic frameworks, the
standard and nonstandard sets correspond to the natural extensions and the
internal sets, whereas there are no external sets.

###  4.2. Additional principles

Recall that SPOT proves that standard integers are an initial segment of
${\mathbb{N}}$ [7, Lemma 2.1].

######  Lemma 4.2 (Countable Idealisation).

Let $\phi$ be an $\in$-formula with arbitrary parameters. The theory SPOT
proves the following:

$\forall^{\rm st}n\in{\mathbb{N}}\;\exists x\;\forall m\in{\mathbb{N}}\;(m\leq
n\rightarrow\phi(m,x))\;\longleftrightarrow\;\exists x\;\forall^{\rm
st}n\in{\mathbb{N}}\;\phi(n,x).$

This is proved in [7, Lemma 2.2]. One could elucidate Countable Idealization
by means of an equivalent version with countable $A$ in words as follows. If
for every standard finite subset $a\subseteq A$ there is some $x$ such that
for all $z\in a$, one has $\phi(z,x)$, then there is a single $x$ such that
$\phi(z,x)$ holds for all standard $z\in A$ simultaneously (the converse is
obvious given that all elements of a standard finite set are standard, which
is a consequence of [7, Lemma 2.1]). This is analogous to saturation (see
Corollary 2.4).

######  Definition 4.3.

SN is the standardisation principle for st-$\in$-formulas with no parameters.
Namely, let $\phi(v)$ be an ${\rm st}$-$\in$-formula with no parameters. Then

$\forall^{\rm st}\\!A\;\exists^{\rm st}S\;\forall^{\rm st}x\;(x\in
S\longleftrightarrow x\in A\,\wedge\,\phi(x)).$ (4.1)

It is proved in [7, Lemma 6.1] that SN is equivalent to standardisation for
formulas with only standard parameters.

Although separation does not hold, SN is a kind of _approximation_ to it in
the following sense. The standard elements of $S$ (but not all elements) are
exactly those for which $\phi(x)$ holds. Note also that the assumption that
all parameters are standard is necessary to maintain conservativity over ZF,
because otherwise one could prove the existence of nonprincipal ultrafilters
(see [7]).

Note that SPOT+SN is also conservative over ZF [7, Theorem B, p. 4]. The axiom
SN enables one to give a simple infinitesimal definition of the derivative
function conservatively over ZF.444To dot the i’s, let $\phi_{f}(x,L)$ be the
formula of (3.1) depending on the standard parameter $f$, a real-valued
function. Let $A={\mathbb{R}}^{2}$ in (4.1). Then passing from $f$ to
$f^{\prime}$ is enabled by the following consequence of (4.1) containing only
standard parameters: $\exists^{\rm st}f^{\prime}\;\forall^{\rm
st}(x,L)\;\big{(}(x,L)\in
f^{\prime}\longleftrightarrow(x,L)\in{\mathbb{R}}^{2}\wedge\phi_{f}(x,L)\big{)}$
where $f^{\prime}$ is thought of as its graph in the plane.

SCOT incorporates the following choice-type axiom CC (which is a strengthening
of SP); see [7, Section 3, p. 10].

######  Definition 4.4.

(CC) Let $\phi(u,v)$ be an ${\rm st}$-$\in$-formula with arbitrary parameters.
Then

$\forall^{{\rm st}}n\in{\mathbb{N}}\;\exists
x\;\phi(n,x)\;\longrightarrow\;\exists f\,(f\text{ is a
function}\,\wedge\,\forall^{{\rm st}}n\in{\mathbb{N}}\;\phi(n,f(n)).$

The following definition was given in [7, p. 10].

######  Definition 4.5.

SCOT is the theory SPOT+ADC+SN+CC.

SCOT (in fact, its subtheory SPOT+CC) also proves the following statement SC
[7, Lemma 3.1].

######  Definition 4.6.

SC (Countable Standardisation) Let $\psi(v)$ be an ${\rm st}$-$\in$-formula
with arbitrary parameters. Then

$\exists^{{\rm st}}S\;\forall^{{\rm st}}n\;(n\in S\longleftrightarrow
n\in{\mathbb{N}}\,\wedge\,\psi(n)).$

##  5\. Compactness in internal set theories

In this section, we use infinitesimals to deal with compactness conservatively
over ZF or ZF+ADC, as indicated below (the traditional extension view was
already elaborated in Section 2).

Let $T$ be a standard topological space. A point $x\in T$ is _nearstandard in
$T$_ if there is a standard $p\in T$ such that $p\in O$ implies $x\in O$ for
every standard open set $O$ (in other words, $x$ is in the _halo_ of $p$.)

######  Lemma 5.1.

Assume $T$ is a standard Lindelöf space. If every $x$ in $T$ is nearstandard
in $T$ then $T$ is compact.

###### Proof.

Suppose $T$ is not compact. By downward transfer, there is a standard
countable cover $\mathcal{U}$ of $T$ by open sets such that for every
(standard) finite $k$-tuple $O_{1},\ldots,O_{k}\in\mathcal{U}$ there is a
$p\in T\setminus\bigcup_{1\leq i\leq k}O_{i}$. By Countable Idealisation with
the standard parameters $T$, $\mathcal{U}$, there is $x\in T$ such that
$x\not\in O$ for any standard $O\in\mathcal{U}$. Such an $x$ is not
nearstandard in $T$, because if $x$ were in the halo of some standard $p\in
T$, we would have a standard $O\in\mathcal{U}$ such that $p\in O$
($\mathcal{U}$ is a cover) and hence $x\in O$, a contradiction.555An analogous
proof goes through for arbitrary standard topological spaces if one has _full_
idealisation (with standard parameters) such as in the theory BSPT′ [7], which
is still conservative over ZF (unfortunately it is not known whether SN can be
added to it conservatively over ZF). Note that BSPT′ proves the existence of a
finite set containing all standard reals [7, p. 10]. Such sets are used in
Benci’s approach to measure theory. ∎

######  Lemma 5.2.

Assume $T$ is a standard second countable space. If $T$ is compact then every
$x\in T$ is nearstandard in $T$.

###### Proof.

Suppose $\mu\in T$ is not nearstandard in $T$. Then for every standard $p\in
T$ there is a standard open set $O$ such that $p\in O$ and $\mu\not\in O$. Let
$\mathcal{B}$ be a standard countable base for the topology of $T$, and let

$\mathcal{U}=\,{}^{\rm st}\\{O\in\mathcal{B}:\mu\not\in O\\}.$

This set is obtained by SC (Countable Standardisation, see Definition 4.6)
with a nonstandard parameter (namely, $\mu$), available in SCOT [7, Lemma
3.1]. By the above and transfer, $\mathcal{U}$ is a standard open cover of
$T$. If $T$ were compact, $\mathcal{U}$ would have, by transfer, a standard
finite open subcover $O_{1},\ldots,O_{k}$. Then $\mu\in O_{i}$ for some $1\leq
i\leq k$, contradicting the definition of $\mathcal{U}$. ∎

Since second countable implies Lindelöf, we have the equivalence of the two
definitions of compactness, for second-countable spaces in SCOT.

##  6\. Continuity

Based on the results of Section 5, the following can be proved conservatively
over ZF+ADC using infinitesimals. We will first discuss continuity over SPOT.

In this section, $f$ is a standard map between standard topological spaces.
$f$ is said to be S-_continuous at_ $c$ if whenever $x\simeq c$, one has
$f(x)\simeq f(c)$.

######  Lemma 6.1.

If a standard map $f$ from a first countable topological space into a
topological space is S-continuous at a standard point $c$ then $f$ is
continuous at $c$.

###### Proof.

Let $\mathcal{B}_{c}$ be a standard countable base of open neighborhoods of
$c$. Assume that $f$ is not continuous at $c$. Then there is a standard open
neighborhood $U$ of $f(c)$ such that for every (standard) finite
$O_{1},\ldots,O_{k}\in\mathcal{B}_{c}$ there is $x\in\bigcap_{1\leq i\leq
k}O_{i}$ with $f(x)\notin U$. By Countable Idealization there is $x$ such that
$x\in O$ holds for all standard $O\in\mathcal{B}_{c}$ and $f(x)\notin U$. Then
$x\simeq c$ and $f(x)\not\simeq f(c)$, a contradiction. ∎

######  Lemma 6.2.

If a standard function $f$ is continuous at a standard point $c$ then $f$ is
S-continuous at $c$.

###### Proof.

Assume that $f$ is not S-continuous at $c$. Then there is $x\simeq c$ for
which $f(x)\not\simeq f(c)$, i.e., $f(x)\notin U$ holds for some standard
neighborhood $U$ of $f(c)$. By continuity of $f$ there is a standard open
neighborhood $O$ of $c$ such that $z\in O$ implies $f(z)\in U$. As $x\simeq
c$, we have $x\in O$ and hence $f(x)\in U$, a contradiction. ∎

##  7\. Continuous image of compacts

We prove the following well-known result in SCOT.

######  Theorem 7.1.

Let $f:T\to Y$ be a continuous map between second-countable topological
spaces. Let $E\subseteq T$ be compact. Then $f(E)$ is compact.

###### Proof.

We prove the theorem under the assumption that $f,T,Y$ are standard; its
validity for arbitrary $f,T.Y$ follows by transfer. By Lemma 5.2, every point
$x\in E$ is infinitely close to a standard point $p\in E$. By the nonstandard
characterisation of continuity of $f$ (Lemma 6.2), the point $f(x)$ is
infinitely close to $f(p)$. Thus every point $f(x)$ in the image $f(E)$ is
infinitely close to a standard point $f(p)\in f(E)$. By Lemma 5.1, applied to
$f(E)$, the space $f(E)$ is compact. ∎

The proof compares favorably with the traditional proof using pullbacks of
open covers, and is as effective (in the sense explained in Section 1) as the
traditional proof.

##  8\. Characterisation of uniform continuity

Let $D,E$ be standard metric spaces; we will denote the distance functions by
$|\cdot|$. A standard map $f\colon D\to E$ is _uniformly continuous_ on $D$ if

$\displaystyle(\forall\epsilon$
$\displaystyle\in{\mathbb{R}}^{+})(\exists\delta\in{\mathbb{R}}^{+})$ (8.1)
$\displaystyle\underline{(\forall x\in D)(\forall x^{\prime}\in
D)\;\big{[}|x^{\prime}-x|<\delta\rightarrow|f(x^{\prime})-f(x)|<\epsilon\big{]}.}$

$f$ is _S-continuous on_ $D$ if

$(\forall x\in D)(\forall x^{\prime}\in D)\left[x\simeq
x^{\prime}\;\rightarrow\;f(x)\simeq f(x^{\prime})\right].$ (8.2)

######  Lemma 8.1.

If $f$ is uniformly continuous on $D$ then it is $S$-continuous there.

###### Proof.

To show that condition (8.1) implies (8.2), fix a standard parameter
$\epsilon$. By downward transfer, there is a standard $\delta$ such that the
underlined part of formula (8.1) holds:

$(\forall x\in D)(\forall x^{\prime}\in
D)\;\big{[}|x^{\prime}-x|<\delta\rightarrow|f(x^{\prime})-f(x)|<\epsilon\big{]}.$
(8.3)

If $x\simeq x^{\prime}$ then the condition $|x-x^{\prime}|<\delta$ is
satisfied regardless of the value of the standard number $\delta>0$. Therefore

$|f(x^{\prime})-f(x)|<\epsilon.$ (8.4)

Since (8.4) is true for each standard $\epsilon>0$, we conclude that
$f(x^{\prime})\simeq f(x)$, proving (8.2). ∎

######  Lemma 8.2.

If $f$ is S-continuous on $D$ then $f$ is uniformly continuous there.

###### Proof.

We will show the contrapositive statement, namely that $\neg\eqref{e571z}$
implies $\neg\eqref{i2b}$. Assume the negation of (8.1). By downward transfer
it follows that there exists a standard number $\epsilon>0$ such that

$(\forall\delta\in{\mathbb{R}}^{+})(\exists x\in D)(\exists x^{\prime}\in
D)\;\big{[}|x^{\prime}-x|<\delta\;\wedge\;|f(x^{\prime})-f(x)|>\epsilon\big{]}.$
(8.5)

The formula is true for all positive $\delta$, so in particular it holds for
an infinitesimal $\delta_{0}>0$. For this value, we obtain

$(\exists x\in D)(\exists x^{\prime}\in
D)\;\big{[}|x^{\prime}-x|<\delta_{0}\;\wedge\;|f(x^{\prime})-f(x)|>\epsilon\big{]}.$
(8.6)

Fix such $x$ and $x^{\prime}$. The condition $|x^{\prime}-x|<\delta_{0}$
implies that $x\simeq x^{\prime}$, while $|f(x^{\prime})-f(x)|>\epsilon$. As
the lower bound $\epsilon>0$ is standard, it follows that
$f(x^{\prime})\not\simeq f(x)$. This violates condition (8.2) and establishes
the required contrapositive implication
$\neg\eqref{e571z}\implies\neg\eqref{i2b}$. ∎

##  9\. Continuity implies uniform continuity

As shown in Section 8, the theory SPOT proves that uniform continuity of a map
between metric spaces amounts to S-continuity at all points (standard and
nonstandard) of the domain.

######  Theorem 9.1.

A continuous map from a compact metric space to a metric space is uniformly
continuous.

###### Proof.

Let $f:E\to Y$ where $f,E,Y$ are standard. By the characterisation of the
compactness of $E$ (Lemma 5.2), if $x\in E$ then $x$ is infinitely close to a
standard point $p\in E$. For each $x^{\prime}\simeq x$, one has
$x^{\prime}\simeq p\simeq x$. If $f$ is continuous at $p$ then
$f(x^{\prime})\simeq f(p)\simeq f(x)$, and therefore $f$ is S-continuous at
all points of $E$, establishing uniform continuity by Lemma 8.2. By transfer,
the theorem holds for arbitrary $f,E,Y$. ∎

This proof in SPOT compares favorably with the traditional proof: given
$\epsilon>0$, we need to find $\delta>0$ such that if $d_{E}(x,y)<\delta$ then
one has $d_{Y}(f(x),f(y))<\epsilon$. By continuity, for each $x\in E$ there
exists a $\delta_{x}>0$ such that if $d(x,y)<\delta_{x}$ then
$d(f(x),f(y))<\frac{\epsilon}{2}$. Then

$\left\\{B(x,\tfrac{\delta_{x}}{2}):x\in E\right\\}$

is an open cover of $E$. By compactness, there are points
$x_{1},\ldots,x_{n}\in E$ such that
$\left\\{B(x_{1},\frac{\delta_{1}}{2}),\ldots,B(x_{n},\frac{\delta_{n}}{2})\right\\}$
is a finite subcover covering $E$. Let
$\delta=\min(\frac{\delta_{1}}{2},\ldots,\frac{\delta_{n}}{2})$. If $y,z\in E$
and $d(y,z)<\delta\leq\frac{\delta_{k}}{2}$ for each $k=1,\ldots,n$, then by
the triangle inequality

$d(x_{k},z)\leq
d(x_{k},y)+d(y,z)\leq\tfrac{\delta_{k}}{2}+\tfrac{\delta_{k}}{2}<\delta_{k}.$

Therefore

$d(f(y),f(z))\leq
d(f(y),f(x_{k}))+d(f(x_{k}),f(z))<\tfrac{\epsilon}{2}+\tfrac{\epsilon}{2}=\epsilon,$

establishing uniform continuity.

##  10\. Heine–Borel theorem

Here we present an effective approach to the Heine–Borel theorem exploiting
the characterisation of compactness of Section 5. A standard set $C$ in a
standard metric space is _closed_ if every standard element near some element
of $C$ is actually in $C$. It is _bounded_ 666Here $C$ must be a subset of a
metric space for the notion of boundedness to make sense. Note that Countable
Idealisation (CI) is needed to prove its equivalence to the usual definition
“There is a real $r$ such that for all $x\in C$, $d(x,p)<r$ holds for some
(equivalently, all) $p\in C$.” CI is available in SPOT. if it contains no
unlimited elements. If standard $x$ and $y$ are infinitely close then $x=y$.

######  Lemma 10.1.

If $C$ is compact then it is closed and bounded.

###### Proof.

Every element of $C$ is nearstandard in $C$ by compactness, so there are no
unlimited elements, i.e., $C$ is bounded. Let a standard point $x$ be
infinitely close to some $y\in C$. By compactness of $C$ there is a standard
$z\in C$ such that $z\simeq y$. Thus $x=z\in C$ and $C$ is closed. ∎

######  Lemma 10.2.

For standard $n$, if $C\subseteq{\mathbb{R}}^{n}$ is closed and bounded then
it is compact.

###### Proof.

For standard $n$, the condition of infinite proximity in ${\mathbb{R}}^{n}$
amounts to the condition of infinite proximity for each of the $n$
coordinates. A similar remark applies to boundedness.

Let $x\in C$. Since $C$ is bounded, $x$ is limited and hence infinitely close
to a standard $y\in{\mathbb{R}}^{n}$. By closure, $y\simeq x$ entails $y\in
C$. Thus $x$ is nearstandard in $C$. This proves that $C$ is compact. ∎

##  11\. Radically Elementary Probability Theory

Nelson’s _Radically Elementary Probability Theory_ is based on traditional
mathematics plus axioms 1 through 5 stated in [13, Section 4, pp. 13–14]. The
axioms 1 through 4 hold in SPOT. Axiom 5, which according to Nelson is rarely
used, is the axiom CC (see Definition 4.4). It follows that _Radically
Elementary Probability Theory_ is conservative over ZF+ADC. Furthermore, it
follows that all results from [13] automatically hold in SCOT. In particular,
this includes Nelson’s S-integral.

Further applications include proofs in SPOT of Peano and Osgood theorems for
ordinary differential equations [9].

Our perspective fits with a relative view of the foundations of mathematics
such as that provided by Hamkins’ multiverse. For the relation between the
Gitman–Hamkins “toy” model of the multiverse [4] and nonstandard analysis, see
Fletcher et al. [3, Section 7.3].

Acknowledgment. The authors wish to thank the referee for his constructive
critique of the first draft. We are grateful to Karl Kuhlemann for helpful
comments.

## References

  * [1] J. Bair, P. Błaszczyk, R. Ely, M. Katz, and K. Kuhlemann, _Procedures of Leibnizian infinitesimal calculus: An account in three modern frameworks_ , British Journal for the History of Mathematics 36 (2021), no. 3, 170–209. https://doi.org/10.1080/26375451.2020.1851120, https://arxiv.org/abs/2011.12628, https://mathscinet.ams.org/mathscinet-getitem?mr=4353153
  * [2] J. Bair, A. Borovik, V. Kanovei, M. Katz, S. Kutateladze, S. Sanders, D. Sherry, and M. Ugaglia, _Historical infinitesimalists and modern historiography of infinitesimals_ , Antiquitates Mathematicae 16 (2022), 189–257. http://arxiv.org/abs/2210.14504, https://doi.org/10.14708/am.v16i1.7169
  * [3] P. Fletcher, K. Hrbacek, V. Kanovei, M. Katz, C. Lobry, and S. Sanders, _Approaches to analysis with infinitesimals following Robinson, Nelson, and others_ , Real Analysis Exchange 42 (2017), no. 2, 193–252. https://arxiv.org/abs/1703.00425, http://doi.org/10.14321/realanalexch.42.2.0193
  * [4] V. Gitman and J. Hamkins, _A natural model of the multiverse axioms_ , Notre Dame Journal of Formal Logic, 51 (2010), no. 4, 475–484.
  * [5] R. Goldblatt, _Lectures on the hyperreals. An introduction to Nonstandard Analysis_ , Springer, 1998.
  * [6] K. Hrbacek, _Axiomatic foundations for nonstandard analysis_ , Fundamenta Mathematicae 98 (1978), no. 1, 1–19.
  * [7] K. Hrbacek and M. Katz, _Infinitesimal analysis without the Axiom of Choice_ , Annals of Pure and Applied Logic 172 (2021), no. 6, 102959. https://doi.org/10.1016/j.apal.2021.102959, https://arxiv.org/abs/2009.04980
  * [8] K. Hrbacek and M. Katz, _Constructing nonstandard hulls and Loeb measures in internal set theories_ , Bulletin of Symbolic Logic 29 (2023), no. 1, 97–127. https://www.doi.org/10.1017/bsl.2022.43, https://arxiv.org/abs/2301.00367
  * [9] K. Hrbacek and M. Katz, _Peano and Osgood theorems via effective infinitesimals_ , in preparation (2023).
  * [10] V. Kanovei and M. Reeken, _Nonstandard Analysis, Axiomatically_ , Springer-Verlag, Berlin Heidelberg New York, 2004.
  * [11] M. Katz, K. Kuhlemann, D. Sherry, and M. Ugaglia, _Leibniz on bodies and infinities: rerum natura and mathematical fictions_ , Review of Symbolic Logic (2023). https://www.doi.org/10.1017/S1755020321000575, https://arxiv.org/abs/2112.08155
  * [12] E. Nelson, _Internal set theory: a new approach to nonstandard analysis_ , Bulletin of the American Mathematical Society 83 (1977), no. 6, 1165–1198.
  * [13] E. Nelson, _Radically Elementary Probability Theory_ , Annals of Mathematics Studies 117, Princeton University Press, Princeton, NJ, 1987, 98 pp.
  * [14] A. Robinson, _Non-standard analysis_ , North-Holland Publishing, Amsterdam, 1966.