1–LABEL:LastPageJan. 09, 2018Oct. 16, 2018

# Applicable Mathematics in a Minimal Computational Theory of Sets

Arnon Avron  Tel Aviv University, Tel-Aviv, Israel<EMAIL_ADDRESS>and
Liron Cohen  Cornell University, Ithaca, NY, USA<EMAIL_ADDRESS>
###### Abstract.

In previous papers on this project a general static logical framework for
formalizing and mechanizing set theories of different strength was suggested,
and the power of some predicatively acceptable theories in that framework was
explored. In this work we first improve that framework by enriching it with
means for coherently extending by definitions its theories, without destroying
its static nature or violating any of the principles on which it is based.
Then we turn to investigate within the enriched framework the power of the
minimal (predicatively acceptable) theory in it that proves the existence of
infinite sets. We show that that theory is a computational theory, in the
sense that every element of its minimal transitive model is denoted by some of
its closed terms. (That model happens to be the second universe in Jensen’s
hierarchy.) Then we show that already this minimal theory suffices for
developing very large portions (if not all) of scientifically applicable
mathematics. This requires treating the collection of real numbers as a proper
class, that is: a unary predicate which can be introduced in the theory by the
static extension method described in the first part of the paper.

##  1\. Introduction

Formalized mathematics and mathematical knowledge management (MKM) are
extremely fruitful and quickly expanding fields of research at the
intersection of mathematics and computer science (see, e.g., [3, 13, 33]). The
declared goal of these fields is to develop computerized systems that
effectively represent all important mathematical knowledge and techniques,
while conforming to the highest standards of mathematical rigor. At present
there is no general agreement what should be the best framework for this task.
However, since most mathematicians view set theory as the basic foundation of
mathematics, formalized set theories should certainly be taken as one of the
most natural choice.111Already in [14] it was argued that “a main asset gained
from Set theory is the ability to base reasoning on just a handful of axiom
schemes which, in addition to being conceptually simple (even though
surprisingly expressive), lend themselves to good automated support”. More
recently, H. Friedman wrote (in a message on FOM on Sep 14, 2015): “I envision
a large system and various important weaker subsystems. Since so much math can
be done in systems much weaker than ZFC, this should be reflected in the
choice of Gold Standards. There should be a few major Gold Standards ranging
from Finite Set Theory to full blown ZFC”. 222Notable set-based automated
provers are Mizar [43], Metamath [37], and Referee (aka AetnaNova) [41, 15].

In [6, 7] a logical framework for developing and mechanizing set theories was
introduced. Its key properties are that it is based on the usual (type-free)
set theoretic language and makes extensive use of abstract set terms. Such
terms are extensively used of course in all modern texts in all areas of
mathematics (including set theory itself). Therefore their availability is
indispensable for the purpose of mechanizing real mathematical practice and
for automated or interactive theorem proving in set theories. Accordingly,
most of the computerized systems for set theories indeed allow dynamic ways of
introducing abstract set terms. The great advantage of the framework of [6, 7]
is that it does so in a static way, so the task of verifying that a given term
or formula in it is well-formed is decidable, easily mechanizable, and
completely separated from any task connected with proving theorems (like
finding proofs or checking validity of given ones). Furthermore, this
framework enables the use of different logics and set theories of different
strength. This modularity of the system has been exploited in [8], where a
hierarchy of set theories for formalizing different levels of mathematics
within this framework was presented.

The current paper is mainly devoted to one very basic theory, $RST_{HF}^{m}$,
from the above-mentioned hierarchy, and to its minimal model. The latter is
shown to be the universe $J_{2}$ in Jensen’s hierarchy [32]. Both
$RST_{HF}^{m}$ and $J_{2}$ are _computational_ (in a precise sense defined
below). With the help of the formal framework of [6, 7, 8] they can therefore
be used to make explicit the potential computational content of set theories
(first suggested and partially demonstrated in [14]). Here we show that they
also suffice for developing large portions of scientifically applicable
mathematics [23], especially analysis.333The thesis that $J_{2}$ is sufficient
for core mathematics was first put forward in [46]. In [21, 22, 23] it was
forcefully argued by Feferman that scientifically applicable mathematics, the
mathematics that is actually indispensable to present-day natural science, can
be developed using only predicatively acceptable mathematics. We provide here
further support to this claim, using a much simpler framework and by far
weaker theory than those employed by Feferman.

The restriction to a minimal framework has of course its price. Not all of the
standard mathematical structures can be treated as elements of $J_{2}$. (The
real line is a case in point.) Hence we have to handle such objects in a
different manner. To do this, we first enrich the framework used in [6, 7, 8]
with means for coherently extending by definitions theories in it, without
destroying its static nature, or violating any of the principles on which it
is based. (This step is a very important improvement of the framework on each
own right.) This makes it possible to introduce the collection of real numbers
in $RST_{HF}^{m}$ as a proper class, that is: a legal defined unary predicate
to which no closed term of $RST_{HF}^{m}$ corresponds. (Classes are introduced
here into the formal framework of [6, 7, 8] for the first time.)

The paper is organized as follows: In Section 2 we review the formal framework
and the way various standard set theoretical notions have been introduced in
in it. We also define in this section the notions of computational theory and
universe, and describe the computational theories which are minimal within the
framework (as well as the corresponding minimal universes). Section 3 is
dedicated to the introduction of standard extensions by definitions of the
framework, done in a static way. The notion of a class is then introduced as a
particular case, and is used for handling global relations and functions in
the system. In Section 4 we introduce the natural numbers in the system.
Unlike in [8], this is done here using an absolute characterization of the
property of being a natural number, and without any appeal to $\in$-induction.
In Section 5 we turn to real analysis, and demonstrate how it can be developed
in our minimal computational framework, although the reals are a proper class
in it. This includes the introduction of the real line and real functions, as
well as formulating and proving classical results concerning these
notions.444A few of the claims in Section 5 have counterparts in [8]. However,
the models used in that paper are based on universes which are more extensive
than the minimal one which is studied here. Hence the development and proofs
there were much simpler. In particular: there was no need in [8] to use proper
classes, as is essential here. Another, less crucial but still important,
difference is that unlike in [8], the use of $\in$-induction is completely
avoided at the present paper. Section 6 concludes with directions for future
continuation of the work.

##  2\. The Formal System and its Minimal Model

###  2.1. Preliminaries: the Framework and the Main Formal System

To avoid confusion, the parentheses
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\,{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
are used in our formal languages _,_ for constructing abstract set terms in
it, while in the meta-language we use the ordinary $\left\\{\,\right\\}$.555To
be extremely precise, we should have also used different notations in the
formal languages and in the meta-language for $\in$ and $=$, as well as for
many other standard symbols which are used below. However, for readability we
shall not do so, and trust the reader to deduce the correct use from the
context. We use the letters $X,Y,Z,...$ for collections; $\Phi,\Theta$ for
finite sets of variables; and $x,y,z,...$ for variables in the formal
language. $Fv(exp)$ denotes the set of free variables of $exp$, and
$\varphi\left[\nicefrac{{t_{1}}}{{x_{1}}},\ldots,\nicefrac{{t_{n}}}{{x_{n}}}\right]$
denotes the result of simultaneously substituting $t_{i}$ for $x_{i}$ in
$\varphi$. When the identity of $t$ and $x$ is clear from the context, we just
write $\varphi(t)$ instead of $\varphi\left[\nicefrac{{t}}{{x}}\right]$.

One of the foundational questions in set theory is which formulas should be
excluded from defining sets by an abstract term of the form
$\left\\{x\mid\varphi\right\\}$ in order to avoid the paradoxes of naive set
theory. Various set theories provide different answers to this question, which
are usually based on _semantical_ considerations (such as the limitation of
size doctrine [25, 28]). Such an approach is not very useful for the purpose
of mechanization. In this work we use instead the general _syntactic_
methodology of safety relations developed in [6, 7]. A safety relation is a
syntactic relation between formulas and sets of variables. The addition of a
safety relation to a logical system allows to use in it statically defined
abstract set term of the form $\left\\{x\mid\varphi\right\\}$, provided that
$\varphi$ is safe with respect to $\\{x\\}$. Intuitively, a statement of the
form “$\varphi$ is _safe_ with respect to $\left\\{y_{1},...,y_{k}\right\\}$”,
where $Fv(\varphi)=\left\\{x_{1},...,x_{n},y_{1},...,y_{k}\right\\}$, has the
meaning that for every “accepted” sets $a_{1},...,a_{n}$, the collection
$\left\\{\left\langle
y_{1},...,y_{k}\right\rangle\mid\varphi(a_{1},...,a_{n},y_{1},...,y_{k})\right\\}$
is an “accepted” set, which is constructed from the previously “accepted” sets
$a_{1},...,a_{n}$ (see discussion below for further details).

Let $C$ be a finite set of constants. The language _$\mathcal{L}_{RST}^{C}$_
and the associated safety relation $\succ$ are simultaneously defined as
follows:

  * •

Terms:

    * –

Every variable is a term.

    * –

Every $c\in C$ is a term (taken to be a constant).

    * –

If $x$ is a variable and $\varphi$ is a formula such that
$\varphi\succ\left\\{x\right\\}$, then
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
is a term
($Fv\left({\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right)=Fv\left(\varphi\right)-\left\\{x\right\\}$).

  * •

Formulas:

    * –

If $s,t$ are terms, then $t=s$, $t\in s$ are atomic formulas.

    * –

If $\varphi,\psi$ are formulas and $x$ is a variable, then
$\neg\varphi,\left(\varphi\wedge\psi\right),\left(\varphi\vee\psi\right)$,
$\exists x\varphi$ are formulas.666Our official language does not include
$\forall$ and $\rightarrow$. However, since the theory studied in this paper
is based on classical logic, we take here $\forall x_{1}...\forall
x_{n}\left(\varphi\rightarrow\psi\right)$ as an abbreviation for $\neg\exists
x_{1}...\exists x_{n}\left(\varphi\wedge\neg\psi\right)$.

  * •

The safety relation $\succ$:

    * –

If $\varphi$ is an atomic formula, then $\varphi\succ\emptyset$.

    * –

If $t$ is a term such that $x\notin Fv\left(t\right)$, and
$\varphi\in\left\\{x\neq x,x\in t,x=t,t=x\right\\}$, then
$\varphi\succ\left\\{x\right\\}$.

    * –

If $\varphi\succ\emptyset$, then $\neg\varphi\succ\emptyset$.

    * –

If $\varphi\succ\Theta$ and $\psi\succ\Theta$, then
$\varphi\vee\psi\succ\Theta$.

    * –

If $\varphi\succ\Theta$, $\psi\succ\Phi$ and $\Phi\cap
Fv\left(\varphi\right)=\emptyset$ or $\Theta\cap
Fv\left(\psi\right)=\emptyset$, then $\varphi\wedge\psi\succ\Theta\cup\Phi$.

    * –

If $\varphi\succ\Theta$ and $y\in\Theta$, then $\exists
y\varphi\succ\Theta-\left\\{y\right\\}$.

_Notation_. We take the usual definition of $\subseteq$ in terms of $\in$,
according to which $t\subseteq s\succ\emptyset$. An $RST$-theory 777‘RST’
stands for Rudimentary Set Theory. See Theorem 5 below. is a classical first-
order system with variable binding term operator ([19]), in a language of the
form _$\mathcal{L}_{RST}^{C}$_ , which includes the following axioms:

  * •

Extensionality: $\forall z\left(z\in x\leftrightarrow z\in y\right)\rightarrow
x=y$

  * •

Comprehension Schema: $\forall
x\left(x\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\leftrightarrow\varphi\right)$

######  Lemma 1.

[7] The following notations are available (i.e. they can be introduced as
abbreviations and their basic properties are provable) in every $RST$-theory:

  * •

$\emptyset:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x\neq x{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}t_{1},...,t_{n}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x=t_{1}\vee...\vee
x=t_{n}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
where $x$ is fresh.

  * •

$\left\langle
s,t\right\rangle:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}s{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}},{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}s,t{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
$\left\langle t_{1},...,t_{n}\right\rangle:=\left\langle\left\langle
t_{1},...,t_{n-1}\right\rangle,t_{n}\right\rangle$.

  * •

$\pi_{1}\left(t\right):={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
y.t=\left\langle
x,y\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}},\,\pi_{2}\left(t\right):={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
x.t=\left\langle
x,y\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\in
t\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x\in
t\wedge\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
provided $\varphi\succ\emptyset$ and $x\notin Fv\left(t\right)$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}t\mid x\in
s{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
x.x\in s\wedge
y=t{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$, where
$y$ is fresh and $x\notin Fv\left(s\right)$.

  * •

$s\times
t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
a\exists b.a\in s\wedge b\in t\wedge x=\left\langle
a,b\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
where $x,a,b$ are fresh.

  * •

$s\cup
t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid x\in
s\vee x\in t{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
where $x$ is fresh.

  * •

$s\cap
t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid x\in
s\wedge x\in
t{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$, where $x$
is fresh.

  * •

$\cup
t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
y\in t.x\in
y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$, where
$x,y$ are fresh.

  * •

$\cap t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x\in\cup t\wedge\forall y\in t.x\in
y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$, where
$x,y$ are fresh.

  * •

$\iota
x.\varphi:=\bigcup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
provided $\varphi\succ\left\\{x\right\\}$.888Due to the Extensionality Axiom,
if $\varphi\succ\left\\{x\right\\}$, then the term above for $\iota x.\varphi$
denotes $\emptyset$ if there is no set which satisfies $\varphi$, and it
denotes the union of all the sets which satisfy $\varphi$ otherwise. In
particular: this term has the property that if there is exactly one set which
satisfies $\varphi$, then $\iota x.\varphi$ denotes this unique set since
$\cup\left\\{a\right\\}=a$. Note that the definition of $\iota x.\varphi$
taken here is simpler than the definition used in [7], which was
$\cap{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
(where some caution was taken so that the term is always well defined).

  * •

$\lambda x\in
s.t:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
x.x\in s\wedge y=\left\langle
x,t\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
provided $x\notin Fv\left(s\right)$.

  * •

$Dom\left(t\right):={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
z\exists v\exists y.z\in t\wedge v\in z\wedge y\in v\wedge x\in v\wedge
z=\left\langle
x,y\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
($z,v,x,y$ fresh).

  * •

$Im\left(t\right):={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
z\exists v\exists x.z\in t\wedge v\in z\wedge y\in v\wedge x\in v\wedge
z=\left\langle
x,y\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
($z,v,x,y$ fresh).

######  Lemma 2.

[6] There are formulas, $t\check{=}\left\langle r,s\right\rangle$ and
$\left\langle r,s\right\rangle\check{\in}t$ in $\mathcal{L}_{RST}^{\\{HF\\}}$
such that:

  1. (1)

$t\check{=}\left\langle x,s\right\rangle\succ\left\\{x\right\\}$,
$t\check{=}\left\langle s,x\right\rangle\succ\left\\{x\right\\}$ and
$t\check{=}\left\langle x,y\right\rangle\succ\left\\{x,y\right\\}$ for
$x,y\notin Fv\left(t\right)$.

  2. (2)

$\left\langle x,s\right\rangle\check{\in}t\succ\left\\{x\right\\}$,
$\left\langle s,x\right\rangle\check{\in}t\succ\left\\{x\right\\}$ and
$\left\langle x,y\right\rangle\check{\in}t\succ\left\\{x,y\right\\}$ for
$x,y\notin Fv\left(t\right)$.

  3. (3)

$r=\left\langle s,t\right\rangle\leftrightarrow r\check{=}\left\langle
s,t\right\rangle$ is provable in every $RST$-theory.

  1. (1)

$RST^{m}$ is the minimal $RST$-theory. In other words: $RST^{m}$ is the theory
in $\mathcal{L}_{RST}^{\emptyset}$ whose axioms are those given in Definition
2.1. 999 $RST^{m}$ can be shown to be equivalent to Gandy’s basic set theory
[27].

  2. (2)

$RST_{HF}^{m}$ is the $RST$-theory in $\mathcal{L}_{RST}^{\\{HF\\}}$ in which
the following axioms are added to those given in Definition 2.1:

     * •

$\emptyset\in HF$

     * •

$\forall x\forall y\left(x\in HF\wedge y\in HF\rightarrow
x\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\in
HF\right)$

     * •

$\forall y\left(\emptyset\in y\wedge\forall v,w\in
y.v\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}w{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\in
y\rightarrow HF\subseteq y\right)$

Discussion.

  * •

In [6] it was suggested that the computationally meaningful instances of the
Comprehension Axiom are those which determine the collections they define in
an absolute way, independently of any “surrounding universe”. In the context
of set theory, a formula $\varphi$ is “computable” w.r.t. $x$ if the
collection $\left\\{x\mid\varphi\left(x,y_{1},...,y_{n}\right)\right\\}$ is
completely and uniquely determined by the identity of the parameters
$y_{1},...,y_{n}$, and the identity of other objects referred to in the
formula (all of which are well-determined beforehand). Note that $\varphi$ is
computable for $\emptyset$ iff it is absolute in the usual sense of set
theory. In order to translate this idea into an exact, _syntactic_ definition,
the safety relation is used. Thus, in an $RST$-theory only those formulas
which are safe with respect to $\left\\{x\right\\}$ are allowed in the
Comprehension Scheme. It is not difficult to see that the safety relation
$\succ$ used in an $RST$-theory indeed possesses the above
property.101010Recently it was shown [10] that up to logical equivalence, and
as long as we restrict ourselves to the basic first-order language, the
converse holds as well. It is not known yet whether this is true also in the
presence of abstract set terms. Thus the formula $x\in y$ should be safe
w.r.t. $\left\\{x\right\\}$ (but not w.r.t. $\left\\{y\right\\}$), since if
the identity of $y$ is computationally acceptable as a set, then any of its
elements must be previously accepted as a set, and $\left\\{x\,|\,x\in
y\right\\}=y$. Another example is given by the clause for negation. The
intuitive meaning of $\left\\{x\,|\,\neg\varphi\right\\}$ is the complement
(with respect to some universe) of $\left\\{x\,|\,\varphi\right\\}$, which is
not in general computationally accepted. However, if $\varphi$ is absolute,
then so is its negation.

  * •

$RST^{m}$ and $RST_{HF}^{m}$ differ from the systems $RST$ and $RST_{HF}$ used
in [8] with respect to the use of $\in$-induction. In principle,
$\in$-induction does not seem to be in any conflict with the notion of a
computational theory, since it only imposes further restrictions on the
collection of acceptable sets. Accordingly, it was indeed adopted and used in
[6, 7, 8]. Nevertheless, in order not to impose unnecessary constraints on our
general framework, and in particular to allow to develop in it set theories
which adopt the anti-foundation axiom AFA, $\in$-induction is not included in
$RST^{m}$ and $RST_{HF}^{m}$.

  * •

It is not difficult to prove that $\mathcal{HF}$, the set of all hereditary
finite sets, is a model of $RST^{m}$. (In fact, it is the minimal one.) It
follows that the set $\mathbb{N}$ of the natural numbers is not definable as a
set in $RST^{m}$. To solve this problem, the special constant $HF$ was added
in $RST_{HF}^{m}$, together with appropriate axioms. (These axioms replace in
$RST_{HF}^{m}$ the usual infinity axiom of $ZF$.) The intended interpretation
of the new constant $HF$ is $\mathcal{HF}$, and the axioms for it ensure (as
far as it is possible on the first-order level) that $HF$ is indeed to be
interpreted as this collection. In particular, we have:

######  Lemma 3.

[8] The followings are provable in $RST_{HF}^{m}$:

  1. (1)

$x\in HF\leftrightarrow x=\emptyset\vee\exists u,v\in
HF.u\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}v{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}=x$.

  2. (2)

$\left(\psi\left[\nicefrac{{\emptyset}}{{x}}\right]\wedge\forall x\forall
y\left(\psi\wedge\psi\left[\nicefrac{{y}}{{x}}\right]\rightarrow\psi\left[\nicefrac{{x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}}}{{x}}\right]\right)\right)\rightarrow\forall
x\in HF.\psi$, for $\psi\succ\emptyset$.

  3. (3)

$\psi\left[\nicefrac{{HF}}{{a}}\right]\wedge\forall a\left(\psi\rightarrow
HF\subseteq a\right)$, for $\psi:=\forall x\left(x\in a\leftrightarrow
x=\emptyset\vee\exists u,v\in
a.u\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}v{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}=x\right)$.

  1. (1)

An important feature of $RST$-theories is that their two axioms directly lead
(and are equivalent) to the _set-theoretical_ $\beta$ and $\eta$ reduction
rules (see [6]).

  2. (2)

While the formal language allows the use of set terms, it also provides a
mechanizable static check of their validity due to the syntactic safety
relation. To obtain decidable syntax, logically equivalent formulas are not
taken to be safe w.r.t. the same set of variables. However, if
$\varphi\leftrightarrow\psi$ is provable in some $RST$-theory, then so is
$x\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\leftrightarrow\psi$.
Therefore for such $\varphi,\psi$ we might freely write in what follows
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\psi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
instead of
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.111111Further
discussion on decidability issues for safety-based languages can be found in
[5].

  3. (3)

It is easy to verify that the system $RST_{HF}^{m}$ is a proper subsystem of
$ZF$. While the latter is not an $RST$-theory, in [6] it was shown that it can
be obtained from the former by adding the following clauses to the definition
of its safety relation:

     * •

Separation: $\varphi\succ\emptyset$ for every formula $\varphi$.

     * •

Powerset: $x\subseteq t\succ\\{x\\}$ if $x\not\in Fv(t)$.

     * •

Replacement: $\exists y\varphi\wedge\forall y(\varphi\rightarrow\psi)\succ X$,
provided $\psi\succ X$, and $X\cap Fv(\varphi)=\emptyset$.

  4. (4)

Unlike in this paper, in general the framework for set theories just reviewed
is not confined to the first-order level or to classical logic. Thus in [7] it
was used together with ancestral logic ([35, 38, 44, 4, 17]). (This involves
adding a special clause to the definition of $\succ$ that treats the operation
of transitive closure.) Intuitionistic versions have been investigated too.

  5. (5)

A safety relation like $\succ$ presents a difficult challenge for mechanized
logical frameworks of the Edinburgh LF’s type ([29]). First, it is a strictly
syntactic relation between formulas and variables, whose direct implementation
requires the use of meta-variables for the variables of the object language —
something which is particularly difficult to handle in this type of logical
frameworks ([9]). Second, $\succ$ does not have a fixed arity like all
judgements in the Edinburgh LF do: it is actually a relation between formulas
and finite sets of object-level variables. Therefore it seems that current
logical frameworks should be significantly extended and refined in order to be
able to handle the syntactic framework for set theories that was proposed in
[6] (and is used here).

###  2.2. The Minimal Model

We next recall the definition of rudimentary functions (for more on this topic
see [20, 30]).121212To be precise, the definition we take here is given in The
Basis Lemma in [20]. It was shown there that this definition is equivalent to
the standard definition of rudimentary functions. Rudimentary functions are
just the functions obtained by omitting the recursion schema from the usual
list of schemata for primitive recursive set functions. Every rudimentary
function is a composition of the following functions:

  * •

$F_{0}\left(x,y\right)=\left\\{x,y\right\\}$

  * •

$F_{1}\left(x,y\right)=x-y$

  * •

$F_{2}\left(x,y\right)=x\times y$

  * •

$F_{3}\left(x,y\right)=\left\\{\left\langle u,z,v\right\rangle\,|\,z\in
x\wedge\left\langle u,v\right\rangle\in y\right\\}$

  * •

$F_{4}\left(x,y\right)=\left\\{\left\langle z,v,u\right\rangle\,|\,z\in
x\wedge\left\langle u,v\right\rangle\in y\right\\}$

  * •

$F_{5}\left(x,y\right)=\left\\{Im\left(x|_{z}\right)\,|\,z\in y\right\\}$
where $Im\left(x|_{z}\right)=\left\\{w\,|\,\exists u\in z.\left\langle
u,w\right\rangle\in x\right\\}$

  * •

$F_{6}\left(x\right)=\underset{z\in x}{\bigcup}z$

  * •

$F_{7}\left(x\right)=Dom\left(x\right)=\left\\{v\,|\,\exists w.\left\langle
v,w\right\rangle\in x\right\\}$

  * •

$F_{8}\left(x\right)=\left\\{\left\langle u,v\right\rangle\,|\,u\in x\wedge
v\in x\wedge u\in v\right\\}$

  1. (1)

A function is called $HF$-rudimentary if it can be generated by composition of
the functions $F_{0},...,F_{8}$ in Definition 12, and the following constant
function:

     * •

$F_{9}\left(x\right)=\mathcal{HF}$ (the set of hereditary finite sets).

  2. (2)

An $HF$-universe (universe in short) is a transitive collection of sets that
is closed under $HF$-rudimentary functions.

_Terminology._ In what follows, we do not distinguish between a universe $W$
and the structure for $\mathcal{L}_{RST}^{\\{HF\\}}$ with domain $W$ and an
interpretation function $I$ that assigns the obvious interpretations to the
symbols $\in$, $=$, and $\mathcal{HF}$ to $HF$. We denote by
$v\left[x:=a\right]$ the $x$-variant of $v$ which assigns $a$ to $x$. If
$\vec{y},\overrightarrow{a}$ are two vectors of the same length we abbreviate
$v\left[y_{1}:=a_{1},...,y_{n}:=a_{n}\right]$ by
$v\left[\vec{y}:=\overrightarrow{a}\right]$. We denote by
$\left[x_{1}:=a_{1},...,x_{n}:=a_{n}\right]$ any assignment which assigns to
each $x_{i}$ the element $a_{i}$.131313As long as we apply
$\left[x_{1}:=a_{1},...,x_{n}:=a_{n}\right]$ to expressions whose set of free
variables is contained in $\left\\{x_{1},...,x_{n}\right\\}$ the exact
assignment does not matter.

Let $W$ be a universe, $v$ an assignment in $W$. For any term $t$ and formula
$\varphi$ of $\mathcal{L}_{RST}^{\\{HF\\}}$, we recursively define a
collection $\left\|t\right\|_{v}^{W}$ and a truth value
$\left\|\varphi\right\|_{v}^{W}\in\left\\{\mathbf{t},{\bf f}\right\\}$
(respectively) by:

  * •

$\left\|x\right\|_{v}^{W}=v\left(x\right)$ for $x$ a variable.

  * •

$\left\|HF\right\|_{v}^{W}=\mathcal{HF}$

  * •

$\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|_{v}^{W}=\left\\{a\in
W\mid\left\|\varphi\right\|_{v\left[x:=a\right]}^{W}={\bf t}\right\\}$

  * •

$\left\|v\right\|_{v}{t=s}={\bf t}$ iff
$\left\|t\right\|_{v}^{W}=\left\|s\right\|_{v}^{W}$ ; $\left\|t\in
s\right\|_{v}^{W}={\bf t}$ iff
$\left\|t\right\|_{v}^{W}\in\left\|s\right\|_{v}^{W}$

  * •

$\left\|\neg\varphi\right\|_{v}^{W}={\bf t}$ iff
$\left\|\varphi\right\|_{v}^{W}={\bf f}$

  * •

$\left\|\varphi\wedge\psi\right\|_{v}^{W}={\bf t}$ iff
$\left\|\varphi\right\|_{v}^{W}={\bf t}\wedge\left\|\psi\right\|_{v}^{W}={\bf
t}$

  * •

$\left\|\varphi\vee\psi\right\|_{v}^{W}={\bf t}$ iff
$\left\|\varphi\right\|_{v}^{W}={\bf t}\vee\left\|\psi\right\|_{v}^{W}={\bf
t}$

  * •

$\left\|\exists x\varphi\right\|_{v}^{W}={\bf t}$ iff $\exists a\left(a\in
W\wedge\left\|\varphi\right\|_{v\left[x:=a\right]}^{W}={\bf t}\right)$

Given $W$ and $v$, we say that the term $t$ defines the collection
$\left\|t\right\|_{v}^{W}$.

######  Remark 4.

From Theorem 6 below it follows that $\left\|t\right\|_{v}^{W}$ is an element
of $W$ (and it denotes the value in $W$ that the term $t$ gets under $v$), and
$\left\|\varphi\right\|_{v}^{W}$ denotes the truth value of the formula
$\varphi$ under $W$ and $v$.

In case $exp$ is a closed term or a closed formula, we denote by
$\left\|exp\right\|^{W}$ the value of $exp$ in $W$, and at times we omit the
superscript $W$ and simply write $\left\|exp\right\|$.

The following theorem is a slight generalization of a theorem proved in [7].

######  Theorem 5.

  1. (1)

If $F$ is an $n$-ary $HF$-rudimentary function, then there is a formula
$\varphi_{F}$ of $\mathcal{L}_{RST}^{\\{HF\\}}$ s.t.:

     * •

$Fv\left(\varphi_{F}\right)\subseteq\left\\{y,x_{1},...,x_{n}\right\\}$

     * •

$\varphi_{F}\succ\left\\{y\right\\}$

     * •

$F\left(x_{1},...,x_{n}\right)=\left\\{y\mid\varphi_{F}\right\\}$

  2. (2)

If $\varphi$ is a formula of $\mathcal{L}_{RST}^{\\{HF\\}}$ such that:

     * •

$Fv\left(\varphi\right)\subseteq\left\\{y_{1},...,y_{k},x_{1},...,x_{n}\right\\}$

     * •

$\varphi\succ\left\\{y_{1},...,y_{k}\right\\}$

then there exists a $HF$-rudimentary function $F_{\varphi}$ such that:

$F_{\varphi}\left(x_{1},...,x_{n}\right)=\left\\{\left\langle
y_{1},...,y_{k}\right\rangle\mid\varphi\right\\}$

  3. (3)

If $t$ is a term of $\mathcal{L}_{RST}^{\\{HF\\}}$ such that
$Fv\left(t\right)\subseteq\left\\{x_{1},...,x_{n}\right\\}$, then there exists
a $HF$-rudimentary function $F_{t}$ such that
$F_{t}\left(x_{1},...,x_{n}\right)=t$ for every $x_{1},...,x_{n}$.

######  Proof 2.1.

The corresponding theorem in [7] establishes the connection between
$\mathcal{L}_{RST}^{\\{HF\\}}$ without the constant $HF$ and rudimentary
functions. Thus, the only modification required here is the treatment of the
new function in (1), and the treatment of the constant $HF$ in (2) and (3)
(which are then incorporated in the original proof that was carried out by
induction). For (1), it is easy to verify that $\varphi_{F_{9}}:=\,y=HF$. For
(2) and (3) (which are proved by simultaneous induction on the structure of
terms and formulas), the case for the constant $HF$ is immediate from the
definition of $HF$-rudimentary functions.

######  Theorem 6.

Let $W$ be a universe, and $v$ an assignment in $W$.

  * •

For $t$ a term of $\mathcal{L}_{RST}^{\\{HF\\}}$, $\left\|t\right\|_{v}^{W}\in
W$.

  * •

For $\varphi$ a formula of $\mathcal{L}_{RST}^{\\{HF\\}}$:

    * –

If $\varphi\succ\left\\{y_{1},...,y_{n}\right\\}$ and $n>0$, then:

$\left\\{\left\langle a_{1},...,a_{n}\right\rangle\in
W^{n}\mid\left\|\varphi\right\|_{v\left[\vec{y}:=\overrightarrow{a}\right]}^{W}={\bf
t}\right\\}\in W$

.

    * –

If $\varphi\succ\emptyset$ and $\left\\{y_{1},...,y_{n}\right\\}\subseteq
Fv\left(\varphi\right)$, then for any $X\in J_{2}$:

$\left\\{\left\langle a_{1},...,a_{n}\right\rangle\in
X^{n}\mid\left\|\varphi\right\|_{v\left[\vec{y}:=\overrightarrow{a}\right]}^{W}={\bf
t}\right\\}\in W$

######  Proof 2.2.

The proof is straightforward using Theorem 5. Claims (1) and (2a) are
immediate. For (2b) let $\varphi$ be a formula s.t. $\varphi\succ\emptyset$
and $\left\\{y_{1},...,y_{n}\right\\}\subseteq Fv\left(\varphi\right)$. Using
Theorem 5 we get that $\varphi$ defines a $HF$-rudimentary predicate,
$P_{\varphi}$ (i.e. one whose characteristic function is $HF$-rudimentary).
Define:

$H\left(x_{1},...,x_{k},y_{1},...,y_{n}\right)=\begin{cases}\left\\{\left\langle
y_{1},...,y_{n}\right\rangle\right\\}&\mathrm{if}\,\,\,P_{\varphi}\left(x_{1},...,x_{k},y_{1},...,y_{n}\right)\\\
\emptyset&\mathrm{otherwise}\end{cases}$

$H$ is a $HF$-rudimentary function (see Lemma 1.1 in [20]). Now, define:

$F\left(z,x_{1},...,x_{k}\right)=z^{n}\cap\left\\{\left\langle
y_{1},...,y_{n}\right\rangle|P_{\varphi}\left(x_{1},...,x_{k},y_{1},...,y_{n}\right)\right\\}$

$F$ is also $HF$-rudimentary since

$F\left(z,x_{1},...,x_{k}\right)=\bigcup_{\left\langle
y_{1},...,y_{n}\right\rangle\in
z^{n}}H\left(x_{1},...,x_{k},y_{1},...,y_{n}\right)$

Now, the fact that $W$ is a universe entails that for every assignment $v$ in
$W$ and every $X\in W$,
$F\left(X,v\left(x_{1}\right),....,v\left(x_{k}\right)\right)\in W$, and so
$\left\\{\left\langle a_{1},...,a_{n}\right\rangle\in
X^{n}\mid\left\|\varphi\right\|_{v\left[\vec{y}:=\overrightarrow{a}\right]}^{W}={\bf
t}\right\\}\in W$.

######  Proposition 7.

Let $W$ be a universe. Then, $W$ is a model of $RST_{HF}^{m}$.

######  Proof 2.3.

The Extensionality axiom is clearly satisfied in any universe. Theorem 6
entails that the interpretation of any term is an element of the universe.
This immediately implies that the other axioms are satisfied in any universe.
It is also straightforward to verify that the interpretation of $HF$ as
$\mathcal{HF}$ satisfies the three axioms for $HF$.

###  2.3.  Computational Theories and Universes

Computations within a set of objects require concrete representations of these
objects. Accordingly, we call a theory _computational_ if its set of closed
terms induces in a natural way a minimal model of the theory, and it enables
the key properties of these elements to be provable within it. Next we provide
a more formal definition for the case of set theories which are defined within
our general framework. Note that from a Platonist point of view, the set of
closed terms of such a theory $\mathcal{T}$ induces some subset
$\mathcal{S_{T}}$ of the cumulative universe of sets $V$, as well as some
subset $\mathcal{M_{T}}$ of any transitive model $\mathcal{M}$ of
$\mathcal{T}$.

  1. (1)

A theory $\mathcal{T}$ in the above framework is called _computational_ if the
set $\mathcal{S_{T}}$ it induces is a transitive model of $\mathcal{T}$, and
the identity of $\mathcal{S_{T}}$ is absolute in the sense that
$\mathcal{M_{T}}=\mathcal{S_{T}}$ for any transitive model $\mathcal{M}$ of
$\mathcal{T}$ (implying that $\mathcal{S_{T}}$ is a _minimal_ transitive model
of $\mathcal{T}$).

  2. (2)

A set is called computational if it is $\mathcal{S_{T}}$ for some
computational theory $\mathcal{T}$.

The most basic computational theories are $RST^{m}$ and $RST_{HF}^{m}$, which
are the two minimal theories in the hierarchy of systems developed in [8].
This fact, as well as the corresponding computational universes, are described
in the following three results from [8].

######  Proposition 8.

Let $J_{1}$ and $J_{2}$ be the first two elements in Jensen’s hierarchy
[32].141414$J_{1}=\mathcal{HF}$ and $J_{2}=Rud\left(J_{1}\right)$, where
$Rud\left(x\right)$ denotes the smallest set $y$ such that $x\subseteq y$,
$x\in y$, and $y$ is closed under application of all rudimentary functions.

  1. (1)

$J_{1}$ is a model of $RST$.

  2. (2)

$J_{2}$ with the interpretation of $HF$ as $J_{1}$ is a model of
$RST_{HF}^{m}$.

######  Proof 2.4.

The first claim is trivial. The second claim follows from Corollary 7, since
$J_{2}$ is clearly a universe.

######  Theorem 9.

  1. (1)

$X\in J_{1}$ iff there is a closed term $t$ of $\mathcal{L}_{RST}$ s.t.
$\left\|t\right\|^{J_{1}}=X$.

  2. (2)

$X\in J_{2}$ iff there is a closed term $t$ of $\mathcal{L}_{RST}^{\\{HF\\}}$
such that $\left\|t\right\|^{J_{2}}=X$.

######  Proof 2.5.

We prove the second item, leaving the easy proof of the first to the reader.
Theorem 6 entails the right-to-left implication. The converse is proved by
induction, using Lemma 1. Clearly,
$\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x\in
x{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}=\emptyset$
and $\left\|HF\right\|^{J_{2}}=J_{1}$. Now, suppose that for $A,B\in J_{2}$
there are closed terms $t_{A}$ and $t_{B}$ such that
$\left\|t_{A}\right\|^{J_{2}}=A$ and $\left\|t_{B}\right\|^{J_{2}}=B$. We show
that there are closed terms for any of the results of applications of
$F_{0},...,F_{8}$ to $A$ and $B$.

  * •

$F_{0}\left(A,B\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}t_{A},t_{B}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

  * •

$F_{1}\left(A,B\right)=\left\|t_{A}-t_{B}\right\|^{J_{2}}$

  * •

$F_{2}\left(A,B\right)=\left\|t_{A}\times t_{B}\right\|^{J_{2}}$

  * •

$F_{3}\left(A,B\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
z\in t_{A}\exists u,v.\left\langle u,v\right\rangle\check{\in}t_{B}\wedge
x=\left\langle
u,z,v\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

  * •

$F_{4}\left(A,B\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
z\in t_{A}\exists u,v.\left\langle u,v\right\rangle\check{\in}t_{B}\wedge
x=\left\langle
z,v,u\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

  * •

$F_{5}\left(A,B\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}Im\left({\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}w\mid
w\in t_{A}\wedge\pi_{1}\left(w\right)\in
z{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right)\mid
z\in
t_{B}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

  * •

$F_{6}\left(A\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
u\in t_{A}.x\in
u{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

  * •

$F_{7}\left(A\right)=\left\|Dom\left(t_{A}\right)\right\|^{J_{2}}$

  * •

$F_{8}\left(A\right)=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
u\in t_{A}\exists v\in t_{a}.u\in v\wedge x\check{=}\left\langle
u,v\right\rangle{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|^{J_{2}}$

######  Corollary 10.

$RST^{m}$ and $RST_{HF}^{m}$ are computational, and $J_{1}$ and $J_{2}$ are
their computational models.

Now $J_{1}$, the minimal computational set, is the set of hereditary finite
sets. Its use captures the standard data structures used in computer science,
like strings and lists. However, in order to be able to capture computational
structures with infinite objects, we have to move to $RST_{HF}^{m}$, whose
computational universe, $J_{2}$, seems to be the minimal universe that
suffices for this purpose. $RST_{HF}^{m}$ still allows for a very concrete,
computationally-oriented interpretation, and it is appropriate for mechanical
manipulations and interactive theorem proving. As noted in the introduction,
the main goal of this paper is to show that this theory and its corresponding
universe $J_{2}$ are sufficiently rich for a systematic development of (great
parts of) applicable mathematics.

##  3\. Classes and Static Extensions by Definitions

When working in a minimal computational universe such as $J_{2}$ (as done in
the next section), many of the standard mathematical objects (such as the real
line and real functions) are only available in our framework as proper
classes. Thus, in order to be able to formalize standard theorems regarding
such objects we must enrich our language to include them. However, introducing
classes into our framework is a part of the more general method of extensions
by definitions, which is an essential part of every mathematical research and
its presentation. There are two principles that govern this process in our
framework. First, the static nature of our framework demands that
conservatively expanding the language of a given theory should be reduced to
the use of _abbreviations_. Second, since the introduction of new predicates
and function symbols creates new atomic formulas and terms, one should be
careful that the basic conditions concerning the underlying safety relation
$\succ$ are preserved. Thus only formulas $\varphi$ s.t.
$\varphi\succ\emptyset$ can be used for defining new predicate symbols.

We start with the problem of introducing new predicate symbols. Since $n$-ary
predicates can be reduced in the framework of set theory to unary predicates,
we focus on the introduction of new unary predicates. In standard practice
such extensions are carried out by introducing a new unary predicate symbol
$P$ and either treating $P\left(t\right)$ as an abbreviation for
$\varphi\left[\nicefrac{{t}}{{x}}\right]$ for some formula $\varphi$ and
variable $x$, or (what is more practical) adding $\forall
x\left(P\left(x\right)\leftrightarrow\varphi\right)$ as an axiom to the
(current version of the base) theory, obtaining by this a conservative theory
in the extended language. However, in the set theoretical framework it is
possible and frequently more convenient to uniformly use class terms, rather
than introduce a new predicate symbol each time. Thus, instead of writing
“$P\left(t\right)$” one uses an appropriate class term $S$ and writes “$t\in
S$”. Whatever approach is chosen – in order to respect the definition of a
safety relation, class terms should be restricted so that “$t\in S$” is safe
w.r.t. $\emptyset$. Accordingly, we extend our language by incorporating class
terms, which are objects of the form
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
where $\varphi\succ\emptyset$. The use of these terms is done in the standard
way. In particular,
$t\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
(where $t$ is free for $x$ in $\varphi$) is equivalent to (and may be taken as
an abbreviation for) $\varphi\left[\nicefrac{{t}}{{x}}\right]$. It should be
emphasized that a class term is not a valid term in the language, but only a
definable predicate. Thus the addition of the new notation does not enhance
the expressive power of languages like _$\mathcal{L}_{RST}^{\\{HF\\}}$_ , but
only increases the ease of using them.

######  Remark 11.

Further standard abbreviations (see [34]) are:

  * •

$t\subseteq{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
is an abbreviation for $\forall z\left(z\in t\rightarrow
z\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right)$.

  * •

$t={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
and
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}=t$
stand for $\forall z\left(z\in t\leftrightarrow
z\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right)$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\hat{\,\mid\,}\psi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
is an abbreviation for $\forall
z\left(z\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\leftrightarrow
z\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\hat{\,\mid\,}\psi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right)$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\in
t$ is an abbreviation for $\exists
z.z={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\wedge
z\in t$.

  * •

${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\hat{\,\mid\,}\psi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
is an abbreviation for $\exists
z.z={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\wedge
z\in{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\hat{\,\mid\,}\psi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

Note that these formulas are merely abbreviations for formulas which are _not_
necessarily atomic (even though,
$t\subseteq{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
also happens to be safe with respect to $\emptyset$).

A further conservative extension of the language that we shall use
incorporates free class variables,
$\boldsymbol{X},\boldsymbol{Y},\boldsymbol{Z}$, and free function variables,
$\boldsymbol{F},\boldsymbol{G}$, into $\mathcal{L}_{RST}^{\\{HF\\}}$ (as in
free-variable second-order logic [44]). These variables stand for arbitrary
class or function terms (the latter is defined in Def. 16), and they may only
appear as _free_ variables, _never to be quantified_. We allow occurrences of
such variables inside a formula in a class term or a function term. One may
think of a formula with such variables as a schema, where the variables play
the role of “place holders”, and whose substitution instances abbreviate
official formulas of the language. (See Example 5.2.) In effect, a formula
$\psi\left(\boldsymbol{X}\right)$ with free class variable $\boldsymbol{X}$
can be intuitively interpreted as “for any _given_ class $X$,
$\psi\left(X\right)$ holds”. Thus, a free-variable formulation has the flavor
of a universal formula. Therefore, this addition allows statements about _all_
potential classes and _all_ potential functions.

Let $W$ be a universe, $v$ an assignment in $W$, and let
$\varphi\succ\emptyset$. Define:

$\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|_{v}^{W}:=\left\\{a\in
W\mid\left\|\varphi\right\|_{v\left[x:=a\right]}^{W}={\bf t}\right\\}$

Given $W$ and $v$, we again say that the class term on the left defines here
the collection on the right (even though it might not be an element of $W$).

Let $X$ be a collection of elements in a universe $W$.

  * •

$X$ is a $\succ$_-set_ (in $W$) if there is a closed term that defines it.
(See Definition 2.2.) If $X$ is a _$\succ$_ -set, $\widetilde{X}$ denotes some
closed term that defines it.

  * •

$X$ is a _$\succ$ -class_ (in $W$) if there is a closed class term that
defines it. If $X$ is a _$\succ$_ -class, $\bar{X}$ denotes some closed class
term that defines it.

Note that by Corollary 6, if $X$ is a $\succ$_-set_ in $W$ then $X\in W$.

######  Proposition 12.

The following holds for every universe $W$:

  1. (1)

Every $\succ$-set is a _$\succ$_ -class.

  2. (2)

The intersection of a _$\succ$_ -class with a _$\succ$_ -set is a _$\succ$_
-set.

  3. (3)

Every $\succ$-class that is contained in a _$\succ$_ -set is a _$\succ$_ -set.

######  Proof 3.1.

  1. (1)

If $X$ is a _$\succ$_ -set, then $x\in\widetilde{X}\succ\\{x\\}$. Hence (see
[6]) $x\in\widetilde{X}\succ\emptyset$. This implies that
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}x\in\widetilde{X}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
is a class term which defines $X$, and so $X$ is a _$\succ$_ -class.

  2. (2)

Let $X$ be a _$\succ$_ -class and $Y$ be a _$\succ$_ -set. Then, $X\cap Y$ can
be defined by the term
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\mid
z\in\bar{X}\wedge
z\in\widetilde{Y}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
Since $z\in\bar{X}\succ\emptyset$ and
$z\in\widetilde{Y}\succ\left\\{z\right\\}$ we get that $z\in\bar{X}\wedge
z\in\widetilde{Y}\succ\left\\{z\right\\}$. Hence $X\cap Y$ is a _$\succ$_
-set.

  3. (3)

Follows from (2), since if $X\subseteq Y$ then $X=X\cap Y$.

######  Remark 13.

A semantic counterpart of our notion of a $\succ$-class was used in [46], and
is called there an $\iota$-class. It is defined as a definable subset of
$J_{2}$ whose intersection with any element of $J_{2}$ is in $J_{2}$. The
second condition in this definition seems somewhat ad hoc. More importantly,
it is unclear how it can be checked in general, and what kind of set theory is
needed to establish that certain collections are $\iota$-classes. In contrast,
the definition of a $\succ$-class used here is motivated by, and based on,
purely syntactical considerations. It is also a simplification of the notion
of $\iota$-class, as by Prop. 12(2) every $\succ$-class is an
$\iota$-class.151515Two other ideas that appear in the sequel were adopted
from [46]: treating the collection of reals as a proper class, and the use of
codes for handling certain classes. It should nevertheless be emphasized that
the framework in [46] is exclusively based on semantical considerations, and
it is unclear how it can be turned into a formal (and suitable for
mechanization) theory like $ZF$ or $PA$.

######  Proposition 14.

The following holds for every universe $W$:

  * •

Let $Y$ be a _$\succ$_ -set. If $\varphi\succ\emptyset$ and
$Fv\left(\varphi\right)\subseteq\left\\{x\right\\}$, then $\left\\{x\in
Y\mid\varphi\right\\}$ is a _$\succ$_ -set.

  * •

If $\varphi\succ\left\\{x_{1},...,x_{n}\right\\}$, then $\left\\{\left\langle
x_{1},...,x_{n}\right\rangle\mid\varphi\right\\}$ is a _$\succ$_ -set.

######  Proof 3.2.

  * •

$\left\\{x\in Y\mid\varphi\right\\}$ is defined by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid
x\in\widetilde{Y}\wedge\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

$\left\\{\left\langle x_{1},...,x_{n}\right\rangle\mid\varphi\right\\}$ is
defined by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\mid\exists
x_{1}...\exists x_{n}\left(\varphi\wedge z=\left\langle
x_{1},...,x_{n}\right\rangle\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
where $z$ is fresh.

######  Proposition 15.

For every $n$-ary $HF$-rudimentary function $f$ there is a term $t$ with
$Fv\left(t\right)\subseteq\left\\{x_{1},...,x_{n}\right\\}$ s.t. for any
$\left\langle A_{1},...,A_{n}\right\rangle\in W^{n}$, $f$ returns the
_$\succ$_ -set
$\left\|t\right\|_{\left[x_{1}:=A_{1},...,x_{n}:=A_{n}\right]}^{W}$.

######  Proof 3.3.

It is easy to see that if $X_{1},...,X_{n}$ are $\succ$-sets, and $\varphi$ is
a formula such that
$Fv\left(\varphi\right)\subseteq\left\\{y,v_{1},...v_{n}\right\\}$ and
$\varphi\succ\left\\{y\right\\}$, then
$\left\\{y\mid\varphi\left\\{\frac{\widetilde{X_{1}}}{v_{1}},...,\frac{\widetilde{X_{n}}}{v_{n}}\right\\}\right\\}$
is a _$\succ$_ -set. Therefore the proposition easily follows from Theorem 5.

######  Proposition 16.

If $X,Y$ are $\succ$-classes (in a universe $W$), so are $X\cup Y$, $X\cap Y$,
$X\times Y$, $J_{2}-X$, and $P_{J_{2}}\left(X\right)=\left\\{z\in J_{2}\mid
z\subseteq X\right\\}$.

Proof:

  * •

$\overline{X\cup
Y}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}x\in\bar{X}\vee
x\in\bar{Y}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

$\overline{X\cap
Y}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}x\in\bar{X}\wedge
x\in\bar{Y}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

$\overline{X\times
Y}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\exists
a\exists b\left(a\in\bar{X}\wedge b\in\bar{Y}\wedge x\check{=}\left\langle
a,b\right\rangle\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
(See Lemma 2.)

  * •

$\overline{J_{2}-X}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}x\notin\bar{X}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.

  * •

$P_{J_{2}}\left(X\right)={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}z\subseteq\bar{X}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}\forall
a\left(a\in z\rightarrow
a\in\bar{X}\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
(See footnote 6.) ∎

For a class term $s$ we denote by $2^{s}$ the class term
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}z\subseteq
s{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$. Note that
for any assignment $v$ in $W$ and class term $s$,
$\left\|2^{s}\right\|_{v}^{W}$ is equal to
$P_{W}\left(\left\|s\right\|_{v}^{W}\right)$, i.e., the intersection of the
power set of $\left\|s\right\|_{v}^{W}$ and $W$. This demonstrates the main
difference between set terms and class terms. The interpretation of set terms
is absolute, whereas the interpretation of class terms might not be (though
membership in the interpretation of a class term is absolute). Let $W$ be a
universe. A _$\succ$_ -_relation (in $W$) from _a _$\succ$_ -_class $X$ to _a
_$\succ$_ -_class $Y$ _is a _$\succ$_ -class $A$ s.t. $A\subseteq X\times Y$.
A $\succ$-relation is called _small_ if it is a _$\succ$_ -set (of $W$).

Next we extend our framework by the introduction of new function symbols. This
poses a new difficulty. While new relation symbols are commonly introduced in
a static way, new function symbols are usually introduced _dynamically_ : a
new function symbol is made available after appropriate existence and
uniqueness theorems had been proved. However, one of the main guiding
principles of our framework is that its languages should be treated
exclusively in a _static_ way. Thus function symbols, too, are introduced here
only as abbreviations for definable operations on sets.161616In this paper, as
in standard mathematical textbooks, the term “function” is used both for
collections of ordered pairs and for set-theoretical operations (such as
$\cup$).  Let $W$ be a universe. (The various definitions should be taken with
respect to $W$.)

  * •

For a closed class term $\mathsf{T}$ and a term $t$ of
$\mathcal{L}_{RST}^{\\{HF\\}}$, $\lambda x\in\mathsf{T}.t$ is a _function
term_ which is an abbreviation for
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}\exists
x\exists y\left(z\check{=}\left\langle x,y\right\rangle\wedge
x\in\mathsf{T}\wedge
y=t\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.171717We
abbreviate by $z\check{=}\left\langle x,y\right\rangle$ and $\left\langle
x,y\right\rangle\check{\in}z$ the two formulas that are provably equivalent to
$z=\left\langle x,y\right\rangle$ and $\left\langle x,y\right\rangle\in z$ and
are safe w.r.t. $\left\\{x,y\right\\}$ which were introduced in [8].

  * •

A _$\succ$_ -class $F$ is a _$\succ$_ -_function on a_ _$\succ$ -class $X$_ if
there is a function term $\lambda x\in\mathsf{T}.t$ such that
$X=\left\|\mathsf{T}\right\|$, $Fv\left(t\right)\subseteq\left\\{x\right\\}$
and $F=\left\|\lambda x\in\mathsf{T}.t\right\|$. $t$ is called a term which
_represents_ $F$.

  * •

A $\succ$-class is called a $\succ$-function if it is a $\succ$-function on
some $\succ$-class.

  * •

A $\succ$-function is called _small_ if it is a _$\succ$_ -set.

Note that the standard functionality condition is always satisfied by a
_$\succ$_ -_function_.

_Terminology._ In what follows, claiming that an object is _available in
$RST_{HF}^{m}$ as a $\succ$-function ($\succ$-relation)_ means that for every
universe $W$, the object is definable in $\mathcal{L}_{RST}^{\\{HF\\}}$ as a
$\succ$-function _( $\succ$-relation)_ of $W$, and that its basic properties
are provable in $RST_{HF}^{m}$.181818The “basic properties” of a certain
object is of course a fuzzy notion. However, it is not difficult to identify
its meaning in each particular case, as will be demonstrated in several
examples below.

######  Proposition 17.

Let $X,Y$ be $\succ$-classes and $R$ a _$\succ$_ -relation from $X$ to $Y$.

  1. (1)

$R$ is small iff $Dom\left(R\right)$ and $Im\left(R\right)$ are $\succ$-sets.

  2. (2)

$R^{-1}=\left\\{\left\langle y,x\right\rangle|\left\langle x,y\right\rangle\in
R\right\\}$ is available in $RST_{HF}^{m}$ as a _$\succ$_ -relation from $Y$
to $X$. If $R$ is small, then so is $R^{-1}$.

  3. (3)

If $Z\subseteq X$ and $U\subseteq Y$ are _$\succ$_ -classes, then
$R\cap\left(Z\times U\right)$ is available in $RST_{HF}^{m}$ as a _$\succ$_
-relation from $Z$ to $U$ .

######  Proof 3.4.

  1. (1)

$(\Rightarrow)$ If $R$ is a $\succ$-set, then $\exists y.\left\langle
x,y\right\rangle\check{\in}\widetilde{R}\succ\left\\{x\right\\}$ and $\exists
x.\left\langle
x,y\right\rangle\check{\in}\widetilde{R}\succ\left\\{y\right\\}$. Thus,
$Dom\left(R\right)$ is defined by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid\exists
y.\left\langle
x,y\right\rangle\check{\in}\widetilde{R}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
and $Im\left(R\right)$ by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
x.\left\langle
x,y\right\rangle\check{\in}\widetilde{R}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
$(\Leftarrow)$ If $Dom\left(R\right)$ and $Im\left(R\right)$ are $\succ$-sets,
then $Dom\left(R\right)\times Im\left(R\right)$ is a $\succ$-set as $\times$
is a rudimentary function. Since $R$ is a $\succ$-class such that $R\subseteq
Dom\left(R\right)\times Im\left(R\right)$, Prop. 12 entails that $R$ is a
$\succ$-set.

  2. (2)

Since $R$ is a $\succ$-class, we can define
$\overline{R^{-1}}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}\exists
x\exists y\left(\left\langle x,y\right\rangle\in\bar{R}\wedge
z\check{=}\left\langle
y,x\right\rangle\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
Now, $\exists x\exists y\left(\left\langle x,y\right\rangle\in\bar{R}\wedge
z\check{=}\left\langle y,x\right\rangle\right)\succ\emptyset$, as
$z\check{=}\left\langle y,x\right\rangle\succ\left\\{x,y\right\\}$ and
$\left\langle x,y\right\rangle\in\bar{R}\succ\emptyset$. It is standard to
prove in $RST_{HF}^{m}$ properties such as $\left\langle x,y\right\rangle\in
R\leftrightarrow\left\langle y,x\right\rangle\in R^{-1}$ and
$\left(R^{-1}\right)^{-1}=R$. If $R$ is a $\succ$-set, $R^{-1}$ can be defined
by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\mid\exists
x\exists y\left(\left\langle x,y\right\rangle\in\widetilde{R}\wedge
z=\left\langle
y,x\right\rangle\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
hence $R^{-1}$ is a $\succ$-set.

  3. (3)

Surely $R\cap\left(Z\times U\right)\subseteq Z\times U.$ By Prop.16, since
$R,Z,U$ are $\succ$-classes, we have that $R\cap\left(Z\times U\right)$ is a
$\succ$-class.

######  Proposition 18.

A $\succ$-set is a function according to the standard mathematical definition
(a single-valued relation) iff it is a small $\succ$-function.

######  Proof 3.5.

Let $A$ be a $\succ$-set which is a relation that satisfies the functionality
condition. Since $A$ is a _$\succ$_ -set, there is a closed term
$\widetilde{A}$ that defines it. $A$ is a $\succ$_-_ function on the __
$\succ$-set $Dom\left(A\right)$ since the term $t=\iota y.\left\langle
x,y\right\rangle\check{\in}\widetilde{A}$ represents it (see Lemma 1). The
term $t$ is legal and it represents $A$ since $\left\langle
x,y\right\rangle\check{\in}\widetilde{A}\succ\left\\{y\right\\}$ and $A$
satisfies the functionality condition. The converse is trivial, since for
every small $\succ$-function there is a term representing it, and thus the
functionality condition clearly holds by the equality axioms of $FOL$.

_Notation_. Let $F=\left\|\lambda x\in\bar{X}.t\right\|$ be a _$\succ$_
-function. We employ standard $\beta$-reduction for $\lambda$ terms. Thus, we
write $F\left(s\right)$ for $t\left[\nicefrac{{s}}{{x}}\right]$ if $s$ is free
for $x$ in $t$. Hence $F\left(s\right)=y$ stands for
$t\left[\nicefrac{{s}}{{x}}\right]=y$, and so if $y\notin Fv\left[t\right]\cup
Fv\left[s\right]\setminus\left\\{x\right\\}$, then
$F\left(s\right)=y\succ\left\\{y\right\\}$.

######  Proposition 19 (Replacement axiom in class form).

Let $F$ be a _$\succ$_ -function on a _$\succ$_ -class $X$. Then for every
$\succ$-set $A\subseteq X$, $F\left[A\right]=\left\\{F\left(a\right)\,|\,a\in
A\right\\}$ is a _$\succ$_ -set.

######  Proof 3.6.

The term
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y\mid\exists
a\in\widetilde{A}.F\left(a\right)=y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
defines $F\left[A\right]$.

Below is a natural generalization of Def. 16 to functions of several
variables.

######  Lemma 20.

If $X_{1},...,X_{n}$ _are $\succ$_-classes and $t$ is a term s.t.
$Fv\left(t\right)\subseteq\left\\{x_{1},...,x_{n}\right\\}$, then
$F=\left\|\lambda x_{1}\in\bar{X_{1}},...,x_{n}\in\bar{X_{n}}.t\right\|$ is
available in $RST_{HF}^{m}$ as a __ $\succ$_-_ function on __
$X_{1}\times...\times X_{n}$. _(Here_ $\lambda
x_{1}\in\bar{X_{1}},...,x_{n}\in\bar{X_{n}}.t$ abbreviates
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\left\langle\left\langle
x_{1},...,x_{n}\right\rangle,t\right\rangle\hat{\,\mid\,}\left\langle
x_{1},...,x_{n}\right\rangle\in\bar{X_{1}}\times...\times\bar{X_{n}}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$_)._

######  Corollary 21.

Every $HF$-rudimentary function is available in $RST_{HF}^{m}$ as a _$\succ$_
-function.

######  Proposition 22.

Let $F$ be a _$\succ$_ -function on a _$\succ$_ -class $X$.

  1. (1)

$F$ is small iff $X$ is a _$\succ$_ -set.

  2. (2)

If $Y_{0}$ is a _$\succ$_ -class, then $F^{-1}\left[Y_{0}\right]=\left\\{a\in
X\mid F\left(a\right)\in Y_{0}\right\\}$ is a _$\succ$_ -class. If $F$ is
small, then $F^{-1}\left[Y_{0}\right]$ is a _$\succ$_ -set.

  3. (3)

If $X_{0}\subseteq X$ is a _$\succ$_ -class, then $F\upharpoonright_{X_{0}}$
is available in $RST_{HF}^{m}$ as a _$\succ$_ -function.

  4. (4)

$G\circ F$ is available in $RST_{HF}^{m}$ as a _$\succ$_ -function on $X$, in
case $G$ is a _$\succ$_ -function on a _$\succ$_ -class $Y$ and
$Im(F)\subseteq Y$.

  5. (5)

If $G$ is a _$\succ$_ -function on a _$\succ$_ -class $Y$ and $F$ and $G$
agree on $X\cap Y$, then $G\cup F$ is available in $RST_{HF}^{m}$ as a
_$\succ$_ -function on $X\cup Y$.

  6. (6)

If $Z$ is a _$\succ$_ -class then the identity on $Z$ and any constant
function on $Z$ are available in $RST_{HF}^{m}$ as _$\succ$_ -functions.

######  Proof 3.7.

  1. (1)

$(\Rightarrow)$ If $F$ is a $\succ$-set, then $Dom\left(F\right)=X$ is also a
$\succ$-set, since $Dom$ is rudimentary.
$(\Leftarrow)$ Suppose $t$ represents $F$. If $X$ is a $\succ$-set, then
$F=\left\|\lambda x\in\widetilde{X}.t\right\|$ which is a $\succ$-set.

  2. (2)

$\overline{F^{-1}\left[Y_{0}\right]}={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}a\hat{\,\mid\,}a\in\bar{X}\wedge
F\left(a\right)\in\bar{Y_{0}}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
. Since $a\in\bar{X}\wedge F\left(a\right)\in\bar{Y_{0}}\succ\emptyset$, we
get that $F^{-1}\left[Y_{0}\right]$ is a $\succ$-class. If $F$ is small, then
by (1) we have that $X$ is a $\succ$-set. The fact that
$F^{-1}\left[Y_{0}\right]\subseteq X$ entails that $F^{-1}\left[Y_{0}\right]$
is a $\succ$-set.

  3. (3)

If $t$ is a term that represents $F$, it also represents
$F\upharpoonright_{X_{0}}$.

  4. (4)

Denote by $t_{F},t_{G}$ terms that represent the $\succ$-functions $F,G$
respectively. Thus, $G\circ F=\left\|\lambda
x\in\overline{X}.t_{G}\left\\{\frac{t_{F}\left(x\right)}{x}\right\\}\right\|$.
It is easy to see that standard properties, such as the associativity of
$\circ$, are provable in $RST_{HF}^{m}$.

  5. (5)

Denote by $t_{F},t_{G}$ terms that represent the $\succ$-functions $F,G$
respectively. Then:

$F\cup G=\left\|\lambda x\in\bar{X}\cup\bar{Y}.\iota y.\left(x\in\bar{X}\wedge
y=t_{F}\right)\vee\left(x\in\bar{Y}-\bar{X}\wedge y=t_{G}\right)\right\|$

Since each of the disjuncts is safe w.r.t $\left\\{y\right\\}$, we get that
the term is valid. It is easy to verify that in $RST_{HF}^{m}$ basic
properties, such as $\forall x\in\bar{X}$.$\overline{G\cup
F}\left(x\right)=\bar{F}\left(x\right)$, are provable.

  6. (6)

$id_{Z}=\left\|\lambda z\in\bar{Z}.z\right\|$, and for any $A\in J_{2}$,
$const_{A}=\left\|\lambda z\in\bar{Z}.\tilde{A}\right\|$. Proving basic
properties such as $\forall
x,y\in\bar{Z}.const_{A}\left(x\right)=const_{A}\left(y\right)$ in
$RST_{HF}^{m}$ is routine.

##  4\. The Natural Numbers

We introduce the natural numbers by following their standard construction in
set theory: $0:=\emptyset;\,\,\,\,\,\,n+1:=S\left(n\right)$, where
$S\left(x\right)=x\cup\left\\{x\right\\}$. Obviously, each $n\in\mathbb{N}$ is
a _$\succ$_ -set in any universe, and $\mathbb{N}$ (the set of natural
numbers) is contained in $\mathcal{HF}=J_{1}$. What is more, the property of
being a natural number is defined in any universe by the following formula:

$N(x):=\ \forall y\in x\cup\\{x\\}.y=\emptyset\vee\exists w\in
x.y=w\cup{\\{}w{\\}}$

Note that this formula has the same extension in any transitive set which
includes $\emptyset$ and is closed under the operation $\lambda
x.x\cup\\{x\\}$.191919This is a significant improvement on [8], in which
another formula, $Ord\left(x\right)$, has been used for characterizing
$\mathbb{N}$ as $\\{x\mid x\in HF\wedge Ord(x)\\}$. However,
$Ord\left(x\right)$ is actually true for all ordinals, and so it lacks the
strong absoluteness property that $N(x)$ has. It follows that from a semantic
point of view it should be taken as safe with respect to $x$. However,
syntactically we have only that $N(x)\succ\emptyset$ (that is: $N(x)$ is
absolute), but not that $N(x)\succ\\{x\\}$. As a result, $\mathbb{N}$ is
available in $RST^{m}$ (and its minimal model $J_{1}$) only as a proper
$\succ$-class. In contrast, $\mathbb{N}$ is available as a $\succ$-set in
$RST_{HF}^{m}$, since it is definable in all the universes (including of
course $J_{2}$) by the term:

$\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}:=\
{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\mid x\in
HF\wedge N(x){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$

Now we show that appropriate counterparts of Peano’s axioms for $\mathbb{N}$
are provable in $RST_{HF}^{m}$. For this we need the following two lemmas.

######  Lemma 23.

$\vdash_{RST_{HF}^{m}}\forall x\in H\\!F\forall y.y\in x\rightarrow x\not\in
y$.

######  Proof 4.1.

Let $\psi:=\forall u\forall v.u\in z\wedge v\in u\rightarrow u\not\in v$. We
first show that $\vdash_{RST_{HF}^{m}}\forall z\in H\\!F\psi$. By Lemma 3(2),
it suffices to show that $\psi\left[\nicefrac{{\emptyset}}{{z}}\right]$ and
$\forall x\forall
y\left(\psi\left[\nicefrac{{x}}{{z}}\right]\wedge\psi\left[\nicefrac{{y}}{{z}}\right]\rightarrow\psi\left[\nicefrac{{x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}}}{{z}}\right]\right)$
are theorems of $RST_{HF}^{m}$. This is obvious for
$\psi\left[\nicefrac{{\emptyset}}{{z}}\right]$. To prove the other formula, we
reason in $RST_{HF}^{m}$ as follows. Assume
$\psi\left[\nicefrac{{x}}{{z}}\right]$ and
$\psi\left[\nicefrac{{y}}{{z}}\right]$. We show $\psi$ for
$z=x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
So suppose that $u\in z$ and $v\in u$. Then either $u\in x$ or $u=y$. In the
first case the assumptions $\psi\left[\nicefrac{{x}}{{z}}\right]$ and $v\in u$
implies that $u\not\in v$. In the second case $v\in y$, and so it follows from
the assumption $\psi\left[\nicefrac{{y}}{{z}}\right]$ that if $u\in v$ then
$v\not\in u$, contradicting the assumption that $v\in u$. Hence $u\not\in v$
in this case as well.

To complete the proof of the lemma, let $x\in H\\!F$. Then $\\{x\\}\in H\\!F$
as well, and so $\psi\left[\nicefrac{{\\{x\\}}}{{z}}\right]$. Since
$x\in\\{x\\}$, this implies that $\forall y.y\in x\rightarrow x\not\in y$.

######  Lemma 24.

$\vdash_{RST_{HF}^{m}}\forall x\in H\\!F\forall y.y\subseteq x\rightarrow y\in
H\\!F$.

######  Proof 4.2.

Let $\psi:=\forall u.u\subseteq z\rightarrow u\in H\\!F$. We have to show that
$\vdash_{RST_{HF}^{m}}\forall z\in H\\!F\psi$. By Lemma 3(2), it suffices to
show that $\psi\left[\nicefrac{{\emptyset}}{{z}}\right]$ and $\forall x\forall
y\left(\psi\left[\nicefrac{{x}}{{z}}\right]\wedge\psi\left[\nicefrac{{y}}{{z}}\right]\rightarrow\psi\left[\nicefrac{{x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}}}{{z}}\right]\right)$
are theorems of $RST_{HF}^{m}$. This is obvious for
$\psi\left[\nicefrac{{\emptyset}}{{z}}\right]$. To prove the other formula, we
reason in $RST_{HF}^{m}$ as follows. Assume
$\psi\left[\nicefrac{{x}}{{z}}\right]$ and
$\psi\left[\nicefrac{{y}}{{z}}\right]$. We show $\psi$ for
$z=x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
So suppose that $u\subseteq z$. Then there exists $v\subseteq x$ such that
either $u=v$ or
$u=v\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
Now the assumption that $\psi\left[\nicefrac{{x}}{{z}}\right]$ implies that
$v\in HF$, while the assumption that $\psi\left[\nicefrac{{y}}{{z}}\right]$
implies that $y\in HF$. Hence Lemma 3(1) entails that
$v\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\in
HF$. It follows that in both cases $u\in HF$.

######  Proposition 25.

  1. (1)

$\vdash_{RST_{HF}^{m}}0\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$

  2. (2)

$\vdash_{RST_{HF}^{m}}\forall x.S(x)\neq 0$

  3. (3)

$\vdash_{RST_{HF}^{m}}\forall
x.x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\leftrightarrow
S(x)\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$

  4. (4)

$\vdash_{RST_{HF}^{m}}\forall
x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\forall
y\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}.S(x)=S(y)\rightarrow x=y$

######  Proof 4.3.

The first two items, and the fact that $RST_{HF}^{m}$ proves that if
$x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$ then
$S(x)\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$, are very easy, and are left
to the reader.

To prove the other direction of (3), assume that
$S(x)\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$. We show that
$x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$. Since
$S(x)\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$, by definition $S(x)\in HF$.
Hence Lemma 24 implies that $x\in H\\!F$ as well. To show that also $N(x)$,
let $y\in x\cup\\{x\\}$, and suppose that $y\neq\emptyset$. These assumptions
about $y$, and the assumption that
$S(x)\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$, together imply that there
is $w\in S(x)$ such that $y=w\cup\\{w\\}$. It remains to show that actually
$w\in x$. This is obvious in case $y=x$, since $w\in y$ (because
$y=w\cup\\{w\\}$). If $y\in x$ then $x\not\in y$ by Lemma 25 (because $x\in
HF$), while the assumption that $y=w\cup\\{w\\}$ implies that $w\in y$. It
follows that $w\neq x$. Since $w\in S(x)$, this implies that $w\in x$ in this
case too.

Finally, to prove item (4), we show that $\vdash_{RST_{HF}^{m}}\forall x\in
HF\forall y.S(x)=S(y)\rightarrow x=y$. So suppose that $x\in HF$ and
$S(x)=S(y)$. Assume for contradiction that $x\neq y$. Since $S(x)=S(y)$, this
implies that both $x\in y$ and $y\in x$, which is impossible by Lemma 25.

The induction rule is available in $RST_{HF}^{m}$ as well, but only for
$\varphi\succ\emptyset$.

######  Proposition 26.

$\vdash_{RST_{HF}^{m}}\left(\varphi\left[\nicefrac{{0}}{{x}}\right]\wedge\forall
x\left(\varphi\rightarrow\varphi\left[\nicefrac{{S\left(x\right)}}{{x}}\right]\right)\right)\rightarrow\forall
x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}.\varphi$, for
$\varphi\succ\emptyset.$

######  Proof 4.4.

Let $\varphi\succ\emptyset$, and assume that

$(*)\ \ \varphi\left[\nicefrac{{0}}{{x}}\right]\wedge\forall
x\left(\varphi\rightarrow\varphi\left[\nicefrac{{S\left(x\right)}}{{x}}\right]\right)$

We show that $\forall x\in HF.\varphi$. Let $\psi$ be the formula
$(x\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\rightarrow\varphi)\wedge\left(\forall
z\in
x.z\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\rightarrow\varphi\left[\nicefrac{{z}}{{x}}\right]\right)$.
Since $\varphi\succ\emptyset$, also $\psi\succ\emptyset$. Hence Lemma 3(2)
implies:

$(**)\ \left(\psi\left[\nicefrac{{\emptyset}}{{x}}\right]\wedge\forall
x\forall
y\left(\psi\wedge\psi\left[\nicefrac{{y}}{{x}}\right]\rightarrow\psi\left[\nicefrac{{x\cup\;{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}}}{{x}}\right]\right)\right)\rightarrow\forall
x\in HF.\psi$

Clearly $\psi\left[\emptyset\right]$ is provable in $RST_{HF}^{m}$,202020To
make the text more readable, at the rest of the proof we write
$\psi\left[t\right]$ and $\varphi\left[t\right]$ instead of
$\psi\left[\nicefrac{{t}}{{x}}\right]$ and
$\varphi\left[\nicefrac{{t}}{{x}}\right]$ (respectively). since we have
$\varphi\left[\emptyset\right]$ by (*). Now assume
$\psi\left[x\right]\wedge\psi\left[y\right]$. We show that
$\psi\left[x\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right]$.

  1. (1)

Let $z\in
x\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
and suppose that $z\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$. Then either
$z\in x$ or $z=y$, and in both cases the assumptions $\psi\left[x\right]$,
$\psi\left[y\right]$, and $z\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$
immediately imply that $\varphi\left[z\right]$.

  2. (2)

Let
$z=x\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$,
and suppose that $z\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$. The first of
these assumptions implies that $z\neq\emptyset$, and so the second one entails
that there exists $w$ such that $z=w\cup\\{w\\}$. Then $w\in z$, and so
$w\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\rightarrow\varphi\left[w\right]$
by item (1). But $w\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$ by Proposition
25(2) and the assumption $z\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}$. It
follows that $\varphi\left[w\right]$. Therefore (*) implies that
$\varphi\left[z\right]$ in this case too.

From (1) and (2) it follows that indeed
$\psi\left[x\cup{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right]$
follows from $\psi\left[x\right]\wedge\psi\left[y\right]$. Therefore (**)
implies that $\forall x\in HF.\psi$. This, in turn, implies that $\forall x\in
HF.\varphi$.

######  Remark 27.

The restriction to absolute formulas in Proposition 26 is not a real problem
for developing the theory of natural numbers that we need. With the help of
Proposition 28 below, Proposition 26 easily implies that all the formulas in
the language of first-order Peano’s arithmetics and proofs in that theory can
be translated into $RST_{HF}^{m}$ and its language. This is because in this
translation, all the quantifications are bounded in $\mathbb{N}$, and thus
they are safe w.r.t. $\emptyset$. 212121It can be shown that the power of full
induction over $\mathbb{N}$ (i.e. for _any_ formula $\varphi$) can be achieved
by adding to $RST_{HF}^{m}$ the full $\in$-induction scheme.

Next we show that addition and multiplication on $\mathbb{N}$ are available in
$RST_{HF}^{m}$ as small $\succ$-functions. In view of Propositions 25 and 26,
this suffices (as has been shown by Gödel) for having all recursive functions
available in $RST_{HF}^{m}$ as small $\succ$-functions.222222Using the method
given in the proof of Proposition 28 below, it is also not difficult to
directly show that every primitive recursive function is available in
$RST_{HF}^{m}$ as a small $\succ$-function. 232323In [8] it was essentially
shown (using a different terminology) that every primitive recursive function
is available as a small $\succ$-function in the extension of $RST_{HF}^{m}$
with $\in$-induction. Our present results show that $\in$-induction is not
really needed for this.

######  Proposition 28.

  1. (1)

The standard ordering $<$ on $\mathbb{N}$ is available in $RST_{HF}^{m}$ as a
small $\succ$-relation.

  2. (2)

The standard addition and multiplication of natural numbers are available in
$RST_{HF}^{m}$ as small $\succ$-functions.

######  Proof 4.5.

  1. (1)

The standard ordering $<$ on $\mathbb{N}$ coincides with $\in$. Thus it is
definable by the term
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\left\langle
m,n\right\rangle\check{\in}\widetilde{\mathbb{N}\times\mathbb{N}}\mid m\in
n{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$. Since
$\mathbb{N}$ is a $\succ$-set, so is $\mathbb{N}\times\mathbb{N}$. Hence the
fact that $m\in n\succ\emptyset$ and Prop. 14 imply that $<$ is a __
$\succ$-set. It is now straightforward to prove in $RST_{HF}^{m}$ its two
characteristic properties: $\forall x.x\not<0$ and $\forall x\forall
y.x<S(y)\leftrightarrow x<y\vee x=y$. Using Proposition 26, this suffices (as
is well-known) for deriving all the basic properties of <, like its being a
linear order or the existence of a <-successor for each element in
$\mathbb{N}$.

  2. (2)

Define:

     * •

$Func\left(f\right):=\ \forall a,b,c\left(\left\langle
a,b\right\rangle\check{\in}f\wedge\left\langle
a,c\right\rangle\check{\in}f\rightarrow b=c\right)$

     * •

$add\left(z,u,n,f\right):=\ \left(z=0\wedge u=n\right)\vee\exists
z_{1},u_{1}\in\widetilde{\mathbb{N}}\left(\left\langle
z_{1},u_{1}\right\rangle\check{\in}f\wedge z=S\left(z_{1}\right)\wedge
u=S\left(u_{1}\right)\right)$.

     * •

$\psi_{+}(n,k,f):=Func\left(f\right)\wedge\forall x\left(x\in
f\leftrightarrow\exists z,u\in\mbox{$\mathbb{\widetilde{N}}$}\left(z\leq
k\wedge x=\left\langle z,u\right\rangle\wedge
add\left(z,u,n,f\right)\right)\right)$

Intuitively, $\psi_{+}(n,k.f)$ says that $f$ stands for $\left\\{\left\langle
0,n\right\rangle,\left\langle 1,n+1\right\rangle,\left\langle
2,n+2\right\rangle,...,\left\langle k,n+k\right\rangle\right\\}$. It is easy
to check that $\psi_{+}(n,f)\succ\emptyset$. Hence (Lemma 1) addition is
definable by:

$+:=\lambda
n\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}},k\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}.\iota
m.\exists f\in HF\left(\psi_{+}(n,k,f)\wedge\left\langle
k,m\right\rangle\check{\in}f\right).$

$+$ is a valid term since $f\in HF\succ\left\\{f\right\\}$ and $\left\langle
k,m\right\rangle\check{\in}f\wedge\psi_{+}(n,f)\succ\left\\{m\right\\}$, and
it is a small $\succ$-function, as $\mathbb{N}\times\mathbb{N}$ is a
$\succ$-set.

Multiplication is defined similarly. The only difference is that
$add\left(z,u,n,f\right)$ is replaced with $\left(z=0\wedge
u=0\right)\vee\exists
z_{1},u_{1}\in\mathbb{\mbox{$\mathbb{\widetilde{N}}$}}\left(\left\langle
z_{1},u_{1}\right\rangle\check{\in}f\wedge z=S\left(z_{1}\right)\wedge
u=n+u_{1}\right).$ This is legitimate, since $+$ is a small $\succ$-function.

It is not difficult now to prove in $RST_{HF}^{m}$ the fundamental properties
that characterize addition and multiplication in first-order Peano’s
arithmetics:

$\displaystyle\forall x.x+0=x$ $\displaystyle\,\,\,\mathrm{and}\,\,\,$
$\displaystyle\forall x,y.x+S\left(y\right)=S\left(x+y\right)$
$\displaystyle\forall x.x\cdot 0=0$ $\displaystyle\,\,\,\mathrm{and}\,\,\,$
$\displaystyle\forall x,y.x\cdot S\left(y\right)=x+\left(x\cdot y\right)$

Once these properties are proved, it is a standard matter to use Prop. 26 for
proving all the standard properties of addition and multiplication, such as
commutativity, associativity, and distributivity.

##  5\. Real Analysis in $J_{2}$

In this section we turn at last to the main goal of this paper: developing
real analysis in $J_{2}$. Now it is not difficult to formalize the
definitions, claims, and proofs of this section in our formal framework.__
These translations are straightforward, but rather tedious. Hence we shall
omit them, with the exception of a few outlined examples.

_Notation and Terminology_. Henceforth we restrict our attention to the
computational theory $RST_{HF}^{m}$ and its computational universe $J_{2}$.
Therefore we simply write $\left\|exp\right\|_{v}$ instead of
$\left\|exp\right\|_{v}^{J_{2}}$. Similarly, when we talk about a $\succ$-set
or a $\succ$-class, we mean $\succ$-set/$\succ$-class in $J_{2}$.

###  5.1. The Construction of the Real Line

The standard construction of $\mathbb{Z}$, the set of integers, as the set of
ordered pairs
$\left(\mathbb{N}\times\left\\{0\right\\}\right)\cup\left(\left\\{0\right\\}\times\mathbb{N}\right)$
can be easily carried out in $RST_{HF}^{m}$, as can the usual construction of
$\mathbb{Q}$, the set of rationals, in terms of ordered pairs of relatively
prime integers. There is also no difficulty in defining the standard orderings
on $\mathbb{Z}$ and $\mathbb{Q}$ as small $\succ$-relations, as well as the
standard functions of addition and multiplication as small $\succ$-functions.
The main properties of addition and multiplication are provable in
$RST_{HF}^{m}$, as the standard proofs by induction can be carried out within
it. Furthermore, all the basic properties of $\mathbb{Z}$ and $\mathbb{Q}$
(such as $\mathbb{Q}$ being a dense unbounded field) are straightforwardly
proved in $RST_{HF}^{m}$.

Now we turn to the standard construction of the real line using Dedekind cuts.
Since it is well known that the real line and its open segments are not
absolute, they cannot be $\succ$-sets. Thus the collection of real numbers in
$RST_{HF}^{m}$ will not be a term but merely a _definable predicate._ , that
is: a $\succ$-class.242424As noted in Footnote 4, this is in sharp difference
from the development of real analysis in [8].

Let $\psi:=\forall x,y\in\widetilde{\mathbb{Q}}.x\in u\wedge y<x\rightarrow
y\in u$, $\ \ \ \varphi:=\neg\exists x\in u\forall y\in u.y\leq x$. [The
Reals] $\mathbb{R}$ is
$\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}u\in\overline{P_{J_{2}}\left(\mathbb{Q}\right)\setminus\left\\{\emptyset,\mathbb{Q}\right\\}}\hat{\,\mid\,}\psi\wedge\varphi{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|$.
The above term is a valid class term as
$P_{J_{2}}\left(\mathbb{Q}\right)\setminus\left\\{\emptyset,\mathbb{Q}\right\\}$
is a $\succ$-class, and $\varphi,\psi\succ\emptyset$. Note that it does not
denote the “real” real-line (if such a thing really exists). However, it does
contain all _computable_ real numbers, such as $\sqrt{2}$ and $\pi$. (This can
be shown by the same method that was used in [8].)

_Notation_. We employ the following notations:
$\mathbb{Q}^{+}=\left\\{q\in\mathbb{Q}\mid 0<q\right\\}$,
$\mathbb{R}^{+}=\left\\{r\in\mathbb{R}\mid 0<r\right\\}$,
$\left(a,b\right)=\left\\{r\in\mathbb{R}\mid a<r<b\right\\}$ and
$\left[a,b\right]=\left\\{r\in\mathbb{R}\mid a\leq r\leq b\right\\}$, for
$a,b$ real numbers. 252525Notice that $\mathbb{Q}^{+}$ is a $\succ$-set and
$\mathbb{R}^{+}$ is a $\succ$-class.

######  Proposition 29.

The following holds:

  1. (1)

The standard ordering $<$ on $\mathbb{R}$ is available in $RST_{HF}^{m}$ as a
_$\succ$_ -relation.

  2. (2)

The standard addition and multiplication of reals are available in
$RST_{HF}^{m}$ as $\succ$-functions.

######  Proof 5.1.

  1. (1)

The relation $<$ on $\mathbb{R}$ coincides with $\subset$, thus we can define
the relation $<$ by
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\left\langle
x,y\right\rangle\in\overline{\mathbb{R}\times\mathbb{R}}\hat{\,\mid\,}x\subset
y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$. We have
that $x\subset y\succ\emptyset$, hence $<$ is a _$\succ$_ -class. It is
straightforward to prove in $RST_{HF}^{m}$ properties concerning $<$, such as
it being a total order on $\mathbb{R}$, the density of the rationals in
$\mathbb{R}$, the Archimedean Principle, etc.

  2. (2)

The $\succ$-function $+$ can be represented (using Lemma 20) by the term

$+=\lambda
x\in\mathbb{\bar{R}},y\in\bar{\mathbb{R}}.{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\mid\exists
u\in x\exists v\in
y.z=u+v{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$

since $\exists u\in x\exists v\in y.z=u+v\succ\left\\{z\right\\}$.

To define multiplication, let $F_{1}$ be the _$\succ$_ -function:

$F_{1}=\left\|\lambda
a\in\bar{\mathbb{R}^{+}},b\in\bar{\mathbb{R}^{+}}.{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\mid
z\leq 0\vee\exists u\in a\exists v\in b\left(0\leq u\wedge 0\leq v\wedge
z=u\cdot
v\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|$

Next, define the _$\succ$_ -function $-$ on $\mathbb{R}$ by

$-=\left\|\lambda
x\in\bar{\mathbb{R}}.{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}z\hat{\,\mid\,}\exists
u\in\widetilde{\mathbb{Q\setminus}x}\exists
a\in\widetilde{\mathbb{Q}}.z+b=a{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|.$

Then, for $0\leq a\wedge b<0$ define $F_{2}\left(\left\langle
a,b\right\rangle\right):=-F_{1}\left(\left\langle a,-b\right\rangle\right)$,
for $a<0\wedge 0\leq b$ define $F_{3}\left(\left\langle
a,b\right\rangle\right):=-F_{1}\left(\left\langle-a,b\right\rangle\right)$,
and for $a<0\wedge b<0$ define $F_{4}\left(\left\langle
a,b\right\rangle\right):=F_{1}\left(\left\langle-a,-b\right\rangle\right)$.
Now the $\succ$-function $\cdot$ on $\mathbb{R}\times\mathbb{R}$ can be
defined by $\cdot:=F_{1}\cup F_{2}\cup F_{3}\cup F_{4}$.
Proving in $RST_{HF}^{m}$ basic properties regarding these $\succ$-functions,
such as $\mathbb{R}$ being an ordered field, is again straightforward.

###  5.2. The Least Upper Bound Principle and the Topology of the Reals

In this section we examine to what extent the least upper bound principle is
available in $RST_{HF}^{m}$. We start with the following positive result:

######  Theorem 30.

It is provable in $RST_{HF}^{m}$ that every nonempty $\succ$-subset of
$\mathbb{R}$ that is bounded above has a least upper bound in $\mathbb{R}$.
Furthermore, the induced mapping ($l.u.b$) is available in $RST_{HF}^{m}$ as a
$\succ$-function.

######  Proof 5.2.

Let $X$ be a nonempty $\succ$-subset of $\mathbb{R}$ that is bounded above.
$\cup X$ is a $\succ$-set, and since $X$ is bounded above, standard arguments
show that $\cup X$ is a Dedekind cut and thus belongs to $\mathbb{R}$. Since
the order $\succ$-relation $\leq$ coincides with the inclusion relation, it
follows that $\cup X$ is a least upper bound for $X$. Moreover, the function
that maps each $X$ to $\cup X$ is a rudimentary function (from
$P_{J_{2}}\left(\mathbb{R}\right)$ to $P_{J_{2}}\left(\mathbb{Q}\right)$), and
hence it is a $\succ$-function. Denote it by $F$. The desired function $l.u.b$
is $F\upharpoonright_{F^{-1}\left[\mathbb{R}\right]}$, which by Proposition 22
is a $\succ$-function.

Encouraging as it may be, Theorem 30 only states that _$\succ$ -subsets_ of
$\mathbb{R}$ have the least upper bound property. Therefore it is insufficient
for developing in $RST_{HF}^{m}$ most of standard mathematics. The reason is
that even the most basic substructures of $\mathbb{R}$, like the intervals,
are not $\succ$-sets in $RST_{HF}^{m}$, but only proper $\succ$-classes.
Hence, a stronger version of the theorem, which ensures that the least upper
bound property holds for standard $\succ$-subclasses of $\mathbb{R}$, is
needed. Theorem 37 below provides such an extension, but it requires some
additional definitions and propositions.262626It should be noted that the full
least upper bound principle has not been derivable also in Weyl’s approach
[47]. To obtain the principle for standard mathematical objects, we use in
what follows coding techniques that are similar to those employed by Weyl.

First we consider $\succ$-classes $U\subseteq\mathbb{R}$ which are open _._
These $\succ$-classes are generally not $\succ$-sets (unless empty), since
they contain an interval of positive length, which is a proper $\succ$-class
and thus cannot be contained in a $\succ$-set (see Prop. 12(3)). Clearly,
there is no such thing as a $\succ$-set of $\succ$-classes, as a proper
$\succ$-class can never be an element of another $\succ$-set or $\succ$-class.
However, the use of coding (following [45], [46]272727In [46] such codings are
called “proxies”.) allows us, for example, to replace the meaningless
statement “the union of a $\succ$-set of $\succ$-classes is a $\succ$-class”
with “given a $\succ$-set of codes for $\succ$-classes, the union of the
corresponding $\succ$-classes is a $\succ$-class”.

The coding technique we use is based on the standard mathematical notation for
a “family of sets”, $\left(A_{i}\right)_{i\in I}$, where $I$ is a set of
indices and $A_{i}$ is a set for each $i\in I$. In $RST_{HF}^{m}$ we cannot
construct the collection of all such $A_{i}$’s if $A_{i}$ is a $\succ$-class
for some $i\in I$. Thus, we treat the $\succ$-set $I$ as a code for the
“family of classes” $\left(A_{i}\right)_{i\in I}$. In fact, we mainly use the
union of such families, i.e., $\underset{i\in I}{\bigcup A_{i}}$.

For $p,q\in\mathbb{R}$, the open ball $B_{q}\left(p\right)$ is the
$\succ$-class $\left\\{r\in\mathbb{R}\mid\left|r-p\right|<q\right\\}$. Let
$U\subseteq\mathbb{R}$ be a $\succ$-class. If there exists a $\succ$-set
$u\subseteq\mathbb{Q}\times\mathbb{Q}^{+}$ such that $U=\bigcup_{\left\langle
p,q\right\rangle\in u}B_{q}\left(p\right)=\left\\{r\in\mathbb{R}\mid\exists
p,q\left(\left\langle p,q\right\rangle\in
u\wedge\left|r-p\right|<q\right)\right\\}$, then $U$ is called _open_ and $u$
is a _code_ for $U$. In what follows, the formalizations in $RST_{HF}^{m}$ are
carried out as follows:

  * •

To quantify over open $\succ$-classes:
$Qu\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}$
($Q\in\left\\{\forall,\exists\right\\}$).

  * •

To decode the open $\succ$-class whose code is $u$:

$dec\left(u\right):={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}r\in\bar{\mathbb{R}}\hat{\,\mid\,}\exists
p,q\left(\left\langle
p,q\right\rangle\check{\in}u\wedge\left|r-p\right|<q\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$

  * •

To state that a class variable $\boldsymbol{U}$ is an open $\succ$-class:

$Open\left(\boldsymbol{U}\right):=\exists
u\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}.\boldsymbol{U}=dec\left(u\right)$

######  Proposition 31.

The following are provable in $RST_{HF}^{m}$:

  1. (1)

For any $\succ$-set $u\subseteq\mathbb{R}\times\mathbb{R}^{+}$,
$\left\\{r\in\mathbb{R}\mid\exists p,q\left(\left\langle p,q\right\rangle\in
u\wedge\left|r-p\right|<q\right)\right\\}$ is an open $\succ$-class.

  2. (2)

The open ball $B_{q}\left(p\right)$ is an open $\succ$-class for any
$p\in\mathbb{R}$ and $q\in\mathbb{R}^{+}$.

######  Proof 5.3.

  1. (1)

Take $w$ to be
$\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\left\langle
p,q\right\rangle\in\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}\mid\exists
r,s\left(\left\langle r,s\right\rangle\check{\in}u\wedge
q+\left|r-p\right|\leq
s\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|$.
Since $\mathbb{Q}\times\mathbb{Q}^{+}$ is a $\succ$-set and $\exists
r,s\left(\left\langle r,s\right\rangle\check{\in}u\wedge
q+\left|r-p\right|\leq s\right)\succ\emptyset$, $w$ is a $\succ$-set that is a
code for an open $\succ$-class. It can easily be proved in $RST_{HF}^{m}$ that
$w$ codes $U$.

  2. (2)

$u=\left\\{\left\langle p,q\right\rangle\right\\}$ is a code of
$B_{q}\left(p\right)$ (by 1.).

######  Proposition 32.

The following are provable in $RST_{HF}^{m}$:

  1. (1)

The union of a $\succ$-set of open $\succ$-classes is an open $\succ$-class.
i.e, given a $\succ$-set of codes of open $\succ$-classes, the union of the
corresponding open $\succ$-classes is an open $\succ$-class.

  2. (2)

The intersection of finitely many open $\succ$-classes is an open
$\succ$-class.

######  Proof 5.4.

  1. (1)

Let $X$ be a $\succ$-set of codes for open $\succ$-classes. Thus, $\cup X$ is
a code for the union of the corresponding open $\succ$-classes.

  2. (2)

If $U$ and $V$ are open $\succ$-classes, a code for their intersection is
obtained by intersecting every ball in a code for $U$ with every ball in a
code for $V$.

######  Remark 33.

_In general,_ when we say that a theorem about a $\succ$-class or a
$\succ$-function is provable in $RST_{HF}^{m}$ (as in Prop. 32) we mean that
it can be formalized and proved as a scheme, that is: its proof can be carried
out in $RST_{HF}^{m}$ using a uniform scheme. However, propositions about open
$\succ$-classes form an exception, because due to the coding machinery, they
can be fully formalized and proved in $RST_{HF}^{m}$.

As an example of the use of the coding technique, we demonstrate the
formalization of Prop. 32(1):

$\displaystyle\forall z.(\forall x\in
z.x\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}})\rightarrow\exists
w\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}.dec\left(w\right)={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}r\hat{\,\mid\,}\exists
x\in z.r\in
dec\left(x\right){\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$

A $\succ$-class $X\subseteq\mathbb{R}$ is _closed_ if $\mathbb{R}-X$ is open.

######  Lemma 34.

It is provable in $RST_{HF}^{m}$ that if $U\subseteq\mathbb{R}$ is an open
$\succ$-class, then for every $x\in U$ there is an open ball about $x$ which
is contained in $U$.

######  Proof 5.5.

If $x\in U$, then there is some $\left\langle p,q\right\rangle$ in the code of
$U$ such that $x\in B_{q}\left(p\right)$. Take $\varepsilon=\left|p-x\right|$.
It is straightforward to see that $B_{\varepsilon}\left(x\right)\subseteq
B_{q}\left(p\right)\subseteq U$.

The proof of the next Lemma is trivial.

######  Lemma 35.

Let $X\subseteq\mathbb{R}$ be a $\succ$-class and $A\subseteq X$ be a
$\succ$-set. The following are equivalent in $RST_{HF}^{m}$:

  1. (1)

Every open ball about a point in $X$ intersects $A$.

  2. (2)

Every open $\succ$-class that intersects $X$ also intersects $A$.

As an example of a full formalization which uses class variables, the
formalization of the Lemma above is:

$\displaystyle\phi:=\boldsymbol{X}\subseteq\bar{\mathbb{R}}\rightarrow\forall
a\subseteq\boldsymbol{X}\left(\forall
x\in\boldsymbol{X}\forall\varepsilon\in\bar{\mathbb{R}^{+}}\left(B_{\varepsilon}\left(x\right)\cap
a\neq\emptyset\right)\leftrightarrow\right.$ $\displaystyle\left.\forall
u\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}\left(dec\left(u\right)\cap\boldsymbol{X}\neq\emptyset\rightarrow
dec\left(u\right)\cap a\neq\emptyset\right)\right)$

We now demonstrate how to obtain an equivalent schema in the basic
$\mathcal{L}_{RST}^{\\{HF\\}}$ by replacing each appearance of a class term or
a variable with the formula it stands for. First, we explain the translation
of $x\in\bar{\mathbb{R}}$ to $\mathcal{L}_{RST}^{\\{HF\\}}$ . One iteration of
the translation entails
$x\in\overline{P_{J_{2}}\left(\mathbb{Q}\right)\setminus\left\\{\emptyset,\mathbb{Q}\right\\}}\wedge\varphi\left(x\right)\wedge\psi\left(x\right)$
for $\varphi,\psi$ as in Def. 5.1. A second iteration yields
$R\left(x\right):=x\subseteq\tilde{\mathbb{Q}}\wedge
x\neq\tilde{\mathbb{Q}}\wedge
x\neq\emptyset\wedge\varphi\left(x\right)\wedge\psi\left(x\right)$ which is in
$\mathcal{L}_{RST}^{\\{HF\\}}$. For the translation of $\phi$, first
substitute
${\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\hat{\,\mid\,}\theta{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$
for $\boldsymbol{X}$, where $\theta\succ\emptyset$. Proceeding with the
translation steps results in the following formula (scheme) of
$\mathcal{L}_{RST}^{\\{HF\\}}$, for $\theta\succ\emptyset$:

$\displaystyle{\normalcolor\forall b\left(\theta\left(b\right)\rightarrow
R\left(b\right)\right)\rightarrow\forall a\left(\left(\forall z.z\in
a\rightarrow\theta\left(z\right)\right)\rightarrow\forall
x\left(\theta\left(x\right)\rightarrow\forall\varepsilon\left(\left(R\left(\varepsilon\right)\wedge
0<\varepsilon\right)\rightarrow\right.\right.\right.}$
$\displaystyle{\normalcolor\exists w.\left|w-x\right|<\varepsilon\wedge w\in
a\leftrightarrow\forall
u\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}\left(\exists
w.R\left(w\right)\wedge\exists p,q\left(\left\langle
p,q\right\rangle\check{\in}u\wedge\left|w-p\right|<q\right)\wedge\right.}$
$\displaystyle{\normalcolor\left.\left.\theta\left(w\right)\right)\rightarrow\exists
w.R\left(w\right)\wedge\exists p,q\left(\left\langle
p,q\right\rangle\check{\in}u\wedge\left|w-p\right|<q\right)\wedge w\in
a\right)}$

Let $X\subseteq\mathbb{R}$ be a $\succ$-class, and $A\subseteq X$ a
$\succ$-set. $A$ is called _dense in $X$ _if one of the conditions of Lemma 35
holds. $X$ is called _separable_ if it contains a dense $\succ$-subset.

######  Proposition 36.

It is provable in $RST_{HF}^{m}$ that an open $\succ$-subclass of a separable
$\succ$-class is separable.

######  Proof 5.6.

Let $X$ be an open $\succ$-subclass of the separable $\succ$-class $S$, and
let $D$ be the dense $\succ$-subset in $S$. Let $B$ be an open ball with
center $x\in X$. By Lemma 34 there is a ball $B^{\prime}$ about $x$ s.t.
$B^{\prime}\subseteq B\cap X$. Since $D$ is dense in $S$, $B^{\prime}\cap
D\neq\emptyset$. Hence, $B\cap D\cap X\neq\emptyset$, and so $D\cap X$ is
dense in $X$.

Now we can finally turn to prove a more encompassing least upper bound
theorem.

######  Theorem 37.

It is provable in $RST_{HF}^{m}$ that every nonempty separable
$\succ$-subclass of $\mathbb{R}$ that is bounded above has a least upper bound
in $\mathbb{R}$.

######  Proof 5.7.

Let $X$ be a nonempty separable $\succ$-subclass of $\mathbb{R}$ that is
bounded above, and let $A$ be a dense $\succ$-subset in $X$. By Theorem 30,
$A$ has a least upper bound, denote it $m$. Suppose $m$ is not an upper bound
of $X$, i.e. there exists $x\in X-A$ s.t. $x>m$. Take
$\varepsilon_{m}=\left|x-m\right|$. Then, there is no $a\in A$ s.t. $a\in
A\cap\left(x-\varepsilon_{m},x+\varepsilon_{m}\right)$, which contradicts $A$
being dense in $X$. That $m$ is the least upper bound of $X$ is immediate.

To demonstrate the formalization in $\mathcal{L}_{RST}^{\\{HF\\}}$ of the last
theorem, denote by $separ\left(\boldsymbol{U}\right)$ the formula $\exists
d.d\subseteq\boldsymbol{U}\wedge\forall
x\in\boldsymbol{U}\forall\varepsilon\in\bar{\mathbb{R}^{+}}B_{\varepsilon}\left(x\right)\cap\boldsymbol{U}\neq\emptyset$,
and by $bound_{\boldsymbol{U}}\left(w\right)$ the formula $\forall
x\in\boldsymbol{U}.x\leq w$. Now, the full formalization is:

$\displaystyle\left(\boldsymbol{U}\subseteq\mathbb{R}\wedge\boldsymbol{U}\neq\emptyset\wedge
separ\left(\boldsymbol{U}\right)\wedge\exists
w\in\bar{\mathbb{R}}.bound{}_{\boldsymbol{U}}\left(w\right)\right)\rightarrow$
$\displaystyle\exists
v\in\bar{\mathbb{R}}\left(bound_{\boldsymbol{U}}\left(v\right)\wedge\forall
w\in\bar{\mathbb{R}}\left(bound_{\boldsymbol{U}}\left(w\right)\rightarrow
v\leq w\right)\right)$

A $\succ$-class $X\subseteq\mathbb{R}$ is called an _interval_ if __ for any
$a,b\in X$ s.t. $a<b$: if $c\in\mathbb{R}\wedge a<c<b$ then $c\in X$.

######  Proposition 38.

It is provable in $RST_{HF}^{m}$ that any non-degenerate interval is
separable.

######  Proof 5.8.

Let $X$ be a non-degenerate interval. Take $A$ to be $X\cap\mathbb{Q}$. By
Prop. 12(2) $A$ is a $\succ$-set. A standard argument shows that in every open
ball about a point in $X$ there is a rational number, and thus it intersects
$A$.

######  Corollary 39.

It is provable in $RST_{HF}^{m}$ that any non-degenerate interval that is
bounded above has a least upper bound.

A $\succ$-class $X\subseteq\mathbb{R}$ is called _connected_ if there are no
open $\succ$-classes $U$ and $V$ such that $X\subseteq U\cup V$, $U\cap
V\neq\emptyset$, $X\cap U\neq\emptyset$ and $X\cap V\neq\emptyset$. The
formalization of the above definition can be given by:

$\displaystyle connected\left(\boldsymbol{X}\right):=\neg\exists
u,v\subseteq\widetilde{\mathbb{Q}\times\mathbb{Q}^{+}}\left(\boldsymbol{X}\subseteq
decode\left(u\right)\cup decode\left(v\right)\wedge\right.$
$\displaystyle\left.decode\left(u\right)\cap
decode\left(v\right)\neq\emptyset\wedge\boldsymbol{X}\cap
decode\left(u\right)\neq\emptyset\wedge\boldsymbol{X}\cap
decode\left(v\right)\neq\emptyset\right)$

######  Proposition 40.

Let $X\subseteq\mathbb{R}$ be a $\succ$-class. It is provable in
$RST_{HF}^{m}$ that $X$ is connected if and only if it is an interval.

######  Proof 5.9.

Assume that there are open $\succ$-classes $U$ and $V$ such that $X\subseteq
U\cup V$, $U\cap V\neq\emptyset$, $X\cap U\neq\emptyset$, and $X\cap
V\neq\emptyset$ (recall that the formalization of the existence of open
$\succ$-classes is done using their codes). Choose $u\in U$ and $v\in V$ and
assume that $u<v$. Let $U_{0}=U\cap\left\\{z\in\mathbb{R}\mid z<v\right\\}$
and $V_{0}=V\cap\left\\{z\in\mathbb{R}\mid z>u\right\\}$. Prop. 32 and Prop.
36 entail that $U_{0}$ and $V_{0}$ are open, separable $\succ$-subclass of
$\mathbb{R}$. Standard arguments show that they are non-empty and bounded
above. Thus, by Theorem 37, $U_{0}$ and $V_{0}$ have least upper bounds.
Following the standard proof found in ordinary textbooks we can deduce that
the least upper bounds are elements in $\left[u,v\right]$, but not elements of
$U_{0}$ or of $V_{0}$, which is a contradiction, since
$\left[u,v\right]\subseteq U_{0}\cup V_{0}$. The classical proof of the
converse direction can easily be carried out in $RST_{HF}^{m}$.

###  5.3. Real Functions

Let $X$ be a $\succ$-class. A $\succ$-_sequence_ in $X$ is a $\succ$-function
on $\mathbb{N}$ whose image is contained in $X$.

######  Lemma 41.

It is provable in $RST_{HF}^{m}$ that Cauchy $\succ$-sequences in $\mathbb{R}$
converge to limits in $\mathbb{R}$. The induced map ($lim$) is available in
$RST_{HF}^{m}$ as a $\succ$-function.

######  Proof 5.10.

Let $a$ be a Cauchy $\succ$-sequence, and let $a_{k}$ abbreviate
$a\left(k\right)$. For $n\in\mathbb{N}$ define $v_{n}:=\bigcap_{k\geq
n}a_{k}$. The $l.u.b$ of $\lambda n.v_{n}$ equals the limit of $\lambda
n.a_{n}$. Thus, $lim\,\lambda
n.a_{n}:=\underset{}{\bigcup}{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}v_{n}\mid
n\in\widetilde{\mathbb{N}}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}.$

######  Proposition 42.

It is provable in $RST_{HF}^{m}$ that if $X\subseteq\mathbb{R}$ is closed,
then every Cauchy $\succ$-sequence in $X$ converges to a limit in $X$.

######  Proof 5.11.

Let $a$ be a Cauchy $\succ$-sequence in $X$, and let $a_{k}$ abbreviate
$a\left(k\right)$. By Lemma 41, $lim\,\lambda n.a_{n}$ is an element in
$\mathbb{R}$, denote it by $l$. Assume by contradiction that
$l\in\mathbb{R}-X$. Since $X$ is closed, $\mathbb{R}-X$ is open, and thus
there exists $\varepsilon>0$ such that
$B_{\varepsilon}\left(l\right)\subseteq\mathbb{R}-X$. From this follows that
for every $a_{k}$, $a_{k}\notin B_{\varepsilon}\left(l\right)$, which
contradicts the fact that $lim\,\lambda n.a_{n}=l$.

Next we want to study sequences of functions, but Def. 5.3 cannot be applied
as is, since $\succ$-functions which are proper $\succ$-classes cannot be
values of a $\succ$-function (in particular, of a _$\succ$ -_sequence).
Instead, we use the standard Un-currying procedure. For $X,Y$ $\succ$-classes,
a $\succ$-_sequence of_ $\succ$-_functions_ on $X$ whose image is contained in
$Y$ is a $\succ$-function on $\mathbb{N}\times X$ with image contained in $Y$.

######  Proposition 43.

Any point-wise limit of a $\succ$-sequence of $\succ$-functions on a
$\succ$-class $X\subseteq\mathbb{R}$ whose image is contained in $\mathbb{R}$
is available in $RST_{HF}^{m}$ as a $\succ$-function.

######  Proof 5.12.

Let $F$ be a $\succ$-sequence of $\succ$-functions on $X$ whose image is
contained in $\mathbb{R}$. Suppose that for each $a\in X$ the $\succ$-sequence
$\lambda n.F\left(n,a\right)$ is converging, and so it is Cauchy. Define:
$G_{a}:={\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}\left\langle
n,\bar{F}\left(n,a\right)\right\rangle\mid
n\in\widetilde{\mathbb{N}}{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}$.
Then, $\left\|\lambda a\in\bar{X}.limG_{a}\right\|$ is the desired
$\succ$-function.

Next we turn to continuous real $\succ$-functions. One possibility of doing
so, adopted e.g., in [45, 47], is to introduce codes for continuous real
$\succ$-functions (similar to the use of codes for open $\succ$-classes). This
is of course possible as such $\succ$-functions are determined by their values
on the $\succ$-set $\mathbb{Q}$. However, we prefer to present here another
approach, which allows for almost direct translations of proofs in standard
analysis textbook into our system. This is done using free function variables.
Accordingly, the theorems which follow are schemes. Implicitly, the previous
sections of this paper can also be read and understood as done in this manner.
Therefore, in what follows we freely use results from them. Let
$X\subseteq\mathbb{R}$ be a $\succ$-class and let $F$ be a $\succ$-function on
$X$ whose image is contained in $\mathbb{R}$. $F$ is called a _continuous real
$\succ$-function _if:

$\forall a\in
X\forall\varepsilon\in\mathbb{R}^{+}\exists\delta\in\mathbb{R}^{+}\forall x\in
X.\left|x-a\right|<\delta\rightarrow\left|F\left(x\right)-F\left(a\right)\right|<\varepsilon$

######  Proposition 44.

Let $X\subseteq\mathbb{R}$ be a $\succ$-class and $F$ be a $\succ$-function on
$X$ whose image is contained in $\mathbb{R}$. It is provable in $RST_{HF}^{m}$
that if for every open $\succ$-class $B\subseteq\mathbb{R}$, there is an open
$\succ$-class $A$ s.t. $F^{-1}\left[B\right]=A\cap X$, then $F$ is continuous.

######  Proof 5.13.

Let $a\in X$, $\varepsilon>0$, and
$V=B_{\varepsilon}\left(F\left(a\right)\right)$. Since $V$ is an open
$\succ$-class, there is an open $\succ$-class $A$ s.t.
$F^{-1}\left[V\right]=A\cap X$ (which is a $\succ$-class by Prop. 22(3)).
Also, $F\left(a\right)\in V$ which entails $a\in F^{-1}\left[V\right]$, and
thus $a\in A$. Since $A$ is open there exists $\delta_{a}$ s.t.
$B_{\delta_{a}}\left(a\right)\subseteq A$. Take $\delta=\delta_{a}$. For any
$x\in X$, if $\left|x-a\right|<\delta_{a}$ then $x\in
B_{\delta_{a}}\left(a\right)\subseteq A$. Hence $x\in A\cap
X=F^{-1}\left[V\right]$, and therefore $F\left(x\right)\in
V=B_{\varepsilon}\left(F\left(a\right)\right)$, i.e.
$\left|F\left(x\right)-F\left(a\right)\right|<\varepsilon$.

######  Lemma 45.

The following are provable in $RST_{HF}^{m}$:

  1. (1)

The composition, sum and product of two continuous real $\succ$-functions is a
continuous real $\succ$-function.

  2. (2)

The uniform limit of a $\succ$-sequence of continuous real $\succ$-functions
is a continuous real $\succ$-function.

######  Proof 5.14.

The standard proofs of these claims can be easily carried out in
$RST_{HF}^{m}$. Note that they require the triangle inequality which is
provable in $RST_{HF}^{m}$.

Next we prove, as examples, the Intermediate Value Theorem and the Extreme
Value Theorem, which are two key properties of continuous real functions.

######  Theorem 46 (Intermediate Value Theorem).

Let $F$ be a continuous real $\succ$-function on an interval
$\left[a,b\right]$ with $F\left(a\right)<F\left(b\right)$. It is provable in
$RST_{HF}^{m}$ that for any $d\in\mathbb{R}$ s.t.
$F\left(a\right)<d<F\left(b\right)$, there is $c\in\left[a,b\right]$ s.t.
$F\left(c\right)=d$.

######  Proof 5.15.

Let $d\in\mathbb{R}$ such that $F\left(a\right)<d<F\left(b\right)$. Define

$Q_{d}:=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\in\mathbb{\tilde{Q}}\mid
x\in\overline{\left[a,b\right]}\wedge F\left(x\right)\leq
d{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|.$

$Q_{d}$ is clearly bounded (e.g. by $b$). Since $F\left(a\right)<d$ , standard
arguments that use the continuity of $F$ and the denseness of $\mathbb{Q}$ in
$\mathbb{R}$ show that there is a rational $a\leq q$ s.t. $F\left(q\right)\leq
d$. Thus, $Q_{d}$ is non-empty and by Thm. 30 it has a least upper bound,
denote it by $c$. Since $Q_{d}$ is non-empty and $b$ is an upper bound for it,
$c\in\left[a,b\right]$. Assume by contradiction that $F\left(c\right)<d$, and
pick $\varepsilon=d-F\left(c\right)$. By the continuity of $F$ there exists
$\delta>0$ s.t. for any $x\in\left[a,b\right]$, if $\left|x-c\right|<\delta$,
then
$\left|F\left(x\right)-F\left(c\right)\right|<\varepsilon=d-F\left(c\right)$.
This yields the existence of a rational $q\in\left(c,c+\delta\right)$ (again,
by the denseness of $\mathbb{Q}$ in $\mathbb{R}$) s.t. $F\left(q\right)<d$,
which is a contradiction. Now, assume by contradiction that
$F\left(c\right)>d$, and pick $\varepsilon=F\left(c\right)-d$. In this case
there exists $\delta>0$ s.t. for any $x\in\left[a,b\right]$, if
$\left|x-c\right|<\delta$, then $F\left(x\right)>d$. But then $c-\delta$ is
also an upper bound for $Q_{d}$, which is again a contradiction. Hence,
$F\left(c\right)=d$.

######  Theorem 47 (Extreme Value Theorem).

Let $F$ be a continuous real $\succ$\- function on a non-degenerate interval
$\left[a,b\right]$. It is provable in $RST_{HF}^{m}$ that $F$ attains its
maximum and minimum.

######  Proof 5.16.

Let $Q$ be the $\succ$-set $\left[a,b\right]\cap\mathbb{Q}$. $F\left[Q\right]$
is a $\succ$-set by Prop. 19, and it is non-empty by the denseness of
$\mathbb{Q}$ in $\mathbb{R}$. Assume by contradiction that $F\left[Q\right]$
is not bounded, and define for every $n\in\mathbb{N}$
$C_{n}=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}x\in\tilde{Q}\mid
F\left(x\right)>n{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|$.
By the assumption $C_{n}$ is a non-empty, bounded $\succ$-set. Therefore, by
Thm. 30, each $C_{n}$ has a least upper bound, denote it $c_{n}$. It is easy
to see that $c_{n}\in\left[a,b\right]$ for each $n\in\mathbb{N}$. Now, define
the $\succ$-sequence $\lambda n\in\mathbb{N}.c_{n}$ (which is indeed a
$\succ$-sequence by Thm. 30). Standard arguments show that since
$\left[a,b\right]$ is closed and bounded, there is a subsequence of $\lambda
n\in\mathbb{N}.c_{n}$, $\lambda k\in\mathbb{N}.c_{n_{k}}$, which converges to
a limit, denote it $m$. By Prop. 42 we have that $m\in\left[a,b\right]$. Now,
since $F$ is continuous, we easily get that $\lambda
k\in\mathbb{N}.F\left(c_{n_{k}}\right)$ converges to $F\left(m\right)$. But,
for each $k\in\mathbb{N}$: $F\left(c_{n_{k}}\right)>n_{k}\geq k$, which
contradicts the convergence of the sequence. Hence, $F\left[Q\right]$ is
bounded, and by Thm. 30 it has a least upper bound, denote it by $d$. Assume
by contradiction that there exists $u\in\left[a,b\right]$ s.t.
$F\left(u\right)>d$. Picking $\varepsilon=F\left(u\right)-d$, the continuity
of $F$ entails that there exists $\delta$ s.t. for every $x\in
B_{\delta}\left(u\right)$, $F\left(x\right)\geq d$. But the denseness of
$\mathbb{Q}$ entails that there is a rational number $q\in
B_{\delta}\left(u\right)$, and thus $F\left(q\right)\geq d$, which is a
contradiction. The proof that there exists $x\in\left[a,b\right]$ s.t. that
$F\left(x\right)=d$ uses arguments similar to the ones used in the proof of
Thm. 46. The proof that $F$ attains its minimum is symmetric.

The next step is to introduce in $RST_{HF}^{m}$ the concepts of
differentiation, integration, power series, etc, and develop their theories.
It should now be clear that there is no difficulty in doing so. Since a
thorough exposition obviously could not fit in one paper we omit it here, but
use some relevant facts in what follows.

We end this section by showing that all elementary functions that are relevant
to $J_{2}$ are available in $RST_{HF}^{m}$ in the sense that they are
formalizable as $\succ$-functions and their basic properties are provable in
$RST_{HF}^{m}$. Of course, not all constant functions on the “real” real line
are available in $J_{2}$, even though for every $y$ in $\mathbb{R}$, $\lambda
x\in\mathbb{R}.y$ is available in $RST_{HF}^{m}$ as a $\succ$-function. The
reason is that $\lambda x\in\mathbb{R}.y$ does not exists in $J_{2}$ for
_every_ “real” number $y$ (for the simple fact that not every “real” real
number is available in $RST_{HF}^{m}$). Thus we next define what is an
“$J_{2}$-elementary function” (see, for example, [42] for a standard
definition of “elementary function”). The collection of $J_{2}$-elementary
functions is the minimal collection that is closed under addition,
subtraction, multiplication, division, and composition, and includes the
following:

  * •

$J_{2}$-constant functions: $\lambda x\in\mathbb{R}.c$ where $c$ is a real
number in $J_{2}$.

  * •

Exponential: $\lambda x\in\mathbb{R}.e^{x}$

  * •

Natural logarithm: $\lambda x\in\mathbb{R}^{+}.\mbox{ln}x$

  * •

Trigonometric functions:$\lambda x\in\mathbb{R}.\mbox{sin}x$.

  * •

Inverse trigonometric functions: $\lambda
x\in\left[-1,1\right].\mbox{arcsin}x$.

######  Proposition 48.

All $J_{2}$-polynomials (i.e. with coefficients in $J_{2}$) on $\mathbb{R}$
are available in $RST_{HF}^{m}$ as $\succ$-function, and it is provable in
$RST_{HF}^{m}$ that they are continuous.

######  Proof 5.17.

$J_{2}$-constant functions and the identity function are available in
$RST_{HF}^{m}$ by Prop. 22, and the proofs of their continuity is immediate.
Composition of $\succ$-functions is also available in $RST_{HF}^{m}$. All
$J_{2}$-polynomials on $\mathbb{R}$ are therefore available in $RST_{HF}^{m}$,
since $+$ and $\cdot$ are $\succ$-functions, and they are continuous by Lemma
45.

######  Proposition 49.

The exponential and trigonometric functions are available in $RST_{HF}^{m}$,
and it is provable in $RST_{HF}^{m}$ that they are continuous.

######  Proof 5.18.

Since the exponential and the trigonometric functions all have power series,
their definability as $\succ$-functions follows from Prop. 43. It is
straightforward to verify that the basic properties of these $\succ$-functions
are provable in $RST_{HF}^{m}$. Examples of such properties are: the
monotonicity of the exponential, the power rules of the exponential,
trigonometric identities like
$\mathrm{sin}\left(\alpha+\beta\right)=\mathrm{sin}\,\alpha\,\mathrm{cos\,}\beta\,+\mathrm{sin}\,\beta\mathrm{\,cos}\,\alpha$,
the fact that $\mathrm{sin}$ has a period of $2\pi$ (where $\pi$ is its first
positive root), etc.282828We can prove the standard properties of the exponent
and the trigonometric functions as listed, e.g., in [2], using the notion of
differentiation. The continuity of these functions follows from Lemma 45 and
Prop. 43.

######  Lemma 50.

Let $F$ be a continuous, monotone real $\succ$-function on a real interval
$\left[a,b\right]$, and suppose $F\left(a\right)<F\left(b\right)$. It is
provable in $RST_{HF}^{m}$ that

$\forall y\in\bar{\mathbb{R}}\left(\exists
x\in\overline{\left[a,b\right]}.\bar{F}\left(x\right)=y\leftrightarrow
y\in\overline{\left[F\left(a\right),F\left(b\right)\right]}\right)$

######  Proof 5.19.

The left-to-right implication is immediate from the monotonicity of $F$. The
right-to-left implication follows from Thm. 46.

######  Proposition 51.

Let $F$ be a continuous, strictly monotone real $\succ$-function on a real
interval. Then it is provable in $RST_{HF}^{m}$ that the inverse function
$F^{-1}$ is available in $RST_{HF}^{m}$ as a $\succ$-function, and its
continuity is provable in $RST_{HF}^{m}$.

######  Proof 5.20.

We here prove the claim for continuous, strictly monotone real
$\succ$-function on a finite closed interval $\left[a,b\right]$. The extension
from finite closed intervals to arbitrary interval is standard. Suppose $F$ is
increasing. The proof is similar to the proof of Thm. 46. For any
$y\in\left[F\left(a\right),F\left(b\right)\right]$ define the $\succ$-set
$Q_{y}:=\left\|{\left\\{\right.\negthickspace\negthickspace\negthickspace\circ}q\in\widetilde{\mathbb{Q}}\mid
q\in\overline{\left[a,b\right]}\wedge F\left(q\right)\leq
y{\circ\negthickspace\negthickspace\negthickspace\left.\right\\}}\right\|$. It
is easy to see that $Q_{y}$ is non-empty and bounded, thus, by Thm. 30,
$Q_{y}$ has a least upper bound. Now, $\left\|\lambda
y\in\overline{\left[F\left(a\right),F\left(b\right)\right]}.l.u.b(\widetilde{Q_{y}})\right\|$
is the desired inverse $\succ$-function. It is not difficult to prove the
basic properties of the inverse function in $RST_{HF}^{m}$. We demonstrate the
proof that $F^{-1}\circ F=id_{\left[a,b\right]}$. For this we need to show
that for any $x\in\left[a,b\right]$, $l.u.b(Q_{F\left(x\right)})=x$. By the
monotonicity of $F$, $x$ is clearly an upper bound for $Q_{F\left(x\right)}$.
Assume by contradiction that there is a real number $w<x$ which is an upper
bound of $Q_{F\left(x\right)}$. Thus, in the interval $\left(w,x\right)$ there
is a rational number $q$ such that $F\left(q\right)\leq F\left(x\right)$ (by
monotonicity). But then, $q\in Q_{F\left(x\right)}$ and $w<q$, which is a
contradiction.

######  Proposition 52.

All $J_{2}$-elementary functions are available in $RST_{HF}^{m}$.

######  Proof 5.21.

Props. 48 and 49 show that $J_{2}$-polynomials on $\mathbb{R}$, the
exponential and trigonometric functions are available in $RST_{HF}^{m}$. Prop.
51 then enables the availability in $RST_{HF}^{m}$ of the inverse
trigonometric functions, and of the natural logarithm as the inverse of the
exponential.

It is not difficult to see that many standard discontinuous functions are also
available in $RST_{HF}^{m}$, as the next proposition shows.

######  Proposition 53.

Any piecewise defined function with finitely many pieces such that its
restriction to any of the pieces is a $J_{2}$-elementary function, is
available in $RST_{HF}^{m}$.

######  Proof 5.22.

If the function has finitely many pieces and each of the pieces is a
$J_{2}$-elementary function, then it can be constructed in $RST_{HF}^{m}$
using Prop. 22(5).

##  6\. Conclusion and Further Research

In this paper we showed that a minimal computational framework is sufficient
for the development of applicable mathematics. Of course, a major future
research task is to implement and test the framework. A critical component of
such implementation will be to scale the cost of checking the safety relation.
We then plan to use the implemented framework to formalize even larger
portions of mathematics, including first of all more analysis, but also
topology and algebra.

Another important task is to fully exploit the computational power of
$RST_{HF}^{m}$ and $J_{2}$. This includes finding a good notion of canonical
terms, and investigating various reduction properties such as strong
normalization. We intend to try also to profit from this computational power
in other ways, e.g., by using it for proofs by reflection as supported by
well-known proof assistant like Coq [16], Nuprl [18] and Isabelle/HOL [40].

An intuitionistic variant of the system $RST_{HF}^{m}$ can be also considered.
It is based on intuitionistic first-order logic (which underlies constructive
counterparts of $ZF$, like $CZF$ [1] and $IZF$ [12]), and is obtained by
adding to $RST_{HF}^{m}$ the axiom of Restricted Excluded Middle:
$\varphi\vee\neg\varphi$, where $\varphi\succ\emptyset$. This axiom is
computationally acceptable since it simply asserts the definiteness of
absolute formulas. The resulting computational theory should allow for a
similar formalization of constructive analysis (e.g., [39]).

Further exploration of the connection between our framework and other related
works is also required. This includes works on: computational set theory [1,
12, 14, 26, 39], operational set theory [24, 31], and rudimentary set theory
[11, 36].

Another direction for further research is to consider larger computational
structures. This includes $J_{\omega}$ or even $J_{\omega^{\omega}}$ (which is
the minimal model of the minimal computational theory based on ancestral logic
[7, 17]). On the one hand, in such universes standard mathematical structures
can be treated as sets. On the other hand, they are more comprehensive and
less concrete, thus include more objects which may make computations harder.

## Acknowledgements

The second author is supported by: Fulbright Post-doctoral Scholar program;
Weizmann Institute of Science – National Postdoctoral Award program for
Advancing Women in Science; Eric and Wendy Schmidt Postdoctoral Award program
for Women in Mathematical and Computing Sciences.

## References

  * [1] P. Aczel and M. Rathjen.  Notes on constructive set theory.  Technical Report 40, Mittag-Leffler, 2001.
  * [2] L. V. Ahlfors.  Complex analysis.  McGraw-Hill Book Co., Oliver and Boyd Ltd., 1964.
  * [3] J. Avigad and J. Harrison.  Formally verified mathematics.  Communications of the ACM, 57(4):66–75, 2014.
  * [4] A. Avron.  Transitive closure and the mechanization of mathematics.  In Thirty Five Years of Automating Mathematics, pages 149–171. Springer, 2003.
  * [5] A. Avron.  Constructibility and decidability versus domain independence and absoluteness.  Theoretical Computer Science, 394(3):144–158, 2008.
  * [6] A. Avron.  A framework for formalizing set theories based on the use of static set terms.  In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of computer science, LNCS 4800, pages 87–106. Springer, 2008.
  * [7] A. Avron.  A new approach to predicative set theory.  In R. Schindler, editor, Ways of Proof Theory, pages 31–63. Onto Series in Mathematical Logic, Verlag, 2010.
  * [8] A. Avron and L. Cohen.  Formalizing scientifically applicable mathematics in a definitional framework.  Journal of Formalized Reasoning, 9(1):53–70, 2016.
  * [9] A. Avron, F. Honsell, I. A. Mason, and R. Pollack.  Using typed lambda calculus to implement formal systems on a machine.  Journal of Automated Reasoning, 9:309–354, 1992.
  * [10] A. Avron, S. Lev, and N. Levy.  Safety, absoluteness, and computability.  2018\.  To appear.
  * [11] A. Beckmann, S. R. Buss, and SD. Friedman.  Safe recursive set functions.  The Journal of Symbolic Logic, 80(3):730–762, 2015.
  * [12] M. J. Beeson.  Foundations of constructive mathematics: Metamathematical studies, volume 6.  Springer Science & Business Media, 2012.
  * [13] J. J. J. Campbell, J. C. G. Dos Reis, P. S. M. Wenzel, and V. Sorge, editors.  Intelligent Computer Mathematics.  Springer, 2008.
  * [14] D. Cantone, E. Omodeo, and A. Policriti.  Set theory for computing: from decision procedures to declarative programming with sets.  Springer, 2001.
  * [15] D. Cantone, E. G. Omodeo, and J. T. Schwartz.  Computational Logic and Set Theory: Applying Formalized Logic to Analysis.  Springer, 2011.
  * [16] A. Chlipala.  Certified Programming with Dependent Types.  MIT Press, Cambridge, MA, 2013.
  * [17] L. Cohen and A. Avron.  The middle ground–ancestral logic.  Synthese, pages 1–23, 2015.
  * [18] R. L. Constable, S. F. Allen, M. Bromley, R. Cleaveland, et al.  Implementing mathematics with the Nuprl proof development system.  Prentice Hall, 1986.