10.6092/issn.1972-5787/4573
In [Arnon08, A framework for formalizing set theories based on the use of static set terms.] a new framework for formalizing mathematics was developed. The main new features of this framework are that it is based on the usual first-order set theoretical foundations of mathematics (in particular, it is type-free), but it reflects real mathematical practice in making an extensive use of statically defined abstract set terms of the form { x | p(i) }, in the same way they are used in ordinary mathematical discourse.In this paper we show how large portions of fundamental, scientifically applicable mathematics can be developed in this framework in a straightforward way, using just a rather weak set theory which is predicatively acceptable and essentially first-order. The key property of that theory is that every object which is used in it is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented interpretation of the theory. However, the development is not committed to such interpretation, and can easily be extended for handling stronger set theories (including ZF).
application/pdf
1972-5787
4573
1
en
Liron Cohen
Journal of Formalized Reasoning
safety relations
Formalizing Scientifically Applicable Mathematics in a Definitional Framework
Text.Serial.Journal
https://jfr.unibo.it/
9
QED 20th anniversary
2016-01-29
2014-12-17
2016-01-29
2016-12-23
53-70
JFR
Liron Cohen
2016/01/29
10.6092/issn.1972-5787/4573
53
Tel Aviv University
1972-5787
1
safety relations
en
70
Jeff Zucker. Formalization of classical mathematics in automath. Studies in Logic and the Foundations of Mathematics, 133:127--139, 1994.
Formalizing Scientifically Applicable Mathematics in a Definitional Framework
https://jfr.unibo.it/article/download/4573/5758
9
Formalizing Scientifically Applicable Mathematics in
a Definitional Framework
ARNON AVRON
School of Computer Science, Tel Aviv University

and
LIRON COHEN
School of Mathematical Sciences, Tel Aviv University


In [3] a new framework for formalizing mathematics was developed. The main new features of this
framework are that it is based on the usual first-order set theoretical foundations of mathematics
(in particular, it is type-free), but it reflects real mathematical practice in making an extensive
use of statically defined abstract set terms of the form {x | ϕ}, in the same way they are used in
ordinary mathematical discourse.
   In this paper we show how large portions of fundamental, scientifically applicable mathematics
can be developed in this framework in a straightforward way, using just a rather weak set theory
which is predicatively acceptable and essentially first-order. The key property of that theory is
that every object which is used in it is defined by some closed term of the theory. This allows for
a very concrete, computationally-oriented interpretation of the theory. However, the development
is not committed to such interpretation, and can easily be extended for handling stronger set
theories (including ZF ).




1.   INTRODUCTION
While formalized mathematics and mathematical knowledge management (MKM)
are bound to ultimately have a huge impact on the culture of mathematical practice
and education, the past decades have unfortunately seen an increasing estrangement
between the reality of informal mathematical practice and computer-implemented
theorem proving. On one hand, type-free set theory is viewed by most mathemati-
cians as the foundation of the mathematics they practice, and as such it is the most
natural framework for MKM, especially for goals like those of the AUTOMATH
project ([30, 23, 9]) and the QED manifesto ([5, 29]). On the other hand, most of
the current work in the field of formalized mathematics and MKM is devoted to
approaches and systems that are rather different from the set theoretical one. It
either employs sophisticated type theories, with different notions of constructibil-
ity and computation that move more and more away from the common ground of
“standard” mathematics and its standard first-order foundations (like in Coq [6, 7]
or Nuprl [8]), or it uses various fractions of higher-order logic which are able to
cover relevant parts of mathematics, without ever aiming at the full spectrum (like
in Isabelle/HOL [24]).1

1 Two notable exceptions are Mizar [25, 26] and Metamath [21]. However, the approaches used
there are very different from the one we are going to use in this work.


                                        Journal of Formalized Reasoning Vol. 9, No. 1, 2016 Pages 53–70.
   We believe that the use for MKM of convenient set-theoretical frameworks could
help overcome this increasing rift between what most mathematicians consider to
be the basis of mathematics and what existing formal-reasoning systems actually
implement, and will allow mathematics to be formalized and managed in as natural
terms as possible. However, for doing this satisfactorily one should tackle the serious
gaps that exist between the “official” formulations of set theory (such as Zermelo-
Fraenkel Set Theory ZF ) and actual mathematical practice. In particular: the
language of such a framework should provide strong, direct means for defining
objects, akin to those used in informal mathematical texts.
   In [3] a new framework of the above sort for formalizing mathematics was devel-
oped. Its main advantages are that it is close in spirit and formulation to ZF on one
hand, while the language it employs has great definitional power on the other (yet
this language includes nothing that is not used in ordinary mathematical discourse).
In particular: the language is type-free, and makes an extensive use of abstract set
terms of the form {x | ϕ}. A crucial property of those terms is that unlike those
used in current mathematical texts, their introduction does not depend on proving
first corresponding existence theorems. Instead they are statically defined in a pre-
cise formal way (using the mechanism of safety relations). This feature makes the
framework a congenial environment for practicing standard mathematics, which is
also appropriate for mechanical manipulations and for interactive theorem proving.
  The work reported in this paper is a part of a project which has two main goals:
(1) The first is to explore what parts of “everyday” mathematics can be carried
    out within the framework suggested in [3], in a way that reflects how rigorous
    mathematics is (informally) presented in standard textbooks.
(2) In [10, 11, 12] it was forcefully argued by Feferman that already predicative
    mathematics suffices for developing all of scientifically applicable mathemat-
    ics, i.e. the mathematics that is actually indispensable to present-day natural
    science. This 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 second goal of our project is
    to show that this definitional approach to mathematics can be implemented in
    a user friendly way, without essential conflicts with mathematical practice.
   The goal of this paper is to examine to what extent the above goals can be
achieved within the above-mentioned framework when we restrict ourselves to the
first-order level, and use a rather weak, predicatively acceptable, set theory. We
show that large portions of fundamental scientifically applicable mathematics can
be straightforwardly formalized in such a theory. The key feature of the theory
we investigate is that it is definitional in the sense that every object which is used
is defined by some closed term of the theory. This allows for a very concrete,
computationally-oriented interpretation of the theory. However, the development
is not committed to such interpretations, and the framework can easily be extended
for handling stronger set theories (including ZF ).
   The paper is organized as follows: In Section 2 we present the basic language
and theory. In Section 3 we show how the standard set theoretical notions are
dealt with in our system. Section 4 introduces the natural numbers in our frame-
work. In Section 5 we outline how classical analysis can be developed within the
                                            54
resulting framework in a natural, predicatively acceptable way. This includes the
introduction of the real line and functions, and formulating and proving the main
classical results concerning these notions. We conclude with directions for future
continuation of the work.

2.   THE LANGUAGE LC
                   RST AND THE SYSTEM RST
                                          C

 We start by recalling the most basic formal systems for set theory presented in [4, 3].
 To avoid confusion, we use different kinds of parentheses for collections in our formal
 language and in the meta-language in which the paper is written. The parentheses
◦{ }◦ will be used in our formal languages LC  RST , while for a collection defined in
 the meta-language we use { }. We use uppercase letters X, Y, Z, ... for collections
 in the meta-language, Φ, Θ for sets of variables, and x, y, z, ... for variables in the
 formal
    n     languages.
               o     We denote by F v(exp) the set of free variables of exp, and by
     t1        tn
ϕ    x1 , ..., xn   the result of simultaneously substituting ti for the free occurrences
of xi in ϕ (i = 1, ..., n). Note that at present we take the meta-language to be the
language of ZF or more correctly GB [22], and the theorems to follow can all be
formulated and proven in GB. However, we believe that this can also be done in
weaker systems. This is left for further work.
   One of the foundational questions in set theory is which formulas should be
excluded from defining sets by an abstract term of the form {x | ϕ} in order to avoid
the paradoxes of naive set theory. More generally, the question is: what formulas
can be taken as defining a construction of a set from given objects (including other
sets)? Various set theories provide different answers to this question. Usually
these answers are based on semantical considerations (such as the limitation of
size doctrine [13, 15]). 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 [1, 3, 4].
   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 {x | ϕ}, provided that ϕ is safe with respect
to {x}. Intuitively, a statement of the form “ϕ is safe with respect to {y1 , ..., yk }”,
where F v(ϕ) = {x1 , ..., xn , y1 , ..., yk }, has the meaning that for every “accepted” sets
a1 , ..., an , the collection {hy1 , ..., yk i | ϕ(a1 , ..., an , y1 , ..., yk )} is an “accepted” set,
which is constructed from the previously “accepted” sets a1 , ..., an . Predicatively
(or definitionally) acceptable safety relations are those which determine the sets
they define in an absolute way, independently of any “surrounding universe”.
Definition 1. Let C be a finite set of constants. The language LC    RST and the
associated safety relation C are simultaneously defined as follows:
—Terms:
 —Every variable is a term.
 —Every c ∈ C is a term (taken to be a constant).
 —If x is a variable and ϕ is a formula such that ϕ C {x}, then ◦{x | ϕ◦
                                                                        } is a term
                   ◦x | ϕ◦
   (for which F v ({     }) = F v (ϕ) − {x}).
—Formulas:
 —If t and s are terms, then t = s and t ∈ s are atomic formulas.
                                                  55
 —If ϕ and ψ are formulas and x is a variable, then ¬ϕ, (ϕ ∧ ψ) , (ϕ ∨ ψ), and
  ∃xϕ are formulas.
—The safety relation C is defined as follows:
 —If ϕ is an atomic formula, then ϕ C ∅.
 —If t is a term such that x ∈ / F v (t), and ϕ ∈ {x ∈ x, x ∈ t, x = t, t = x}, then
  ϕ C {x}.
 —If ϕ C ∅, then ¬ϕ C ∅.
 —If ϕ C Θ and ψ C Θ, then ϕ ∨ ψ C Θ.
 —If ϕ C Θ and ψ C Φ, and either Φ ∩ F v (ϕ) = ∅ or Θ ∩ F v (ψ) = ∅, then
   ϕ ∧ ψ C Θ ∪ Φ.
 —If ϕ C Θ and y ∈ Θ, then ∃yϕ C Θ − {y}.
In case C = ∅ we write LRST instead of L∅RST and  instead of ∅ .
Remark 2. The notion of a term being free for substitution in LC      RST has to be
generalized, since in LCRST , unlike in first-order logic, a variable can be bound
within a term. The generalization amounts to avoiding the capture of free variables
within the scope of a binding operator.
Remark 3. It is easy to see that C has the following properties:
—If ϕ C Θ and Φ ⊆ Θ, then ϕ C Φ.
                             / F v (ϕ), then ϕ xy C Θ − {x} ∪ {y}.
                                               
—If ϕ C Θ, x ∈ Θ, and y ∈
—If ϕ C Θ and x ∈ Θ , then ϕ xt C Θ − {x}.
                                   

                     / Θ , then ϕ xt C Θ − F v (t).
                                   
—If ϕ C Θ and x ∈
—If ϕ C {x1 , ..., xn } and ψ C ∅, then ∀x1 , ..., xn (ϕ → ψ) C ∅. 2
—If x ∈
      / F v (t) and ϕ C ∅, then ∀x (x ∈ t → ϕ) C ∅ and ∃x (x ∈ t ∧ ϕ) C ∅.
 Hence, ϕ C ∅ for every ∆0 formula in LZF .
Definition 4. The system RST C is the first-order system in LC
                                                             RST which is based
on the following axioms:
—Extensionality: ∀z (z ∈ x ↔ z ∈ y) → x = y
—The Comprehension Schema: ∀x (x ∈ ◦{x | ϕ◦ } ↔ ϕ)
                            ∀x ∀y y ∈ x → ϕ xy → ϕ → ∀xϕ
                                                 
—The ∈-induction Schema:
Note. As explained in [3], with the exception of the infinity axiom (which will be
handled in the sequel), the other comprehension axioms of ZF can be incorporated
by adding corresponding clauses to the definition of the safety relation:
—The full power of the separation scheme can be achieved be assuming that ϕ C ∅
 for any ϕ (not only atomic ones).
                                                                     / F v {t}3 .
—The power set axiom is equivalent to letting x ⊆ t C {x} in case x ∈
—The full power of replacement is achieved by letting ∃yϕ ∧ ∀y (ϕ → ψ) C Θ if
 ψ C Θ and Θ ∩ F v (ϕ) = ∅.

2 Though  LC
           RST officially does not include ∀ and →, we take ∀x (ϕ → ψ) as an abbreviation for
¬∃x (ϕ ∧ ¬ψ).
3 Here we can take the usual definition of ⊆ in terms of ∈. However, it will be better to add ⊆ as

a new primitive symbol, together with the corresponding axiom connecting it to ∈.
                                               56
Definition 5. A universe (of sets) is a transitive collection of sets which is closed
under rudimentary operations [14, 18].4
Notation. We denote by v [x := a] the x-variant of v which assigns a to x. If ~x, →  −
                                                                                     a are
two vectors of the same length we abbreviate v [x1 := a1 , ..., xn := an ] by v [~x := →
                                                                                       −
                                                                                       a ].
                                                          →
                                                          −
We denote by [x := a , ..., x := a ] (or just by [~x := a ]) any assignment which
                    1     1       n       n
assigns to each xi the element ai .
Definition 6. Let W be a universe which interprets all the constants in C, and let
v be an assignment in W . For any term t and formula ϕ of LC  RST , we recursively
          v                                           v
define ktkW (designed to be an element of W ) and kϕkW ∈ {t, f } by:
        v
—kxkW = v (x) for x a variable.
    v
—kckW = cW (the interpretation of c in W ) for c ∈ C.
              n                            o
          v                     v[x:=a]
  ◦x | ϕ◦
—k{     }kW = a | a ∈ W ∧ kϕkW          =t
            v             v           v             v             v        v
—kt = skW = t iff ktkW = kskW ; kt ∈ skW = t iff ktkW ∈ kskW
      v             v
—k¬ϕkW = t iff kϕkW = f
          v           v         v
—kϕ ∧ ψkW = t iff kϕkW = t ∧ kψkW = t
          v           v         v
—kϕ ∨ ψkW = t iff kϕkW = t ∨ kψkW = t
                                        
        v                      v[x:=a]
—k∃xϕkW = t iff ∃a a ∈ W ∧ kϕkW        =t
                v                                                                             v
Remark. ktkW denotes the value in W that the term t gets under v, and kϕkW
denotes the truth value of the formula ϕ under W and v.
Proposition 7. Let W be a universe which interprets all the constants in C. If t
                                                        v
is a term of LC
              RST , then for any assignment v in W , ktkW is an element of W .

 Proof. The proof is carried out by simultaneous induction on terms t and for-
mulas ϕ, where for the latter we prove the following for any assignment v in W :
                                                                         y :=→
                                                                             −
                                                                                  
                                                                      v [~   a]
—If ϕ C {y1 , ..., yn } and n > 0, then ha1 , ..., an i ∈ W n | kϕkW           = t ∈ W.

                                                              y :=→
                                                                  −
                                                                         
                                                   n       v [~   a]
—If ϕ C ∅ and X ∈ W then ha1 , ..., an i ∈ X | kϕkW                 = t ∈ W.

It is straightforward to see that the result holds when t is a variable or a constant. If
t is of the form ◦{x | ϕ◦
                        } the claim follows from the induction hypothesis for ϕ (since
ϕ C {x}). For atomic formulas the claim easily follows from the induction hy-
pothesis for terms and the fact that W is closed under rudimentary operations. For
ϕ a compound formula the claim again holds since W is closed under rudimentary
operations. We demonstrate the most difficult case as an example. So assume that
ϕ = ψ∧θ, where ψ C Θ, θ C Φ, and Φ∩F v (ψ) = ∅. To simplify notation, assume
that F v (ψ) = {x, z}, F v (θ) = F v (ϕ) = {x,n y, z}, Θ = {x}, and Φ = {y}. oIn this
                                                                       v[x:=a,y:=b]
case ϕ C {x, y}, and we show that D = ha, bi ∈ W 2 | kϕkw                            = t ∈ W.

4 The standard notion is “rudimentary function”. We prefer to use instead the term “rudimen-
tary operation”, since we want to reserve the term “function” for functions in the sense used in
basic courses in set theory or discrete mathematics, i.e. sets of ordered pairs which satisfy the
functionality condition.
                                               57
                             n                        o
                                           v[x:=a]
Since ψ C {x} we have that a ∈ W | kψkW           = t ∈ W for any v. In par-
                           n                            o
                                         [x:=a,z:=c]
ticular, for any c ∈ W Ac = a ∈ W | kψkW             = t ∈ W . Since θ C {y},
n the induction hypothesis weo have that for any c ∈ W , if d ∈ Ac then Bc,d =
by
               [x:=d,y:=b,z:=c]
 b ∈ W | kθkW                     = t ∈ W . Now, D equals to ∪ ({d} × Bc,d ). Hence
                                                                    d∈Ac
the closure of W under rudimentary operations implies that D ∈ W .
Notation. In case exp is a closed term or a closed formula we denote by kexpkW
the value of exp in W , and at times we omit the W and simply write kexpk.
Proposition 8. Every universe is a model of RST C .5
  Proof. Easily follows from Prop. 7.
Note. The converse of the last proposition is also true, i.e., any transitive collection
of sets which is a model of RST C is a universe (see [2]).6
  The following simple lemma will be useful in the sequel.
Lemma 9 (Substitution Theorem). Let t, s1 , ..., sn be terms and ϕ a formula of
LC
 RST . If v is an assignment in W , then:
                     o v      v [x1 :=ks1 kv                 v
                                            W ,...,xn :=ksn kW ]
    n
— t xsii , ..., xsnn     = ktkW
                       W
                     o v         v [x1 :=ks1 kv                v
                                              W ,...,xn :=ksn kW ]
     n
       si         sn
— ϕ xi , ..., xn         = kϕkW
                      W

   Next we want to show that the meaning of terms in LC
                                                      RST is actually independent
of W . The following theorem is a more precise and more general formulation of a
theorem proven in [4].
Theorem 10. Let W1 , W2 be two universes which agree on the interpretations of
all c ∈ C.
(1 ) If v1 , v2 are assignments in W1 and W2 respectively that agree on the values of
                                                 v        v
     all the free variables in a term t, then ktkW11 = ktkW22 .
(2 ) If v1 , v2 are assignments in W1 and W2 respectively that agree on the values of
                                                      v         v
     all the free variables in a formula ϕ, then kϕkW11 = kϕkW22 .
  Proof. The proof is carried out by simultaneous induction on t and ϕ (similar
to the proof in [4]).
Theorem 10 entails that every term of LC  RST has the same interpretation in all
transitive models of RST C (i.e. universes) which contains the values of its pa-
rameters and interprets the constants in C in the same way. Thus the identity of
the set denoted by a term t is independent of the exact extension of the assumed
surrounding universe of sets. A formula is safe with respect to {x1 , ..., xn } if it
has the same extension (which should be a set) in all universes which contains the

5 The more precise formulation of the proposition is as follows: Let W be a universe. By assigning
the obvious interpretations to the symbols ∈ and = and assigning some interpretations in W for
the constants in C, we get a model of RST C .
6 The system in [2] was RST , however, the addition of the constants C does not make a difference.


                                               58
values of its other parameters. In particular: ϕ C ∅ iff it is absolute relative to
RST C in the usual sense of set theory (see e.g. [19]), while ϕ C F v (ϕ) iff it is
domain-independent in the sense of database theory (see e.g. [27]) for universes.
Note again that a universe is here any transitive collection of sets which is closed
under rudimentary operations. For instance, we can take W to be V , the cumu-
lative universe of ZF (with the obvious interpretations of the symbols ∈ and =)7 .
We can also take W to be Vκ for any κ such that Vκ is a universe. However, W
can also be taken as a much smaller, and very concrete set. Thus in [28], J2 (the
second set in Jensen’s constructible hierarchy) was implicitly chosen. This is in fact
the minimal universe which includes an infinite set. Still, for our purposes bigger
constructible sets, like Jω or Jωω , are better choices.
Definition 11.
—If t is a closed term we say that t defines the set ktkW . The set X is called
 definable if there is a closed term t such that ktkW = X.
—If t is a term with F v (t) ⊆ {x1 , ...xn } we say that t defines the operation Ft that
                                                    [x :=A ,...,xn :=An ]
 for any hA1 , ..., An i ∈ W n returns the set ktkW1 1                    .
Note. We use above the term “operation” because Ft might be a proper class of
ordered pairs. (The existence of such class for every term t can be proved in GB.)
Terminology. From now on we use the term “operation" for functions on the entire
universe which are defined by some term.
Notation. If s is a term free for substitution for x in t, and Ft is an operation      we
write F̂t (s) instead of t xs . Hence F̂t (s) = y is an abbreviation for t xs = y,
                                                                               

and so if y ∈/ F v (t) ∪ F v (s) \ {x}, then F̂t (s) = y C {y}. (Intuitively, F̂t (s) = y
means that the result of the application of the operation Ft to the object denoted
by s is the object denoted by y.)
  The following theorem is also proven in [4].
Theorem 12. If F is an n-ary rudimentary operation, then there exists a formula
ϕF such that:
—F v (ϕF ) ⊆ {y, x1 , ..., xn }.
—ϕF C {y}.
—F (x1 , ..., xn ) = {y | ϕF }.
Corollary 13. Every rudimentary operation is indeed an operation in the sense
defined above (i.e., is definable by some term of LC
                                                   RST ).

3.     BASIC SET THEORETICAL NOTIONS
In LC
    RST we can introduce as abbreviations many standard notations used in math-
ematics and prove their basic properties in RST C . Here are some examples:
—∅ := ◦{x | x ∈ x◦    }.
 ◦t1 , ..., tn}◦ := ◦{x | x = t1 ∨ ... ∨ x = tn}◦ (where x is fresh).
—{

7 As for the constants in C we will use in this paper, each of them will have some obvious intended
interpretation too.
                                                59
—hs, ti := ◦{◦{s◦
                }, ◦{s, t◦
                         }}◦. ht1 , ..., tn i := hht1 , ..., tn−1 i , tn i.
 ◦x ∈ t | ϕ◦
—{           } := ◦{x | x ∈ t ∧ ϕ◦     }, provided ϕ C ∅ and x ∈           / F v (t).
 ◦t | x ∈ s◦
—{          } := ◦{y | ∃x.x ∈ s ∧ y = t◦        }, where y is a fresh variable and x ∈ / F v (s).
—s × t := ◦{x | ∃a∃b.a ∈ s ∧ b ∈ t ∧ x = ha, bi }◦, where x, a, b are fresh.
—s ∪ t := ◦{x | x ∈ s ∨ x ∈ t◦      }, where x is fresh.
—s ∩ t := ◦{x | x ∈ s ∧ x ∈ t◦      }, where x is fresh.
—∪t := ◦{x | ∃y ∈ t.x ∈ y◦     }, where x, y are fresh.
—∩t := ◦{x | x ∈ ∪t ∧ ∀y ∈ t.x ∈ y◦          }, where x, y are fresh.
—ιx.ϕ := ∪{  ◦x | ϕ◦ }, provided ϕ C {x}.8
—dom (t) := ◦{x | ∃z∃v∃y.z ∈ t ∧ v ∈ z ∧ y ∈ v ∧ x ∈ v ∧ z = hx, yi }◦, where z, v, x,
 and y are fresh.
—rng (t) := ◦{y | ∃z∃v∃x.z ∈ t ∧ v ∈ z ∧ y ∈ v ∧ x ∈ v ∧ z = hx, yi }◦, where z, v, x,
 and y are fresh.
  It is routine to verify that all these terms are indeed well-defined, and that their
basic properties are provable in RST C . For example, ∀x (x ∈ ∪t ↔ ∃y ∈ t.x ∈ y) is
a trivial consequence of the comprehension axiom and the definition of ∪t.

  The fact that hs, ti is a term in our language implies only that if z ∈
                                                                        / F v (t)∪F v (s)
then z = hs, ti C {z} and hs, ti = z C {z}. However, in [3] another formula was
constructed that states that t is equal to the ordered pair hr, si:
                   ˇ hr, si := ∃u∃v (P (t, u, v) ∧ P (u, r, r) ∧ P (v, r, s))
                  t=
where P (t, x, y) = x ∈ t ∧ y ∈ t ∧ ∀w (w ∈ t → w = x ∨ w = y) and w is a fresh
                           ˇ t the formula: ∃u ∈ t (u=
variable. Denote by hr, si ∈                            ˇ hr, si) where u is a fresh
variable which does not occur in t, r or s. The following is then proved in [3]:
Proposition 14.
      ˇ hx, yi C {x, y} provided x, y ∈
(1 ) t=                                 / F v (t).
            ˇ t C {x, y} provided x, y ∈
(2 ) hx, yi ∈                           / F v (t).
(3 ) `RST C r = hs, ti ↔ r= ˇ hs, ti
  Note that we can extract the first and second coordinate of a pair by
                                    ˇ hx, yi , P2 (z) := ιy.∃x.z =
                  P1 (z) := ιx.∃y.z =                            ˇ hx, yi
Proposition 15. {hx1 , ..., xn i | ϕ} is a definable set, provided ϕ C {x1 , ..., xn }
and F v (ϕ) ⊆ {x1 , ..., xn }.
   Proof. For z a fresh variable ∃x1 ...∃xn (ϕ ∧ z = hx1 , ..., xn i) C {z}, and {z} =
 F v (∃x1 ...∃xn (ϕ ∧ z = hx1 , ..., xn i)), thus {hx1 , ..., xn i | ϕ} is definable by the term
◦{z | ∃x1 ...∃xn (ϕ ∧ z = hx1 , ..., xn i) }◦.
Proposition 16. Let Ft be an operation. The result of the application of Ft to
definable sets is a definable set.

8 Due to the extensionality axiom, if ϕ C {x}, then the term above for ιx.ϕ denotes ∅ if there
is no set which satisfies ϕ, and it denotes the union of all the sets which satisfy ϕ otherwise. In
particular: if there is exactly one set which satisfies ϕ, then ιx.ϕ denotes this unique set.
                                                60
  Proof. Suppose F v (t) = {x1 , ..., xn }. If A1 , ..., An are definable sets then
there exist terms s1 , ..., sn that define them (respectively), and Ft (A1 , ..., An ) =
                            [x1 :=ks1 kW ,...,xn :=ksn kW ]
  n                 o
 t xs11 , ..., xsnn   = ktkW                                .
                 W
Corollary 17. The result of any application of a rudimentary operation to definable
sets is a definable set. In particular, if X, Y are definable sets, so are X ∪Y , X ∩Y ,
X − Y , X × Y , ∪X, ∩X, dom (X), and rng (X).

The standard definition of a set being a relation or a function are available in LRST
in the form of formulas which are safe w.r.t ∅.
—Rel (r) := ∀z ∈ r∃x, y.z =ˇ hx, yi
                                            ˇ f ∧ ha, ci ∈
—F unc (f ) := Rel (f ) ∧ ∀a, b, c. (ha, bi ∈            ˇf) → b = c
It is straightforward to prove the following:
Lemma 18. The standard operations on relations (such as: composition, inverse,
domain and range) are definable operations, and their basic properties are provable
in RST C .
  In LCRST we can also introduce as abbreviations standard notations for handling
functions as they are used in mathematics. For example:
—λx ∈ s.t := ◦{ hx, ti | x ∈ s◦
                              }, provided x ∈/ F v (s).
—f (x) := ιy. hx, yi ∈ˇ f where y is a fresh variable.
—f  s := ◦{ hx, f (x)i | x ∈ s◦
                               }
Proposition 19.
(1 ) The β and η rules obtain in RST C , i.e. the followings are provable in RST C :
                                         nuo
                u ∈ s → (λx ∈ s.t) u = t         where u is free for x in t
                                           x
                   u∈/ s → (λx ∈ s.t) u = ∅ where u is free for x in t
                           (λx ∈ s.t) x = t  s where x ∈
                                                        / F v (t)
(2 ) The following is provable in RST C :
                (F unc (f )) → (F unc (f  a) ∧ ∀x ∈ a.f (x) = (f  a) (x))
(3 ) Let f, g be variables. Then there exists a term g ◦ f s.t. F v (g ◦ f ) = {g, f }
     and the following is provable in RST C :
          (F unc (f ) ∧ F unc (g)) → (F unc (g ◦ f ) ∧ ∀x. (g ◦ f ) (x) = g (f (x)))
                                                       ˙ s.t. F v (g ∪f
(4 ) Let f, g be variables. Then there exists a term g ∪f            ˙ ) = {g, f } and
     the following is provable in RST C :
          (F unc (f ) ∧ F unc (g) ∧ Dom (f ) ∩ Dom (g) = ∅) → [F unc (g ∪f˙ )∧
                            ˙ ) (x) = f (x)) ∧ (∀x ∈ Dom (g) . (g ∪f
        (∀x ∈ Dom (f ) . (g ∪f                                    ˙ ) (x) = g (x))]
  Proof. The proofs are all straightforward. For example, in (3) we take g ◦ f to
                                   ˇ f ∧ hb, ci ∈
be the term ◦{z | ∃a, b, c. ha, bi ∈            ˇ g ∧ ha, ci = z◦
                                                                }.
                                            61
Proposition 20. If F is an operation (i.e. F = Ft for some term t), then:
—It is provable in RST C that for any set A, F  A is a function.
—If A is a definable set, so is F  A.
                                       D       E
 Proof. Denote by F  a the term ◦{ x, F̂ (x) | x ∈ a◦  } for a a fresh variable. It
is easy to prove in RST C that for any a, F  a is a binary relation which satisfies
the functionality condition. This proves the first part of the proposition. For the
second part, note that if there is a term sA that defines A then the closed term
(F  a) saA defines F  A.
Corollary 21 (Restricted axiom of replacement). If F is an operation, then:
—It is provable in RST C that the image of every set under F is a set.
—If A is a definable set, so is F [A].
  Proof. The first part easily follows by taking F [a] := rng (F  a). For the
second part of the claim, notice that if A is a definable set, so is F  A, and by
Corollary 17, so is rng (F  A).

4.   THE NATURAL NUMBERS
The collection of hereditary finite sets is the minimal model of RST C ; hence N (the
set of natural numbers) is not definable as a set in LC  RST . Therefore, in order to
introduce N as a set we need to extend our language and our system. There are
several ways to do this. One possible route is to extend the safety relation. However,
in order to do so while preserving the syntactical, compositional approach, one has
to extend the language as well. Since in this paper we want to stick to the first-
order level, this is best done by adding new constants together with corresponding
characterizing axioms.9 Thus, in this paper we enhance RST C by including in C
a constant whose intended interpretation is the set HF of all hereditary finite sets.
In addition, we add to RST C counterparts of Peano’s axioms which ensure (as far
as possible on the first-order level) that HF is indeed interpreted as this set.10
Conventions.
(1) In the rest of the paper we assume that C includes the constant HF .
(2) From now on we shall use the same symbols in the language and in the meta-
    language for standard sets, relations, functions and operations. Thus both
    the formal language and the meta-language will use HF to denote the set of
    hereditary finite sets, while N will be used to denote the set of natural numbers,
    as well the term which defines it in the formal language.
                               C
Definition 22. The system RSTHF  for the language LC
                                                   RST is obtained by adding
to RST C the following axioms:
(1) ∅ ∈ HF .

9A  different approach, which does not require additional axioms, but is based instead on going
beyond the first-order level, was described in [3].
10 The resulting system is still acceptable from the point of view of the Weil-Feferman predicativist

program, since this program accepts the natural numbers and the hereditary finite sets.
                                                 62
(2) ∀x∀y (x ∈ HF ∧ y ∈ HF → x ∪ ◦{y◦  } ∈ HF ).
(3) ∅ ∈ y ∧ ∀v, w ∈ y.v ∪ ◦{w◦
                             } ∈ y → HF ⊆ y.
  Next we prove the most characteristic properties of HF .
                                                  C
Proposition 23. The followings are provable in RSTHF :
(1 ) x ∈ HF ↔ x = ∅ ∨ ∃u, v ∈ HF.u ∪ ◦{v◦  } = x.
(2 ) (ϕ (∅) ∧ ∀x∀y (ϕ (x) ∧ ϕ (y) → ϕ (x ∪ ◦{y◦
                                              }))) → ∀x ∈ HF.ϕ (x) for ϕ C ∅.
        HF
(3 ) ψ a ∧ ∀a (ψ (a) → HF ⊆ y), where ψ (a) denotes the formula:
     ∀x (x ∈ a ↔ x = ∅ ∨ ∃u, v ∈ a.u ∪ ◦{v◦
                                          } = x)



  Proof.
(1) The first two axioms for HF imply x = ∅ ∨ ∃u, v ∈ HF.u ∪ ◦{v◦          } = x →
                                    C
    x ∈ HF is provable in RSTHF       . For the converse define B := ◦{x ∈ HF |
                                                                                C
    x = ∅ ∨ ∃u, v ∈ HF.u ∪ ◦{v◦   } = x◦ }. Clearly, there is a proof in RSTHF      for
    ∅ ∈ B ∧ ∀v, w ∈ B.v ∪ ◦{w◦     } ∈ B. Thus, by the third axiom of HF we
    get that ∀x ∈ HF.x ∈ B, which by the Axiom of Comprehension implies
    ∀x ∈ HF (x = ∅ ∨ ∃u, v ∈ HF.u ∪ ◦{v◦  } = x).
(2) Suppose ϕ (∅) ∧ ∀x∀y (ϕ (x) ∧ ϕ (y) → ϕ (x ∪ ◦{y◦ })). Take ◦{z ∈ HF | ϕ (z) }◦ for
    y. (This term is legal, since we assume that ϕ C ∅.) From the assumption and
    the first two axioms for HF it is easy to see that ∅ ∈ y ∧ ∀v, w ∈ y.v ∪ ◦{w◦
                                                                                } ∈ y.
    Therefore, by the third axiom for HF we get ∀x ∈ HF.x ∈ ◦{z ∈ HF | ϕ (z) }◦,
    which by the Axiom of Comprehension implies ∀x ∈ HF.ϕ (x).
(3) By part (1) of the proposition, we have ψ HF
                                                  
                                                    a   , and
                                                             by the third axiom for
    HF we can easily derive ∀z ψ az → ∀y ∈ HF.y ∈ z .


Note. Actually, Prop 23(2) can be proven for arbitrary ϕ. This can be done using
Prop. 28 below, whose proof in turn depends on the special case stated above.
Since we are not using this stronger version in the sequel, we omit the proof.
  Next we follow the standard construction of the natural numbers and encode
them in the following way:
                                      0 : = ∅,
                                   n + 1 : = S (n) ,
where S (n) = n ∪ ◦{n◦
                     }. It is easy to see that each n ∈ N is a definable set. Clearly
N is contained in the interpretation of HF .
Proposition 24. The set of natural numbers is a definable set.
  Proof. Denote by Ord (n) the formula T rans (n) ∧ Linear (n), where
           Linear (n) :=∀x∀y (x ∈ n ∧ y ∈ n → (x ∈ y ∨ y ∈ x ∨ x = y))
            T rans (n) :=∀x∀y (y ∈ n ∧ x ∈ y → x ∈ n)
It is easy to see that Ord (n) C ∅. Hence the set of natural numbers is definable
by the term N := ◦{n ∈ HF | Ord (n) }◦.
                                          63
                                            C
Lemma 25. The followings are provable in RSTHF :
(1 ) ∀a.Ord (a) → ∀z ∈ a.Ord (z)
(2 ) ∀a, b. (Ord (a) ∧ Ord (b)) → (a ∈ b ∨ b ∈ a ∨ a = b)
                                          C
Lemma 26. The following is provable in RSTHF :
              ∀x ∈ HF.x = ∅ ∨ ∃z ∈ x¬Ord (z) ∨ ∃z ∈ x.max (x) = z
where max (x) = z denotes the formula ∀w ∈ x.w ∈ z ∨ w = z.
  Proof. Let ϕ (x) be the formula x = ∅ ∨ ∃z ∈ x¬Ord (z) ∨ ∃z ∈ x.max (x) = z.
Then ϕ C ∅, and so we can prove ∀x ∈ HF.ϕ by induction on HF (Prop. 23(2)).
Clearly we have ϕ (∅). Assume ϕ (x) ∧ ϕ (y). We prove ϕ (x ∪ ◦{y◦    }). If x = ∅ then
max (x ∪ ◦{y◦
            }) = y, thus ϕ (x ∪ ◦{y◦}). If ∃z ∈ x¬Ord (z) then ∃z ∈ x ∪ {y} .¬Ord (z)
and again ϕ (x ∪ ◦{y◦}). Otherwise, we have that x 6= ∅ ∧ ∀z ∈ xOrd (z) ∧ ∃z ∈
x.max (x) = z. If y is not an ordinal then ∃z ∈ x ∪ {y} .¬Ord (z), otherwise, denote
by z0 the maximum of x. Then we have Ord (y) ∧ Ord (z0 ) and by Lemma 25(2) we
get y ∈ z0 ∨ z0 ∈ y ∨ y = z0 . If y ∈ z0 or y = z0 then max (x ∪ ◦{y◦
                                                                    }) = z0 , otherwise
the transitivity of y implies that max (x ∪ ◦{y◦ }) = y.
Proposition 27. `RSTHF
                    C  ∀n ∈ N.n = 0 ∨ ∃k ∈ n.n = S(k).
   Proof. Let n be an element in N. Then Ord (n) and n ∈ HF . By Lemma 25(1)
we get ∀z ∈ n.Ord (z). Hence Lemma 26 implies that n = ∅ ∨ ∃z ∈ n.max (n) = z.
If n = ∅ we are done. Otherwise, denote by z0 the maximum of n. We prove that
n = S (z0 ). If x ∈ n then x ∈ z0 (i.e. x ∈ z0 ∨ x = z0 ) by the maximality of z0 . For
the converse, assume x ∈ z0 . If x = z0 then clearly x ∈ n. If x ∈ z0 then by the
transitivity of n we again conclude that x ∈ n.
  The next proposition shows that we can prove within our formal system the full
induction rule of Peano’s arithmetics.
Proposition 28. `RSTHF
                    C  (ϕ (0) ∧ ∀x (ϕ (x) → ϕ (S (x)))) → ∀x ∈ Nϕ (x)
                                                                               C
  Proof. By ∈-induction, the following strong induction in N is provable in RSTHF :
            ∀x ∈ N ((∀y ∈ N (y ∈ x → ϕ (y))) → ϕ (x)) → ∀x ∈ N.ϕ (x)
From this the standard induction principle formulated above can easily be derived
with the help of Proposition 27.
Proposition 29. Let F be a binary operation which for elements of HF returns
                                             C
an element of HF . Then it is provable in RSTHF that for any A ∈ HF there is a
                    F
definable function HA with domain N s.t.
                             F
                            HA (0) = A
                             F                 F
                                                         
                            HA (S (n)) = F A, HA (n)
  Proof. By a well-known theorem (see, e.g., [16]), the proof of which can easily
                    C
be reproduced in RSTHF , it suffices to show that given a definable unary operation
                                                 F
F with the same property, there is a function HA   with domain N s.t.
                               F
                              HA (0) = A
                               F              F
                                                   
                              HA (S (n)) = F HA (n)
                                          64
 Let Seqf in (f ) stand for the formula F unc (f ) ∧ ∃m ∈ N.dom (f ) = S (m), and take
 F INaF to be:
                                                                D              E   
◦{f ∈ HF | Seqf in (f )∧h0, ai ∈ f ∧∀n < S (m) ∀z hn, zi ∈  ˇ f → S (n) , F̂ (z) ∈ f }◦
                  F
                             F INaF . Since A ∈ HF , there is a term tA which defines
                           S
 Next, define H   a to be
             F tA
                                                       F
 it. Then Ha a is a closed term which defines HA          .
Proposition 30. The following holds:
(1 ) The standard ordering ≤ on N is a definable relation.
(2 ) Any primitive recursive function is a definable function.
     Proof.
(1) The standard ordering < on N coincides with ∈. Thus the term ◦{ hm, ni | m ∈
    N ∧ n ∈ N ∧ (m = n ∨ m ∈ n) }◦ defines ≤ by Prop. 15.
(2) The result immediately follows from Prop. 29.



5.    THE REAL LINE
We now turn to real analysis. Once we have the natural numbers, it is straightfor-
ward to translate into our framework the standard constructions of Z (the integers)
and Q (the rationals), to define (as sets) the basic relations and functions on them
                                             C
(such as, <, +, ·), and to prove in RSTHF       their basic properties. Note that by
defining a relation like < as a set we not only mean that there is a formula ϕ that
defines it, but that there is a term t whose interpretation is the relation < taken
as a set of ordered pairs. This is equivalent to requiring that the defining formula
ϕ (x, y) is safe w.r.t. {x, y}.
   Next we define the real line using the standard construction of the real numbers
as Dedekind cuts (see, e.g. [20]). However, in our current language and system it
is again not possible to define the statement “x is a real number” using a formula
which is safe with respect to x. Therefore, much like in the case of the natural
numbers, in order to introduce the real numbers as a set we again extend our lan-
guage and our system. For this we include in C a new constant symbol U , to be
interpreted as an element of W that includes HF and is a universe (and so it is
closed under rudimentary operations). This imposes some constraints on W which
now must contain as an element both HF and some universe. The minimal such
W is J3 in which we can take the interpretation of U to be J2 . From a defini-
tional/computational/constructive point of view, a better choice for W might be
Jωω , the use of which is still justified from a predicative point of view (see [4]). In
Jωω one can use e.g. Jω as a sufficiently extensive interpretation of U .

In what follows C is any set of constants that includes both HF and U .
                               C
Definition 31. The system RSTHF,U for the language LC
                                                    RST is obtained by adding
       C
to RSTHF the following axioms:
(1) HF ∈ U .

                                          65
(2) ∀x∀y (x ∈ U ∧ y ∈ x → y ∈ U ).
(3) ∀y1 , ..., yn ∈ U.{
                      ◦x | ϕ◦
                            } ∈ U , provided ϕ C {x}, F v (ϕ) = {y1 , ..., yn }, and U
    does not occur in ϕ.11
Note. While for HF we have a unique interpretation, the interpretation of U is
deliberately left open to allow stronger extensions of the system. The development
of scientifically applicable mathematics which is outlined below is independent of
the interpretation of U .
   Now define ψ (u) := ∀x, y ∈ Q (x ∈ u ∧ y < x → y ∈ u), ϕ (u) := ¬∃x ∈ u∀y ∈
u.x ≤ y and θ (u) := u 6= Q ∧ u 6= ∅ ∧ ∀x ∈ u.x ∈ Q, where x ≤ y is an abbreviation
for x < y ∨ x = y. The formula ψ (u) states that u contains every rational num-
ber less than any rational number it contains, ϕ (u) states that u has no greatest
element, and θ (u) asserts that u is a non empty proper subset of Q. It is easy to
check that ψ (u) , ϕ (u) , θ (u) C ∅. This fact justifies our next definition.
Definition 32 (The reals R).
                           R = ◦{u ∈ U | θ (u) ∧ ψ (u) ∧ ϕ (u) }◦
 Note. It is important to notice that the interpretation of the term R in W may not
 be the “real” real-line (if such a thing really exists), as√it depends on the interpre-
 tation of U . However, standard real numbers such as 2, π,etc. are elements of R
 for any legal choice of W and any interpretation of U in it. For example, to see
 that π is a member of R it suffices to know that π is the interpretation of the term:
                            n              
                                  1      1
                           P
◦{r ∈ Q | ∃n ∈ N.r < 4 ·        4k+1 − 4k+3 }  ◦ (a variant of the Leibniz series).
                           k=0
  It is again straightforward to show that the standard ordering < on R and the
standard addition and multiplication of reals are definable elements of W , and to
               C
prove in RSTHF,U    that R equipped with them is an Archimedean ordered field.
                                                                       C
Next we show that the least upper bound principle is provable in RSTHF,U   .
                                        C
Proposition 33. It is provable in RSTHF,U    that every nonempty bounded subset of
R has a least upper bound. Also, the map that takes each nonempty bounded subset
of R to its least upper bound is an operation.
   Proof. Let X be a nonempty subset of R that is bounded above. ∪X is a
set that belongs to R since X is bounded above. Since the order relation ≤ coin-
cides with the inclusion relation, it follows that ∪X is a least upper bound for X.
Moreover, the mapping of X to ∪X is a rudimentary operation, and hence it is an
operation (by Corollary 13).
Next we show that we are able to express real recursive functions in our framework.
Proposition 34. Let F be an operation which for elements of U returns an element
of U . Then:

11 To be more precise, for a concrete C we should specify which other constants may occur in ϕ
or not. HF is always allowed. As for the other constants in C this will depend on their intended
interpretation. In this paper we may assume that C = {HF, U }.



                                              66
                      C                                            F
—It is provable in RSTHF,U that for any A ∈ U there is a function HA in U with
 domain N s.t.
                              F
                             HA (0) = A
                              F                 F
                                                          
                             HA (S (n)) = F A, HA (n)
                                F
—If A is a definable set, then HA is a definable function.
  Proof. The proof is similar to the proof of Prop. 29, replacing f ∈ HF by
f ∈ U in the definition of F INaF
Definition 35. Let X be a set. A sequence in X is a function with domain N
whose range is contained in X.
                                  C
Lemma 36. It is provable in RSTHF,U    that every Cauchy sequence in R converges
to a limit in R, and the map (lim) that takes a Cauchy sequence in R to its limit
is an operation.
  Proof. Let a be aTCauchy sequence, and let ak abbreviate a (k).
                                                                T For each
n ∈ N define vn :=  ak (by Prop. 34 there is a function for λn.   ak in U ).
                      k≥n                                                k≥n

            S bound of λn.vn is equal to the limit of λn.an (See [17]). Thus,
The least upper
lim λn.an := ◦{vn | n ∈ N◦
                         }.

Given sets X and Y , we next want to talk about sequence of functions from X
to Y . However, we cannot apply Definition 35 as is because the collection of all
functions from X to Y is not necessarily a set in our framework. Instead we use
the standard procedure of Currying.
Definition 37. Let X and Y be sets. A sequence of functions with domain X
and range contained in Y is a function F with domain N × X whose range is
contained in Y . (Intuitively, F denotes the sequence f (0) , f (1) , f (2) , ... where
f (n) = λx ∈ X.F̂ (n, x)).
                                                         C
Proposition 38. Let X ⊆ R be a set. It is provable in RSTHF,U  that any pointwise
limit of a sequence of functions with domain X whose range is contained in R is a
function.
  Proof. Let F be a sequence of functions with domain X whose range is con-
tained in R. Suppose that for each a ∈ X the sequence
                                                D     λn.F̂E(n, a) is converging,
and so is a Cauchy sequence. Define: Ga := ◦{ n, F̂ (n, a) | n ∈ N◦}. Then,
λa ∈ X.lim Ga (where lim is the operation defined in Lemma 36) is the desired
function.
                                                                C
Corollary 39. All elementary functions on R are available in RSTHF,U .
Note. We should be careful here as to what we mean by elementary functions on
                                                                            C
R. For example, by saying that all constant functions are available in RSTHF,U  we
                                                          C
mean that ∀y ∈ R.F unc (λx ∈ R.y) is provable in RSTHF,U      . This of course does
not mean that λx ∈ R.y exists in W for any “real” number y (in V ), but only for
those who are elements of the interpretation of U . Unfortunately, we find it very
difficult to express the exact intention of the proposition in a way which will be
                                          67
both precise and readable. Still, we trust the reader to understand the content of
the proposition.
                                                       C
   Proof. All polynomials on R are available in RSTHF,U     since + and · are func-
tions. Constant functions, the identity map on R, and compositions of functions are
                     C
also available in RSTHF,U  (as they are rudimentary operations and R is a definable
set). Hence, the proposition easily follows from Prop. 38.
Note. It is not difficult to see that many discontinuous functions (such as the jump
                                      C
function) are also available in RSTHF,U   .
                                                 C
  The next step is to define and prove in RSTHF,U      the basic properties of contin-
uous functions (such as the intermediate value theorem). Now the collection of all
                                                                           C
(continuous) functions from R to R is not available as a set in RSTHF,U        . Fortu-
nately, we do not need it for our current task. It suffices for it to have the property
of being a partial function from R to R definable in our language by a formula
which is safe with respect to ∅. This can be done by the formula:
              realF unc (f ) := F unc (f ) ∧ dom (f ) ⊆ R ∧ rng (f ) ⊆ R
Below is an example of a standard theorem about real functions, whose classical
                               C
proof can be reproduced in RSTHF,U  without any difficulty, using the completeness
                             C
of R which is provable in RSTHF,U (see Prop. 33).
Proposition 40 (Intermediate value theorem). Let
                           |a − b| < c := b − c < a < b + c

Cont (f ) := ∀c ∈ dom (f ) ∀ > 0∃δ > 0∀x ∈ dom (f ) . |x − c| < δ → |f (x) − f (c)| < 

                            [a, b] := ◦{x ∈ R | a ≤ x ≤ b◦
                                                         }
                                C
The following is provable in RSTHF,U :
           ∀a, b ∈ R∀f [(realF unc (f ) ∧ dom (f ) = [a, b] ∧ Cont (f )) →
            ∀u ∈ R.f (a) < u < f (b) → ∃c ∈ R (a < c < b ∧ f (c) = u)]

6.   CONCLUSIONS AND FURTHER RESEARCH
This paper is devoted to the task of developing scientifically applicable mathematics
within the framework of [3], using a predicatively acceptable yet mechanizable set
theory. A lot of work is of course still required in order to develop larger parts
of mathematics within this framework. Obviously, at later stages of the project
predicative set theories as used here will not suffice, and so stronger set theories
will be used (see the Note after Definition 4). However, this should not be necessary
at the current stage, in which the efforts are still devoted to the fundamentals of
basic mathematical areas, like discrete mathematics and analysis. In all stages an
important criterion for success will again be the extent to which things will be done
in a natural way, as close as possible to rigorous mathematical practice.
  Further work will also be devoted to investigate different directions for strength-
ening our framework:

                                          68
—Since realF unc (f ) C ∅, another direction for how we can further develop anal-
 ysis is to continue the method of introducing new constants for bigger universes
 (similar to what we have done in this paper with HF and U ), from which we
 are going to take our real functions. This can still be done in our definitional
 framework if we take W to be Jωω , the interpretation of U as Jω , and handling
 n-order constructs as elements of Jωn , after introducing the necessary constant
 symbols. In practice, scientifically applicable mathematics uses at most 4-order
 constructs, so we shall not need more than a finite number of constants.
—Another research direction is to explore the possibility of replacing the static
 approach to terms described above with a dynamic approach, in which both
 being a legal term and equality of terms are major judgements. Our goal is that
 a user would be able to introduce any term s/he finds natural and useful. For
 this we might like {x | ϕ} to be a valid term whenever {x | ψ} is a valid term,
 and ϕ is logically equivalent to ψ (according to the formal logical system which
 underlies the set-theory used). Note that in such a dynamic framework all parts
 of a theory (terms, formulas, safety relation, logical principles and non-logical
 axioms) are defined by a simultaneous recursion.
It is also important to determine to what extent do previous works concerned with
predicative set theory fit into our framework. This includes Feferman’s various
systems for predicative mathematics, as well as the works on constructive set theory
by Aczel, Beeson, Friedman, Gambino, Rathjen, and others.

Acknowledgment
This research was partially supported by the Ministry of Science, Technology and
Space, Israel.

References
 [1] Arnon Avron. Formalizing set theory as it is actually used. In Mathematical
     Knowledge Management, pages 32–43. Springer, 2004.
 [2] Arnon Avron. Constructibility and decidability versus domain independence
     and absoluteness. Theoretical Computer Science, 394(3):144–158, 2008.
 [3] Arnon Avron. A framework for formalizing set theories based on the use of
     static set terms. In Pillars of computer science, pages 87–106. Springer, 2008.
 [4] Arnon Avron. A new approach to predicative set theory. Ways of Proof Theory,
     pages 31–63, 2010.
 [5] Robert Boyer et al. The QED manifesto. Automated Deduction–CADE,
     12:238–251, 1994.
 [6] Adam Chlipala. An introduction to programming and proving with dependent
     types in Coq. Journal of Formalized Reasoning (JFR), 3(2):1–93, 2010.
 [7] Adam Chlipala. Certified Programming with Dependent Types. MIT Press,
     Cambridge, MA, 2013.
 [8] Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F.
     Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler,
     Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing
     mathematics with the Nuprl proof development system. Prentice Hall, 1986.
                                        69
 [9] N. G. de Bruijn. A survey of the project AUTOMATH.
[10] Solomon Feferman. Systems of predicative analysis. Journal of Symbolic logic,
     pages 1–30, 1964.
[11] Solomon Feferman. Systems of predicative analysis, ii: Representations of
     ordinals. Journal of Symbolic Logic, pages 193–220, 1968.
[12] Solomon Feferman. A more perspicuous formal system for predicativity. Kon-
     struktionen versus Positionen, 1:68–93, 1978.
[13] Abraham Adolf Fraenkel, Yehoshua Bar-Hillel, and Azriel Levy. Foundations
     of set theory. Elsevier, 1973.
[14] Robin Oliver Gandy. Set-theoretic functions for elementary syntax. In Proc.
     Symp. in Pure Math, volume 13, pages 103–126, 1974.
[15] Michael Hallett. Cantorian set theory and limitation of size. Clarendon Press
     Oxford, 1984.
[16] Karel Hrbacek and Thomas Jech. Introduction to Set Theory, Revised and
     Expanded, volume 220. Crc Press, 1999.
[17] Albert E. Hurd and Peter A. Loeb. An introduction to nonstandard real anal-
     ysis, volume 118. Academic Press, 1985.
[18] R. Björn Jensen. The fine structure of the constructible hierarchy. Annals of
     Mathematical Logic, 4(3):229–308, 1972.
[19] Kenneth Kunen. Set theory. an introduction to independence proofs, 2nd print.
     Studies in Logic and the Foundations of Mathematics, 102.
[20] Azriel Levy. Basic set theory perspectives in mathematical logic. Berlim:
     Spring, 1979.
[21] Norman Megill. Metamath: A computer language for pure mathematics. 1997.
[22] Elliott Mendelson. Introduction to mathematical logic. CRC press, 1997.
[23] Rob P. Nederpelt, Jan Herman Geuvers, and R.C. De Vrijer. Selected papers
     on Automath. Elsevier, 1994.
[24] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: a
     proof assistant for higher-order logic, volume 2283. Springer, 2002.
[25] Piotr Rudnicki. An overview of the mizar project. In Proceedings of the 1992
     Workshop on Types for Proofs and Programs, pages 311–330, 1992.
[26] Andrzej Trybulec and Howard A. Blair. Computer aided reasoning. In Logics
     of Programs, pages 406–412. Springer, 1985.
[27] Jeffrey D. Ullman. Principles of Database and Knowledge-base Systems, Vol.
     I. Computer Science Press, Inc., New York, NY, USA, 1988.
[28] Nik Weaver. Analysis in J2 . arXiv preprint math/0509245, 2005.
[29] Freek Wiedijk. The QED manifesto revisited. Studies in Logic, Grammar and
     Rhetoric, 10(23):121–133, 2007.
[30] Jeff Zucker. Formalization of classical mathematics in automath. Studies in
     Logic and the Foundations of Mathematics, 133:127–139, 1994.




                                       70
