Analysis in a Formal Predicative Set Theory

Abstract

We present correct and natural development of fundamental analysis in a predicative set theory we call ${\mathsf {PZF}^{\mathsf {U}}}$. This is done by using a delicate and careful choice of those Dedekind cuts that are adopted as real numbers. ${\mathsf {PZF}^{\mathsf {U}}}$ is based on ancestral logic rather than on first-order logic. Its key feature is that it is definitional in the sense that every object which is shown in it to exist is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented model of it, and makes it very suitable for MKM (Mathematical Knowledge Management) and ITP (Interactive Theorem Proving). The development of analysis in ${\mathsf {PZF}^{\mathsf {U}}}$ does not involve coding, and the definitions it provides for the basic notions (like continuity) are the natural ones, almost the same as one can find in any standard analysis book.

1 Introduction

Axiomatic set theory is almost universally accepted as the basic theory which provides the foundations of mathematics, and in which the whole of present day mathematics can (and many say: should) be developed. As such it should be considered to be the most natural framework for MKM (Mathematical Knowledge Management) in general, and ITP (Interactive Theorem Proving) in particular (especially for goals like those of the AUTOMATH project ([7, 15, 22]) and the QED manifesto ([21]). Moreover: as is emphasized and demonstrated in [4], set theory has not only a great pragmatic advantage as a basic language for mathematical discourse, but it also has a great computational potential as a basis for specification languages, declarative programming, and proof verifiers. However, in order to be used for any of these tasks it is necessary to overcome the following serious gaps that exist between the “official” formulations of set theory (as given e.g. by Zermelo Fränkel Set Theory ZF; see e.g. [11]), and actual mathematical practice:

• 1. The official formalizations of axiomatic set theories in almost all textbooks are based on some standard first-order languages. In such languages terms are variables, constants, and sometimes function applications (like $x\cap y$). What is not available in the official languages of those formalizations is the use of set terms of the form ($\{x\mid \varphi \}$). As a result, already the formulation of the axioms is quite cumbersome, and even the formalization of elementary proofs becomes something practically incomprehensible.

• 2. ZF treats all the mathematical objects on a par, and so hid the computational significance of many of them. Thus although certain functions are first-class citizens in many programming languages, in set theory they are just “infinite sets”, and ZF in its usual presentation is an extremely poor framework for computing with such sets (or handling them constructively).

• 3. Full ZF is far too strong for core mathematics, which practically deals only with a small fraction of the set-theoretical “universe”. It is obvious that much weaker (and easier to mechanize) systems should do.

The first of these three problems can be overcome by using the framework for formalizing mathematics that was developed In [1]. This framework is based on set theory and is close in many ways to ZF on one hand, but is definitional in spirit on the other. In particular: it makes an extensive use of abstract set terms of the form $\{x \mid \varphi \}$. One of its crucial features is that all abstract set terms that it allows to use are statically defined in a precise formal way (using the mechanism of safety relations). Therefore it preserves the very useful complete separation we have in first-order logic between the (easy) check whether a given expression is a well-formed term or formula, and the (difficult) check whether it is a theorem. This feature makes the framework particularly appropriate for mechanical manipulations and for interactive theorem proving.¹

The other two problems mentioned above have been tackled in [2, 3, 5] by employing predicative set theories. By this, these papers followed Poincaré ([16, 17]), Weyl ([20]), and Feferman, who in [9, 10] forcefully argued that predicative mathematics suffices for developing all of scientifically applicable mathematics, i.e. the mathematics that is actually indispensable to present-day natural science. Poincaré-Weyl-Feferman’s predicativist program is essentially based on the principle that higher-order constructs, such as sets or functions, are acceptable only when introduced through non-circular definitions. The main goal of [3, 5] was to show that using the framework of [1], this definitional approach to mathematics can be implemented in a user friendly way, which is based on set theory, and has no essential conflicts with mathematical practice.

The main problem of predicative mathematics is how to introduce and handle the real numbers, and what is usually taken as their characteristic property: their completeness with respect to their standard ordering. This principle has in fact been abandoned (and replaced by a weaker principle) by Weyl and Feferman. In contrast, it is preserved in [5]. However, its applicability there is severely limited by the fact that most of the important collections of real numbers, (including ${\mathbb {R}}$ itself and all intervals) are not available as sets according to the theory ${\mathsf {RST}^{\mathsf {HF}}}$ used there, but only as proper classes. Moreover, because of this fact the development of analysis there is not natural, and involves a lot of coding (much like the development of analysis carried out in reverse mathematics [19]). What seemed to be a successful attempt to avoid this state of affairs was made in [3], using a (still predicative) extension of ${\mathsf {RST}^{\mathsf {HF}}}$. Unfortunately, there was a subtle, but rather difficult to repair, mistake in the proof given there of the completeness of what is taken there as ${\mathbb {R}}$. In fact, the theorem is wrong! (See Remarks 5 and 7 below.) Since all proofs that come later in [3] depend on the completeness of its ${\mathbb {R}}$, that mistake invalidates them as well.

In this paper we achieve the goals of [3] by presenting correct and natural development of fundamental analysis in a predicative set theory which is based on the framework given in [1]. We use for this an extension called ${\mathsf {PZF}^{\mathsf {U}}}$ of the system PZF developed in [2] (which is based on ancestral logic rather than on first-order logic), and a more delicate and careful choice of those Dedekind cuts that we adopt as real numbers. Like the systems used in [3] and [5], the key feature of ${\mathsf {PZF}^{\mathsf {U}}}$ is that it is definitional in the sense that every object which is shown in it to exist is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented model of it. The development of analysis in ${\mathsf {PZF}^{\mathsf {U}}}$ does not involve coding (like in [19] and [5]), and the definitions it provides for the basic notions (like continuity) are the natural ones, almost the same as one can find in any standard analysis book (e.g. [12]).

2 Preliminaries

2.1 Notations

We denote formulas by $\varphi$, $\psi$, $\chi$, $\theta$, $\alpha$, $\beta$, terms by r, s, t, and variables by x, y, z, w, a, b, indexed or not. Given an expression (i.e. a formula or a term) e, we denote by $\mathsf {Fv}(e)$ ($\mathsf {Bv}(e)$) its set of free variables (bound variables). Let $x_1 ,\ldots ,x_k$ be k different variables, and $t_1 ,\ldots ,t_k$ be k terms. We write $e \{t_1/x_1 ,\ldots ,t_k/x_k\}$ for the expression that is obtained from e by simultaneously substituting the terms $t_i$s for the free occurrences of the variables $x_i$s (we do not assume that $\mathsf {Fv}(e)=\{x_1 ,\ldots ,x_k\}$, or even that $\mathsf {Fv}(e) \subseteq \{x_1 ,\ldots ,x_k\}$). We always assume that during a substitution no free variable of the substituted terms is getting captured (renaming the bounded variables in e to fresh new ones if needed). We write $\bar{x}$ as a shorthand for $x_1 ,\ldots ,x_n$.

2.2 The Theory ${\mathsf {PZF}^{\mathsf {U}}}$

In this section we define the theories $\mathsf {PZF}$ and ${\mathsf {PZF}^{\mathsf {U}}}$. The theory $\mathsf {PZF}$ was presented in [2].² (See there for more information.) We start by introducing $\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$, the language of ${\mathsf {PZF}^{\mathsf {U}}}$. $\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$ contains three major notions: the notion of term, the notion of formula, and the notion of a safety relation $\succ _{{\mathsf {PZF}^{\mathsf {U}}}}$, which is a relation between formulas and sets of variables. The definitions of those notions are mutual recursive.

Definition 1

The terms, formulas, and the safety relation $\succ _{{\mathsf {PZF}^{\mathsf {U}}}}$ of $\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$ are:

• Terms:

  • 1. Every variable is a term.

  • 2. The constant $\mathsf {U}$ is a term.

  • 3. If x is a variable and $\varphi$ is a formula s.t. $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\{x\}$, then $\{x \ \big |\ \varphi \}$ is a term.

• Formulas:

  • 4. If t and s are terms than $t \in s$, $t = s$ are (atomic) formulas.

  • 5. If $\varphi$, and $\psi$ are formulas, and x is a variable, then $\lnot \varphi$, $\varphi \vee \psi$, $\varphi \wedge \psi$, and $\exists x \varphi$ are formulas.

  • 6. If $\varphi$ is a formula; s, t are terms; and x, y are distinct variables, then $({\mathsf {TC}}_{x,y}\varphi )(t,s)$ is a formula.

• The safety relation $\succ _{{\mathsf {PZF}^{\mathsf {U}}}}$:

  • 7. $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\emptyset$ if $\varphi$ is atomic.

  • 8. $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\{x\}$ if $\varphi \in \{x \ne x, x=t , t=x , x \in t\}$, provided that $x \notin \mathsf {Fv}(t)$.

  • 9. $\lnot \varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\emptyset$ if $\varphi \succ _{\mathsf {RST}}\emptyset$.

  • 10. $\varphi \vee \psi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$ if $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$ and $\psi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$.

  • 11. $\varphi \wedge \psi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X \cup Y$ if $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$; $\psi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}Y$; and $Y \cap \mathsf {Fv}(\varphi ) = \emptyset$.

  • 12. $\exists y \varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X - \{y\}$ if $y \in X$ and $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$.

  • 13. $({\mathsf {TC}}_{x,y}\varphi )(x,y) \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X$ if $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X \cup \{x\}$ or $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}X \cup \{y\}$.

Definition 2

The definition of $\mathcal{{L}}_\mathsf {PZF}$ (the language $\mathsf {PZF}$) is (almost) identical to Definition 1, but with the constant $\mathsf {U}$ omitted. (the safety relation of $\mathcal{{L}}_\mathsf {PZF}$ is denoted by $\succ _{\mathsf {PZF}}$ .)

Definition 3

A formula $\varphi$ of $\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$ ($\mathcal{{L}}_\mathsf {PZF}$) is absolute if $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\emptyset$ ($\varphi \succ _{\mathsf {PZF}}\emptyset$).

Definition 4

The logic which underlies ${\mathsf {PZF}^{\mathsf {U}}}$ and $\mathsf {PZF}$ is ${\mathsf {TC}}$-logic (transitive closure logic), also called AL (ancestral logic). See [2, 6, 13, 14, 18].

Definition 5

$\mathsf {PZF}$ is the set-theory in $\mathcal{{L}}_\mathsf {PZF}$ that has the following axioms:

• Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \leftrightarrow x=y$

• Comprehension: $\forall x.x \in \{x \mid \psi \} \leftrightarrow \psi$, provided $\psi \succ _{\mathsf {PZF}}\{x\}$.

• $\in$-induction scheme: $\Big (\forall x.\big (\forall y \in x .\varphi \{y/x\} \big ) \rightarrow \varphi \Big ) \rightarrow \forall x \varphi$ (provided y is free for x in $\varphi$).³

Definition 6

${\mathsf {PZF}^{\mathsf {U}}}$ is the set-theory in $\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$ that has all the axioms of $\mathsf {PZF}$ (with $\succ _{\mathsf {PZF}}$ replaced by $\succ _{{\mathsf {PZF}^{\mathsf {U}}}}$) and the following schema for $\mathsf {U}$:

$\mathsf {U}$-closure scheme: $\forall y_1 \ldots y_n \in \mathsf {U}. t \in \mathsf {U}$, provided t is a term, $\mathsf {Fv}(t) = \{y_1,\ldots ,y_n\}$, and $\mathsf {U}$ does not occur in t. (i.e., t is a term of $\mathsf {PZF}$.)

Some notes concerning Definition 6:

• By straightforward structural induction it can be proved that if e is an (absolute) formula than $e \{t_1/x_1 ,\ldots ,t_k/x_k\}$ remains an (absolute) formula, and that if e is a term than $e \{t_1/x_1 ,\ldots ,t_k/x_k\}$ remains a term. It holds for $\mathsf {PZF}$ and for ${\mathsf {PZF}^{\mathsf {U}}}$.

• The constant $\mathsf {U}$ stands for “Universe”. In [2] it was shown that every rudimentary operation⁴ can be defined by a set-term of $\mathsf {PZF}$ (even without the use of the ${\mathsf {TC}}$ operator).⁵ Hence by the $\mathsf {U}$-closure scheme (see Definition 6), the universe $\mathsf {U}$ is closed under the rudimentary operations. For example if $x,y\in \mathsf {U}$ then $x \times y$, $x \cup y$, $x \cap y$, $\cup x$ are also elements of $\mathsf {U}$.

• In the sequel, we shall always indicate which definitions and which claims take place in $\mathsf {PZF}$ and which in ${\mathsf {PZF}^{\mathsf {U}}}$. Usually we shall do it by writing in parenthesize whether it is $\mathsf {PZF}$ (for example “Definition 1.1 ($\mathsf {PZF}$)”) or ${\mathsf {PZF}^{\mathsf {U}}}$ (for example “Lemma 1.1 (${\mathsf {PZF}^{\mathsf {U}}}$)”). We have a special concern with definitions of set-terms that belong to $\mathsf {PZF}$ because we can apply to them the $\mathsf {U}$-closure scheme (see Definition 6).

2.3 Extending the Base Language

Although the official language of ${\mathsf {PZF}^{\mathsf {U}}}$ (and of $\mathsf {PZF}$) is the one defined above, it is a standard mathematical practice to introduce new symbols and notations as the work progresses. So practically we shall enrich our language, and this will be done by adding to the language two kinds of defined symbols: defined predicates, and defined operations.

Defined Predicates. This is done much like as adding new predicate symbols to a standard FOL language $\mathcal{{L}}$. In general, given a formula $\varphi$ of $\mathcal{{L}}$ s.t. $\mathsf {Fv}(\varphi )=\{x_1 ,\ldots ,x_n\}$ we may extend $\mathcal{{L}}$ with a new n-ary predicate symbol $P^\varphi$ that abbreviates $\varphi$ (this of course must come with appropriate axioms that “define” $P^\varphi$). In our work we shall do the same, but with the constraint that we shall add new predicate symbols only for absolute formulas. The reason for this is that we want to preserve property (7) of Definition 1 (atomic formulas need to be absolute).

Defined Operations. In a usual FOL one may add new operations symbols.⁶ Working in a theory T (in a language $\mathcal{{L}}$), if $\varphi$ is a formula of $\mathcal{{L}}$ s.t. $\mathsf {Fv}(\varphi )=\{y,x_1 ,\ldots ,x_n\}$, and if $T \vdash \forall x_1 ,\ldots ,x_n\exists ! y. \varphi$, we may extend $\mathcal{{L}}$ with a new n-ary operation symbol $f^\varphi$, with the following intuitive meaning: given $x_1 ,\ldots ,x_n$, $f^\varphi (x_1 ,\ldots ,x_n)$ is that unique y. (Of course we need to add to T appropriate axioms that “defines” $f^\varphi$). Hence, in the process of adding a new operation symbol, there is usually a need to prove (inside the theory) the existence and uniqueness of the object “returned” by the operation. An exception is the case where the new operation symbol is introduced as an abbreviation of some term in the language. (More formally the above $\varphi$ is of the form $y=t$ where t is a term. The existence and uniqueness of that y is obvious.) While working in $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$) this is the only way we shall use when we add new operation symbols. For example consider the term $t=\{a \mid a\in x_1 \vee a\in x_2\}$ (the union of $x_1$ and $x_2$). We add a new 2-ary operation symbol “$\cup$” corresponding to t (or more formally corresponding to the formula $y=t$). Given two terms r and s, we may view the term $r \cup s$ simply as an abbreviation of $\{a \mid a\in r \vee a\in s\}$.

Remark 1

• 1. We stress that at any point in the future, our extended language will always satisfy all the properties specified in Definition 1. Specifically, an atomic formula will always be absolute, and given a term t of $\mathcal{{L}}_\mathsf {PZF}$, $x \in t \succ _{\mathsf {PZF}}\{x\}$, and $x = t \succ _{\mathsf {PZF}}\{x\}$ (same for ${\mathsf {PZF}^{\mathsf {U}}}$).

• 2. If one wants to translate a formula that involves new predicate-symbols/operation-symbols to a formula of the original language, all he needs to do to is to unravel the definitions of the defined notions, which are merely abbreviations of formulas/terms in the original language.

• 3. One delicate point concerns the schemes in Definition 6 (the Comprehension scheme, the $\in$-induction scheme, and the $\mathsf {U}$-closure scheme). The formulas and terms that appear there are expressions in the original language $\mathcal{{L}}_\mathsf {PZF}$ ($\mathcal{{L}}_{{\mathsf {PZF}^{\mathsf {U}}}}$), while we will use those schemes also with expressions that involve new defined symbols. Practically no real problem arises because the new symbols merely represent new ways of abbreviating formulas and terms. We shall be more careful with the $\mathsf {U}$-closure scheme, when applying it to a term t. We shall always check that t is a term of the (extended) language of $\mathsf {PZF}$.

• 4. Let $t_1 ,\ldots ,t_n$ be n terms, let P be an n-ary predicate symbols, and f be an n-ary operation symbols. The standard convention of applying P to $t_1 ,\ldots ,t_n$, is $P(t_1 ,\ldots ,t_n)$ (and $f(t_1 ,\ldots ,t_n)$ when applying f to them). To enhance clarity, we leave the symbols “(,)” only for the case when we apply a function to an element. Instead of $P(t_1 ,\ldots ,t_n)$ we shall always write $P[t_1 ,\ldots ,t_n]$, and instead of $f(t_1 ,\ldots ,t_n)$ we shall always write $f\langle t_1 ,\ldots ,t_n \rangle$.

2.4 Basic Notations

In what follows we shall use the following.

• 1. In [2] it was shown how basic predicates and operations can be defined. In the sequel we shall use the following: $x \subseteq y$ (the usual meaning), ${\mathsf {func}} [f]$ (f is a function), ${\mathsf {func}} [f,x,y]$ (f is a function from x to y), $\mathsf {bijection}[f,x,y]$, $\mathsf {surjection}[f,x,y]$ (f is a bijection/surjection from x to y), $\mathsf {seq}[s]$ (s is a function with domain ${\mathbb {N}}$), $\mathsf {seqFin}[s]$ (s is a function from a proper initial segment of ${\mathbb {N}}$). $\emptyset ,x \cup y \ ,\ x \cap y\ ,\ x \setminus y\ ,\ x \times y \ ,\ \cup x$ (the usual meaning), $\{x\}\ ,\ \{x_1 ,\ldots ,x_n\}$(the usual meaning), $\langle x,y \rangle$ (ordered pair), ${\mathsf {dom}} \langle r \rangle \ ,\ {\mathsf {rng}} \langle r \rangle$ (the domain/range of a relation r), $f \upharpoonright x$ (the restriction of a function f to x). We note that all the above take place in $\mathsf {PZF}$.

  The next four notations are merely abbreviations for set-terms. (For more information see [3]).

• 2. $\iota x.\varphi$ (provided $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\{x\}$) stands for the unique element x s.t. $\varphi$.

• 3. $\lambda x \in s.t$ (provided $x \notin \mathsf {Fv}(s)$). Moreover, we note that if s and t do not involve the constant $\mathsf {U}$, and if $\mathsf {Fv}(s) \cup \mathsf {Fv}(t) \subseteq \{x_1,\ldots ,x_n\}$ then ${\mathsf {PZF}^{\mathsf {U}}}\vdash \forall x_1 ,\ldots ,x_n \in \mathsf {U}. (\lambda x \in s.t) \in \mathsf {U}$.

• 4. If f is a function, f(x) stands for $\iota y. \langle x,y \rangle \in f$, where y is a fresh new variable.

• 5. Restricted replacement: if t is a term s.t. $\{\bar{x}\} \subseteq \mathsf {Fv}(t)$, $\psi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\{\bar{x}\}$, we write $\{t \mid \psi \}$ instead of $\{a \mid \exists \bar{x}. a=t \wedge \psi \}$.

• 6. Definition by cases: assume that $t_1$, $t_2$ are terms, and that $\varphi _1,\varphi _2$ are absolute formulas s.t. $\mathsf {PZF}({\mathsf {PZF}^{\mathsf {U}}}) \vdash \lnot (\varphi _1 \wedge \varphi _2)$. Let a be a fresh new variable, and consider the following term: $t :=\{a \mid a \in t_1 \wedge \varphi _1\} \cup \{a \mid a \in t_2 \wedge \varphi _2\}$. It is provable in $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$) that:

  $$ \big (\varphi _1 \rightarrow t=t_1 \big ) \wedge \big (\varphi _2 \rightarrow t=t_2 \big ) \wedge \big ( (\lnot \varphi _1 \wedge \lnot \varphi _2) \rightarrow t=\emptyset \big ). $$

  In the sequel we introduce t simply by writing:

  $$t :=\left\{ \begin{array}{@{}ll} t_1 &{} \text { if }\, \varphi _1 \\ t_2 &{} \text { if }\, \varphi _2 \\ \emptyset &{} \text { else} \\ \end{array} \right. $$

Remark 2

For simplicity, we stated the above notation for a two-cases term, but we shall use this type of notations also for more than two terms. Also, if it holds that $\mathsf {PZF}({\mathsf {PZF}^{\mathsf {U}}}) \vdash \varphi _1 \vee \ldots \vee \varphi _k$ we shall omit the “else”.

2.5 Mathematics in $\mathsf {PZF}$

We summarize facts from [2, 3, 5] about the development of mathematics in $\mathsf {PZF}$.⁷

The Sets ${\mathbb {N}},{\mathbb {Z}},{\mathbb {Q}}$. For every element of $J_{\omega ^\omega }$, the $\omega ^\omega$ level of Jensen’s hierarchy, there exists a closed set-term that represents it. Specifically, there are closed set-terms that represent:

• The set of natural numbers, the set of integers, and the set of rational numbers. Those set-terms are denoted as usual by ${\mathbb {N}}$, ${\mathbb {Z}}$, and ${\mathbb {Q}}$.

• The following relations and functions (on ${\mathbb {Q}}$): $<_{\mathbb {Q}}, +_{\mathbb {Q}}, -_{\mathbb {Q}}, \times _{\mathbb {Q}}, /_{\mathbb {Q}}, \left|\cdot \right|_{\mathbb {Q}}$

It can be proved in $\mathsf {PZF}$ that the above sets, functions, and relations have their usual properties.

Induction Scheme. The full induction scheme can be proved, namely for every formula $\varphi$ of $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$):

$$ \vdash _{\mathsf {PZF}({\mathsf {PZF}^{\mathsf {U}}})} \big (\varphi \{0/n\} \wedge \forall n (\varphi \rightarrow \varphi \{n+1/n\})) \big ) \rightarrow \forall n\in {\mathbb {N}}. \varphi . $$

Dedekind Cuts. We define Dedekind cuts in the usual way.

Definition 7

r is a Dedekind cut:

$$\begin{aligned} \mathsf {dedCut}[r] :=&\big (\emptyset \ne r \subsetneq {\mathbb {Q}}\big ) \wedge \big ( r \text { doesn't have a maximum } \big ) \wedge \\&\big ( \forall x,y \in {\mathbb {Q}}. x \in r \wedge y<x \rightarrow y \in r \big ) \end{aligned}$$

After defining Dedekind cuts, we can define the usual operations $+,-,\times ,/,|\cdot |$, and the predicate <. For example the term that defines the operation $+$ is: $r+s :=\{q +_{\mathbb {Q}}q' \mid q\in r \wedge q'\in s\}$. Similarly we define $-,\times ,/,|\cdot |,<$. It is a standard matter to prove in $\mathsf {PZF}$ that these operations and relations have their usual properties. In addition, for every Dedekind-cut r, and every $k \in {\mathbb {N}}$, the exponentiation term $r^k$ is defined and it has its usual properties.

The following completeness theorem can be proved in $\mathsf {PZF}$:

Theorem 1

($\mathsf {PZF}$)(Completeness). Let X be a non empty set of Dedekind cuts. Assume also that there exists a Dedekind cut d s.t. $\forall x\in X. x \le r$ (namely X is bounded from above). Then $\cup X$ is a Dedekind cut and it is the supremum of X. (Later we shall denote $\cup X$ by $\sup \langle X \rangle$)

2.6 Recursive Definitions

In the sequel we shall define several terms by recursion. In this section we prove that such definitions are indeed legitimate. The following theorem is actually a schema in $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$):

Theorem 2

Let $t_i,t_s$ be terms of $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$) s.t. $\mathsf {Fv}(t_i)=\{\bar{x}\}$ and $\mathsf {Fv}(t_s) = \{n,p,\bar{x}\}$.⁸ Then there exists a term $t_\mathsf {rec}$ of $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$) with $\mathsf {Fv}(t_\mathsf {rec}) = \{\bar{x}\}$ s.t. the following is provable in $\mathsf {PZF}$ (${\mathsf {PZF}^{\mathsf {U}}}$):

$$\begin{aligned} \forall \bar{x}.&\ {\mathsf {func}} [t_\mathsf {rec}]\ \wedge \ {\mathsf {dom}} \langle t_\mathsf {rec} \rangle ={\mathbb {N}}\ \wedge \ t_\mathsf {rec}(0)=t_i \ \wedge \end{aligned}$$

(1)

$$\begin{aligned}&\ \forall n \in {\mathbb {N}}^+ \, \forall p. p = t_\mathsf {rec}(n-1) \rightarrow t_\mathsf {rec}(n)=t_s \end{aligned}$$

(2)

Informally, $t_i$ is the initial value, and $t_s$ is the “step” function that “gets” the previous value in the variable p, and outputs current value.

Remark 3

When using this theorem, we shall introduce $t_\mathsf {rec}$ by writing:

$$ t_\mathsf {rec}\langle \bar{x} \rangle :=\lambda n \in {\mathbb {N}}.\left\{ \begin{array}{@{}ll} t_i\langle \bar{x} \rangle &{} \text { if } n=0 \\ t_s\langle n,t_\mathsf {rec}\langle \bar{x} \rangle (n-1),\bar{x} \rangle &{} \text { if } n>0 \\ \end{array} \right. $$

Proof

See in the appendix.

2.7 Finite Sums

Using Theorem 2 we can define the 2-ary operation of finite sum $\sum _{i=0}^n a(i)$. It is provable in $\mathsf {PZF}$ that it has all its usual properties.

3 Sequences of Dedekind Cuts

In this section we develop the notion of a limit of a sequence (of Dedekind cuts).

Definition 8

($\mathsf {PZF}$). Define the following:

• $\mathsf {seq}^{\mathsf {dc}}[s] :=\mathsf {seq}[s] \wedge \forall a \in {\mathsf {rng}} \langle s \rangle .\mathsf {dedCut}[a]$

• $\mathsf {bounded}[a] :=\mathsf {seq}^{\mathsf {dc}}[a] \wedge \exists q \in {\mathbb {Q}}\, \forall n \in {\mathbb {N}}. |a(n)| \le q$.

• The following term maps a bounded sequence a, to its $\limsup$. Define first the term $t\langle a \rangle :=\{q \in {\mathbb {Q}}\mid \forall n \in {\mathbb {N}}\, \exists k \ge n. q \in a(k)\}$. Note that $t\langle a \rangle$ is not necessarily a Dedekind cut, because it might contain a maximal element. In that case we simply remove it:

  $$ \mathsf {limsup}\langle a \rangle = \left\{ \begin{array}{@{}ll} t\langle a \rangle &{} \text { if } \lnot \exists q \in t\langle a \rangle \forall q' \in t\langle a \rangle . q' \le q \\ t\langle a \rangle \setminus \{\iota q. q\in t\langle a \rangle \wedge \forall q' \in t\langle a \rangle .&{} q' \le q\} \, \, \, \, \text {else } \\ \end{array} \right. $$

• $\mathsf {liminf}\langle a \rangle$ is defined in a similar way.

• $\mathsf {converge}[a] :=\mathsf {bounded}[a] \wedge \mathsf {liminf}\langle a \rangle =\mathsf {limsup}\langle a \rangle$.

• The term $\mathsf {limit}\langle a \rangle$ maps a convergent sequence to its limit:

  $$\begin{aligned} \mathsf {limit}\langle a \rangle :=\mathsf {liminf}\langle a \rangle \end{aligned}$$

• The sequence a converges to (the Dedekind cut) r:

  $$\begin{aligned} \mathsf {converge}[a,r] :=&\mathsf {seq}^{\mathsf {dc}}[a] \wedge \mathsf {dedCut}[r] \wedge \\&\forall \varepsilon \in {\mathbb {Q}}^+ \, \exists N\in {\mathbb {N}}\, \forall n \ge N. |a(n)-r| < \varepsilon \end{aligned}$$

  It is straightforward to prove that $\mathsf {converge}[a,r] \wedge \mathsf {converge}[a,r'] \rightarrow r=r'$.

• The sequence a is a Cauchy sequence if:

  $$\begin{aligned}&\mathsf {cauchySeq}[a] :=\mathsf {seq}^{\mathsf {dc}}[a] \wedge \forall \varepsilon \in {\mathbb {Q}}^+ \, \exists N\in {\mathbb {N}}\, \forall n,m \ge N. |a(n)-a(m)| < \varepsilon&\end{aligned}$$

Proposition 1

( $\mathsf {PZF}$ ).

$$\begin{aligned} \forall a. \mathsf {seq}^{\mathsf {dc}}[a] \wedge \mathsf {bounded}[a] \rightarrow \mathsf {dedCut}[\mathsf {limsup}\langle a \rangle ] \wedge \mathsf {dedCut}[\mathsf {liminf}\langle a \rangle ] \end{aligned}$$

Proof

The proof is straightforward and left for the reader.

Proposition 2

($\mathsf {PZF}$). Assume that $\mathsf {seq}^{\mathsf {dc}}[a]$. The following holds:

• 1. $\mathsf {converge}[a] \rightarrow \exists r.\mathsf {converge}[a,r] \wedge r=\mathsf {limit}\langle a \rangle$

• 2. $\forall r. \mathsf {converge}[a,r] \rightarrow (\mathsf {converge}[a] \wedge \mathsf {limit}\langle a \rangle =r)$

• 3. $\mathsf {converge}[a] \leftrightarrow \mathsf {cauchySeq}[a]$

Proof

The proof of the above propositions is straightforward. In the appendix we sketch for example the proof that $\mathsf {cauchySeq}[a] \rightarrow \mathsf {converge}[a]$.

Remark 4

It is tempting to define $\mathsf {converge}[a]$ as $\exists r.\mathsf {dedCut}[r] \wedge \mathsf {converge}[a,r]$. But the last formula is not absolute, while our definition of $\mathsf {converge}[a]$ is done by an absolute one.

4 The Real Line

Up to now all the terms, absolute formulas, and claim took place in $\mathsf {PZF}$, namely we did not use the constant $\mathsf {U}$ in our definitions. Since we want to treat ${\mathbb {R}}$ (the real numbers) as a set, we move to work in ${\mathsf {PZF}^{\mathsf {U}}}$ and define ${\mathbb {R}}$ as follows.

Definition 9

( ${\mathsf {PZF}^{\mathsf {U}}}$ ).

• The real line ${\mathbb {R}}:=\{r \in \mathsf {U}\mid \mathsf {dedCut}[r]\}$

• r is a real number (or simply real) if $r\in {\mathbb {R}}$. Note that “r is real” is not equivalent to $\mathsf {dedCut}[r]$, since not all Dedekind cuts belong to $\mathsf {U}$.

It is straightforward to prove the following theorem:

Theorem 3

(${\mathsf {PZF}^{\mathsf {U}}}$)($\mathsf {U}$-completeness). Let $X \subseteq {\mathbb {R}}$, $X \ne \emptyset$, and assume that X is bounded from above. If $X \in \mathsf {U}$ then $\sup \langle X \rangle \in {\mathbb {R}}$.

Remark 5

In [3] it was claimed that already in the theory ${\mathsf {RST}^{\mathsf {HF},\mathsf {U}}}$ (and so also in ${\mathsf {PZF}^{\mathsf {U}}}$, which is stronger) one can prove that every nonempty bounded subset of ${\mathbb {R}}$ has a supremum in ${\mathbb {R}}$. As we noted in the introduction, this claim and its proof in [3] are wrong. The problem was that the need in Theorem 3 of the condition $X \in \mathsf {U}$ had been missed.

In addition we have:

Theorem 4

(${\mathsf {PZF}^{\mathsf {U}}}$).${\mathbb {R}}$ is closed under $+,-,\times ,/$ and $|\cdot |$. (In the case of / we exclude division by 0, of course.)

Notations: Henceforth we use the usual notations for closed/open intervals, like: $[a,b] :=\{r \in {\mathbb {R}}\mid a \le r \le b\}$, and $(a,b) :=\{r \in {\mathbb {R}}\mid a< r < b\}$.

Warning: Although ${\mathbb {R}}$ is a subset of $\mathsf {U}$, it is not necessarily an element of U. The same is true for [a, b] and (a, b) in case $a<b$ (for every $a,b\in R$).

Proposition 3

(${\mathsf {PZF}^{\mathsf {U}}}$)(Convergence in $\mathsf {U}$). Let $a \in \mathsf {U}$ be a sequence. Then:

$$\mathsf {converge}[a] \rightarrow \exists r \in {\mathbb {R}}.\mathsf {converge}[a,r] \wedge r=\mathsf {limit}\langle a \rangle $$

Proof

See in the appendix.

5 Continuous Functions

In this section we define the notion of continuous functions. The major obstacle we need to overcome is the fact that we do not have a “full” completeness of ${\mathbb {R}}$, rather a completeness with respect to subsets of ${\mathbb {R}}$ which are elements of $\mathsf {U}$ (see Theorem 3). To overcome this problem we only consider a restricted class of functions. Functions that are quasi element of $\mathsf {U}$, in the sense that their parts whose domains are available in the universe $\mathsf {U}$, are also in $\mathsf {U}$. The definition of these functions is the following:

Definition 10

( ${\mathsf {PZF}^{\mathsf {U}}}$ )( ${\mathsf {Ufunc}}$ ).

• 1. ${\mathsf {Ufunc}}[f] :={\mathsf {func}} [f] \wedge \forall x \in \mathsf {U}. x \subseteq {\mathsf {dom}} \langle f \rangle \rightarrow f \upharpoonright x \in \mathsf {U}$.

• 2. ${\mathsf {P}^{{\mathbb {R}}}}:=\{x\in \mathsf {U}\mid x \subseteq {\mathbb {R}}\}$

• 3. ${\mathsf {Ufunc}^{\mathbb {R}}}[f] :={\mathsf {func}} [f] \wedge {\mathsf {dom}} \langle f \rangle \subseteq {\mathbb {R}}\wedge {\mathsf {rng}} \langle f \rangle \subseteq {\mathbb {R}}\wedge \forall x \in {\mathsf {P}^{{\mathbb {R}}}}. f \upharpoonright x \in \mathsf {U}$ (which is obviously equivalent to ${\mathsf {Ufunc}}[f] \wedge {\mathsf {dom}} \langle f \rangle \subseteq {\mathbb {R}}\wedge {\mathsf {rng}} \langle f \rangle \subseteq {\mathbb {R}}$).

Proposition 4

( ${\mathsf {PZF}^{\mathsf {U}}}$ ).

• $\forall f,g. {\mathsf {Ufunc}^{\mathbb {R}}}[f] \wedge {\mathsf {Ufunc}^{\mathbb {R}}}[g] \wedge {\mathsf {rng}} \langle g \rangle \subseteq {\mathsf {dom}} \langle f \rangle \rightarrow {\mathsf {Ufunc}^{\mathbb {R}}}[f \circ g]$

• $\forall c\in {\mathbb {R}}\,\forall f,g. {\mathsf {Ufunc}^{\mathbb {R}}}[f] \wedge {\mathsf {Ufunc}^{\mathbb {R}}}[g] \rightarrow {\mathsf {Ufunc}^{\mathbb {R}}}[c \cdot f] \wedge {\mathsf {Ufunc}^{\mathbb {R}}}[f+g] \wedge {\mathsf {Ufunc}^{\mathbb {R}}}[f \cdot g] \wedge {\mathsf {Ufunc}^{\mathbb {R}}}[\frac{1}{f}]$

Proof

The proof is straightforward and left for the reader.

Definition 11

(${\mathsf {PZF}^{\mathsf {U}}}$)(continuous function). Assume that ${\mathsf {Ufunc}^{\mathbb {R}}}[f]$.

• 1. Let $x \in {\mathsf {dom}} \langle f \rangle$.

  We say that f is continuous at x (and denote it by ${\mathsf {continuous}}[f,x]$) if f is defined in a neighborhood of x (namely $\exists \delta \in {\mathbb {R}}^+. (x-\delta ,x+\delta ) \subseteq {\mathsf {dom}} \langle f \rangle$) and:

  $$\begin{aligned} \forall \varepsilon \in {\mathbb {R}}^+ \, \exists \delta \in {\mathbb {R}}^+ \, \forall x'. |x'-x|<\delta \rightarrow |f(x')-f(x)| < \varepsilon \end{aligned}$$

  (3)

• 2. The notion of left continuity and right continuity is defined is a similar way.

• 3. We say that f is continuous on a closed segment [a, b] if $[a,b] \subseteq {\mathsf {dom}} \langle f \rangle$, f is right-continuous at a, f is left-continuous at b, and f is continuous at every $x \in (a,b)$.

• 4. If the domain of f 0is a closed or open segment, or ${\mathbb {R}}$, we say that f is continuous if it is continuous on its entire domain. (In the case of closed segment [a, b], we only require right/left continuity on a/b (respectively). We denote it by ${\mathsf {continuous}}[f]$.

Remark 6

It is tempting to drop the condition ${\mathsf {Ufunc}}[f]$ in the above definition. But it turns out that this approach falls too short. See Remarks 5 and 7.

In the following we show that Definition 11 is not void, and actually every polynomial is a continuous function at every $x \in {\mathbb {R}}$. We start with the definition of the set of all polynomials:

Definition 12

( ${\mathsf {PZF}^{\mathsf {U}}}$ ).

• $\mathsf {seqFin}^{\mathbb {R}}[a] :=\mathsf {seqFin}[a] \wedge \forall i\in {\mathsf {dom}} \langle a \rangle .a(i) \in {\mathbb {R}}$

• $\mathsf {poly}\langle a \rangle :=\lambda x\in {\mathbb {R}}. \sum _{i=0}^ {{\mathsf {dom}} \langle a \rangle -1} a(i)\cdot x^i$

• $\mathsf {Polynomials}:=\{\mathsf {poly}\langle a \rangle \mid a \in \mathsf {seqFin}^{\mathbb {R}}\}$

Proposition 5

( ${\mathsf {PZF}^{\mathsf {U}}}$ ).

• ${\mathsf {continuous}}[\lambda x\in {\mathbb {R}}. x]$, and $\forall c \in {\mathbb {R}}. {\mathsf {continuous}}[\lambda x \in {\mathbb {R}}.c]$.

• Let f, g be functions from a subset of ${\mathbb {R}}$ to ${\mathbb {R}}$, and let $c\in {\mathbb {R}}$.

  • If $x \in {\mathsf {dom}} \langle f \rangle \cap {\mathsf {dom}} \langle g \rangle$ and ${\mathsf {continuous}}[f,x] \wedge {\mathsf {continuous}}[g,x]$ then

    $${\mathsf {continuous}}[f+g,x] \wedge {\mathsf {continuous}}[f \cdot g,x] \wedge {\mathsf {continuous}}[c \cdot f,x]$$

  • If $x \in {\mathsf {dom}} \langle f \rangle \wedge f(x) \ne 0$ then ${\mathsf {continuous}}[\frac{1}{f},x]$

  • If $x \in {\mathsf {dom}} \langle f \rangle \wedge f(x) \in {\mathsf {dom}} \langle g \rangle$ then ${\mathsf {continuous}}[f \circ g,x]$.

Proof

For every $x \in {\mathbb {R}}$, condition (3) of Definition 11 is proved in the usual way (for all the above cases). The fact that the above functions are indeed ${\mathsf {Ufunc}^{\mathbb {R}}}$, follows from Proposition 4.

Corollary 1

(${\mathsf {PZF}^{\mathsf {U}}}$). For every $p \in \mathsf {Polynomials}$, p is continuous at every $x \in {\mathbb {R}}$.

Proof

This is a straightforward induction using Proposition 5.

Power Series and Elementary Functions. Using theorem 2 (recursive definitions) it is possible to define the set of the elementary functions, and prove that they continuous. We sketch it in the appendix.

5.1 Intermediate Value Theorem

To demonstrate our definition of continuity, we prove the intermediate value theorem:

Theorem 5

(${\mathsf {PZF}^{\mathsf {U}}}$)(intermediate value theorem). Let f be a continuous function from [0, 1] to ${\mathbb {R}}$, s.t. $f(0)<0$ and $f(1)>0$. Then there exits $r \in [0,1]$ s.t. $f(r)=0$.

Proof

Define the following set:

$$X = \{q \in {\mathbb {Q}}\mid 0\le q\le 1 \wedge f(q)< 0\} \ \ \big ( =\{q \in {\mathbb {Q}}\mid 0\le q\le 1 \wedge (f\upharpoonright {\mathbb {Q}}) (q) < 0\}\big ) . $$

By the closure properties of $\mathsf {U}$, and the fact that $f \upharpoonright _{\mathbb {Q}}\in \mathsf {U}$, we conclude that $X \in \mathsf {U}$. Obviously X is non-empty and bounded from above, hence by the completeness of ${\mathbb {R}}$ it has a supremum - denote it by s. Obviously $s \in [0,1]$. We prove that $f(s)=0$. Assume that it is not the case, say $f(s) > 0$. By the continuity of f at s, there exists $\delta \in {\mathbb {R}}^+$ s.t.

$$\begin{aligned} \forall x. |x-s|<\delta \rightarrow |f(x)-f(s)| < \frac{f(s)}{2} \end{aligned}$$

(4)

Since $s = \sup \langle X \rangle$, there exists $q' \in (s-\delta ,s) \cap X$. By the definition of X, $f(q') < 0$, but by (4), $f(q')>\frac{f(s)}{2} > 0$ - a contradiction.

Remark 7

As we noted in Remark 6, it is tempting to define the notion of continuity for every function f from (subset of) ${\mathbb {R}}$ to ${\mathbb {R}}$, and not demand that ${\mathsf {Ufunc}}[f]$. Indeed, that was the definition that was adopted in [3]. We note that the assumption ${\mathsf {Ufunc}}[f]$ is crucial in the above proof, otherwise we could not deduce that $s=\sup \langle X \rangle \in {\mathbb {R}}$. In [3], although the definition of continuity did not assume that ${\mathsf {Ufunc}}[f]$, the intermediate value theorem was “proved” in a very similar way. This is due to the mistake in the proof of Theorem 3 (completeness of ${\mathbb {R}}$),⁹ where the assumption that the bounded subset of ${\mathbb {R}}$ is an element of $\mathsf {U}$ was omitted.

A Appendix

Proof

(proof of Theorem 2). We prove the case of $\mathsf {PZF}$ (the case of ${\mathsf {PZF}^{\mathsf {U}}}$ is identical). In the following proof we argue in $\mathsf {PZF}$ .

Define first the formula $\varphi$ to be:

$$\begin{aligned}&\big (f=\emptyset \wedge g = \{\langle 0,t_i \rangle \} \big )\ \vee \\&\big ( f\ne \emptyset \wedge g = f \cup \{\langle {\mathsf {dom}} \langle f \rangle ,t_s\{{\mathsf {dom}} \langle f \rangle /n ,f({\mathsf {dom}} \langle f \rangle -1)/p\} \rangle \} \big ) \end{aligned}$$

Informally, we set g to be the finite sequence achieved from the finite sequence f by expanding the domain of f by 1 according to the “step function” $t_s$. Obviously $\varphi \succ _{{\mathsf {PZF}^{\mathsf {U}}}}\{g\}$. Let

$$ X=\{ g \mid g=\{\langle 0,t_i \rangle \} \vee \exists f. f = \emptyset \wedge ({\mathsf {TC}}_{f,g}\varphi )(f,g)\} $$

and define $t_\mathsf {rec}= \cup X$. Obviously $t_\mathsf {rec}$ is a term of $\mathsf {PZF}$.

Let $x_1 ,\ldots ,x_n$ be n sets. We observe first that for all $g \in X$ it holds that:

$$\begin{aligned} \mathsf {seqFin}[g] \wedge g(0)=t_i \wedge \forall n \in {\mathsf {dom}} \langle g \rangle . n>0 \rightarrow g(n)=t_s\{g(n-1)/p\} \end{aligned}$$

(5)

The proof is by a straightforward application of the induction rule for the ${\mathsf {TC}}$ operator.

Next we prove that ${\mathsf {func}} [t_\mathsf {rec}]$. Since every $g \in X$ is a function s.t. ${\mathsf {dom}} \langle g \rangle \subseteq {\mathbb {N}}$, it is obvious that ${\mathsf {rel}} [t_\mathsf {rec}]$, and that ${\mathsf {dom}} \langle t_\mathsf {rec} \rangle \subseteq {\mathbb {N}}$. Therefore it suffices to show by induction on n that

$$ \forall n \in {\mathbb {N}}\, \forall g,g' \in X. n \in {\mathsf {dom}} \langle g \rangle \cap {\mathsf {dom}} \langle g' \rangle \rightarrow g(n) = g'(n) $$

If $n=0$ then by (5), $g(0) = g'(0) = t_i$. Assume that $n>0$. Since $n \in {\mathsf {dom}} \langle g \rangle \cap {\mathsf {dom}} \langle g' \rangle$ and since $\mathsf {seqFin}[g] \wedge \mathsf {seqFin}[g']$, $n-1 \in {\mathsf {dom}} \langle g \rangle \cap {\mathsf {dom}} \langle g' \rangle$. By the induction hypothesis, $g(n-1) = g'(n-1)$, hence by (5), $g(n) = g'(n) = t_s$, and overall $t_\mathsf {rec}$ is a function.

We prove now by induction on n that $\forall n\in {\mathbb {N}}. n\in {\mathsf {dom}} \langle t_\mathsf {rec} \rangle$ (and hence ${\mathsf {dom}} \langle t_\mathsf {rec} \rangle ={\mathbb {N}}$). Let $g_0=\{\langle 0,t_i \rangle \}$. Since $\varphi \{\emptyset /f,g_0/g\}$, it holds that $g_0\in X$ and hence $0 \in {\mathsf {dom}} \langle t_\mathsf {rec} \rangle$. Assume that $n \in {\mathsf {dom}} \langle t_\mathsf {rec} \rangle$. Then there exists $g \in X$ s.t. $n \in {\mathsf {dom}} \langle g \rangle$. If $n+1 \in {\mathsf {dom}} \langle g \rangle$ we are done. Otherwise, let $g' :=g \cup \{\langle n+1 , t_s\langle n+1 , g(n) , \bar{x} \rangle \rangle \}$. Obviously $\varphi \{g/f,g'/g\}$, hence $g' \in X$, and hence $n+1 \in {\mathsf {dom}} \langle g \rangle$ as desired.

Overall we proved (1) ($t_\mathsf {rec}$ is a function with domain ${\mathbb {N}}$). Proving (2) is done by (5) and a straightforward ${\mathsf {TC}}$-induction.

Proof

(part of the proof of Proposition 2). We sketch the proof for $\mathsf {cauchySeq}[a] \rightarrow \mathsf {converge}[a]$. So assume that $\mathsf {cauchySeq}[a]$. It is straightforward to show that a is bounded. We prove that $\mathsf {liminf}\langle a \rangle =\mathsf {limsup}\langle a \rangle$. It is straightforward to show that $\mathsf {liminf}\langle a \rangle \subseteq \mathsf {limsup}\langle a \rangle$ (even without any assumption on a). Assume for contradiction that $\exists q \in \mathsf {limsup}\langle a \rangle \setminus \mathsf {liminf}\langle a \rangle$. Since $\mathsf {dedCut}[\mathsf {limsup}\langle a \rangle ]$ and $\mathsf {dedCut}[\mathsf {liminf}\langle a \rangle ]$ it also holds that

$$\begin{aligned} \exists q,q',q'' \in {\mathbb {Q}}. q<q'<q'' \wedge q,q',q'' \in \mathsf {limsup}\langle a \rangle \setminus \mathsf {liminf}\langle a \rangle . \end{aligned}$$

Let $\varepsilon = q''-q'$. Since $\mathsf {cauchySeq}[a]$, there exists $N \in {\mathbb {N}}$ s.t.

$$\begin{aligned} \forall m,k \ge N. |a(m)-a(k)| < \varepsilon . \end{aligned}$$

(6)

Since $q' \notin \mathsf {liminf}\langle a \rangle$, there exists $k' \ge N$ s.t. $q' \notin a(k')$, and hence $a(k') \le q < q'$. Since $q'' \in \mathsf {limsup}\langle a \rangle$, there exists $k'' \ge N$ s.t. $q'' \in a(k'')$, and hence $q'' < a(k'')$. Putting it together, it holds that

$$\begin{aligned} a(k')< q'< q'' < a(k'') \end{aligned}$$

Hence $|a(k'')-a(k')| > q''-q' = \varepsilon$, that contradicts (6).

Proof

(proof of Proposition 3 ).

By Proposition 2-(1) it follows that $\mathsf {converge}[a,\mathsf {limit}\langle a \rangle ]$. Since the term $\mathsf {limit}\langle \cdot \rangle$ is a term of $\mathcal{{L}}_\mathsf {PZF}$), and since $a \in \mathsf {U}$, by the $\mathsf {U}$-closure scheme it holds that $\mathsf {limit}\langle a \rangle \in \mathsf {U}$. Hence not just $\mathsf {dedCut}[\mathsf {limit}\langle a \rangle ]$ (Proposition 1), but also $\mathsf {limit}\langle a \rangle \in {\mathbb {R}}$, and the claim follows.

1.1 A.1 Uniformly Convergence and Power Series

In this section we want to talk about sequences of (real) functions. We use the standard procedure of Currying. Define the following:

Definition 13

( ${\mathsf {PZF}^{\mathsf {U}}}$ )(sequence of functions).

• ${\mathsf {seqFunc}}[F] :={\mathsf {func}} [F] \wedge {\mathsf {dom}} [F]={\mathbb {N}}\times {\mathbb {R}}\wedge {\mathsf {rng}} \langle F \rangle \subseteq {\mathbb {R}}$.

• ${\mathsf {uniformlyConvergence}}[F,f] :={\mathsf {seqFunc}}[F] \wedge {\mathsf {func}} [f,{\mathbb {R}},{\mathbb {R}}] \wedge \forall \varepsilon \in {\mathbb {R}}^+ \, \exists N \in {\mathbb {N}}\, \forall x \in {\mathbb {R}}\, \forall n \ge N. |F(n,x)-f(x)| < \varepsilon$.

Proposition 6

(${\mathsf {PZF}^{\mathsf {U}}}$). Assume that ${\mathsf {uniformlyConvergence}}[F,f]$. Then:

• 1. $\forall x \in {\mathbb {R}}. \mathsf {converge}[\lambda n \in {\mathbb {N}}. F(n,x),f(x)]$.

• 2. $\forall x \in {\mathbb {R}}. \mathsf {limit}\langle \lambda n \in {\mathbb {N}}.F(n,x) \rangle = f(x)$.

Proof

• 1. Let $x \in {\mathbb {R}}$. From ${\mathsf {uniformlyConvergence}}[F,f]$ it follows that $\forall \varepsilon \in {\mathbb {R}}^+ \, \exists N \in {\mathbb {N}}\, \forall x \in {\mathbb {R}}\, \forall n \ge N. |F(n,x)-f(x)| < \varepsilon$. Hence $\forall \varepsilon \in {\mathbb {R}}^+ \, \exists N \in {\mathbb {N}}\, \forall n \ge N. |F(n,x)-f(x)| < \varepsilon$, and hence $\mathsf {converge}[\lambda n \in {\mathbb {N}}. F(n,x),f(x)]$ as desired.

• 2. It follows immediately from previous item and Proposition 2-(2).

Proposition 7

(${\mathsf {PZF}^{\mathsf {U}}}$). Assume that: ${\mathsf {uniformlyConvergence}}[F,f]$, ${\mathsf {Ufunc}}[F]$, and that $\forall n \in {\mathbb {N}}. {\mathsf {continuous}}[\lambda x\in {\mathbb {R}}.F(n,x)]$. Then ${\mathsf {continuous}}[f]$.

Proof

For every $x\in {\mathbb {R}}$, condition (3) of Definition 11 is proved in the usual way. It remains to prove that ${\mathsf {Ufunc}^{\mathbb {R}}}[f]$ holds. Since ${\mathsf {Ufunc}}[F]$, and since for every $x \in {\mathbb {R}}$, ${\mathbb {N}}\times \{x\} \in \mathsf {U}$, it follows that $F \upharpoonright {\mathbb {N}}\times \{x\} \in \mathsf {U}$ and hence for every $x\in {\mathbb {R}}$,

$$\begin{aligned} \lambda n \in {\mathbb {N}}.F(n,x) = \lambda n \in {\mathbb {N}}.(F \upharpoonright {\mathbb {N}}\times \{x\})(n,x) \in \mathsf {U}. \end{aligned}$$

(7)

Let $A \in {\mathsf {P}^{{\mathbb {R}}}}$. By Proposition 6-(2),

$$ f \upharpoonright A = \lambda x \in A.f(x) = \lambda x \in A. \mathsf {limit}\langle \lambda n \in {\mathbb {N}}.F(n,x) \rangle $$

and by Proposition 6-(1) for every $x \in A$, the sequence $\lambda n \in {\mathbb {N}}.F(n,x)$ converges. By (7), for every $x \in A$, $\lambda n \in {\mathbb {N}}.F(n,x) \in \mathsf {U}$, and since $\mathsf {limit}\langle \cdot \rangle$ maps convergent sequences from $\mathsf {U}$ to real numbers (in $\mathsf {U}$), we conclude that

$$ \lambda x \in A. \mathsf {limit}\langle \lambda n \in {\mathbb {N}}.F(n,x) \rangle \in \mathsf {U}$$

and the claim follows.

Remark 8

To ease notations, Definition 13 and hence Proposition 7 deal only with sequences of functions from ${\mathbb {R}}$ to ${\mathbb {R}}$. However, it can easily be extended to deal with sequences of functions from open segments to ${\mathbb {R}}$.

Definition 14

(${\mathsf {PZF}^{\mathsf {U}}}$)(Series). Define the following term that maps sequences $a \in \mathsf {U}$ such that $\mathsf {converge}[\lambda n\in {\mathbb {N}}.\sum _{k=0}^{n} a(k)]$ to their sum:

$$ \mathsf {series}\langle a \rangle :=\mathsf {limit}\langle \lambda n\in {\mathbb {N}}.\sum _{k=0}^{n} a(k) \rangle .$$

We denote $\mathsf {series}\langle a \rangle$ by the usual convention $\sum _{k=0}^{\infty } a(k)$.

Proposition 8

( ${\mathsf {PZF}^{\mathsf {U}}}$ )(Power Series).

Let $a \in \mathsf {U}$ be a sequence, and let $c \in {\mathbb {R}}^+$. If $\mathsf {converge}[\lambda n \in {\mathbb {N}}.|a(n)| \cdot c^n]$, then $\forall x\in (-c,c). \mathsf {converge}[\lambda n\in {\mathbb {N}}.\sum _{k=0}^{n} a(k) \cdot x^k]$, and $\lambda x \in (-c,c).\sum _{k=0}^{\infty } a(k) \cdot x^k$ is continuous (on $(-c,c)$).

Proof

(proof of Proposition 8 ).

The proof that $\forall x\in (-c,c). \mathsf {converge}[\lambda n\in {\mathbb {N}}.\sum _{k=0}^{n} a(k) \cdot x^k]$ is standard hence omitted. Define the functions $f :=\lambda x \in (-c,c).\sum _{k=0}^{\infty } a(k) \cdot x^k$, and $F = \lambda n \in {\mathbb {N}}, \lambda x \in (-c,c).\sum _{k=0}^{n} a(k) \cdot x^k$. We wish to apply Proposition 7 to F and f, and conclude that ${\mathsf {continuous}}[f]$.

The proof for ${\mathsf {uniformlyConvergence}}[F,f]$ is also standard and omitted. By Proposition 5 and straightforward induction, it holds that

$$ \forall n\in {\mathbb {N}}. {\mathsf {continuous}}[\lambda x \in (-c,c).\sum _{k=0}^{n} a(k) \cdot x^k]. $$

It remains to prove that ${\mathsf {Ufunc}}[F]$. Let $X \in \mathsf {U}$ s.t. $X \subseteq {\mathbb {N}}\times {\mathbb {R}}$. By the closure properties of $\mathsf {U}$, it is obvious that $\big (\lambda \langle n,r \rangle \in X. \sum _{k=0}^{n} a(k) \cdot x^k \big ) \in \mathsf {U}$, and the claim follows.

Corollary 2

(${\mathsf {PZF}^{\mathsf {U}}}$). Let $a \in \mathsf {U}$ be a sequence of rational numbers. If for every $c \in {\mathbb {R}}^+$, $\mathsf {converge}[\lambda n \in {\mathbb {N}}.|a(n)| \cdot c^n]$, then $\forall x\in {\mathbb {R}}. \mathsf {converge}[\lambda n\in {\mathbb {N}}.\sum _{k=0}^{n} a(k) \cdot x^k]$, and $\lambda x \in {\mathbb {R}}.\sum _{k=0}^{\infty } a(k) \cdot x^k$ is continuous (on ${\mathbb {R}}$).

Proof

It is straightforward from previous proposition.

1.2 A.2 Elementary Functions

Define the following sequence:

$$ a^{\sin } = \lambda n\in {\mathbb {N}}. \left\{ \begin{array}{@{}ll} \frac{1}{n!} &{} \text { if } n \equiv 1 \pmod 4 \\ -\frac{1}{n!} &{} \text { if } n \equiv 3 \pmod 4 \\ 0 &{} \text { else } \\ \end{array} \right. $$

It is straightforward to show that for every $c \in {\mathbb {R}}^+$, $\mathsf {converge}[\lambda n \in {\mathbb {N}}.|a^{\sin }(n)| \cdot c^n]$. Hence by Corollary 2 the following function is continuous:

$$ \sin = \lambda x \in {\mathbb {R}}. \sum _{k=0}^{\infty } a^{\sin }(k) \cdot x^k $$

Similarly we can define the other trigonometric functions, the inverse trigonometric functions, the hyperbolic/inverse hyperbolic functions, the exponentiation, and the logarithmic functions. Using Corollary 2 or Proposition 8, we can then prove that those functions are continuous. (Note that not all of these functions have domain ${\mathbb {R}}$.) Next, we define the elementary functions to be all the functions obtained by adding, subtracting, multiplying, dividing, and composing any of the previously mentioned functions. By Proposition 5, we conclude that every elementary function is a continuous function.