# Multi-level Nonstandard Analysis and the Axiom of Choice

Karel Hrbacek  Department of Mathematics
City College of CUNY
New York, NY 10031
<EMAIL_ADDRESS>
(Date: April 19, 2024)

###### Abstract.

Model-theoretic frameworks for Nonstandard Analysis depend on the existence of
nonprincipal ultrafilters, a strong form of the Axiom of Choice
($\mathbf{AC}$). Hrbacek and Katz, APAL 72 (2021) formulate axiomatic
nonstandard set theories $\mathbf{SPOT}$ and $\mathbf{SCOT}$ that are
conservative extensions of respectively $\mathbf{ZF}$ and
$\mathbf{ZF}+\mathbf{ADC}$ (the Axiom of Dependent Choice), and in which a
significant part of Nonstandard Analysis can be developed. The present paper
extends these theories to theories with many levels of standardness, called
respectively $\mathbf{SPOTS}$ and $\mathbf{SCOTS}$. It shows that Jin’s recent
nonstandard proof of Szemerédi’s Theorem can be carried out in
$\mathbf{SPOTS}$, which is conservative over $\mathbf{ZF}+\mathbf{ACC}$ (the
Axiom of Countable Choice). The theory $\mathbf{SCOTS}$ is a conservative
extension of $\mathbf{ZF}+\mathbf{ADC}$.

###### Key words and phrases:

nonstandard analysis; levels of standardness; levels of infinity; axiom of
choice; iterated ultrapower, Szemerédi’s theoerm

###### Contents

  1. 1 Introduction
  2. 2 Theories SPOT and SCOT
  3. 3 Ultrafilters, ultrapowers, and their iterations
  4. 4 SPOTS
  5. 5 Jin’s proof of Ramsey’s Theorem in SPOTS
  6. 6 Jin’s proof of Szemerédi’s theorem in SPOTS
  7. 7 Analysis with ultrasmall numbers
  8. 8 Conservativity
    1. 8.1 Forcing
    2. 8.2 Generic Extensions
    3. 8.3 Conservativity of $\mathbf{SCOTS}$ over $\mathbf{ZF}+\mathbf{ADC}$.
    4. 8.4 Finitistic proofs
    5. 8.5 Conservativity of $\mathbf{SPOTS}$ over $\mathbf{ZF}+\mathbf{ACC}$.
    6. 8.6 Conservativity of $\mathbf{SPOT}^{+}$ over $\mathbf{ZF}$.

##  1\. Introduction

Nonstandard Analysis is sometimes criticized for its implicit dependence on
the Axiom of Choice ($\mathbf{AC}$) (see eg. Connes [5]111 Detailed
examination of Connes’s views is carried out in Kanovei, Katz and Mormann
[22], Katz and Leichtnam [25] and Sanders [31]. ). Indeed, model-theoretic
frameworks based on hyperreals require the existence of nonprincipal
ultrafilters over $\mathbb{N}$, a strong form of $\mathbf{AC}$: If $\ast$ is
the mapping that assigns to each $X\subseteq\mathbb{N}$ its nonstandard
extension ${}^{\ast}\\!X$, and if
$\nu\in{}^{\ast}\mathbb{N}\setminus\mathbb{N}$ is an unlimited integer, then
the set $U=\\{X\subseteq\mathbb{N}\,\mid\,\nu\in{}^{\ast}\\!X\\}$ is a
nonprincipal ultrafilter over $\mathbb{N}$.

The common axiomatic/syntactic frameworks for nonstandard methods (see Kanovei
and Reeken [23]), such as IST or HST, include ZFC among their axioms. The
dependence on $\mathbf{AC}$ cannot be avoided by simply removing it from the
list of axioms (see [13]). These theories postulate some version of the
_Standardization Principle_ :

_For every formula $\Phi$ in the language of the theory (possibly with
parameters) and every standard set $A$ there exists a standard set $S$ such
that for all standard $x$,_ $x\in S\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x).$
This set is denoted ${}^{\operatorname{\mathbf{st}}}\\{x\in A\mid\Phi(x)\\}$.
It follows that, for an unlimited $\nu\in\mathbb{N}$, the standard set
$U={}^{\operatorname{\mathbf{st}}}\\{X\in\mathcal{P}(\mathbb{N})\,\mid\,\nu\in
X\\}$ is a nonprincipal ultrafilter over $\mathbb{N}$.

_All work in Nonstandard Analysis based on these two familiar frameworks thus
depends essentially on the Axiom of Choice._ 222 Nonstandard Analysis that
does not use $\mathbf{AC}$, or uses only weak versions of it, can be found in
the work of Chuaqui, Sommer and Suppes (see eg. [33]), in papers on Reverse
Mathematics of Nonstandard Analysis (eg. Keisler [27], Sanders [30], van den
Berg et al. [3] and others), and in the work of Hrbacek and Katz based on
$\mathbf{SPOT}$/$\mathbf{SCOT}$ (see [15, 16, 17] and the present paper).

While strong forms of $\mathbf{AC}$ (Zorn’s Lemma, Prime Ideal Theorem) are
instrumental in many abstract areas of mathematics, such as general topology
(the product of compact spaces is compact), measure theory (there exist sets
that are not Lebesgue measurable) or functional analysis (Hahn-Banach
theorem), it is undesirable to have to rely on them for results in “ordinary”
mathematics such as Calculus, finite combinatorics and number theory.333 The
issue is not the validity of such results but the method of proof. It is a
consequence of Shoenfield’s Absoluteness Theorem (Jech [19], Theoerm 98) that
all $\Pi^{1}_{4}$ sentences of second-order arithmetic that are provable in
ZFC are also provable in $\mathbf{ZF}$. Most theorems of number theory and
real analysis (e.g. Peano’s Theorem; see J. Hanson’s answer in [10]) can be
formalized as $\Pi^{1}_{4}$ statements. But the $\mathbf{ZF}$ proofs obtained
from ZFC proofs by this method are far from “ordinary.”

Hrbacek and Katz [15] introduced nonstandard set theories $\mathbf{SPOT}$ and
$\mathbf{SCOT}$. In order to avoid the reliance on $\mathbf{AC}$,
Standardization needs to be weakened. The theory $\mathbf{SPOT}$ has three
simple axioms: Standard Part, Nontriviality and Transfer. It is a subtheory of
the better known nonstandard set theories IST and HST, but unlike them, it is
a conservative extension of $\mathbf{ZF}$. Arguments carried out in
$\mathbf{SPOT}$ thus do not depend on any form of $\mathbf{AC}$. Infinitesimal
analysis can be conducted in $\mathbf{SPOT}$ in the usual way. It only needs
to be verified that any use of Standardization can be justified by the special
cases of this principle that are available in $\mathbf{SPOT}$.

Traditional proofs in “ordinary” mathematics either do not use $\mathbf{AC}$
at all, or refer only to its weak forms, notably the Axiom of Countable Choice
($\mathbf{ACC}$) or the stronger Axiom of Dependent Choice ($\mathbf{ADC}$).
These axioms are generally accepted and often used without comment. They are
necessary to prove eg. the equivalence of the $\varepsilon$-$\delta$
definition and the sequential definition of continuity at a given point for
functions $f:X\subseteq\mathbb{R}\to\mathbb{R}$, or the countable additivity
of Lebesgue measure, but they do not imply the strong consequences of
$\mathbf{AC}$ such as the existence of nonprincipal ultrafilters or the
Banach–Tarski paradox. The theory $\mathbf{SCOT}$ is obtained by adding to
$\mathbf{SPOT}$ the external version of the Axiom of Dependent Choice; it is a
conservative extension of $\mathbf{ZF}$\+ $\mathbf{ADC}$.

Nonstandard Analysis with _multiple levels of standardness_ has been used in
combinatorics and number theory by Renling Jin, Terence Tao, Mauro Di Nasso
and others. Jin [20] recently gave a groundbreaking nonstandard proof of
Szemerédi’s Theorem:

_If $D\subseteq\mathbb{N}$ has a positive upper density, then $D$ contains a
$k$-term arithmetic progression for every $k\in\mathbb{N}$_
in a model-theoretic framework that has three levels of infinity.

The main objective of this paper is to extend the above two theories to
theories $\mathbf{SPOTS}$ and $\mathbf{SCOTS}$ with many levels of
standardness and consider their relationship to $\mathbf{AC}$. An outline of
$\mathbf{SPOT}$ and $\mathbf{SCOT}$ is given in Section 2. Section 3 reviews
the familiar properties of ultrapowers and iterated ultrapowers in a form
suitable to motivate multi-level versions of these theories, which are
formulated in Section 4. The next three sections illustrate various ways to
use multiple levels of standardness. In Section 5 Jin’s proof of Ramsey’s
Theorem is formalized in $\mathbf{SPOTS}$, and Section 6 explains how Jin’s
proof of Szemerédi’s Theorem can be developed in it. The multi-level
nonstandard approach to Calculus employed in Hrbacek, Lessmann and O’Donovan
[14] can also be formalized in $\mathbf{SPOTS}$ and thus does not require any
more $\mathbf{AC}$ than the traditional approach; this is shown in Section 7.
Finally, in Section 8 it is proved that $\mathbf{SCOTS}$ is a conservative
extension of $\mathbf{ZF}+\mathbf{ADC}$ and that $\mathbf{SPOTS}$ is
conservative over $\mathbf{ZF}+\mathbf{ACC}$. It is an open problem whether
$\mathbf{SPOTS}$ is a conservative extension of $\mathbf{ZF}$.

##  2\. Theories SPOT and SCOT

By an $\in$-language we mean the language that has a primitive binary
membership predicate $\in$. The classical theories $\mathbf{ZF}$ and ZFC are
formulated in the $\in$-language. It is enriched by defined symbols for
constants, relations, functions and operations customary in traditional
mathematics. For example, it contains names $\mathbb{N}$ and $\mathbb{R}$ for
the sets of natural and real numbers; they are viewed as defined in the
traditional way ($\mathbb{N}$ is the least inductive set, $\mathbb{R}$ is
defined in terms of Dedekind cuts or Cauchy sequences).

Nonstandard set theories, including $\mathbf{SPOT}$ and $\mathbf{SCOT}$, are
formulated in the $\operatorname{\mathbf{st}}$-$\in$-language. They add to the
$\in$-language a unary predicate symbol $\operatorname{\mathbf{st}}$, where
$\operatorname{\mathbf{st}}(x)$ reads “$x$ is standard,” and possibly other
symbols. They postulate that standard infinite sets contain also nonstandard
elements. For example, $\mathbb{R}$ contains infinitesimals and unlimited
reals, and $\mathbb{N}$ contains unlimited natural numbers.

We use $\forall$ and $\exists$ as quantifiers over sets and
$\forall^{\operatorname{\mathbf{st}}}$ and
$\exists^{\operatorname{\mathbf{st}}}$ as quantifiers over standard sets. All
free variables of a formula $\Phi(v_{1},\ldots,v_{k})$ are assumed to be among
$v_{1},\ldots,v_{k}$ _unless_ explicitly specified otherwise. This is usually
done informally by saying that the formula has _parameters_ (ie., additional
free variables), possibly restricted to objects of a certain kind).

The axioms of $\mathbf{SPOT}$ are:

$\mathbf{ZF}$ (Zermelo - Fraenkel Set Theory)

$\mathbf{T}$ (Transfer) Let $\phi(v)$ be an $\in$-formula with standard
parameters. Then

$\forall^{\operatorname{\mathbf{st}}}x\;\phi(x)\to\forall x\;\phi(x).$

$\mathbf{O}$ (Nontriviality)
$\exists\nu\in\mathbb{N}\;\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;(n\neq\nu)$.

$\mathbf{SP}$ (Standard Part)

$\forall
A\subseteq\mathbb{N}\;\exists^{\operatorname{\mathbf{st}}}B\subseteq\mathbb{N}\;\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;(n\in
B\;\leftrightarrow\;n\in A).$

Some of the general results provable in $\mathbf{SPOT}$ are (see [15]):

######  Proposition 2.1.

_Standard natural numbers precede all nonstandard ones:_
$\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\forall
m\in\mathbb{N}\;(m<n\to\operatorname{\mathbf{st}}(m)).$

######  Proposition 2.2.

_(Countable Idealization)_ Let $\phi(u,v)$ be an $\in$-formula with arbitrary
parameters.

$\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\exists x\;\forall
m\in\mathbb{N}\;(m\leq n\;\to\phi(m,x))\;\leftrightarrow\;\exists
x\;\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\phi(n,x).$

The dual form of Countable Idealization is

$\exists^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\forall x\;\exists
m\in\mathbb{N}\;(m\leq n\,\wedge\,\phi(m,x))\;\leftrightarrow\;\forall
x\;\exists^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\phi(n,x).$

Countable Idealization easily implies the following more familiar form. We use
$\forall^{\operatorname{\mathbf{st}}\operatorname{\mathbf{fin}}}$ and
$\exists^{\operatorname{\mathbf{st}}\operatorname{\mathbf{fin}}}$ as
quantifiers over standard finite sets.

_Let $\phi(u,v)$ be an $\in$-formula with arbitrary parameters. For every
standard countable set_ $A$

$\forall^{\operatorname{\mathbf{st}}\operatorname{\mathbf{fin}}}a\subseteq
A\,\exists x\,\forall y\in a\;\phi(x,y)\;\leftrightarrow\;\exists
x\,\forall^{\operatorname{\mathbf{st}}}y\in A\;\phi(x,y).$

The axiom $\mathbf{SP}$ is often used in the equivalent form

($\mathbf{SP}^{\prime}$) $\forall x\in\mathbb{R}\;(x\text{ limited
}\to\exists^{\operatorname{\mathbf{st}}}r\in\mathbb{R}\;(x\simeq r)).$

We recall that $x$ is _limited_ iff $|x|\leq n$ for some standard
$n\in\mathbb{N}$, and $x\simeq r$ iff $|x-r|\leq 1/n$ for all standard
$n\in\mathbb{N}$, $n\neq 0$; $x$ is _infinitesimal_ if $x\simeq
0\,\wedge\,x\neq 0$. The unique standard real number $r$ is called the
_standard part of_ $x$ or the _shadow of_ $x$; notation
$r=\operatorname{\mathbf{sh}}(x)$.

The axiom $\mathbf{SP}$ is also equivalent to Standardization over countable
sets for $\in$-formulas (with arbitrary parameters):

_Let $\phi(v)$ be an $\in$-formula with arbitrary parameters. Then_

($\mathbf{SP}^{\prime\prime}$)
$\exists^{\operatorname{\mathbf{st}}}S\;\forall^{\operatorname{\mathbf{st}}}n\;(n\in
S\;\leftrightarrow\;n\in\mathbb{N}\,\wedge\,\phi(n)).$

###### Proof.

Let $A=\\{n\in\mathbb{N}\,\mid\,\phi(n)\\}$ and apply $\mathbf{SP}$. ∎

The “nonstandard” axioms of $\mathbf{SPOT}$ extend to $\mathbf{ZF}$ the
insights of Leibniz about real numbers (see Bair et al. [1, 2], Katz and
Sherry [26] and Katz, Kuhlemann and Sherry [24]):

  * •

assignable vs. inassignable distinction [standard vs. nonstandard]

  * •

law of continuity [Transfer]

  * •

existence of infinitesimals [Nontriviality]

  * •

equality up to infinitesimal terms that need to be discarded [Standard Part].

This can be taken as a justification of the axioms of $\mathbf{SPOT}$
independent of the proof of its conservativity ove $\mathbf{ZF}$.

The scope of the axiom schema $\mathbf{SP^{\prime\prime}}$ can be extended.

######  Definition 2.3.

An $\operatorname{\mathbf{st}}$-$\in$-formula $\Phi(v_{1},\ldots,v_{r})$ is
_special_ if it is of the form

$\mathsf{Q}^{\operatorname{\mathbf{st}}}u_{1}\ldots\mathsf{Q}^{\operatorname{\mathbf{st}}}u_{s}\,\psi(u_{1},\ldots,u_{s},v_{1},\ldots,v_{r})$

where $\psi$ is an $\in$-formula and each $\mathsf{Q}$ stands for $\exists$ or
$\forall$.

We use $\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}\,u\ldots$ and
$\exists^{\operatorname{\mathbf{st}}}_{\mathbb{N}}\,u\ldots$ as shorthand for,
respectively,
$\forall^{\operatorname{\mathbf{st}}}u\,(u\in\mathbb{N}\to\ldots)$ and
$\exists^{\operatorname{\mathbf{st}}}u\,(u\in\mathbb{N}\,\wedge\,\ldots)$.

An $\mathbb{N}$-_special_ formula is a formula of the form

$\mathsf{Q}^{\operatorname{\mathbf{st}}}_{\mathbb{N}}u_{1}\ldots\mathsf{Q}^{\operatorname{\mathbf{st}}}_{\mathbb{N}}u_{s}\,\psi(u_{1},\ldots
u_{s},v_{1},\ldots,v_{r})$

where $\psi$ is an $\in$-formula.

######  Proposition 2.4.

$(\mathbf{SPOT})$ _(Countable Standardization for $\mathbb{N}$-Special
Formulas)_ Let $\Phi(v)$ be an $\mathbb{N}$-special formula with arbitrary
parameters. Then

$\exists^{\operatorname{\mathbf{st}}}S\;\forall^{\operatorname{\mathbf{st}}}n\;(n\in
S\;\leftrightarrow\;n\in\mathbb{N}\,\wedge\,\Phi(n)).$

Of course, $\mathbb{N}$ can be replaced by any standard countable set.

###### Proof.

We give the argument for a typical case

$\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}u_{1}\,\exists^{\operatorname{\mathbf{st}}}_{\mathbb{N}}u_{2}\,\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}u_{3}\;\psi(u_{1},u_{2},u_{3},v).$

By $\mathbf{SP}^{\prime\prime}$ there is a standard set $R$ such that for all
standard $n_{1},n_{2},n_{3},n$

$\langle n_{1},n_{2},n_{3},n\rangle\in R\;\leftrightarrow\;\langle
n_{1},n_{2},n_{3},n\rangle\in\mathbb{N}^{4}\,\wedge\,\psi(n_{1},n_{2},n_{3},n).$

We let $R_{n_{1},n_{2},n_{3}}=\\{n\in\mathbb{N}\,\mid\,\langle
n_{1},n_{2},n_{3},n\rangle\in R\\}$ and

$S=\bigcap_{n_{1}\in\mathbb{N}}\,\bigcup_{n_{2}\in\mathbb{N}}\,\bigcap_{n_{3}\in\mathbb{N}}\,R_{n_{1},n_{2},n_{3}}.$

Then $S$ is standard and for all standard $n$:

$\displaystyle n\in S$ $\displaystyle\;\leftrightarrow\;\forall
n_{1}\in\mathbb{N}\,\exists n_{2}\in\mathbb{N}\,\forall
n_{3}\in\mathbb{N}\;(n\in R_{n_{1},n_{2},n_{3}})$
$\displaystyle\;\leftrightarrow\;\text{(by Transfer)
}\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{1}\,\exists^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{2}\;\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{3}\;(n\in
R_{n_{1},n_{2},n_{3}})$ $\displaystyle\;\leftrightarrow\;\text{ (by definition
of $R$)
}\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{1}\,\exists^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{2}\;\forall^{\operatorname{\mathbf{st}}}_{\mathbb{N}}n_{3}\;\psi(n_{1},n_{2},n_{3},n)$
$\displaystyle\;\leftrightarrow\;\Phi(n).$

∎

Infinitesimal calculus can be developed in $\mathbf{SPOT}$ as far as the
global version of Peano’s Theorem; see Hrbacek-Katz [16, 17].

_Let $F:[0,\infty)\times\mathbb{R}\to\mathbb{R}$ be a continuous function.
There is an interval $[0,a)$ with $0<a\leq\infty$ and a function
$y:[0,a)\to\mathbb{R}$ such that_

$\qquad y(0)=0,\quad\quad y^{\prime}(x)=F(x,y(x))\quad$

_holds for all $x\in[0,a)$, and if $a\in\mathbb{R}$ then $\lim_{x\to
a^{-}}y(x)=\pm\infty$._

We note that the traditional proofs of the global version of Peano Theorem use
Zorn’s Lemma or the Axiom of Dependent Choice.

It is useful to extend $\mathbf{SPOT}$ by two additional special cases of
Standardization.

$\mathbf{SN}$ (Standardization for $\operatorname{\mathbf{st}}$-$\in$-formulas
with no parameters, or, equivalently, with only standard parameters):

_Let $\Phi(v)$ be an $\operatorname{\mathbf{st}}$-$\in$-formula with standard
parameters. Then_

$\forall^{\operatorname{\mathbf{st}}}A\,\exists^{\operatorname{\mathbf{st}}}S\;\forall^{\operatorname{\mathbf{st}}}x\;(x\in
S\;\leftrightarrow\;x\in A\,\wedge\,\Phi(x)).$

SF (Standardization over standard finite sets) _Let $\Phi(v)$ be an
$\operatorname{\mathbf{st}}$-$\in$-formula with arbitrary parameters. Then_

$\forall^{\operatorname{\mathbf{st}}\operatorname{\mathbf{fin}}}A\;\exists^{\operatorname{\mathbf{st}}}S\;\forall^{\operatorname{\mathbf{st}}}x\;(x\in
S\;\leftrightarrow\;x\in A\;\wedge\;\Phi(x)).$

An important consequence of SF is the ability to carry out external induction.

######  Proposition 2.5.

_(External Induction)_ Let $\Phi(v)$ be an
$\operatorname{\mathbf{st}}$-$\in$-formula with arbitrary parameters. Then
$\mathbf{SPOT}+\mathbf{SF}$ proves the following:

$[\,\Phi(0)\,\wedge\,\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\,(\Phi(n)\to\Phi(n+1))\to\forall^{\operatorname{\mathbf{st}}}m\,\Phi(m)\,].$

###### Proof.

Let $m\in\mathbb{N}$ be standard. If $m=0$, then $\Phi(m)$ holds. Otherwise SF
yields a standard set $S\subseteq m$ such that
$\forall^{\operatorname{\mathbf{st}}}n<m\,(n\in S\;\leftrightarrow\;\Phi(n));$
clearly $0\in S$. As $S$ is finite, it has a greatest element $k$, which is
standard by Transfer. If $k<m$, then $k+1\in S$, a contradiction. Hence $k=m$
and $\Phi(m)$ holds. ∎

$\mathbf{SPOT}^{+}$ is $\mathbf{SPOT}$ \+ SN \+ SF.

_The theory_ $\mathbf{SPOT}^{+}$ _is a conservative extension of_
$\mathbf{ZF}$.

This is proved for $\mathbf{SPOT}+\textbf{SN}$ in [15], Theorem B
(Propositions 4.15 and 6.7 there). The argument that SF can be also added
conservatively over $\mathbf{ZF}$ is given at the end of Section 8
(Proposition 8.7).

The theory $\mathbf{SCOT}$ is $\mathbf{SPOT}^{+}+\mathbf{DC}$, where

$\mathbf{DC}$ (Dependent Choice for
$\operatorname{\mathbf{st}}$-$\in$-formulas):
_Let $\Phi(u,v)$ be an $\operatorname{\mathbf{st}}$-$\in$-formula with
arbitrary parameters.
If $B$ is a set, $b\in B$ and $\forall x\in B\,\exists y\in B\;\Phi(x,y)$,
then there is a sequence $\langle b_{n}\,\mid\,n\in\mathbb{N}\rangle$ such
that $b_{0}=b$ and _
$\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\,(b_{n}\in
B\,\wedge\,\Phi(b_{n},b_{n+1}))$.

Some general consequences of $\mathbf{SCOT}$ are (see [15]):

$\mathbf{CC}\;$ (Countable $\operatorname{\mathbf{st}}$-$\in$-Choice)

_Let $\Phi(u,v)$ be an $\operatorname{\mathbf{st}}$-$\in$-formula with
arbitrary parameters. Then_
$\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;\exists
x\;\Phi(n,x)\to\exists f\,(f\text{ is a
function}\,\wedge\,\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\,\Phi(n,f(n)).$

$\mathbf{SC}$ (Countable Standardization)
_Let $\Psi(v)$ be an $\operatorname{\mathbf{st}}$-$\in$-formula with arbitrary
parameters. Then_

$\exists^{\operatorname{\mathbf{st}}}S\;\forall^{\operatorname{\mathbf{st}}}x\;(x\in
S\;\leftrightarrow\;x\in\mathbb{N}\,\wedge\,\Psi(x)).$

$\mathbf{SCOT}$ is a conservative extension of $\mathbf{ZF}+\mathbf{ADC}$
([15],Theorem 5.10).444 It is an open question whether
$\mathbf{SPOT}^{+}+\mathbf{SC}$ is a conservative extension of $\mathbf{ZF}$.
It allows such features as an infinitesimal construction of the Lebesgue
measure. It implies the axioms of Nelson’s _Radically Elementary Probability
Theory_ [28].

##  3\. Ultrafilters, ultrapowers, and their iterations

In this section we review the construction of iterated ultrapowers in a form
suitable for motivation and establishing the conservativity of the theories
formulated in Section 4. We assume ZFC, use classes freely, and give no
proofs. Some references for this material are Chang-Keisler [4], Enayat et al.
[9] and Hrbacek [11, 12].

Model theory deals with structures that are sets. For our purposes we need to
construct ultrapowers of the entire set-theoretic universe $\mathbb{V}$. That
means we have to deal with structures that are proper classes (eg.
$(\mathbb{V},\in)$). We sometimes use the model-theoretic language and say
that such structure _satisfies a formula_ , or that a mapping is an
_elementary embedding_ of one class structure into another. It is well-known
that the satisfaction relation $\vDash$ for such structures cannot be proved
to exist in ZFC. But the concept makes sense for any one particular formula.
Thus, if $\mathfrak{U}=(\mathbb{U};\mathbb{V}_{1},\mathbb{V}_{2},\ldots)$ is a
(class) structure and $\Phi(v_{1},\ldots,v_{r})$ is a formula in the language
of $\mathfrak{U}$, we write $\Phi^{\mathbb{U}}(v_{1},\ldots,v_{r})$ for the
formula obtained from $\Phi$ by restricting all quantifiers to $\mathbb{U}$,
ie., by replacing each occurrence of $\forall v$ by $\forall v\in\mathbb{U}$
and each occurrence of $\exists v$ by $\exists v\in\mathbb{U}$. [We usually
abuse notation by not distinguishing between classes and their names in the
language of $\mathfrak{U}$.] The statement that $\mathbf{J}$ is an elementary
embedding of $\mathfrak{U}^{1}$ to $\mathfrak{U}^{2}$, for example, means
that, given any formula $\Phi$ of the appropriate language,

$\forall
x_{1},\ldots,x_{r}\in\mathbb{U}^{1}\,(\Phi^{\mathbb{U}^{1}}(x_{1},\ldots,x_{r})\;\leftrightarrow\;\Phi^{\mathbb{U}^{2}}(\mathbf{J}(x_{1}),\ldots,\mathbf{J}(x_{r}))).$

Let $U$ be an ultrafilter over $I$. For $f,g\in\mathbb{V}^{I}$ we define

$f=_{U}g\text{ iff }\\{i\in I\,\mid\,f(i)=g(i)\\}\in U,$ $f\in_{U}g\text{ iff
}\\{i\in I\,\mid\,f(i)\in g(i)\\}\in U.$

The usual procedure at this point is to form equivalence classes $[f]_{U}$ of
functions $f\in\mathbb{V}^{I}$ modulo $=_{U}$, using “Scott’s trick” of taking
only the functions of the minimal von Neumann rank to guarantee that the
equivalence classes are sets:

$[f]_{U}=\\{g\in\mathbb{V}^{I}\,\mid\,g=_{U}f\text{ and }\forall
h\in\mathbb{V}^{I}\,(h=_{U}f\to\operatorname{rank}h\geq\operatorname{rank}g)\\};$

see Jech [19], (9.3) and (28.15). Then
$\mathbb{V}^{I}/U=\\{[f]_{U}\,\mid\,f\in\mathbb{V}^{I}\\}$, and
$[f]_{U}\in_{U}[g]_{U}$ iff $f\in_{U}g$.

The _ultrapower_ of $\mathbb{V}$ by $U$ is the structure
$(\mathbb{V}^{I}/U,\in_{U})$.

Let $\pi:I\to J$. Define the ultrafilter $V=\pi[U]$ over $J$ by

$\pi[U]=\\{Y\subseteq J\,\mid\,\pi^{-1}[Y]\in U\\}.$

The mapping $\pi$ induces $\Pi:\mathbb{V}^{J}/V\to\mathbb{V}^{I}/U$ by
$\Pi([g]_{V})=[g\circ\pi]_{U}$.

The following proposition is an easy consequence of Łoś’s Theorem.

######  Proposition 3.1.

The mapping $\Pi$ is well-defined and it is an elementary embedding of
$(\mathbb{V}^{J}\\!/V,\in_{V})$ into $(\mathbb{V}^{I}\\!/U,\in_{U})$.
In detail: For any $\in$-formula $\phi$ and all
$[f_{1}]_{V},\ldots[f_{r}]_{V}\in\mathbb{V}^{J}/V$,

$\phi^{\mathbb{V}^{J}/V}([f_{1}]_{V},\ldots,[f_{r}]_{V})\;\leftrightarrow\;\phi^{\mathbb{V}^{I}/U}(\Pi([f_{1}]_{V}),\ldots,\Pi([f_{r}])_{V}).$

The _tensor product_ of ultrafilters $U$ and $V$, respectively over $I$ and
$J$, is the ultrafilter over $I\times J$ defined by (note the order; [4] uses
the opposite order):

$Z\in U\otimes V\text{ iff }\\{x\in I\,\mid\,\\{y\in J\,\mid\,\langle
x,y\rangle\in Z\\}\in V\\}\in U.$

The $n$-_th tensor power_ of $U$ is the ultrafilter over $I^{n}$ defined by
recursion:

$\otimes^{0}U=\\{\\{\emptyset\\}\\}$; $\otimes^{1}U=U$;
$\otimes^{n+1}U=U\otimes(\otimes^{n}U)$.

In the following, $\mathsf{a}$, $\mathsf{b}$ range over finite subsets of
$\mathbb{N}$.

If $|\mathsf{a}|=n$, let $\pi$ be the mapping of $I^{n}$ onto $I^{\mathsf{a}}$
induced by the order-preserving mapping of $n$ onto $\mathsf{a}$. It follows
that $U_{\mathsf{a}}=\pi[\otimes^{n}U]$ is an ultrafilter over
$I^{\mathsf{a}}$.

For $\mathsf{a}\subseteq\mathsf{b}$ let $\pi^{\mathsf{b}}_{\mathsf{a}}$ be the
restriction map of $I^{\mathsf{b}}$ onto $I^{\mathsf{a}}$ defined by
$\pi^{\mathsf{b}}_{\mathsf{a}}(\mathbf{i})=\mathbf{i}\upharpoonright\mathsf{a}$
for $\mathbf{i}\in I^{\mathsf{b}}$.

It is easy to see that
$U_{\mathsf{a}}=\pi^{\mathsf{b}}_{\mathsf{a}}[U_{\mathsf{b}}]$. We let
$\mathbb{V}_{\mathsf{a}}=\mathbb{V}^{I^{\mathsf{a}}}/U_{\mathsf{a}}$ and write
$[f]_{\mathsf{a}}$ for $[f]_{U_{\mathsf{a}}}$ and $\in_{\mathsf{a}}$ for
$\in_{U_{\mathsf{a}}}$. The mapping $\Pi^{\mathsf{b}}_{\mathsf{a}}$ induced by
$\pi^{\mathsf{b}}_{\mathsf{a}}$ is an elementary embedding of
$(\mathbb{V}_{\mathsf{a}},\in_{\mathsf{a}})$ into
$(\mathbb{V}_{\mathsf{b}},\in_{\mathsf{b}})$.

######  Proposition 3.2.

If $f\in\mathbb{V}^{I^{\mathsf{a}}}$, $g\in\mathbb{V}^{I^{\mathsf{b}}}$ and
$\Pi^{\mathsf{a}\cup\mathsf{b}}_{\mathsf{a}}([f]_{\mathsf{a}})=\Pi^{\mathsf{a}\cup\mathsf{b}}_{\mathsf{b}}([g]_{\mathsf{b}})$,
then there is $h\in\mathbb{V}^{I^{\mathsf{a}\cap\mathsf{b}}}$ such that
$\Pi^{\mathsf{a}\cup\mathsf{b}}_{\mathsf{a}\cap\mathsf{b}}([h]_{\mathsf{a}\cap\mathsf{b}})=\Pi^{\mathsf{a}\cup\mathsf{b}}_{\mathsf{a}}([f]_{\mathsf{a}})=\Pi^{\mathsf{a}\cup\mathsf{b}}_{\mathsf{b}}([g]_{\mathsf{b}})$.

Let $f,g\in\bigcup_{\mathsf{a}}\mathbb{V}^{I^{\mathsf{a}}}$; say
$f\in\mathbb{V}^{I^{\mathsf{a}}}$ and $g\in\mathbb{V}^{I^{\mathsf{b}}}$; we
define

$f=_{\infty}g\text{ iff
}f\circ\,\pi_{\mathsf{a}}^{\mathsf{a}\cup\mathsf{b}}=_{U_{\mathsf{a}\cup\mathsf{b}}}g\circ\,\pi_{\mathsf{b}}^{\mathsf{a}\cup\mathsf{b}},$
$f\in_{\infty}g\text{ iff
}f\circ\,\pi_{\mathsf{a}}^{\mathsf{a}\cup\mathsf{b}}\in_{U_{\mathsf{a}\cup\mathsf{b}}}g\circ\,\pi_{\mathsf{b}}^{\mathsf{a}\cup\mathsf{b}}.$

We let $[f]_{\infty}$ be the equivalence class of $f$ modulo $=_{\infty}$
(again using Scott’s Trick) and let
$\mathbb{V}_{\infty}=\\{[f]_{\infty}\,\mid\,f\in\bigcup_{\mathsf{a}}\mathbb{V}^{I^{\mathsf{a}}}\\}$
and $[f]_{\infty}\in_{\infty}[g]_{\infty}$ iff $f\in_{\infty}g$.

The _iterated ultrapower of $\mathbb{V}$ by_ $U$ is the structure
$(\mathbb{V}_{\infty},\in_{\infty})$. It is the direct limit of the system of
structures
$(\mathbb{V}_{\mathsf{a}},\;\Pi^{\mathsf{b}}_{\mathsf{a}};\;\mathsf{a},\mathsf{b}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\mathbb{N}),\,\mathsf{a}\subseteq\mathsf{b})$.
The mappings
$\Pi_{\mathsf{a}}^{\infty}:\mathbb{V}_{\mathsf{a}}\to\mathbb{V}_{\infty}$
defined by $\Pi_{\mathsf{a}}^{\infty}([f]_{\mathsf{a}})=[f]_{\infty}$ are
elementary embeddings; we identify $\mathbb{V}_{\mathsf{a}}$ with its image by
this embedding. In particular, $\Pi_{\emptyset}^{\infty}$ embeds
$\mathbb{V}\cong\mathbb{V}_{\emptyset}$ elementarily into
$\mathbb{V}_{\infty}$.

In addition to the canonical elementary embeddings
$\Pi_{\mathsf{a}}^{\mathsf{b}}$ for $\mathsf{a}\subseteq\mathsf{b}$, the
iterated ultrapower allows other elementary embeddings, due to the fact that
the same ultrafilter $U$ is used throughout the construction. If
$|\mathsf{a}|=|\mathsf{b}|$ and $\alpha$ is the order-preserving mapping of
$\mathsf{a}$ onto $\mathsf{b}$, define
$\pi_{\mathsf{a}}^{\mathsf{b}}:I^{\mathsf{b}}\to I^{\mathsf{a}}$ by
$\pi_{\mathsf{a}}^{\mathsf{b}}(\mathbf{i})=\mathbf{i}\circ\alpha$ for
$\mathbf{i}\in I^{\mathsf{b}}$. Then $\Pi^{\mathsf{b}}_{\mathsf{a}}$ is an
isomorphism of $(\mathbb{V}_{\mathsf{a}},\in_{\mathsf{a}})$ and
$(\mathbb{V}_{\mathsf{b}},\in_{\mathsf{b}})$.

We fix $r\in\mathbb{N}$. For $f\in\mathbb{V}^{I^{r+n}}$ define
$f|I^{r}:I^{r}\to\mathbb{V}^{I^{n}}$ by $f|I^{r}(\mathbf{i})=f_{\mathbf{i}}$
where $f_{\mathbf{i}}(\mathbf{j})=f(\mathbf{i},\mathbf{j})$ for all
$\mathbf{j}\in I^{n}$. For $[f]_{\infty}\in\mathbb{V}_{\infty}$, say
$f\in\mathbb{V}^{I^{r+n}}$, we let $\Omega([f]_{\infty})=[F]_{U_{r}}$ where
$F(\mathbf{i})=[f_{\mathbf{i}}]_{\infty}$ for all $\mathbf{i}\in I^{r}$. It is
routine to check that
$\Omega:\mathbb{V}_{\infty}\to(\mathbb{V}_{\infty})^{I^{r}}/U_{r}$ is well-
defined.

We use the notations $r\oplus\mathsf{a}=\\{r+s\,\mid\,s\in\mathsf{a}\\}$ and
$r\boxplus\mathsf{a}=r\,\cup\,(r\oplus\mathsf{a}$). Note that if
$\mathsf{a}=n=\\{0,\ldots,n-1\\}\in\mathbb{N}$, then $r\boxplus n=r+n$

######  Proposition 3.3.

(Factoring Lemma) The mapping $\Omega$ is an isomorphism of the structures

$(\mathbb{V}_{\infty},\,\in_{\infty},\,\mathbb{V}_{r\boxplus\mathsf{a}},\,\Pi_{r\boxplus\mathsf{a}}^{r\boxplus\mathsf{b}};\;\mathsf{a},\mathsf{b}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\mathbb{N}),|\mathsf{a}|=|\mathsf{b}|)$

and

$(\mathbb{V}_{\infty},\in_{\infty},\mathbb{V}_{\mathsf{a}},\,\Pi_{\mathsf{a}}^{\mathsf{b}};\,\mathsf{a},\mathsf{b}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\mathbb{N}),|\mathsf{a}|=|\mathsf{b}|)^{I^{r}}/U_{r}.$

##  4\. SPOTS

Theories with many levels of standardness have been developed in Péraire, [29]
(RIST) and Hrbacek [11, 12] (GRIST). The characteristic feature of these
theories is that the unary standardness predicate
$\operatorname{\mathbf{st}}(v)$ is subsumed under a binary _relative
standardness_ predicate $\operatorname{\mathbf{sr}}(u,v)$.

The main advantage of theories with many levels of standardness is that
nonstandard methods can be applied to arbitrary objects, not just the standard
ones. For example, the nonstandard definition of the derivative

$f^{\prime}(a)=\operatorname{\mathbf{sh}}\left(\frac{f(a+h)-f(a)}{h}\right)\;\text{
where }h\text{ is infinitesimal},$

which in a single-level nonstandard analysis works for standard $f$ and $a$
only, in these theories works for all $f$ and $a$, provided “infinitesimal” is
understood as “infinitesimal relative to the level of $f$ and $a$” and
“$\operatorname{\mathbf{sh}}$” is “$\operatorname{\mathbf{sh}}$ relative to
the level of $f$ and $a$.” In the book Hrbacek, Lessmann and O’Donovan [14]
this approach is used to develop elementary calculus.

Jin’s work using multi-level nonstandard analysis goes beyond the features
postulated by these theories in that it also employs nontrivial elementary
embeddings (ie, other than those provided by inclusion of one level in a
higher level).

The language of SPOTS has a binary predicate symbol $\in$, a binary predicate
symbol $\operatorname{\mathbf{sr}}$ ($\operatorname{\mathbf{sr}}(u,v)$ reads
“$v$ is $u$-_standard_ ”) and a ternary function symbol
$\operatorname{\mathbf{ir}}$ that captures the relevant isomorphisms. The
unary predicate $\operatorname{\mathbf{st}}(v)$ stands for
$\operatorname{\mathbf{sr}}(\emptyset,v)$, Variables $\mathsf{a}$,
$\mathsf{b}$ (with decorations) range over _standard finite_ subsets of
$\mathbb{N}$; we refer to them as _labels_. We use the class notation
$\mathbb{S}_{\mathsf{a}}=\\{x\,\mid\,\operatorname{\mathbf{sr}}(\mathsf{a},x)\\}$
and $\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}=\\{\langle
x,y\rangle\,\mid\,\operatorname{\mathbf{ir}}(\mathsf{a},\mathsf{b},x)=y\\}$.
If $\mathsf{a}$ is a standard natural number, we use $\mathsf{n}$ instead of
$\mathsf{a}$; analogously for $\mathsf{b}$ and $\mathsf{m}$. We call
$\mathbb{S}_{\mathsf{n}}$ the $\mathsf{n}$-_th level of standardness_. In
particular, $\mathbb{S}_{0}=\\{x\,\mid\,\operatorname{\mathbf{st}}(x)\\}$ is
the universe of standard sets.

As in Section 3, for standard $r\in\mathbb{N}$ we let
$r\oplus\mathsf{a}=\\{r+s\,\mid\,s\in\mathsf{a}\\}$ and
$r\boxplus\mathsf{a}=r\,\cup\,(r\oplus\mathsf{a})$. Also
$\mathsf{a}<\mathsf{b}$ stands for $\forall s\in\mathsf{a}\;\forall
t\in\mathsf{b}\;(s<t)$.

A formula $\Phi$ is _admissible_ if labels appear in it only as subscripts and
superscripts of $\mathbb{S}$ and $\mathbf{I}$:

######  Definition 4.1.

(_Admissible formulas._)

  * •

$u=v$, $u\in v$, $v\in\mathbb{S}_{\mathsf{a}}$ and
$\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}(u)=v$ are admissible formulas.

  * •

If $\Phi$ and $\Psi$ are admissible, then $\neg\Phi$, $\Phi\wedge\Psi$,
$\Phi\vee\Psi$, $\Phi\to\Psi$ and $\Phi\;\leftrightarrow\;\,\Psi$ are
admissible.

  * •

If $\Phi$ is admissible, then $\forall v\,\Phi$ and $\exists v\,\Phi$ are
admissible.

Let $\Phi^{\uparrow r}$ be the formula obtained from the admissible formula
$\Phi$ by replacing each occurrence of every $\mathbb{S}_{\mathsf{a}}$ with
$\mathbb{S}_{r\boxplus\mathsf{a}}$ and each occurrence of
$\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}$ with
$\mathbf{I}_{r\boxplus\mathsf{a}}^{\,r\boxplus\mathsf{b}}$. In particular, if
$\Phi$ is a formula where only the symbols $\mathbb{S}_{\mathsf{n}}$ and
$\mathbf{I}_{\mathsf{n}}^{\mathsf{m}}$ for
$\mathsf{n},\mathsf{m}\in\mathbb{N}\cap\mathbb{S}_{0}$ occur, then
$\Phi^{\uparrow r}$ is obtained from $\Phi$ by shifting all levels by $r$.
This is the special case that is most often used in practice.

The iterated ultrapower construction described in Section 3 suggests the
axioms IS, GT and HO.

IS (Structural axioms)

  1. (1)

$\operatorname{\mathbf{sr}}(u,v)\to\exists\mathsf{a}\;(u=\mathsf{a})$,
$\operatorname{\mathbf{ir}}(u,v,x)=y\to\exists\mathsf{a},\mathsf{b}\;(u=\mathsf{a}\wedge
v=\mathsf{b})$,
$\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}(u)=v\to|\mathsf{a}|=|\mathsf{b}|$.

  2. (2)

$\forall x\,\exists\mathsf{a}\;(x\in\mathbb{S}_{\mathsf{a}})$.

  3. (3)

For all $\mathsf{a},\mathsf{b}$,
$\mathbb{S}_{\mathsf{a}\,\cap\,\mathsf{b}}=\mathbb{S}_{\mathsf{a}}\,\cap\,\mathbb{S}_{\mathsf{b}}$
(in particular,
$\mathsf{a}\subseteq\mathsf{b}\to\mathbb{S}_{\mathsf{a}}\subseteq\mathbb{S}_{\mathsf{b}}$).

  4. (4)

If $|\mathsf{a}|=|\mathsf{a}^{\prime}|=|\mathsf{a}^{\prime\prime}|$, then

$\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}}:\mathbb{S}_{\mathsf{a}}\to\mathbb{S}_{\mathsf{a}^{\prime}},\quad\mathbf{I}_{\mathsf{a}}^{\mathsf{a}}=\text{Id}_{\mathbb{S}_{\mathsf{a}}},\quad\mathbf{I}_{\mathsf{a}^{\prime}}^{\mathsf{a}}=(\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}})^{-1},\quad\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}}\circ\mathbf{I}_{\mathsf{a}^{\prime}}^{\mathsf{a}^{\prime\prime}}=\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime\prime}};$
$\forall x,z\in\mathbb{S}_{\mathsf{a}}\;(x\in
z\;\leftrightarrow\;\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}}(x)\in\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}}(z)).$

  5. (5)

If $|\mathsf{a}|=|\mathsf{a}^{\prime}|$ and $\mathsf{b}\subset\mathsf{a}$,
then

$x\in\mathbb{S}_{\mathsf{b}}\to\mathbf{I}_{\mathsf{a}}^{\mathsf{a}^{\prime}}(x)=\mathbf{I}_{\mathsf{b}}^{\mathsf{b}^{\prime}}(x),$

where $\mathsf{b}^{\prime}$ is the image of $\mathsf{b}$ by the order-
preserving map of $\mathsf{a}$ onto $\mathsf{a}^{\prime}$.

GT (Generalized Transfer)

Let $\phi(v,v_{1},\ldots,v_{k})$ be an $\in$-formula. Then for all
$\mathsf{a}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\mathbb{N})\cap\mathbb{S}_{0}$

$\forall x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{a}}\;\left(\forall
x\in\mathbb{S}_{\mathsf{a}}\;\phi(x,x_{1},\ldots,x_{k})\to\forall
x\;\phi(x,x_{1},\ldots,x_{k})\right).$

HO (Homogeneous Shift)

Let $\Phi(v_{1},\ldots,v_{k})$ be an admissible formula. For all standard $r$
and all
$\mathsf{a}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\mathbb{N})\cap\mathbb{S}_{0}$,

$\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{a}}\;[\,\Phi(x_{1},\ldots,x_{k})\;\leftrightarrow\;\Phi^{\uparrow
r}(\mathbf{I}_{\mathsf{a}}^{r\oplus\mathsf{a}}(x_{1}),\ldots,\mathbf{I}_{\mathsf{a}}^{r\oplus\mathsf{a}}(x_{k}))\,].$

The language of $\mathbf{SPOTS}$ has an obvious interpretation in the iterated
ultrapower described in Section 3: $\mathbb{S}_{\mathsf{a}}$ is interpreted as
$\mathbb{V}^{I^{\mathsf{a}}}/U_{\mathsf{a}}$ and
$\mathbf{I}^{\mathsf{b}}_{\mathsf{a}}$ is interpreted as
$\Pi^{\mathsf{b}}_{\mathsf{a}}$.

######  Proposition 4.2.

Under the above interpretation, the axioms $\mathbf{IS}$, $\mathbf{GT}$ and
$\mathbf{HO}$ hold in the iterated ultrapower constructed in Section 3.

###### Proof.

The axiom (3) in $\mathbf{IS}$ follows from Proposition 3.2; the rest is
obvious.

Proposition 3.1 implies that, given $\mathsf{a}\subseteq\mathsf{b}$,

$\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{a}}\;\left(\phi^{\mathbb{S}_{\mathsf{a}}}(x_{1},\ldots,x_{k})\;\leftrightarrow\;\phi^{\mathbb{S}_{\mathsf{b}}}(x_{1},\ldots,x_{k})\right).$

By the Elementary Chain Theorem (Chang-Keisler [4], Theorem 3.1.13)

$\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{a}}\;\left(\phi^{\mathbb{S}_{\mathsf{a}}}(x_{1},\ldots,x_{k})\;\leftrightarrow\;\phi(x_{1},\ldots,x_{k})\right).$

The axiom $\mathbf{GT}$ is a special case.

HO is justified by the Factoring Lemma and Łoś’s Theorem (specifically, by the
fact that the canonical embedding of
$(\mathbb{V}_{\infty},\in_{\infty},\mathbb{V}_{\mathsf{a}},\,\Pi_{\mathsf{a}}^{\mathsf{b}})$
into its ultrapower by $U_{r}$ is elementary). ∎

$\mathbf{SPOTS}$ is the theory
$\mathbf{SPOT}^{+}+\textbf{IS}+\textbf{GT}+\textbf{HO}$, where Nontriviality
is modified to
$\exists\nu\in\mathbb{N}\cap\mathbb{S}_{1}\;(\forall^{\operatorname{\mathbf{st}}}n\in\mathbb{N}\;(n\neq\nu)$
and SN and SF admit all formulas in the language of $\mathbf{SPOTS}$.

A consequence of GT is the following proposition.

######  Proposition 4.3.

The mapping $\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}$ is an elementary embedding
of $\mathbb{S}_{\mathsf{a}}$ into $\mathbb{I}$ (where $\mathbb{I}$ is the
class of all sets) and into $\mathbb{S}_{\mathsf{b}^{\prime}}$ for every
$\mathsf{b}^{\prime}\supseteq\mathsf{b}$.

An important consequence of $\mathbf{SPOTS}$ asserts that every natural number
$k\in\mathbb{S}_{\mathsf{a}}$ is either standard or greater than all natural
numbers at levels less than $\min\mathsf{a}$.

######  Proposition 4.4.

_(End Extension)_ Let $\mathsf{a}\neq\emptyset$ and
$n=\min\mathsf{a}\in\mathbb{N}$. Then $\forall
k\in\mathbb{S}_{\mathsf{a}}\cap\mathbb{N}\;(k\in\mathbb{S}_{0}\,\vee\,\forall
m\in\mathbb{S}_{n}\;(m<k)).$

###### Proof.

By Proposition 2.1, $\forall m\in\mathbb{N}\cap\mathbb{S}_{0}\;\forall
k\in\mathbb{N}\;(k\leq m\to k\in\mathbb{S}_{0}).$ By HO this implies $\forall
m\in\mathbb{N}\cap\mathbb{S}_{n}\;\forall k\in\mathbb{N}\;(k\leq m\to
k\in\mathbb{S}_{n}).$ If $k\in\mathbb{S}_{\mathsf{a}}\cap\mathbb{N}$ and
$\exists m\in\mathbb{S}_{\mathsf{n}}\;(m\geq k)$ then $k\in\mathbb{S}_{n}$ by
the above. As $\mathsf{a}\cap n=\emptyset$, we get $k\in\mathbb{S}_{0}$. ∎

Let $\Phi(x_{1},\ldots,x_{k};\mathbb{S})$ denote a formula obtained from some
$\operatorname{\mathbf{st}}$-$\in$-formula by replacing all occurences of
$\operatorname{\mathbf{st}}(v)$ with $v\in\mathbb{S}$, and let $\mathsf{n}$,
$\mathsf{m}$ be variables that do not occur in $\Phi$ and range over standard
natural numbers.

######  Proposition 4.5.

$\mathsf{n}\leq\mathsf{m}\to\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{n}}\;(\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{\mathsf{n}})\;\leftrightarrow\;\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{\mathsf{m}})).$

###### Proof.

Let $r=\mathsf{m}-\mathsf{n}$. By $\mathbf{HO}$ we have

$\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{0}\,(\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{0})\;\leftrightarrow\;\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{r})).$

(Note that $r\oplus 0=0$, $r\boxplus 0=r$ and
$\mathbf{I}_{0}^{0}=\text{Id}_{\mathbb{S}_{0}}$.) Then apply $\mathbf{HO}$
shift by $\mathsf{n}$ to this closed formula to obtain

$\forall
x_{1},\ldots,x_{k}\in\mathbb{S}_{\mathsf{n}}\,(\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{n})\;\leftrightarrow\;\Phi(x_{1},\ldots,x_{k};\mathbb{S}_{\mathsf{m}})).$

∎

In particular, $\Phi(\mathbb{S}_{0})$ implies $\Phi(\mathbb{S}_{\mathsf{n}})$
for every $\mathsf{n}$. Hence the axioms of $\mathbf{SPOT}$, postulated in
$\mathbf{SPOTS}$ only about the level $\mathbb{S}_{0}$, hold there about every
level $\mathbb{S}_{\mathsf{n}}$.

$\mathbf{SCOTS}$ is the theory
$\mathbf{SCOT}+\textbf{IS}+\textbf{GT}+\textbf{HO}$ =
$\mathbf{SPOTS}+\textbf{DC}$, where DC is formulated as follows:

_Let $\Phi(u,v)$ be a formula in the language of $\mathbf{SPOTS}$, with
arbitrary parameters. For any $\mathsf{a}$:
If $B\in\mathbb{S}_{\mathsf{a}}$ is a set, $b\in B\cap\mathbb{S}_{\mathsf{a}}$
and $\forall x\in B\cap\mathbb{S}_{\mathsf{a}},\exists y\in
B\cap\mathbb{S}_{\mathsf{a}}\;\Phi(x,y)$, then there is a sequence
$\bar{b}=\langle b_{n}\,\mid\,n\in\mathbb{N}\rangle\in\mathbb{S}_{\mathsf{a}}$
such that $b_{0}=b$ and _ $\forall n\in\mathbb{N}\cap\mathbb{S}_{0}\,(b_{n}\in
B\,\wedge\,\Phi(b_{n},b_{n+1}))$.

$\mathbf{DC}$ implies Countable Standardization (and hence SF):
$\mathbf{SC}$  _Let $\Psi(v)$ be a formula in the language of
$\mathbf{SPOTS}$, with arbitrary parameters. Then_

$\exists S\in\mathbb{S}_{0}\;\forall x\in\mathbb{S}_{0}\;(x\in
S\;\leftrightarrow\;x\in\mathbb{N}\,\wedge\,\Psi(x)).$

######  Theorem 4.6.

$\mathbf{SCOTS}$ is a conservative extension of $\mathbf{ZF}+\mathbf{ADC}$.

######  Theorem 4.7.

$\mathbf{SPOTS}$ is conservative over $\mathbf{ZF}+\mathbf{ACC}$.

The proofs are given in Section 8.

######  Conjecture.

$\mathbf{SPOTS}$ is a conservative extension of $\mathbf{ZF}$.

##  5\. Jin’s proof of Ramsey’s Theorem in SPOTS

Ramsey’s Theorem. _Given a coloring $c:[\mathbb{N}]^{n}\to r$ where
$n,r\in\mathbb{N}$, there exists an infinite set $H\subseteq\mathbb{N}$ such
that $c\upharpoonright[H]^{n}$ is a constant function. _

We formalize in SPOTS the proof presented by Renling Jin [21] in his invited
talk at the conference _Logical methods in Ramsey Theory and related topics_ ,
Pisa, July 9 – 11, 2023. It is included here with his kind permission.

###### Proof.

It suffices to prove the theorem under the assumption that $n,r,c$ are
standard; the general result then follows by Transfer.

Let $\mathbf{I}=\mathbf{I}_{\\{0,1,\ldots,n-1\\}}^{\\{1,2,\ldots,n\\}}$. Fix
$\nu\in\mathbb{N}\cap(\mathbb{S}_{1}\setminus\mathbb{S}_{0})$ and. define the
$n$-tuple $\bar{x}=\langle x_{1},\ldots,x_{n}\rangle$ by $x_{1}=\nu$,
$x_{i+1}=\mathbf{I}(x_{i})$ for $i=1,2,\ldots,n-1$ (the existence of $\bar{x}$
is justified by SF). Let $c_{0}=c(\bar{x})$.

Define a strictly increasing sequence
$\\{a_{m}\\}_{m=1}^{\bullet}\subseteq\mathbb{N}$, where $\bullet\in\mathbb{N}$
or $\bullet=\infty$, recursively, using the notation
$A_{m}=\\{a_{1},\ldots,a_{m}\\}$ (also $a_{0}=0$ and $A_{0}=\emptyset$):

$a_{m+1}=\text{ the least }a\in\mathbb{N}\text{ such that
}a>a_{m}\,\wedge\,c\upharpoonright[A_{m}\cup\\{a\\}\cup\bar{x}]^{n}=c_{0}$
if such $a$ exists; otherwise $a_{m+1}$ is undefined and the recursion stops.

Let $A=\bigcup_{m=1}^{\bullet}A_{m}$. Then $A$ is a set and by $\mathbf{SP}$
there is a standard set $H$ such that
$\forall^{\operatorname{\mathbf{st}}}x\;(x\in H\;\leftrightarrow\;x\in A)$.
Clearly $c\upharpoonright[H]^{n}=c_{0}$.

It remains to prove that $H$ is infinite, ie, that $a_{m}$ is defined and
standard for all standard $m\in\mathbb{N}\setminus\\{0\\}$.

Fix a standard $m\in\mathbb{N}$. The sentence

$\exists
x\in\mathbb{N}\cap\mathbb{S}_{1}\;\left(x>a_{m}\,\wedge\,c\upharpoonright[A_{m}\cup\\{x,\mathbf{I}(x_{1}),\ldots,\mathbf{I}(x_{n-1})\\}]^{n}=c_{0}\right)$

is true (just let $x=x_{1}$).

By HO, $\exists
x\in\mathbb{N}\cap\mathbb{S}_{0}\;\left(x>a_{m}\,\wedge\,c\upharpoonright[A_{m}\cup\\{x,x_{1},\ldots,x_{n-1}\\}]^{n}=c_{0}\right).$
Let $a_{m+1}$ be the least such $x$ and note that it is standard.

We have $c\upharpoonright[A_{m+1}\cup\\{x_{1},\ldots,x_{n-1}\\}]^{n}=c_{0}$.
It remains to show that
$c\upharpoonright[A_{m+1}\cup\\{x_{1},\ldots,x_{n-1},x_{n}\\}]^{n}=c_{0}$.

Consider
$\bar{b}=\\{b_{1}<\ldots<b_{n}\\}\in[A_{m+1}\cup\\{x_{1},\ldots,x_{n-1},x_{n}\\}]^{n}$.

If $b_{n}<x_{n}$ then $b_{n}\leq x_{n-1}$ and $c(\bar{b})=c_{0}$.

If $b_{1}=x_{1}$ then $\bar{b}=\bar{x}$ and $c(\bar{b})=c(\bar{x}))=c_{0}$.

Otherwise $b_{1}\in\mathbb{N}\cap\mathbb{S}_{0}$ and $b_{n}=x_{n}$. Let $p$ be
the largest value such that $x_{p}\notin\bar{b}$ (clearly $1\leq p<n$) and let
$\mathbf{J}=\mathbf{I}_{\\{0,\ldots,n-1\\}}^{\\{0,\ldots,p-1,p+1,\ldots,x_{n}\\}}$.

Note that $\mathbf{J}(b_{j})=b_{j}$ for $j\leq p$, $b_{j}=x_{j}$, and
$\mathbf{J}(b_{j})=\mathbf{J}(x_{j})=x_{j+1}$ for $p<j\leq n-1$ (because
$\mathbf{I}_{\\{p,\ldots,n-1\\}}^{\\{p+1,\ldots,n\\}}\subseteq\mathbf{I},\mathbf{J}$,
ie., $\mathbf{I}$ and $\mathbf{J}$ agree on
$\mathbb{S}_{\\{p,\ldots,n-1\\}}$). Let
$\bar{b}^{\prime}=\mathbf{J}^{-1}(\bar{b})$. Then
$\bar{b}^{\prime}\in[A_{m+1}\cup\\{x_{1},\ldots,x_{n-1}\\}]^{n}$, hence
$c(\bar{b}^{\prime})=c_{0}$. By HO shift via $\mathbf{J}$, $c(\bar{b})=c_{0}$.
∎

##  6\. Jin’s proof of Szemerédi’s theorem in SPOTS

Jin’s proof in [20] uses four universes
($\mathbb{V}_{0},\mathbb{V}_{1},\mathbb{V}_{2}$ and $\mathbb{V}_{3}$) and some
additional elementary embeddings. Let
$\mathbb{N}_{j}=\mathbb{N}\cap\mathbb{V}_{j}$ and
$\mathbb{R}_{j}=\mathbb{R}\cap\mathbb{V}_{j}$ for $j=0,1,2,3$. Jin summarizes
the required properties of these universes:

0\. $\mathbb{V}_{0}\prec\mathbb{V}_{1}\prec\mathbb{V}_{2}\prec\mathbb{V}_{3}$.

1\. $\mathbb{N}_{j+1}$ is an end extension of $\mathbb{N}_{j}$ ($j=0,1,2$).

2\. For $j^{\prime}>j$, Countable Idealization holds from $\mathbb{V}_{j}$ to
$\mathbb{V}_{j^{\prime}}$:

Let $\phi$ be an $\in$-formula with parameters from $\mathbb{V}_{j^{\prime}}$.
$\forall n\in\mathbb{N}_{j}\;\exists x\;\forall m\in\mathbb{N}\;(m\leq
n\;\to\phi(m,x))\;\leftrightarrow\;\exists x\;\forall
n\in\mathbb{N}_{j}\;\phi(n,x).$

3.There is an elementary embedding $i_{\ast}$ of
$(\mathbb{V}_{2};\mathbb{R}_{0},\mathbb{R}_{1})$ to
$(\mathbb{V}_{3};\mathbb{R}_{1},\mathbb{R}_{2})$.

4\. There is an elementary embedding $i_{1}$ of
$(\mathbb{V}_{1},\mathbb{R}_{0})$ to $(\mathbb{V}_{2},\mathbb{R}_{1})$ such
that $i_{1}\upharpoonright\mathbb{N}_{0}$ is an identity map and
$i_{1}(a)\in\mathbb{N}_{2}\setminus\mathbb{N}_{1}$ for each
$a\in\mathbb{N}_{1}\setminus\mathbb{N}_{0}$.

5.There is an elementary embedding $i_{2}$ of $\mathbb{V}_{2}$ to
$\mathbb{V}_{3}$ such that $i_{2}\upharpoonright\mathbb{N}_{1}$ is an identity
map and $i_{2}(a)\in\mathbb{N}_{3}\setminus\mathbb{N}_{2}$ for each
$a\in\mathbb{N}_{2}\setminus\mathbb{N}_{1}$.

These requirements are listed as Property 2.1 in arXiv versions v1, v2 of
Jin’s paper, and appear in a slightly different form in Section 2 of the
Discrete Analysis version; see especially Property 2,7 there. Our formulations
differ from his in two significant ways.

  * •

Jin works model-theoretically and his universes are superstructures, that is,
sets of ZFC. In contrast, our universes are proper classes. Nonstandard
arguments work similarly in both frameworks.

  * •

In Property 2 Jin postulates Countable Saturation, while the weaker Countable
Idealization stated here is more suited for the axiomatic approach. In all
instances where 2 is used in Jin’s proof, Countable Idealization suffices.

######  Proposition 6.1.

$\mathbf{SPOTS}$ interprets Jin’s Properties 0. – 5.

_Proof._ We define: $\mathbb{V}_{0}=\mathbb{S}_{0}$,
$\mathbb{V}_{1}=\mathbb{S}_{\\{0\\}}$,
$\mathbb{V}_{2}=\mathbb{S}_{\\{0,1\\}}$,
$\mathbb{V}_{3}=\mathbb{S}_{\\{0,1,2\\}}$, and
$i_{1}=\mathbf{I}_{\\{0\\}}^{\\{1\\}}$,
$i_{2}=\mathbf{I}_{\\{0,1\\}}^{\\{0,2\\}}$,
$i_{\ast}=\mathbf{I}_{\\{0,1\\}}^{\\{1,2\\}}$.

Property 0. follows from GT, and Property 1. from Proposition 4.4.

Property 2. Countable Idealization is a consequence of $\mathbf{SPOT}$, so it
suffices to show that each $(\mathbb{S}_{j^{\prime}},\in,\mathbb{S}_{j})$
satisfies the axioms of $\mathbf{SPOT}$. The axiom $\mathbf{SP}$ is the only
issue.

$\mathbf{SP}$ holds in $(\mathbb{I},\in,\mathbb{S}_{0})$, hence it holds in
every $(\mathbb{I},\in,\mathbb{S}_{j})$ by HO. Its validity in
$(\mathbb{S}_{j^{\prime}},\in,\mathbb{S}_{j})$ follows.

Property 3. If $\psi(v_{1},\ldots,v_{r})$ is a formula in the common language
of the structures $(\mathbb{S}_{2},\in,\mathbb{S}_{0},\mathbb{S}_{1})$ and
$(\mathbb{S}_{3},\in,\mathbb{S}_{1},\mathbb{S}_{2})$, then, by HO,

$\forall\,x_{1},\ldots,x_{r}\in\mathbb{S}_{2}\;[\psi^{\mathbb{S}_{2}}(x_{1},\ldots,x_{r})\;\leftrightarrow\;\psi^{\mathbb{S}_{3}}(\mathbf{I}_{\\{0,1\\}}^{\\{1,2\\}}(x_{1}),\ldots,\mathbf{I}_{\\{0,1\\}}^{\\{1,2\\}}(x_{r}))].$

Properties 4. and 5. follow from Propositions 4.3 and 4.4 and the observation
that $i_{1}=i_{\ast}\upharpoonright\mathbb{V}_{1}$. ∎

It remains to show that $\mathbf{SPOT}$ proves the existence of densities used
by Jin. This requires a careful appeal to Standardization.

######  Definition 6.2.

In our notation:

  1. (1)

For finite $A\subseteq\mathbb{N}$ with $|A|$ unlimited, the _strong upper
Banach density of_ $A$ is defined by

$SD(A)=\sup{}^{\operatorname{\mathbf{st}}}\\{\operatorname{\mathbf{sh}}(|A\cap
P|/|P|)\,\mid\,|P|\text{ is unlimited}\\}.$

  2. (2)

If $S\subseteq\mathbb{N}$ has $SD(S)=\eta\in\mathbb{R}$ (note $\eta$ is
standard) and $A\subseteq S$, the _strong upper Banach density of_ $A$
_relative to_ $S$ is defined by

$SD_{S}(A)=\sup{}^{\operatorname{\mathbf{st}}}\\{\operatorname{\mathbf{sh}}(|A\cap
P|/|P|)\,\mid\,|P|\text{ is
unlimited}\,\wedge\,\operatorname{\mathbf{sh}}(|S\cap P|/|P|)=\eta\\}.$

$\mathbf{SPOT}$ does not prove the existence of the standard sets of reals
whose supremum needs to be taken (it does not allow Standardization over the
uncountable set $\mathbb{R}$), but for the purpose of obtaining the supremum,
a set of reals can be replaced by a set of rationals.

######  Proposition 6.3.

$\mathbf{SPOT}$ proves the existence of SD${}_{S}(A)$.

###### Proof.

We note that
$SD_{S}(A)=\sup{}^{\operatorname{\mathbf{st}}}\\{q\in\mathbb{Q}\,\mid\,\Phi(q)\\}$
where $\Phi(q)$ is the formula

$\exists
P\,[\,\forall^{st}_{\mathbb{N}}i\,(|P|>i)\,\wedge\,\forall^{st}_{\mathbb{N}}j(|\,|S\cap
P|/|P|-\eta|<\tfrac{1}{j+1})\,\wedge\,q\leq|A\cap P|/|P|\,].$

The formula $\Phi$ is equivalent to

$\exists P\,\forall^{st}_{\mathbb{N}}i\,[\,(|P|>i)\,\wedge\,(|\,|S\cap
P|/|P|-\eta|<\tfrac{1}{i+1})\,\wedge\,q\leq|A\cap P|/|P|\,],$

which, upon the exchange of the order of $\exists P$ and
$\forall^{st}_{\mathbb{N}}i$, enabled by Countable Idealization, converts to a
special $\operatorname{\mathbf{st}}$-$\in$-formula

$\forall^{st}_{\mathbb{N}}i\,\exists P\,[\,(|P|>i)\,\wedge\,(|\,|S\cap
P|/|P|-\eta|<\tfrac{1}{i+1})\,\wedge\,q\leq|A\cap P|/|P|\,].$

Proposition 2.4 concludes the proof. ∎

The definitions of these densities relativize to every level $j>0$. Their
existence at higher levels in $\mathbf{SPOTS}$ follows from Proposition 4.5.

##  7\. Analysis with ultrasmall numbers

The presentation of analysis in Hrbacek, Lessmann and O’Donovan [14] is based
on the notion of _relative observability_ , which we denote by $\sqsubseteq$.
In this section, $\mathbf{S}_{x}$ is the class $\\{y\,\mid\,y\sqsubseteq x\\}$
and, more generally, $y\in\mathbf{S}_{x_{1},\ldots,x_{k}}$ means that
$y\sqsubseteq x_{i}$ for some $1\leq i\leq k$. The elements of
$\mathbf{S}_{\emptyset}$ are _always observable_ (= standard). We write
formulas using this class notation. Let $\Phi(v_{1},\ldots.v_{k})$ be a
$\operatorname{\mathbf{st}}$-$\in$-formula; then
$\Phi(v_{1},\ldots.v_{k};\mathbf{S})$ is the formula obtained from $\Phi$ by
replacing each occurrence of $\operatorname{\mathbf{st}}(v)$ with
$v\in\mathbf{S}$. We use $\overline{x}$ as shorthand for the list
$x_{1},\ldots,x_{k}$.

The following principles are postulated in [14] (see the Appendix, esp. pp.
277 – 281):

_Relative Observability Principle_ : For all $x$, $y$, $z$

  1. (1)

$x\sqsubseteq x$.

  2. (2)

If $x\sqsubseteq y$ and $y\sqsubseteq z$, then $x\sqsubseteq z$.

  3. (3)

If not $x\sqsubseteq y$, then $y\sqsubseteq x$.

  4. (4)

$0\sqsubseteq x$.

  5. (5)

$\forall x\,\exists y\,(x\sqsubseteq y\,\wedge\,y\not\sqsubseteq x)$.

_Existence Principle_ : There exist $h\in\mathbb{R}$ such that $h\simeq 0$,
$h\neq 0$.

_Observable Neighbor Principle_ :

$\forall x\in\mathbb{R}\;(x\text{ limited }\to\exists
r\in\mathbb{R}\cap\mathbf{S}_{\emptyset}\;(x\simeq r)).$

_Stability Principle_ : Assume the variables $p$, $q$ do not appear in $\Phi$.

$p\sqsubseteq
q\to\forall\,\overline{x}\in\mathbf{S}_{p}\;(\Phi(\overline{x};\mathbf{S}_{p})\;\leftrightarrow\;\Phi(\overline{x};\mathbf{S}_{q})).$

######  Definition 7.1.

Formulas of the form $\Phi(\overline{x};\mathbf{S}_{\overline{x}})$ are
_internal formulas._ (We assume $x_{1},\ldots.x_{k}$ do not appear as bound
variables in $\Phi$.)

Stability for internal formulas can be restated as follows (let
$p=\langle\overline{x}\rangle$, $q=\langle\overline{x},\overline{y}\rangle$):

$\forall\overline{x},\overline{y}\;(\Phi(\overline{x};\mathbf{S}_{\overline{x}})\;\leftrightarrow\;\Phi(\overline{x};\mathbf{S}_{\overline{x},\overline{y}})).$

_Closure Principle_ : Let $\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$
be an internal formula.

$\exists x\;\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})\to\exists
x\in\mathbf{S}_{\overline{x}}\;\Phi(x,\overline{x};\mathbf{S}_{\overline{x}}).$

_Definition Principle_ Let $\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$
be an internal formula. For every set $A$ and all $x_{1},\ldots,x_{k}$ there
is a set $B\in\mathbf{S}_{A,\overline{x}}$ such that

$\forall x\;(x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})).$

Let $\mathbf{HLOD}$ be the theory in the $\sqsubseteq$-$\in$-language whose
axioms are $\mathbf{ZF}$ plus the above principles. In the rest of this
section we show that $\mathbf{HLOD}$ can be interpreted in $\mathbf{SPOTS}$.
In combination with Theorem 4.7 this shows that the presentation of analysis
in [14] relies at the most on the Axiom of Countable Choice, as is customary
in traditional analysis.

In the rest of this section we work in $\mathbf{SPOTS}$. We recall that
$\mathsf{n}$, $\mathsf{m}$ range over standard finite natural numbers and
define

$x\sqsubseteq
y\;\leftrightarrow\;\forall\mathsf{n}\;(y\in\mathbb{S}_{\mathsf{n}}\to
x\in\mathbb{S}_{\mathsf{n}}).$

By the axiom $\mathbf{SF}$, for every $x$ there is a least standard
$n\in\mathbb{N}$ such that $x\in\mathbb{S}_{n}$; we denote it $\mathsf{n}(x)$
(the _level of_ $x$). In this notation, $x\sqsubseteq
y\;\leftrightarrow\;\mathsf{n}(x)\leq\mathsf{n}(y)$ and
$\mathbf{S}_{x}=\mathbb{S}_{\mathsf{n}(x)}$.

Validity of the Relative Observability Principle in this interpretation is
trivial, and Existence and Observable Neighbor follow immediately from the
analogous principles of $\mathbf{SPOTS}$. Stability Principle is Proposition
4.5. We also note that $\mathbf{S}_{x_{1},\ldots,x_{k}}=\mathbf{S}_{\langle
x_{1},\ldots,x_{k}\rangle}=\mathbb{S}_{\mathsf{n}(\langle
x_{1},\ldots,x_{k}\rangle)}$.

To prove Closure, assume $\exists
x\;\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$. Fix some $x$ such that
$\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$ holds, and let
$p=\langle\overline{x}\rangle$, $q=\langle x,\overline{x}\rangle$. From the
formula $\exists x\in\mathbf{S}_{q}\;\Phi(x,\overline{x};\mathbf{S}_{q})$ we
get $\exists x\in\mathbf{S}_{p}\;\Phi(x,\overline{x};\mathbf{S}_{p})$ by the
Stability Principle.

It remains to prove the Definition Principle. Let
$\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$ be an internal formula. By
$\mathbf{SN}$ we get

$\forall\overline{x}\in\mathbb{S}_{0}\;\forall A\in\mathbb{S}_{0}\;\exists
B\in\mathbb{S}_{0}\;\forall x\in\mathbb{S}_{0}\;(x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbb{S}_{0})).$

By applying Proposition 4.5 to this statement we get, for any $\mathsf{n}$,

$\forall\overline{x}\in\mathbb{S}_{\mathsf{n}}\;\forall
A\in\mathbb{S}_{\mathsf{n}}\;\exists B\in\mathbb{S}_{\mathsf{n}}\;\forall
x\in\mathbb{S}_{\mathsf{n}}\;(x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbb{S}_{\mathsf{n}})).$

We now fix $\overline{x}$ and $A$, let $\mathsf{n}=\mathsf{n}(\langle
A,\overline{x}\rangle)$, and let $B\in\mathbb{S}_{\mathsf{n}}$ be such that

$\forall x\in\mathbb{S}_{\mathsf{n}}\;(x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbb{S}_{\mathsf{n}})).$

Applying Proposition 4.5 to this formula (with parameters
$A,B,\overline{x}\in\mathbb{S}_{\mathsf{n}}$) we obtain that for any
$\mathsf{m}\geq\mathsf{n}$

$\forall x\in\mathbb{S}_{\mathsf{m}}\;(x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbb{S}_{\mathsf{m}})).$

For arbitrary $x$ take $\mathsf{m}=\mathsf{n}(\langle
A,x,\overline{x}\rangle)$ to get

$x\in B\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbb{S}_{\mathsf{m}})\;\leftrightarrow\;x\in
A\,\wedge\,\Phi(x,\overline{x};\mathbf{S}_{A,x,\overline{x}}).$

It remains to notice that
$\Phi(x,\overline{x};\mathbf{S}_{A,x,\overline{x}})\;\leftrightarrow\;\Phi(x,\overline{x};\mathbf{S}_{x,\overline{x}})$,
by Stability.

######  Remark 1.

In [14] the basic concepts of Calculus, such as continuity, limit, derivative
and integral, are defined by internal formulas involving ultrasmall numbers
(infinitesimals). It is then necessary to be able to include such previously
defined internal concepts in subsequent internal formulas. This move can be
justified in several different ways.

  * •

One can prove the equivalence of the nonstandard definitions of these concepts
with the traditional $\varepsilon$-$\delta$-definitions. This requires only
straightforward, familiar arguments, but it is somewhat against the spirit of
nonstandard approach.

  * •

One can rely on a general result: _Every internal formula
$\Phi(\overline{x};\mathbf{S}_{\overline{x}})$ is equivalent to an
$\in$-formula $\phi(\overline{x})$. _ This is a consequence of the Reduction
Theorem (Kanovei and Reeken [23], Theorem 3.2.3). However, the proof of
Reduction Theorem uses a strong form of $\mathbf{AC}$ (Boolean Prime Ideal
Theorem). It is not clear whether some version of it could be proved in
$\mathbf{HLOD}$, where $\mathbf{AC}$ is not available.

  * •

We can avoid $\mathbf{AC}$ by relying instead on the Definition Principle. Ler
$R(\overline{z})$ be a predicate defined by an internal formula
$\Psi(\overline{z},\mathbf{S}_{\overline{z}})$ and let $A$ be a standard set
such that
$\forall\overline{z}\,(\Psi(\overline{z},\mathbf{S}_{\overline{z}})\to\overline{z}\in
A)$. The Definition Principle (with $\overline{z}$ in place of $x$ and empty
list $\overline{x}$) provides a standard set $B$ such that

$\qquad\quad\forall\overline{z}\;(\langle\overline{z}\rangle\in
B\;\leftrightarrow\;\langle\overline{z}\rangle\in
A\,\wedge\,\Psi(\overline{z},\mathbf{S}_{\overline{z}})\;\leftrightarrow\;\Psi(\overline{z},\mathbf{S}_{\overline{z}})\;\leftrightarrow\;R(\overline{z})).$

If $\Phi(\overline{x},\mathbf{S}_{\overline{x}})$ is a formula where the
predicate $R(\overline{z})$ also occurs, perhaps with some of the variables
$\overline{z}$ quantified (a _generalized internal formula_), we can replace
each such occurence by its equivalent $\langle\overline{z}\rangle\in B$ and
convert $\Phi$ to an internal formula as in Definition 7.1. Here is one
example.

The derivative of a real-valued function $f$ at $a\in\mathbb{R}$ is defined in
terms of infinitesimals by an internal formula at the beginning of Section 4.
Let $\mathbb{F}=\\{f\subseteq\mathbb{R}\times\mathbb{R}\,\mid\,f\text{ is a
function}\\}$ and let $A=\mathbb{F}\times\mathbb{R}\times\mathbb{R}$. The
Definition Principle guarantees the existence of a standard set $B=\\{\langle
f,a,b\rangle\in A\,\mid\,f^{\prime}(a)=b\\}$. Any generalized internal formula
involving the notion of the derivative can in principle be converted to an
internal formula by replacing each occurence of $f^{\prime}(a)=b$ with
$\langle f,a,b\rangle\in B$. In practice there is hardly ever a need to carry
out such conversions; it suffices to keep in mind that Stability, Closure and
Definition Principles apply to generalized internal formulas.

######  Remark 2.

The proof of the local Peano theorem in [14], Theorems 125 and 161, uses
Standardization over $\mathbb{R}$, which implies the existence of nonprincipal
ultrafilters over $\mathbb{N}$. The density of $\mathbb{Q}$ in $\mathbb{R}$
can be used to replace the argument by one that uses only Countable
Standardization for $\mathbb{N}$-special formulas, which is available in
$\mathbf{SPOTS}$. (See [17] for details; a similar idea is also used in the
proof of the existence of Banach densities in this paper (Proposition 6.3).)

##  8\. Conservativity

Conservativity of $\mathbf{SPOT}$ over $\mathbf{ZF}$ was established in [15]
by a construction that extends and combines the methods of forcing developed
by Ali Enayat [8] and Mitchell Spector [34]. Conservativity of $\mathbf{SCOT}$
over $\mathbf{ZF}+\mathbf{ADC}$ is obtained there as a corollary. Here we give
a simple, more direct proof of the latter result that generalizes
straightforwardly to the proof of conservativity of $\mathbf{SCOTS}$ over
$\mathbf{ZF}+\mathbf{ADC}$.

We prove the following proposition.

######  Proposition 8.1.

Every countable model $\mathcal{M}=(M,\in^{\mathcal{M}})$ of
$\mathbf{ZF}+\mathbf{ADC}$ has an extension to a model of $\mathbf{SCOTS}$ in
which elements of $M$ are exactly the standard sets.

The difficulty is that $\mathcal{M}$ may contain no nonprincipal ultrafilters.
We add such an ultrafilter to $\mathcal{M}$ by forcing, and then carry out the
construction of the iterated ultrapower as in Section 3 inside this generic
extension of $\mathcal{M}$.

Jech [19] is the standard reference for forcing and generic extensions of
well-founded models of $\mathbf{ZF}$. For details on the extension of this
material to non-well-founded models see Corazza [6, 7].

###  8.1. Forcing

In this subsection we work in $\mathbf{ZF}+\mathbf{ADC}$.

######  Definition 8.2.

Let $\mathbb{P}=\\{p\subseteq\omega\mid p\text{ is infinite}\\}$. For
$p,p^{\prime}\in\mathbb{P}$ we say that $p^{\prime}$ _extends_ $p$ (notation:
$p^{\prime}\leq p$) if $p^{\prime}\subseteq p$.

The poset $\mathbb{P}$ is not _separative_ (Jech [19], Section 17); forcing
with $\mathbb{P}$ is equivalent to forcing with
$\widetilde{\mathbb{P}}=\mathcal{P}^{\infty}(\omega)/_{\operatorname{\mathbf{fin}}}$.

The poset $\widetilde{\mathbb{P}}$ is $\omega$-_closed_ : If $\langle
p_{n}\,\mid\,n\in\omega\rangle$ is a sequence of conditions from $\mathbb{P}$
such that, for each $n\in\omega$, $p_{n+1}\setminus p_{n}$ is finite, then
there is $p\in\mathbb{P}$ such that $p\setminus p_{n}$ is finite for all
$n\in\omega$. It follows that the forcing with $\mathbb{P}$ does not add any
new countable sets (note that the proof of this fact uses $\mathbf{ADC}$).

The forcing notion $\mathbb{P}$ is _homogeneous_ in the sense that for
$x_{1},\ldots,x_{s}\in\mathbb{V}$ and $p,p^{\prime}\in\mathbb{P}$ we have
$p\Vdash\phi(\check{x}_{1},\ldots,\check{x}_{s})$ iff
$p^{\prime}\Vdash\phi(\check{x}_{1},\ldots,\check{x}_{s})$.
([19], Lemma 19.10 and related material.)

This is a consequence of the following fact (we let $p^{c}=\mathbb{N}\setminus
p$): For all $p_{1},p_{2}\in\mathbb{P}$ such that $p^{c}_{1},p^{c}_{2}$ are
infinite, there is an automorphim $\pi$ of $\mathbb{P}$ such that
$\pi(p_{1})=p_{2}$. It can be obtained as follows: Fix a one-one mapping
$\alpha$ of $\omega$ onto $\omega$ such that $\alpha$ maps $p_{1}$ onto
$p_{2}$ in an order-preserving way, and maps $p^{c}_{1}$ onto $p^{c}_{2}$ in
an order-preserving way, and then define $\pi(p)=\alpha[p]$.

###  8.2. Generic Extensions

Let $\mathcal{M}=(M,\in^{\mathcal{M}})$ be a countable model of
$\mathbf{ZF}+\mathbf{ADC}$ and let $\mathcal{G}$ be an $\mathcal{M}$-generic
filter over $\mathbb{P}^{\mathcal{M}}$. The generic extension
$\mathcal{M}[\mathcal{G}]$ is a model of $\mathbf{ZF}+\mathbf{ADC}$ extending
$\mathcal{M}$ and the forcing does not add any new reals or countble subsets
of $M$, ie., every countable subset of $M$ in $\mathcal{M}[\mathcal{G}]$
belongs to $M$.

We need the following observation: The structure
$(M[\mathcal{G}],\in^{\mathcal{M}[\mathcal{G}]},M)$ is a model of
$(\mathbf{ZF}+\mathbf{ADC})^{\mathbb{M}}$, a theory obtained by adding a unary
predicate symbol $\mathbb{M}$ to the $\in$-language of $\mathbf{ZF}$ and
postulating that the axioms of Separation, Replacenment and Dependent Choice
hold for formulas in this extended language. This is a piece of folklore; a
proof can be given by adding the predicate $\mathbb{M}$ to the forcing
language and defining

$p\Vdash\mathbb{M}(x)\iff\forall p^{\prime}\leq p\,\exists
p^{\prime\prime}\leq p^{\prime}\,\exists z\,(p^{\prime\prime}\Vdash
x=\check{z}).$

One can then prove the appropriate versions of Forcing Theoerm and the Generic
Model Theorem as in Jech [19], Section 18.

###  8.3. Conservativity of $\mathbf{SCOTS}$ over $\mathbf{ZF}+\mathbf{ADC}$.

We work in the structure $(M[\mathcal{G}],\in^{\mathcal{M}[\mathcal{G}]},M)$,
a model of $(\mathbf{ZF}+\mathbf{ADC})^{\mathbb{M}}$, and use $\omega$ to
denote its set of natural numbers. The generic filter $\mathcal{G}$ is a
nonprincipal ultrafilter over $\omega$ and one can construct the expanded
iterated ultrapower

$\mathcal{M}_{\infty}=(\mathbb{M}_{\infty},\in_{\infty},\mathbb{M}_{\mathsf{a}},\Pi_{\mathsf{a}}^{\mathsf{b}};\mathsf{a},\mathsf{b}\in\mathcal{P}^{\operatorname{\mathbf{fin}}}(\omega),|\mathsf{a}|=|\mathsf{b}|)$

of $\mathbb{M}$ by $\mathcal{G}$ as in Section 3 (let $I=\omega$,
$U=\mathcal{G}$, and replace $\mathbb{V}$ by $\mathbb{M}$).

Łoś’s Theorem holds because $\mathbf{ACC}$ is available, and
$\Pi_{0}^{\infty}$ canonically embeds $\mathbb{M}$ into
$(\mathbb{M}_{\infty},\in_{\infty})$. The structure $\mathcal{M}_{\infty}$
interprets the language of $\mathbf{SPOTS}$ (with $\mathbb{S}_{\mathsf{a}}$
interpreted as $\mathbb{M}_{\mathsf{a}}$ and
$\mathbf{I}_{\mathsf{a}}^{\mathsf{b}}$ interperted as
$\Pi_{\mathsf{a}}^{\mathsf{b}}$). As in Proposition 4.2, the structure
$\mathcal{M}_{\infty}$ satisfies IS, GT and HO. It remains to show that
$\mathbf{SN}$ and $\mathbf{DC}$ hold there.

######  Proposition 8.3.

$\mathbf{DC}$ holds in $\mathcal{M}_{\infty}$.

###### Proof.

Let $\Phi(u,v,w)$ be a formula in the language of $\mathbf{SPOTS}$. Let
$B\in\mathbb{M}_{\mathsf{a}}$, $b\in\mathbb{M}_{\mathsf{a}}$ and
$c\in\mathbb{M}_{\infty}$ be such that

$\Psi(B,b,c):\quad[b\in B\cap\mathbb{S}_{\mathsf{a}}\,\wedge\,\forall x\in
B\cap\mathbb{S}_{\mathsf{a}}\;\exists y\in
B\cap\mathbb{S}_{\mathsf{a}}\;\Phi(x,y,c)]^{\mathcal{M}_{\infty}}$

holds. (The superscript $\mathcal{M}_{\infty}$ indicates that the quantifiers
range over $\mathbb{M}_{\infty}$ and all symbols are interpreted in
$\mathcal{M}_{\infty}$.) $\Psi$ is (equivalent to) a formula of the forcing
language (we identify $B,b,c$ and $\mathsf{a}$ with their names in the forcing
language), hence there is $p\in\mathbb{P}\cap\mathcal{G}$ such that
$p\Vdash\Psi$. Let $p_{0}\leq p$.

We let the variable $a$ (with decorations) range over the names in the forcing
language and define

$A=\\{\langle p^{\prime},a^{\prime}\rangle\,\mid\,p^{\prime}\leq
p_{0}\,\wedge\,p^{\prime}\Vdash[a^{\prime}\in
B\cap\mathbb{S}_{\mathsf{a}}]^{\mathcal{M}_{\infty}}\\}.$

Note that $\langle p_{0},b\rangle\in A$, and define $\mathbf{R}$ on $A$ by

$\langle p^{\prime},a^{\prime}\rangle\mathbf{R}\langle
p^{\prime\prime},a^{\prime\prime}\rangle\text{ iff }p^{\prime\prime}\leq
p^{\prime}\,\wedge\,p^{\prime\prime}\Vdash\Phi^{\mathcal{M}_{\infty}}(a^{\prime},a^{\prime\prime},c).$

It is clear from the properties of forcing that for every $\langle
p^{\prime},a^{\prime}\rangle\in A$ there is $\langle
p^{\prime\prime},a^{\prime\prime}\rangle\in A$ such that $\langle
p^{\prime},a^{\prime}\rangle\mathbf{R}\langle
p^{\prime\prime},a^{\prime\prime}\rangle$. Using $\mathbf{ADC}$ we obtain a
sequence $\langle\langle p_{n},a_{n}\rangle\,\mid\,n\in\omega\rangle$ such
that $a_{0}=b$, and, for all $n\in\omega$, $\langle p_{n},a_{n}\rangle\in A$,
$p_{n+1}\leq p_{n}$ and
$p_{n+1}\Vdash\Phi^{\mathcal{M}_{\infty}}(a_{n},a_{n+1},c)$.

As the forcing is $\omega$-closed, one obtains $p_{\infty}\in\mathbb{P}$ and
$\langle a_{n}\mid n\in\omega\rangle$ such that $p_{\infty}\leq p_{0}$ and
$p_{\infty}\Vdash[a_{n}\in
B\cap\mathbb{S}_{\mathsf{a}}\,\wedge\,\Phi(a_{n},a_{n+1},c)]^{\mathcal{M}_{\infty}}$
for all $n\in\omega$.

By the genericity of $\mathcal{G}$ there is some $p_{\infty}\in\mathcal{G}$
and the associated sequence $\langle a_{n}\mid n\in\omega\rangle$ with this
property. Hence $(M[\mathcal{G}],\in^{\mathcal{M}[\mathcal{G}]},M)$ satisfies
$[a_{n}\in
B\cap\mathbb{S}_{\mathsf{a}}\,\wedge\,a_{0}=b\,\wedge\,\Phi(a_{n},a_{n+1},c)]^{\mathcal{M}_{\infty}}$
for all $n\in\omega$.

The class $\mathbb{S}_{\mathsf{a}}$ is interpreted in $\mathcal{M}_{\infty}$
by the ultrapower
$\mathbb{M}_{\mathsf{a}}=\mathbb{M}^{I_{\mathsf{a}}}/U_{\mathsf{a}}$ (for
$U=\mathcal{G}$) . Since this ultrapower is $\omega_{1}$-saturated, there is
$\bar{b}\in\mathbb{M}_{\mathsf{a}}$ such that $[\bar{b}:\mathbb{N}\to
B\,\wedge\,b_{n}=a_{n}]^{\mathbb{M}_{\mathsf{a}}}$ holds for every
$n\in\omega$. This translates to the desired

$[\bar{b}:\mathbb{N}\to B\,\wedge\,b_{0}=b\,\wedge\,\forall
n\in\mathbb{N}\cap\mathbb{S}_{0}\;\Phi(b_{n},b_{n+1},c)]^{\mathcal{M}_{\infty}}.$

∎

######  Proposition 8.4.

$\mathbf{SN}$ holds in $\mathcal{M}_{\infty}$.

###### Proof.

Let $\Phi(u)$ be a formula in the language of $\mathbf{SPOTS}$ (with no
parameters) and $A\in\mathbb{M}$. Let $\Psi(u)$ be the formula
$\Phi(u)^{\mathcal{M}_{\infty}}$ of the forcing language. By homogeneity of
the forcing, $p\Vdash\Psi(\check{a})$ iff $p^{\prime}\Vdash\Psi(\check{a})$
holds for all $a\in A$ and $p,p^{\prime}\in\mathbb{P}$. Fix some
$p\in\mathcal{G}$ and let $S=\\{a\in A\,\mid\,p\Vdash\Psi(\check{a})\\}$. For
$a\in\mathbb{S}$ then $a\in S$ iff $a\in
A\,\wedge\,\Phi(a)^{\mathcal{M}_{\infty}}$ holds. ∎

The structure $\mathcal{M}_{\infty}$ is a class model of $\mathbf{SCOTS}$
constructed inside the countable model
$(M[\mathcal{G}],\in^{\mathcal{M}[\mathcal{G}]},M)$. It converts into a
countable model $\widetilde{\mathcal{M}}_{\infty}$ in the meta-theory so that
$\Phi^{\mathcal{M}_{\infty}}\;\leftrightarrow\;\widetilde{\mathcal{M}}_{\infty}\vDash\Phi$
for all formulas in the language of $\mathbf{SCOTS}$.

###  8.4. Finitistic proofs

The model-theoretic proof of Proposition 8.1 in Subsections 8.1 – 8.3 is
carried out in $\mathbf{ZF}$. Using techniques from Simpson [32], Chapter II,
esp. II.3 and II.8, it can be verified that the proof goes through in
$\textbf{RCA}_{0}$ (wlog. one can assume that $M\subseteq\omega$).

The proof of Theorem 4.6 from Proposition 8.1 requires the Gödel’s
Completeness Theorem and therefore $\textbf{WKL}_{0}$; see [32], Theorem
IV.3.3. We conclude that Theorem 4.6 can be proved in $\textbf{WKL}_{0}$.

Theorem 4.6, when viewed as an arithmetical statement resulting from
identifying formulas with their Gödel numbers, is $\Pi^{0}_{2}$. It is well-
known that $\textbf{WKL}_{0}$ is conservative over PRA (Primitive Recursive
Arithmetic) for $\Pi^{0}_{2}$ sentences ([32], Theorem IX.3.16); therefore
Theorem 4.6 is provable in PRA. The theory PRA is generally considered to
correctly capture finitistic reasoning (see eg. Simpson [32], Remark IX.3.18).
We conclude that Theorem 4.6 has a finitistic proof.

These remarks apply equally to Theorem 4.7 and Proposition 8.7.

###  8.5. Conservativity of $\mathbf{SPOTS}$ over $\mathbf{ZF}+\mathbf{ACC}$.

The proof of conservativity of $\mathbf{SCOTS}$ over
$\mathbf{ZF}+\mathbf{ADC}$ presented in Subsections 8.1–8.3 relies on
$\mathbf{ADC}$ in three places:

  1. (1)

To prove that forcing with $\mathbb{P}$ does not add new countable sets.

  2. (2)

To prove that Łoś’s Theorem (Proposition 3.1) holds in $\mathcal{M}_{\infty}$.

  3. (3)

To prove that $\mathbf{DC}$ holds in $\mathcal{M}_{\infty}$ (Proposition 8.3).

Łoś’s Theorem (2) requires only $\mathbf{ACC}$. We establish weaker versions
of (1) and (3) assuming only $\mathbf{ZF}$.

Let $\mathcal{M}=(M,\in^{\mathcal{M}})$ be a countable model of $\mathbf{ZF}$
and let $\mathcal{G}$ be a generic filter over $\mathbb{P}^{\mathcal{M}}$. We
work in the structure $(M[\mathcal{G}],\in^{\mathcal{M}[\mathcal{G}]},M)$, a
model of $\mathbf{ZF}^{\mathbb{M}}$, and use $\omega$ to denote its set of
natural numbers.

######  Proposition 8.5.

  1. (1)

The generic filter $\mathcal{G}$ is an $\mathcal{M}$-_ultrafilter_ :

$\text{If }n\in\omega,\langle A_{i}\rangle_{i\in n}\in M\text{ and
}\bigcup_{i\in n}A_{i}\in\mathcal{G},\text{ then }A_{i}\in\mathcal{G}\text{
for some }i\in n.$

  2. (2)

The generic filter $\mathcal{G}$ is $\mathcal{M}$-_iterable_ :

$\text{If }S\in M,S\subseteq\omega\times\omega,\text{ then
}\\{i\in\omega\,\mid\,\\{j\in\omega\,\mid\,\langle i,j\rangle\in
S\\}\in\mathcal{G}\\}\in M.$

_Proof_ (see Enayat [8]).

(1) For every $p\in\mathbb{P}$, $p\subseteq\bigcup_{i\in
n}A_{i}\in\mathcal{G}$, there is $p^{\prime}\leq p$ such that
$p^{\prime}\subseteq A_{i}$ for some $i\in n$.

(2) Let $S_{i}^{0}=\\{j\in\omega\,\mid\,\langle i,j\rangle\in S\\}$ and
$S_{i}^{1}=\omega\setminus S_{i}^{0}$.

We say that $p\in\mathbb{P}$ _decides_ $S_{i}^{0}$ if either $p\setminus
S_{i}^{0}$ or $p\setminus S_{i}^{1}$ is bounded. We prove that for every $p$
there is $p^{\ast}\in\mathbb{P}$ such that $p^{\ast}\leq p$ and $p^{\ast}$
decides $S_{i}^{0}$ for all $i\in\omega$. It then follows that some such
$p^{\ast}$ is in $\mathcal{G}$, and
$\\{i\in\omega\,\mid\,S_{i}^{0}\in\mathcal{G}\\}=\\{i\in\omega\mid
p^{\ast}\setminus S_{i}^{0}\text{ is bounded\\}}\in M$.

For $t\in 2^{n}$ we let $|t|=n$ and $S_{t}=\bigcap_{i\in|t|}S_{i}^{t_{i}}$
($S_{\emptyset}=\omega$). We define a tree $T\subseteq 2^{<\omega}$ by $t\in
T$ iff $p\cap S_{t}$ is unbounded. Since $\bigcup_{|t|=n}S_{t}=\omega$, the
tree $T$ is infinite. By König’s Lemma $T$ has an infinite branch $t^{\ast}$.
We let $p_{i}=p\cap S_{t^{\ast}\upharpoonright i}\in\mathbb{P}$; clearly
$p_{0}=p$ and $p_{i+1}\subseteq p_{i}$ for all $i\in\omega$. We let $n_{0}=$
the least element of $p_{0}$ and $n_{i+1}=$ the least element of $p_{i+1}$
greater than $n_{i}$. Then $p^{\ast}=\\{n_{i}\mid i\in\omega\\}$ is as
required. ∎

This proposition enables the recursive definition of tensor powers
$\otimes^{n}\mathcal{G}$ and an inductive proof that, for $S\in
M,\,S\subseteq\omega\times\omega^{n}$, we have
$\\{i\in\omega\,\mid\,\\{\mathbf{j}\in\omega^{n}\,\mid\,\langle
i,\mathbf{j}\rangle\in S\\}\in\otimes^{n}\mathcal{G}\\}\in M.$ The expanded
iterated ultrapower $\mathcal{M}_{\infty}$ for $I=\omega$ and $U=\mathcal{G}$
is defined as in Section 3, with the understanding that $\mathbb{V}$ is
replaced by $\mathbb{M}$ and only functions in $\mathbb{M}$ are employed; ie.,
$\mathbb{V}^{I}$ is replaced by $\mathbb{M}^{I}\cap\mathbb{M}$ everywhere. In
particular,
$\mathbb{V}_{\mathsf{a}}=\mathbb{V}^{I^{\mathsf{a}}}/U_{\mathsf{a}}$ is
replaced by
$\mathbb{M}_{\mathsf{a}}=(\mathbb{M}^{I^{\mathsf{a}}}\cap\mathbb{M})/U_{\mathsf{a}}$(the
definition of $[f]_{U_{\mathsf{a}}}$ is also restricted to
$g,h\in\mathbb{M}$).

If we assume that $\mathcal{M}$ satisfies $\mathbf{ACC}$, Łoś’s Theorem holds
and the structure $\mathcal{M}_{\infty}$ satisfies IS, GT, HO and
$\mathbf{SN}$. It remains to show that the Standard Part axiom holds there.

######  Proposition 8.6.

$\mathbf{SP}$ holds in $\mathcal{M}_{\infty}$.

###### Proof.

Let $F\in M$, $F:\omega\to\mathcal{P}(\omega)$ (so $[F]_{\mathcal{G}}$ is a
subset of $[c_{\omega}]_{\mathcal{G}}$ in $(M^{\omega}\cap M)/\mathcal{G}$),
Define $S\in M$ by $\langle i,j\rangle\in S$ iff $i\in F(j)$.
$\mathcal{M}$-iterability of $\mathcal{G}$ implies that
$B=\\{i\in\omega\,\mid\,\\{j\in\omega\,\mid\,\langle i,j\rangle\in
S\\}\in\mathcal{G}\\}\in M$. Now

$[c_{i}]_{\mathcal{G}}\in_{\mathcal{G}}[c_{B}]_{\mathcal{G}}\;\leftrightarrow\;i\in
B\;\leftrightarrow\;\\{j\in\mathbb{N}\mid i\in
F(j)\\}\in\mathcal{G}\;\leftrightarrow\;[c_{j}]_{\mathcal{G}}\in_{\mathcal{G}}[F]_{\mathcal{G}}.$

∎

We conclude that $\mathcal{M}_{\infty}$ is a model of $\mathbf{SPOTS}$.

###  8.6. Conservativity of $\mathbf{SPOT}^{+}$ over $\mathbf{ZF}$.

The forcing construction used to establish conservativity of
$\mathbf{SPOT}^{+}$ over $\mathbf{ZF}$ is much more complicated because one
needs to force both a generic filter $\mathcal{G}$ and the validity of Łoś’s
Theorem in the corresponding “extended ultrapower.” We describe the
appropriate forcing conditions (see [15]).

Let $\mathbb{Q}=\\{q\in\mathbb{V}^{\omega}\mid\,\exists k\in\omega\;\forall
i\in\omega\,(q(i)\subseteq\mathbb{V}^{k}\,\wedge\,q(i)\neq\emptyset)\\}$.

The number $k$ is the _rank_ of $q$. We note that $q(i)$ for each
$i\in\omega$, and $q$ itself, are sets, but $\mathbb{Q}$ is a proper class.

The forcing notion $\mathbb{H}$ is defined as follows:
$\mathbb{H}=\mathbb{P}\times\mathbb{Q}$ and $\langle
p^{\prime},q^{\prime}\rangle\in\mathbb{H}$ _extends_ $\langle
p,q\rangle\in\mathbb{H}$ iff $p^{\prime}$ extends $p$,
$\operatorname{rank}q^{\prime}=k^{\prime}\geq k=\operatorname{rank}q$, and for
almost all $i\in p^{\prime}$ and all $\langle
x_{0},\ldots,x_{k^{\prime}-1}\rangle\in q^{\prime}(i)$, $\langle
x_{0},\ldots,x_{k-1}\rangle\in q(i)$.

The forcing with $\mathbb{H}$ adds many new reals; in fact, it makes all
ordinals countable.

######  Proposition 8.7.

$\mathbf{SPOT}^{+}$ is a conservative extension of $\mathbf{ZF}$.

###### Proof.

Conservativity of $\mathbf{SPOT}+\mathbf{SN}$ over $\mathbf{ZF}$ is
established in [15], Theorem B, via forcing with $\mathbb{H}$. It remains only
to show that $\mathbf{SF}$ also holds in the model constructed there.

In [15], Definition 4.4, forcing is defined for $\in$-formulas only, but the
definition can be extended to $\operatorname{\mathbf{st}}$-$\in$-formulas by
adding the clause

(11) $\langle p,q\rangle\Vdash\operatorname{\mathbf{st}}(\dot{G}_{n})$ iff
$\operatorname{rank}q=k>n$ and

$\qquad\exists x\;\forall^{\operatorname{\mathbf{aa}}}i\in p\;\forall\langle
x_{0},\ldots,x_{k-1}\rangle\in q(i)\;(x_{n}=x).$

[15] Proposition 4.6 (“Łoś’s Theorem”) does not hold for
$\operatorname{\mathbf{st}}$-$\in$-formulas, but the equivalence of clauses
(1) and (2) in [15], Proposition 4.12 (The Fundamental Theorem of Extended
Ultrapowers) remains valid ($\mathfrak{N}$ is the extended ultrapower of
$\mathcal{M}$):

_Let $\Phi(v_{1},\ldots,v_{s})$ be an
$\operatorname{\mathbf{st}}$-$\in$-formula with parameters from $M$.
If $G_{n_{1}},\ldots,G_{n_{s}}\in\mathfrak{N}$, then the following statements
are equivalent:_

  1. (1)

$\mathfrak{N}\vDash\Phi(G_{n_{1}},\ldots,G_{n_{s}})$.

  2. (2)

_There is some $\langle p,q\rangle\in\mathcal{G}$ such that $\langle
p,q\rangle\Vdash\Phi(\dot{G}_{n_{1}},\ldots,\dot{G}_{n_{s}})$ holds in
$\mathcal{M}$._

We now prove that $\mathbf{SF}$ holds in $\mathfrak{N}$.

Wlog. we can assume $A=N\in\omega$. For every $\langle
p,q\rangle\in\mathbb{H}$ and every $n\in N$ there is $\langle
p^{\prime}g^{\prime}\rangle\leq\langle p,q\rangle$ such that $\langle
p^{\prime}g^{\prime}\rangle$ decides $\Phi(\check{n})$. By induction on $n$,
for every $\langle p,q\rangle\in\mathbb{H}$ there is $\langle
p_{N},q_{N}\rangle\leq\langle p,q\rangle$ that decides $\Phi(\check{n})$ for
all $n\in N$ simultaneously. Hence there is
$\langle\widetilde{p},\widetilde{q}\rangle\in\mathcal{G}$ with this property.
Let $S=\\{n\in
N\,\mid\,\langle\widetilde{p},\widetilde{q}\rangle\Vdash\Phi(\check{n})\\}$.
By the Fundamental Theorem, $S=\\{n\in N\,\mid\,\mathfrak{N}\vDash\Phi(n)\\}$.
∎

Final Remark. Labels $\mathsf{a},\mathsf{b}$ in $\mathbf{SPOTS}$ range over
standard finite sets. This implies that the levels of standardness are
enumerated by standard natural numbers. It is an open question whether one
could allow labels to range over all finite sets, ie., to have levels of
standardness indexed by all natural numbers. Theories of this kind have been
developed in Hrbacek [12] on the basis of ZFC. It seems likely that the
present work could be generalized analogously.

## Acknowledgments

I am grateful to Mikhail G. Katz for many helpful comments and suggestions.

## References

  * [1] J. Bair, P. Błaszczyk, R. Ely, V. Henry, V. Kanovei, K. Katz, M. Katz, S. Kutateladze, T. McGaffey, P. Reeder, D. Schaps, D. Sherry, S. Shnider, _Interpreting the infinitesimal mathematics of Leibniz and Euler_ , Journal for General Philosophy of Science 48, 2 (2017) 195–238.
http://dx.doi.org/10.1007/s10838-016-9334-z https://arxiv.org/abs/1605.00455

  * [2] J. Bair, P. Błaszczyk, R. Ely, M. Katz, K. Kuhlemann, _Procedures of Leibnizian infinitesimal calculus: An account in three modern frameworks_ , British Journal for the History of Mathematics 36, 3 (2021), 170 – 209.
https://doi.org/10.1080/26375451.2020.1851120
https://arxiv.org/abs/2011.12628 https://mathscinet.ams.org/mathscinet-
getitem?mr=4353153

  * [3] B. van den Berg, E. Briseid, P. Safarik, _A functional interpretation for nonstandard arithmetic_ , Ann. Pure Appl. Logic 163, 12 (2012) 1962–1994.
  * [4] C. C. Chang, H. J. Keisler, _Model Theory, third ed._ , Studies in Logic and the Foundations of Math. 73, North Holland Publ., Amsterdam, 1990, 649 pp.
  * [5] A. Connes, _Noncommutative geometry and reality_. Journal of Mathematical Physics, 36(11) (1995),6194–-6231.
  * [6] P. Corazza, _Forcing with non-well-founded models_ , Australasian J. Logic 5 (2007), 20 – 57.
  * [7] P. Corazza, _Indestructibility of wholeness_ , Fund. Math. 252 (2021), 147 – 170. https://doi:10.4064/fm604-3-2020.
  * [8] A. Enayat, _From bounded arithmetic to second order arithmetic via automorphisms_ , in: A. Enayat, I. Kalantari, and M. Moniri (Eds.), Logic in Tehran, Lecture Notes in Logic, vol. 26, ASL and AK Peters, 2006 http://academic2.american.edu/~enayat
  * [9] A. Enayat, M. Kaufmann and Z. McKenzie, _Iterated ultraowers for the masses_ , urlhttp://arXiv:1702.03487v1 [math.LO] 12 Feb 2017
  * [10] J. Hanson, Answer to Question “Proof of global Peano theorem in ZF,” MathOverflow, 2023. https://mathoverflow.net/a/455875/28128
  * [11] K Hrbacek, _Internally iterated ultrapowers,_ in _Nonstandard Models of Arithmetic and Set Theory,_ ed. by A Enayat and R Kossak, Contemporary Math. 361, American Mathematical Society, Providence, RI, 2004, 87–120.
  * [12] K. Hrbacek, _Relative set theory: Internal view,_ Journal of Logic and Analysis 1:8 (2009), 1–108. https://doi:10.4115/jla.2009.1.8
  * [13] K. Hrbacek, _Axiom of Choice in nonstandard set theory_ , J. Log. Anal. 4:8 (2012), 1–9. https://doi:10.4115/jla.2012.4.8
  * [14] K. Hrbacek, O. Lessmann and R. O’Donovan, _Analysis using Relative Infinitesimals_ , Chapman and Hall, 2015, 316 pp.
  * [15] K. Hrbacek, M.G. Katz, _Infinitesimal analysis without the Axiom of Choice_ , Ann. Pure Appl. Logic 172, 6 (2021)
https://doi.org/10.1016/j.apal.2021.102959
https://arxiv.org/abs/2009.04980

  * [16] K. Hrbacek, M.G. Katz, _Effective infinitesimals in $\mathbb{R}$_, Real Analysis Exchange 48(2), 2023, 1 - 15
https://doi:10.14321/realanalexch.48.2.1671048854

  * [17] K. Hrbacek, M.G. Katz, _Peano and Osgood theorems via effective infinitesimals_ , Journal of Logic and Analysis 15:6 (2023) 1–19 ISSN 1759-9008 https://doi.org/10.4115/jla.2023.15.6
  * [18] T. Jech, _The Axiom of Choice_ , North-Holland Publ., Amsterdam, 1973, 202 pp.
  * [19] T. Jech, _Set Theory_ , Academic Press, New York, 1978, 621 pp.
  * [20] R. Jin, _A simple combinatorial proof of Szemerédi’s theorem via three levels of infinities_ , Discrete Analysis, 2023:15, 27 pp. https://arXiv.org/abs/2203.06322v1 https://doi.org/10.48550/arXiv.2203.06322 Editorial Introduction at https://discreteanalysisjournal.com/article/87772-a-simple-combinatorial-proof-of-szemeredi-s-
theorem-via-three-levels-of-infinities.

  * [21] R. Jin, invited talk at the conference _Logical methods in Ramsey Theory and related topics_ , Pisa July 9 - 11, 2023
https://events.dm.unipi.it/event/151/

  * [22] V. Kanovei, M. G. Katz, T. Mormann, _Tools, objects and chimeras: Connes on the role of hyperreals in mathematics_ , Found. Sci. (2013) 18:259 – 296 https://doi.org/10.1007/S10699-012-9316-5
  * [23] V. Kanovei, M. Reeken, _Nonstandard Analysis, Axiomatically_ , Springer-Verlag, Berlin Heidelberg New York, 2004, 408 pp.
  * [24] M. G. Katz, K. Kuhlemann, D. Sherry, _A Leibniz/NSA comparison_ , London Math Society Newsletter 511 (2024), 16:12, 23 – 27.
  * [25] M. G. Katz, E. Leichtnam, _Commuting and noncommuting infinitesimals_ , Amer. Math. Monthly (2013), 120:7, 631– 641. https://doi.org/10.4169/amer.math.monthly.120.07.631
  * [26] M. Katz, D. Sherry, _Leibniz’s infinitesimals: Their fictionality, their modern implementations, and their foes from Berkeley to Russell and beyond_ , Erkenntnis 78, 3 (2013), 571-625. http://dx.doi.org/10.1007/s10670-012-9370-y, https://arxiv.org/abs/1205.0174
  * [27] H. J. Keisler, _Nonstandard arithmetic and Reverse Mathematics_ , Bull. Symb. Logic, 12, 1 (2006), 100–125. http://www.jstor.org/stable/3515886
  * [28] E. Nelson, _Radically Elementary Probability Theory_ , Annals of Mathematics Studies 117, Princeton University Press, Princeton, NJ, 1987, 98 pp.
  * [29] Y. Péraire, _Théorie relative des ensembles internes_ , Osaka J. Math. 29 (1992), 267–297
  * [30] S. Sanders, _The unreasonable effectiveness of Nonstandard Analysis,_ Journal of Logic and Computation, 30, 1 (2020), 459–524. https://doi.org/10.1093/logcom/exaa019, http://arxiv.org/abs/1508.07434
  * [31] S. Sanders, _Reverse formalism 16_ , Synthese 197 (2):497-544 (2020) https://doi.org/10.1007/s11229-017-1322-2
  * [32] S. G. Simpson, _Subsystems of Second Order Arithmetic_ , second ed., Cambridge University Press, New York, 2009, 444 pp.
  * [33] R. Sommer, P. Suppes, _Finite Models of Elementary Recursive Nonstandard Analysis_ , Notas de la Sociedad Matematica de Chile 15 (1996), 73-95.
  * [34] M. Spector, _Extended ultrapowers and the Vopěnka–Hrbáček theorem without choice_ , Journal of Symboic Logic 56, 2 (1991), 592–607. https://doi.org/10.2307/2274701