Sam Sanders
email: sasander@cage.ugent.be.

Patrick Suppes

Richard Sommer It

MORE INFINITY FOR A BETTER FINITISM

Keywords: 2000 Mathematics Subject Classification. 03H15, 26E35 Relative, stratified, nonstandard, quantifier-free, analysis, ERNA. 1

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed around 1995 by

Introduction

By now, it is well-known that large parts of 'ordinary' mathematics can be developed in systems much weaker than ZFC ( [START_REF] Stephen | Subsystems of second order arithmetic[END_REF], [START_REF]Reverse mathematics[END_REF]). However, most theories under consideration are at least as strong as WKL 0 , which is conservative over IΣ 1 . It is usually mentioned (see e.g. [START_REF] Avigad | Weak theories of nonstandard arithmetic and analysis[END_REF], [START_REF]Number theory and elementary arithmetic[END_REF] and [START_REF] Stephen | Subsystems of second order arithmetic[END_REF]) that it should be possible to develop a large part of mathematics in much weaker systems, in particular in I∆ 0 + exp and related systems. Most notably, there is Friedman's Grand Conjecture (see [START_REF]Number theory and elementary arithmetic[END_REF] and [START_REF] Friedman | Grand Conjectures[END_REF]):

Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e. what logicians call an arithmetical statement) can be proved in EFA. In 1929, Jacques Herbrand already made a similar claim, but without specifying the underlying logical system (see [9, p152]).

In this way, there have been attempts at developing analysis in nonstandard versions of I∆ 0 + exp (see [START_REF] Avigad | Weak theories of nonstandard arithmetic and analysis[END_REF], [START_REF] Chuaqui | Free-variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof[END_REF], [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], [START_REF] Sommer | Finite Models of Elementary Recursive Nonstandard Analysis[END_REF], [START_REF]Dispensing with the Continuum[END_REF] and [START_REF] Suppes | A finitarily consistent free-variable positive fragment of Infinitesimal Analysis[END_REF]). In particular, the theory ERNA and its predecessor NQA + (see [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] and [START_REF] Rössler | Fragment of nonstandard analysis with a finitary consistency proof[END_REF]) are such systems. According to Chuaqui, Sommer and Suppes, the latter theories 'provide a foundation that is close to mathematical practice characteristic of theoretical physics'. In order to achieve this goal, the systems satisfy the following three conditions, listed in [START_REF] Chuaqui | Free-variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof[END_REF]:

(i) The formulation of the axioms is essentially a free-variable one with no use of quantifiers. (ii) We use infinitesimals in an elementary way drawn from nonstandard analysis, but the account here is axiomatically self-contained and deliberately elementary in spirit. (iii) Theorems are left only in approximate form; that is, strict equalities and inequalities are replaced by approximate equalities and inequalities. In particular, we use neither the notion of standard function nor the standard part function. It is also mentioned in [START_REF] Chuaqui | Free-variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof[END_REF], that another standard practice of physics, namely the use of physically intuitive but mathematically unsound reasoning, is not reflected in the system.

By limiting the strength of the systems according to (i)-(iii), the consistency of ERNA can be proved in PRA, using Herbrand's theorem in the following form (see [START_REF] Chuaqui | Free-variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof[END_REF] and [START_REF] Sommer | Finite Models of Elementary Recursive Nonstandard Analysis[END_REF]).

1. Theorem (Herbrand). A quantier-free theory T is consistent if and only if every finite set of instantiated axioms of T is consistent.

In this respect, the item (i) is not merely a technicality to suit Herbrand's theorem: the quantifier-free axioms reflect the absence of existential quantifiers in physics. As all ε-δ definitions of basic analysis are equivalent to universal nonstandard formulas, it indeed seems plausible that one can develop calculus inside ERNA and NQA + in a quantifier-free way, particularly, without the use of ε-δ-statements. However, we discuss two compelling arguments why such a development is impossible.

First, as exemplified by item (iii), NQA + has no 'standard part' function 'st', which maps every finite number x to the unique standard number y such that x ≈ y. Thus, nonstandard objects like integrals and derivatives are only defined 'up to infinitesimals'. This leads to problems when trying to prove e.g. the fundamental theorems of calculus, which express that differentiation and integration cancel each other out. Indeed, in [START_REF] Chuaqui | Free-variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof[END_REF]Theorem 8.3], Chuaqui and Suppes prove the first fundamental theorem of calculus, using the previously proved corollary 7.4. The latter states that differentiation and integration cancel each other out on the condition that the mesh du of the hyperfinite Riemann sum of the integral and the infinitesimal y used in the derivative satisfy du/y ≈ 0. Thus, for every y, there is a du such that for all meshes dv ≤ du the corresponding integral and derivative cancel each other out. The definition of the Riemann integral ([4, Axiom 18]) absorbs this problem, but the former is quite complicated as a consequence. Also, it does not change the fact that ε-δ-statements occur, be it swept under the proverbial nonstandard carpet. Similary, ERNA only proves a version of Peano's existence theorem with a condition similar to du/y ≈ 0, contrary to Sommer and Suppes' claim in [START_REF]Dispensing with the Continuum[END_REF] (see [START_REF] Sanders | ERNA and Friedman's Reverse Mathematics[END_REF]). Thus, ERNA and NQA + cannot develop basic analysis without invoking ε-δ statements.

Second, we consider to what extent classical nonstandard analysis is actually free of ε-δ-statements. For all functions in the standard language, the well-known classical ε-δ definitions of continuity or Riemann integrability, which are Π 3 , can be replaced by universal nonstandard formulas (see e.g. [22, p70]). Given that even most mathematicians find it difficult to work with a formula with more than two quantifier alternations, this is a great virtue. Indeed, using the nonstandard method greatly reduces the sometimes tedious 'epsilon management' when working with several ε-δ statements, see [START_REF] Tao | Ultrafilters, nonstandard analysis, and epsilon management[END_REF]. Yet, nonstandard analysis is not completely free of ε-δ statements. For instance, consider the function δ(x) = 1 π ε ε 2 +x 2 , with ε ≈ 0 and let f (x) be a standard C ∞ function with compact support. Calculating the (nonstandard) Riemann integral of δ(x) × f (x) yields f (0). Hence δ(x) is a nonstandard version of the Dirac Delta. However, not every Riemann sum with infinitesimal mesh is infinitely close to the Riemann integral: the mesh has to be small enough (compared to ε). Moreover, δ(x) ≈ δ(y) is not true for all x ≈ y, only for x and y close enough. In general, most functions which are not in the standard language do not have an elegant universal definition of continuity or integrability and we have to resort to ε-δ statements. Thus, nonstandard analysis only partially removes the ε-δ formalism.

These two arguments show that the 'regular' nonstandard framework does not allow us to develop basic analysis in a quantifier-free way in weak theories of arithmetic. Moreover, for treating more advanced analysis, like the Dirac Delta, prevalent in physics, we would have to resort to ε-δ-statements anyway. Inspired by Hrbacek's 'stratified analysis' (see [START_REF] Hrbacek | Stratified analysis?, The strength of nonstandard analysis[END_REF] and [START_REF]Relative set theory: internal view[END_REF]), we introduce a weak theory of arithmetic, called ERNA A , which will allow us to develop analysis in a quantifierfree way. To this end, the theory ERNA A has a multitude of sets of infinite numbers instead of the usual dichotomy of one set of finite numbers O, complemented with one set of infinite numbers Ω. Indeed, in ERNA A there is a linear ordering (A, ) with least number 0, such that for all nonzero α, β ∈ A, the infinite number ω α is finite compared to ω β for β α. Hence there are many 'degrees' or 'levels' of infinity and the least number 0 in the ordering (A, ) corresponds to the standard level. It should be noted that the first nonstandard set theory involving different levels of infinity was introduced by Péraire in [START_REF] Péraire | Théorie relative des ensembles internes[END_REF]. Another approach was developed by Gordon in [START_REF] Gordon | Nonstandard methods in commutative harmonic analysis[END_REF].

In the second section, we describe ERNA A and its fundamental features and in the third section, we prove the consistency of ERNA A inside PRA. Though important in its own right, in particular for 'strict' finitism (see [START_REF] Tait | Finitism[END_REF]), we not only wish to do quantifier-free analysis in ERNA A , but also study its metamathematics. Thus, in the fourth section, we introduce the 'Stratified Transfer Principle', which expresses that a true formula should hold at all levels (see [START_REF] Hrbacek | Stratified analysis?, The strength of nonstandard analysis[END_REF]). As ERNA A is a weak theory of arithmetic, we limit ourselves to transfer for universal formulas. This will turn out to be sufficient for developing analysis. Stratified Transfer equally applies to external formulas and is thus very different from transfer principles in regular nonstandard arithmetic. In the fifth section, we introduce various transfer principles for ERNA A , which are based on transfer principles for ERNA (see [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] and [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF]). It turns out that these 'regular' transfer principles imply the Stratified Transfer Principle, which is remarkable, given the fundamental difference in scope between both. In the sixth section, we prove several important theorems of analysis in ERNA A and extensions. In the last section, we argue that Stratified Transfer yields a good formal framework for theoretical physics.

ERNA A , the system

In this section, we describe ERNA A and some of its fundamental features.

2.1. The language. Let (A, ) be a fixed linear order with least element 0, e.g. (N, ≤) or (Q + , ≤). For brevity, we write 'α ≺ β' instead of 'α β ∧ α = β'.

2.

Definition. The language L of ERNA A includes ERNA's, minus the symbols 'ω', 'ε' and '≈'. Additionally, it contains, for every nonzero α ∈ A, two constants 'ω α ' and 'ε α ' and, for every α ∈ A, a binary predicate '≈ α '.

The set A and the predicate are not part of the language of ERNA A . However, we shall sometimes informally refer to them in theorems and definitions. Note that there are no constants ω 0 and ε 0 in L.

3.

Definition. For all α ∈ A, the formula 'x ≈ α 0' is read 'x is α-infinitesimal', 'x is α-infinite' stands for 'x = 0 ∧ 1/x ≈ α 0'; 'x is α-finite' stands for 'x is not α-infinite'; 'x is α-natural' stands for 'x is hypernatural and α-finite'.

4.

Definition. If L is the language of ERNA A , then L α-st , the α-standard language of ERNA A , is L without ≈ β for all β ∈ A and without ω β and ε β for β α.

For α = 0, we usually drop the addition '0'. For instance, we write 'natural' instead of '0-natural' and '≈' instead of '≈ 0 '. Note that in this way, L 0-st is L st , the standard language of ERNA A .

Definition.

A term or formula is called internal if it does not involve ≈ α for any α ∈ A; if it does, it is called external.

2.2.

The axioms. The axioms of ERNA A include ERNA's, minus axiom 7.(4) (Hypernaturals), axiom set 11 (Infinitesimals) and axiom set 37 (External minimum). Additionally, ERNA A contains the following axiom set.

Axiom set (Infinitesimals).

(1) If x and y are α-infinitesimal, so are x + y and x × y.

(

) If x is α-infinitesimal and y is α-finite, xy is α-infinitesimal. (3) An α-infinitesimal is α-finite. ( 2
) If x is α-infinitesimal and |y| ≤ x, then y is α-infinitesimal. 4
(5) If x and y are α-finite, then so is x + y. [START_REF] Friedman | Grand Conjectures[END_REF] The number ε α is β-infinitesimal for all β ≺ α. [START_REF] Gordon | Nonstandard methods in commutative harmonic analysis[END_REF] The number ω α = 1/ε α is hypernatural and α-finite.

7.

Theorem. The number ω α is β-infinite for all β ≺ α.

Proof. Immediate from items ( 6) and ( 7) of the previous axiom set. [START_REF] Hájek | Metamathematics of First-Order Aritmetic[END_REF]. Theorem. x is α-finite iff there is an α-natural n such that |x| ≤ n.

Proof. The statement is trivial for x = 0. If x = 0 is α-finite, so is |x| because, assuming the opposite, 1/|x| would be α-infinitesimal and so would 1/x be by axiom 6.(4). By axiom 6.(5), the hypernatural n = |x| < |x| + 1 is then also α-finite. Conversely, let n be α-natural and |x| ≤ n. If 1/|x| were α-infinitesimal, so would 1/n be by axiom 6.(4), and this contradicts the assumption that n is α-finite.

Thus, we see that L α-st is just L st with all α-finite constants added. 9. Corollary. x ≈ α 0 iff |x| < 1/n for all α-natural n ≥ 1.

For completeness, we list ERNA's 'weight' axioms and the related theorems, as we will repeatedly use them.

10. Axiom set (Weight).

(1) if x is defined, then x is a nonzero hypernatural.

(

) if |x| = m/n ≤ 1 (m and n = 0 hypernaturals), then x is defined, x .|x| is hypernatural and x ≤ n (3) if |x| = m/n ≥ 1 (m and n = 0 hypernaturals), then x is defined, x /|x| 2
is hypernatural and x ≤ m.

Theorem.

(1) If x is not a hyperrational, then x is undefined.

(2) If x = ±p/q with p and q = 0 relatively prime hypernaturals, then ± p/q = max{|p|, |q|}.

12. Theorem.

( 13. Notation. For any 0 < n ∈ N we write (x 1 , . . . , x n ) = max{ x 1 , . . . , x n }.

) 0 = 1 (2) if n ≥ 1 is hypernatural, n = n (3) if x is defined, then 1/x = x 1

The consistency of ERNA A

In this section, we prove the consistency of ERNA A inside PRA. We need the details of this proof for the proof of theorem 21.

As ERNA A is a quantifier-free theory, we can use Herbrand's theorem in the same way as in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF] and [START_REF] Sommer | Finite Models of Elementary Recursive Nonstandard Analysis[END_REF], for more details, see [START_REF] Samuel | An introduction to proof theory, Handbook of proof theory[END_REF] or [START_REF] Hájek | Metamathematics of First-Order Aritmetic[END_REF]. To obtain ERNA's original consistency proof from the following, omit ≈ α for α = 0 from the language. 14. Theorem. The theory ERNA A is consistent and this consistency can be proved in PRA.

Proof. In view of Herbrand's theorem, it suffices to show the consistency of every finite set of instantiated axioms of ERNA A . Let T be such a set. We will define a mapping val α on T , similar to the mapping val in ERNA's consistency proof. Thus, val α maps the terms of T to rationals and the relations of T to relations on rationials, in such a way that all axioms of T are true under val α . Hence T is consistent and the theorem follows.

First of all, as there are only finitely many elements of A in T , we interpret (A, ) as a suitable initial segment of (N, ≤).

Second, like in the consistency proof of ERNA, all standard terms of T , except for min, are interpreted as their homomorphic image in the rationals: for all terms occurring in T , except min, ε α , ω α , we define val α (f (x 1 , . . . , x k )) := f (val α (x 1 ), . . . , val α (x k )) [START_REF] Avigad | Weak theories of nonstandard arithmetic and analysis[END_REF] and for all relations R occurring in T , except ≈ α , we define val α (R(x 1 , . . . , x k )) is true ↔ R(val α (x 1 ), . . . , val α (x k )).

(2)

Third, we need to gather some technical machinery. Let D be the maximum depth of the terms in T and let α 0 , α 1 , α 2 , . . . , α N -1 be all numbers of A that occur in T , with α 0 = 0. As ERNA A has the same axiom schema for recursion as ERNA, no standard term of ERNA A grows faster than 2 x k , for k ∈ N. Hence, by [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF]Theorem 30], there is a 0 < B ∈ N such that for every term f ( x) occurring in T , not involving min, we have

||f ( x)|| ≤ 2 || x|| B . (3)
Further assume that t D is the number of terms of depth D one can create using only function symbols occurring in T , and define t := 3t D + 3. With t and D, define the following functions:

f 0 (x) = 2 x B and f n+1 (x) = f t n (x) = f n (f n (. . . (f n (x)))) t fn's . (4)
Furthermore, define a 0 := 1 and

b 1 0 := f D+1 (a 0 ), c 1 0 := b 1 0 , b 2 0 := f D+1 (c 1 0 ), c 2 0 := b 2 0 , . . . , b N 0 := f D+1 c N -1 0 , (5)
(τ )| ∈ [0, a 0 ] ∪ [b 1 0 , c 1 0 ] ∪ • • • ∪ [b N 0 , c N 0 ]. For i = 0 and 1 ≤ l ≤ N -1, we have b 1 i := f D-i+1 (a i ), b l+1 i := f D-i+1 (c l i ) and d i = f D-i+1 (c N i ). ( 8
)
Then suppose that for i ≥ 0 the numbers a i , b l i , c l i and d i have already been calculated and satisfy [START_REF] Hájek | Metamathematics of First-Order Aritmetic[END_REF] and suppose val α interprets all terms τ of depth i in such a way that

|val α (τ )| ∈ [0, a i ] ∪ [b 1 i , c 1 i ] ∪ • • • ∪ [b N i , c N i ].
We will now define a i+1 , b l i+1 , c l i+1 and d i+1 , which will satisfy (8) for i + 1 and interpret all terms τ of depth i + 1 in such a way that

|val α (τ )| ∈ [0, a i+1 ] ∪ [b 1 i+1 , c 1 i+1 ] ∪ • • • ∪ [b N i+1 , c N i+1 ].
In order to obtain a suitable interpretation for min, we define,

n ϕ ( x) := (µn ≤ d i )ϕ(n, val α ( x)). (9)
Let S i+1 be the set of all numbers n ϕ (val α ( τ )) such that min ϕ ( τ ) has depth i + 1 and is in T . Now observe that, due to (8), the intervals

[a i , b 1 i ], [c l i , b l+1 i ] and [c N i , d i ] can be respectively partitioned in t intervals of the form [f j D-i (a i ), f j+1 D-i (a i )], [f j D-i (c l i ), f j+1 D-i (c l i )] and [f j D-i (c N i ), f j+1 D-i (c N i )] (10)
for j = 0, . . . , t -1 = 3t D + 2. Let V i+1 be the set of all numbers n ϕ ( τ ) in S i+1 and all other terms f ( x) of T of depth at most i + 1. Close V i+1 under taking the inverse and the weight, keeping in mind that x = 1/x . Then V i+1 has at most 3t D elements and recall that each partition in (10) has 3t D + 3 elements. Using the pigeon-hole principle, we can pick an interval, say the j 0 -th one, which has empty intersection with V i+1 . Note that we can assume 1 ≤ j 0 ≤ 3t D + 1, because we have a surplus of three intervals. Finally we can define

a i+1 := f j0 D-i (a i ) and b 1 i+1 := f j0+1 D-i (a i ) (11)
The numbers b l i+1 , c l i+1 and d i+1 are defined in the same way. Hence (8) holds for i + 1. Finally, we define

val α (min ϕ ( x)) := (µn ≤ c N i+1 )ϕ(n, val α ( x)) (12)
for all min ϕ ( τ ) with depth i + 1 in T . This definition, together with (3), yields that val α interprets all terms τ of depth i + 1 in such a way that

|val α (τ )| ∈ [0, a i+1 ] ∪ [b 1 i+1 , c 1 i+1 ] ∪ • • • ∪ [b N i+1 , c N i+1 ].
Note that the latter property holds for all terms in V i+1 , in particular for 1/|val α (τ )|.

After repeating this process D times, we obtain numbers a D , b l D , c l D and d D which allow us to interpret all terms of T . Finally, we give an interpretation to the relations

≈ α l : val α (τ ≈ α l 0) is true ↔ |τ | ≤ 1/b l+1 D , ( 13
) for 0 ≤ l ≤ N -1.
What is left is to show that under this interpretation val α , all the axioms of T recieve the predicate true, which is done next.

Because most axioms of ERNA A hold for the rational numbers, the formulas (1) and ( 2) guarantee that all axioms of T have received a valid intepretation under val α , except for axiom set 6 (Infinitesimals) above and ERNA's axiom set 31 (internal minimum).

First we treat the first axiom of 'Infinitesimals'. When either is zero, there is nothing to prove. Assume val α (σ ≈ α l 0) and val α (τ ≈ α l 0) are true and that σ + τ appears in T . By [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF], this implies

|val α (σ)|, |val α (τ )| ≤ 1/b l+1 D or 1/|val α (τ )|, 1/|val α (σ)| ≥ b l+1 D . But since σ and τ have depth at most D -1, we have 1/|val α (τ )|, 1/|val α (σ)| ∈ [0, a D-1 ] ∪ [b 1 D-1 , c 1 D-1 ] ∪ • • • ∪ [b N D-1 , c N D-1 ] and since a D-1 ≤ a D ≤ b l+1 D ≤ b l+1 D-1 , they must be in ∪ l+1≤k≤N [b k D-1 , c k D-1 ]. Hence we have 1/|val α (τ )|, 1/|val α (σ)| ≥ b l+1 D-1 or |val α (τ )|, |val α (σ)| ≤ 1/b l+1 D-1 , from which |val α (σ + τ )| ≤ 2/b l+1 D-1 < 1/b l+1 D . This last inequality is true, since b l+1 D > 2 and (b l+1 D ) 2 < b l+1 D-1 . We have proved that |val α (σ + τ )| ≤ 1/b l+1 D , which is equivalent to val α (σ + τ ≈ α l 0) being true.
Hence the first axiom of the set 'Infinitesimals' receives the predicate true under val α .

The second axiom of 'Infinitesimals' is treated in the same way as the first one.

The third axiom of 'Infinitesimals' holds trivially under val, since we cannot have that

|val α (τ )| ≤ 1/b l+1 D and 1/|val α (τ )| ≤ 1/b l+1 D hold at the same time.
The fact that zero is α l -finite, is immediate by the definition of the predicate 'x is α l -finite'.

The fourth axiom of 'Infinitesimals' holds trivially, thanks to [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF].

The fifth axiom of 'Infinitesimals' is treated like the first and second axiom of the same set.

The sixth and seventh item of 'Infinitesimals' both follow from ( 6), ( 7) and ( 13). Now we will treat the axioms of the schema 'internal minimum'. First, note that the interval [c N i+1 , d N i+1 ], defined as in [START_REF]Relative set theory: internal view[END_REF], has empty intersection with V i+1 . In particular, no term n ϕ ( τ ) of T ends up in this interval. Thus, for terms min ϕ of depth i + 1, we have

val α (min ϕ ( τ )) = (µn ≤ c N i+1 )ϕ(n, val α ( τ )) = (µn ≤ c N D )ϕ(n, val α ( τ )) (14)
as

c N D is in the interval [c N i+1 , d N i+1
]. We are ready to consider items ( 1)-( 3) of the internal minimum schema. It is clear that item (1) always holds. For item [START_REF]Number theory and elementary arithmetic[END_REF], assume that the antecedent holds, i.e. val α (min ϕ ( τ ) > 0) is true. By the definition of val α (min ϕ ) in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], the consequent ϕ(val α (min ϕ ( τ )), val α ( τ )) holds too. Hence item (2) holds. For item [START_REF] Samuel | An introduction to proof theory, Handbook of proof theory[END_REF], assume that the antecedent holds, i.e. ϕ(val α (σ), val α ( τ )) holds for some σ in T . This implies val α (σ) ≤ c N D and thus there is a number n ≤ c N D such that ϕ(n, val α ( τ )). By [START_REF] Kanovei | Nonstandard analysis, axiomatically[END_REF], val α (min ϕ ( τ )) is the least of these and hence the formulas 'min ϕ ( τ ) ≤ σ' and 'ϕ(min ϕ ( τ ), τ )' receive a true interpretation under val α . Thus, item (3) is also interpreted as true and we are done with this schema.

All axioms of T have received a true interpretation under val α , hence T is consistent and, by Herbrand's theorem, ERNA A is. Now, Herbrand's theorem is provable in IΣ 1 and this theory is Π 2 -conservative over PRA (see [START_REF] Samuel | An introduction to proof theory, Handbook of proof theory[END_REF][START_REF] Hájek | Metamathematics of First-Order Aritmetic[END_REF]). As consistency can be formalized by a Π 1 -formula, it follows immediately that PRA proves the consistency of ERNA A .

Note that if we define, in [START_REF] Davey | Is mathematical rigor necessary in physics?[END_REF], a 0 as a number larger than 1 and any c l 0 as a number larger than b l 0 , we still obtain a valid interpretation val α for T and the consistency proof goes through.

The choice of (A, ) is arbitrary, hence it is consistent with ERNA A that A is dense. It is possible to make this explicit by adding the following axiom to ERNA A , for all nonzero α, β ∈ A.

ω α < ω β → ω α < ω α+β 2 < ω β . ( 15
)
The notation ' α+β 2 ' is of course purely symbolic. This axiom receives a valid interpretation by interpreting (A, ) as (Q, ≤).

In the following, we repeatedly need overflow and underflow. Thus, we prove it explicitly in ERNA A . 15. Theorem. Let ϕ(n) be an internal quantifier-free formula, not involving min.

(1) If ϕ(n) holds for every α-natural n, it holds for all hypernatural n up to some α-infinite hypernatural n (overflow ).

(2) If ϕ(n) holds for every α-infinite hypernatural n, it holds for all hypernatural n from some α-natural n on (underflow ).

Both numbers n and n are given by explicit ERNA A -formulas not involving min.

Proof. Let ω be some α-infinite number. For the first item, define

n := (µn ≤ ω)¬ϕ(n + 1), (16)
if (∃n ≤ ω)¬ϕ(n + 1) and zero otherwise. By theorem [12, Theorem 58], this term is available in ERNA and hence in ERNA A . Likewise for underflow.

The previous theorem shows that overflow holds for all α ∈ A, i.e. at all levels of infinity. As no one level is given exceptional status, this seems only natural. Furthermore, one intuitively expects formulas that do not explicitly depend on a certain level to be true at all levels if they are true at one. In the following section, we investigate a general principle that transfers universal formulas to all levels of infinity.

ERNA A and Stratified Transfer

In nonstandard mathematics, Transfer expresses Leibniz's principle that the 'same' laws hold for standard and nonstandard objects alike. Typically, Transfer only applies to formulas involving standard objects, excluding e.g. ERNA's cosine ω i=0 (-1) i x 2i (2i)! . In set theoretical approaches to nonstandard analysis, the standard part function 'st' applied to such an object, results in a standard object, thus solving this problem. The latter function is not available in ERNA, but 'generalized' transfer principles for objects like ERNA's cosine can be obtained (see [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF]Theorem 19] and [START_REF] Sanders | ERNA and Friedman's Reverse Mathematics[END_REF]), at the cost of introducing '≈'. Unfortunately, formulas with occurrences of the predicate '≈' are always excluded from Transfer, even in the classical set-theoretical approach.

For ERNA A , we wish to obtain a transfer principle that applies to all universal formulas, possibly involving ≈. As an example, consider the following formula, expressing the continuity of the standard function f on [0, 1]:

(∀x, y ∈ [0, 1])(x ≈ y → f (x) ≈ f (y)). (17)
Assuming [START_REF] Rössler | Fragment of nonstandard analysis with a finitary consistency proof[END_REF], it seems only natural that if x ≈ α y for α 0, then f (x) ≈ α f (y).

In other words, there should hold, for all α ∈ A,

(∀x, y ∈ [0, 1])(x ≈ α y → f (x) ≈ α f (y)), (18)
which is [START_REF] Rössler | Fragment of nonstandard analysis with a finitary consistency proof[END_REF], with ≈ replaced with ≈ α . Incidentally, when f is a polynomial, an easy computation shows that (18) indeed holds, even for polynomials in L α-st . Below, we turn this into a general principle.

16. Notation. Let Φ α be a formula of L α-st ∪ {≈ α }. Then Φ β is Φ α with all occurrences of ≈ α replaced with ≈ β . 17. Principle (Stratified Transfer). Assume α 0 and let Φ α be a quantifier-free formula of L α-st ∪ {≈ α }, not involving min. For every β α,

(∀ x)Φ α ( x) ↔ (∀ x)Φ β ( x). (19)
Note that Φ may involve α-standard parameters. We always tacitly allow (αstandard) parameters in all transfer principles in this paper, unless explicitly stated otherwise. [START_REF] Sanders | ERNA and Friedman's Reverse Mathematics[END_REF]. Principle (Weak Stratified Transfer). Assume α 0 and let f ( x, k) be a function of L α-st , not involving min and weakly increasing in k. For all β α, the following statements are equivalent 'f ( x, k) is α-infinite for all x and all α-infinite k' and 'f ( x, k) is β-infinite for all x and all β-infinite number k'.

The second transfer principle is a special case of the first. However, by the following theorem, the seemingly weaker second principle is actually equivalent to the first. We sometimes abbreviate 'for all α-infinite ω' by '(∀ α ω)'.

19. Theorem. In ERNA A , Weak Stratified Transfer is equivalent to Stratified Transfer.

Proof. First, assume the Weak Stratified Transfer Principle and let Φ α ( x) be as in the Stratified Transfer Principle. Replace in Φ α ( x) all positive occurrences of

τ i ( x) ≈ α 0 with (∀ α-st n i )(|τ i ( x)| < 1/n i ),
where n i is a new variable not yet appearing in Φ α ( x). Do the same for the negative occurrences, using new variables m i . Bringing all quantifiers in (∀ x)Φ α ( x) to the front, we obtain

(∀ x)(∀ α-st n 1 , . . . , n l )(∃ α-st m 1 , . . . , m k )Ψ( x, n 1 , . . . , n l , m 1 , . . . , m k ),
where Ψ is quantifier-free and in L α-st . Using pairing functions, we can reduce all n i to one variable n and reduce all m i to one variable m. Hence the previous formula becomes

(∀ x)(∀ α-st n)(∃ α-st m)Ξ( x, n, m)
, where Ξ is quantifier-free and in L α-st . Fix some α-infinite number ω 1 , we obtain

(∀ x)(∀ α-st n)(∃m ≤ ω 1 )Ξ( x, n, m),
Applying overflow, with ω = ω 1 in (16), yields

(∀ x)(∀n ≤ n( x, ω 1 ))(∃m ≤ ω 1 )Ξ( x, n, m).
Hence the function n( x, k) is α-infinite for all x and α-infinite k and weakly increasing in k. By the Weak Stratified Transfer Principle, n( x, k) is β-infinite for all x and all β-infinite k, for β α. Hence, for all x, β-finite n and β-infinite k, we have

(∃m ≤ k)Ξ( x, n, m).
Fix x 0 and β-finite n 0 . Since (∃m ≤ k)Ξ( x 0 , n 0 , m) holds for all β-infinite k, underflow yields (∃ β-st m)Ξ( x 0 , n 0 , m). This implies

(∀ x)(∀ β-st n)(∃ β-st m)Ξ( x, n, m).
Unpairing the variables n and m and bringing the quantifiers back in the formula, we obtain (∀ x)Φ β ( x). Thus, we have proved the forward implication in [START_REF]Levels of Reverse Mathematics[END_REF].

In the same way, it is proved that (∀ x)Φ β ( x) implies (∀ x)Φ α ( x), i.e., the reverse implication in [START_REF]Levels of Reverse Mathematics[END_REF], assuming the Weak Stratified Transfer Principle.

Hence we proved that the Weak Stratified Transfer Principle implies the Stratified Transfer Principle. As the reverse implication is trivial, we are done.

By the previous theorem, it suffices to prove the consistency of ERNA A with the Weak Stratified Transfer Principle. Instead of proving this consistency directly, we show, in the next section, that Weak Stratified Transfer follows from Π α 3 -TRANS. The latter is ERNA A 's version of the classical transfer principle limited to Π 3formulas. The schema Π α 3 -TRANS is analogous to Π 1 -TRANS and Σ 2 -TRANS, introduced in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] and [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF]. We suspect that PRA cannot prove the consistency of ERNA A + Π α 3 -TRANS.

To conclude this section, we point to [START_REF] Hrbacek | Stratified analysis?, The strength of nonstandard analysis[END_REF], where the importance of Stratified Transfer is discussed. Moreover, analysis developed in ERNA A in section 6 is more elegant when Stratified Transfer is available. Also, Stratified Transfer (in some form or other) seems to be compatible with the spirit of 'strict' finitism (see [START_REF] Tait | Finitism[END_REF]), as it merely lifts true universal formulas to higher levels. It would be interesting to know the exact logical strength of Stratified Transfer and how it can be weakened by imposing certain 'constructive' limitations on A.

ERNA A and regular Transfer

In this section, we will introduce the 'new' transfer principles Π α 1 -TRANS and Σ α 2 -TRANS, which are ERNA A -versions of the 'old' schemas Π 1 -TRANS and Σ 2 -TRANS. The adaptations made to the latter schemas to obtain the former are both natural and in line with the Stratified Transfer Principle above. We give a consistency proof for the extended theory, which requires significant changes to the consistency proof in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF]. We only sketch a consistency proof for ERNA A + Σ α 2 -TRANS. Finally, using the new transfer principles, we prove that transfer for Π 3formulas is sufficient for the Stratified Transfer Principle. 5.1. Transfer for Π 1 and Σ 1 -formulas. Here, we introduce a 'stratified' version of transfer for Π 1 and Σ 1 -formulas for ERNA A and show that the extended theory is consistent. The following axiom schema is ERNA A 's version of Π 1 -TRANS. [START_REF] Stephen | Subsystems of second order arithmetic[END_REF]. Axiom schema (Stratified Π 1 -transfer). For every quantifier-free formula ϕ(n) of L α-st , not involving min, we have

(∀ α-st n)ϕ(n) → (∀n)ϕ(n). (20)
The previous axiom schema is denoted by Π α 1 -TRANS and its parameter-free counterpart is denoted by Π α 1 -TRANS -. Similarly, let Π 1 -TRANS -be the parameterfree version of Π 1 -TRANS (see also remark 52). After the consistency proof, the reasons for the restrictions on ϕ will become apparent. Resolving the implication in [START_REF] Stephen | Subsystems of second order arithmetic[END_REF], we see that this formula is equivalent to

(0 < min ¬ϕ is α-finite) ∨ (∀n)ϕ(n). (21)
Thus, ERNA A + Π α 1 -TRANS -is equivalent to a quantifier-free theory and we may use Herbrand's theorem to prove its consistency. To obtain the consistency proof in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] from the following proof, omit ≈ α for α = 0 from the language. 21. Theorem. The theory ERNA A + Π α 1 -TRANS -is consistent and this consistency can be proved by a finite iteration of ERNA A 's consistency proof.

Proof. Despite the obvious similarities between the theories ERNA + Π 1 -TRANS - and ERNA A + Π α 1 -TRANS -, the consistency proof of the former (see [12, Theorem 44]) breaks down for the latter. The reason is that one of the explicit conditions for the consistency proof of ERNA + Π 1 -TRANS -to work, is that ϕ must be in L st . But in Π α 1 -TRANS -, ϕ is in L α-st and as such, the formula ϕ in (21) may contain the nonstandard number ω β for β α.

However, it is possible to salvage the original proof. We use Herbrand's theorem in the same way as in the consistency proof of ERNA A . Thus, let T be any finite set of instantiated axioms of ERNA A + Π α 1 -TRANS -. Leaving out the transfer axioms from T , we are left with a finite set T of instantiated ERNA A axioms. Let val α be its interpretation into the rationals as in ERNA A 's consistency proof. However, nothing guarantees that the instances of Π α 1 -TRANS -in T are also interpreted as 'true' under val α . We will adapt val α by successively increasing the starting values defined in [START_REF] Davey | Is mathematical rigor necessary in physics?[END_REF], if necessary. The resulting map will interpret all axioms in T as true, not just those in T .

Let T and T be as in the previous paragraph. Let D be the maximum depth of the terms in T . Let α 0 , . . . , α N -1 be all elements of A in T , with α 0 = 0. For notational convenience, for ϕ as in Π α 1 -TRANS -, we shall write ϕ(n, τ ) instead of ϕ(n), where τ contains all numbers occurring in ϕ that are not in L st . Finally, let the list ϕ 1 (n, τ 1 ), . . . , ϕ M (n, τ M ) consist of the quantifier-free formulas whose Π α 1 -transfer axiom (21) occurs in T . If necessary, we arrange this list of formulas in such a way that i < j implies that all ω α in the range of τ i satisfy ω α ω β for some ω β in the range of τ j . By [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF],

Ω l := l+1≤i≤N [b i D , c i D ]
is the set where val α maps the α l -infinite numbers. Also,

O l := [0, a D ] ∪ [b 1 D , c 1 D ] ∪ • • • ∪ [b l D , c l D ]
is the set where val α maps the α l -finite numbers. If we have, for all i ∈ {1, ..., M } and all l ∈ {0, ..., N -1} such that γ α l for all ω γ in the range of τ i , that

(∃m ∈ O l )¬ϕ i (m, val α ( τ i )) ∨ (∀n ∈ [0, a D ] ∪ Ω 0 )ϕ i (n, val α ( τ i )), (22)
we see that val α provides a true interpretation of the whole of T , not just T , as every instance of ( 21) receives a valid interpretation, in this case. However, nothing guarantees that ( 22) holds for all such numbers i and l. Thus, assume there is an exceptional ϕ (n, τ ) := ϕ i (n, τ i ) and l, for which

(∀m ∈ O l )ϕ (m, val α ( τ )) ∧ ∃n ∈ b l+1 D , c l+1 D ¬ϕ (n, val α ( τ )). (23)
Now fix τ and let l 0 be the least l satisfying the previous formula. Then [START_REF] Sommer | Finite Models of Elementary Recursive Nonstandard Analysis[END_REF] implies (∃n ∈ Ω l0 )¬ϕ (n, val( τ )), i.e. there is an 'α l0 -infinite' n such that ¬ϕ (n, val( τ )). Now choose a number n 0 > c N D (for notational clarity, we write a 0 = c 0 0 , for the case l 0 = 0) and construct a new interpretation val α with the same starting values as in [START_REF] Davey | Is mathematical rigor necessary in physics?[END_REF], except for (c l0 0 ) := n 0 . This val α continues to make the axioms in T true and does the same with the instances in T of the axiom

(0 < min ¬ϕ ( τ ) is α l0 -finite) ∨ (∀n)ϕ (n, τ ) (24)
Indeed, if a number n ∈ Ω l0 is such that ¬ϕ (n, val α ( τ )), the number n is interpreted by val α as an α l0 -finite number because n ≤ c N D ≤ (c l0 0 ) ≤ (c l0 D ) by our choice of (c l0 0 ) . Thus, the sentence (∃n ∈ O l0 )¬ϕ (n, val α ( τ )) is true. By definition, τ only contains numbers ω αi for i ≤ l 0 and (6) implies val α (ω αi ) = b i 0 , for 1 ≤ i ≤ N . But increasing c l0 0 to (c l0 0 ) , as we did before, does not change the numbers b 1 0 ,. . . , b l0 0 . Hence val α ( τ ) = val α ( τ ) and so (∃n ∈ O l0 )¬ϕ (n, val α ( τ )) implies (∃n ∈ O l0 )¬ϕ (n, val α ( τ )). Thus, (0 < min ¬ϕ ( τ ) is α l0 -finite) is true under val α and so is the whole of (24).

Define T as T plus all instances of (24) occurring in T . If there is another exceptional ϕ i and l 0 such that (23) holds, repeat this process. Note that if we increase another c j 0 for j ≥ l 0 and construct val α , the latter still makes the axioms of T true, but the axioms of T as well, since increasing c j 0 does not change the interpretations of the numbers ω αi for i ≤ l 0 either. Hence ( 24) is true under val for the same reason as for val . Recall that the list ϕ 1 (n, τ 1 ), . . . , ϕ M (n, τ M ) is arranged in such a way that i < j implies that all ω α in the range of τ i satisfy ω α ω β for some ω β in the range of τ j . This arrangement of the list guarantees that the changes we make to val α to satisfy a certain transfer axiom, do not invalidate a transfer axiom treated earlier.

This process, repeated, will certainly halt: either the two lists {1, . . . , M } and {1, . . . , N -1} become exhausted or, at some earlier stage, a valid interpretation is found for T . Note that this consistency proof is a finite iteration of ERNA A 's.

The restrictions on the formulas ϕ admitted in [START_REF] Stephen | Subsystems of second order arithmetic[END_REF] are imposed by our consistency proof. Indeed, for every α i occurring in T , the interpretation of ω αj for j > i depends on the choice of c i 0 . By our changing c l0 0 into (c l0 0 ) > c l0 0 , formulas like (24) could loose their 'true' interpretation from one step to the next, if they contain such ω j . Likewise, the changing of c l 0 can change the interpretation of ≈ β , for any β ∈ A, and hence this predicate cannot occur in ϕ. The exclusion of min has, of course, a different reason: min ϕ is only allowed in ERNA when ϕ does not rely on min.

For convenience, we will usually use Π α 1 -TRANS instead of Π α 1 -TRANS -. By contraposition, the schema Π α 1 -TRANS implies the following schema, which we denote Σ α 1 -TRANS. 22. Axiom schema (Stratified Σ 1 -transfer). For every quantifier-free formula ϕ(n) of L α-st , not involving min, we have

(∃n)ϕ(n) → (∃ α-st n)ϕ(n). (25)
Note that both in ( 20) and ( 25), the reverse implication is trivial. For ϕ ∈ L α-st , the levels β α are sometimes called the 'context' levels of ϕ and α is the called the 'minimial' context level, i.e. the lowest level on which all constants occurring in ϕ exist. In this respect, Σ α 1 -transfer expresses that true existential formulas can be pushed down to their minimal context level, which corresponds to their level of standardness.

5.2.

Transfer for Σ 2 and Π 2 -formulas. In order to obtain transfer for Σ 2 and Π 2 -formulas in ERNA, we added a certain axiom schema to ERNA + Π 1 -TRANS and showed that the resulting theory has transfer for Σ 2 and Π 2 -formulas, see [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF] for details. We also discussed why this approach is preferable to a more 'direct' approach. Here, we shall employ the same method to obtain 'Stratified Transfer' for Σ 2 and Π 2 -formulas. As the method is similar to that used in [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF], we only sketch the proofs. Our goal is to obtain the following transfer principle. [START_REF] Sommer | Finite Models of Elementary Recursive Nonstandard Analysis[END_REF]. Axiom schema (Stratified Σ 2 -transfer). For every quantifier-free formula ϕ from L α-st , not involving min, we have

(∃n)(∀m)ϕ(n, m) ↔ (∃ α-st n)(∀ α-st m)ϕ(n, m). ( 26
)
We denote this schema by Σ α 2 -TRANS. By contraposition, it is equivalent to the Π α 2 -transfer principle (∀n

)(∃m)ϕ(n, m) ↔ (∀ α-st n)(∃ α-st m)ϕ(n, m). ( 27
)
In view of the equivalence between ( 26) and ( 27), we will only mention Π α 2 -transfer in the sequel if it is explicitly required. We will add certain axioms to ERNA A + Π α 1 -TRANS and prove the consistency of the resulting theory. Then we show that the extended theory proves the above Σ α 2 -transfer principle. First consider the following theorem of ERNA A + Π α 1 -TRANS.

24.

Theorem. In ERNA A + Π α 1 -TRANS we have, for every quantifier-free formula ϕ(n, m) of L α-st not involving min, the implication

(∃n)(∀m)ϕ(n, m) → (∀ α-st k)(∃ α-st n)(∀m ≤ k)ϕ(n, m). ( 28
)
Proof. If the antecedent holds, we have (∃n)(∀m ≤ k)ϕ(n, m) for every α-finite k. By Σ α 1 -transfer, (∃ α-st n)(∀m ≤ k)ϕ(n, m), hence the consequent of (28).

By the previous theorem, (29) implies the forward implication in [START_REF] Tait | Finitism[END_REF].

25. Axiom schema (TRANS + α ). For every quantifier-free formula ϕ(n, m) of L α-st not involving min, we have

(∃n)(∀m)ϕ(n, m) →   (∀ α-st k)(∃ α-st n)(∀m ≤ k)ϕ(n, m) ↓ (∃ α-st n)(∀ α-st m)ϕ(n, m)   ( 29
)
Theorem 27 will show that Σ α 2 -transfer as stated in ( 26) is provable in ERNA A + Π α 1 -TRANS+TRANS + α . Therefore, the latter theory will be abbreviated to ERNA A + Σ α 2 -TRANS. The schema TRANS + α can be skolemized in exactly the same way as the schema TRANS + , see [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF]Theorem 3] for details. We have the following theorem.

Theorem. The theory ERNA

A + Σ α 2 -TRANS is consistent. Proof.
The proof of the consistency of ERNA + Σ 2 -TRANS in [START_REF]Saturation and Σ 2 -transfer for ERNA[END_REF] can easily be converted into a proof for the theorem at hand. The adaptations are minimal, as the skolemization of ( 29) is also a tautology in the finite setting of the model for an arbitrary finite subset of instantiated ERNA A + Π α 1 -TRANS-axioms. Now we prove the main result of this section, viz. that ERNA A + Σ α 2 -TRANS has Σ α 2 -transfer. 27. Theorem. In ERNA A + Σ α 2 -TRANS, the Σ α 2 -transfer principle, stated in (26), holds.

Proof. By theorem 26 we know that we can consistently add the axiom schema 25 to ERNA A + Π α 1 -TRANS. In the extended theory, theorem 24 yields that (29) implies the forward implication in [START_REF] Tait | Finitism[END_REF]. For the inverse implication, assume that (∃ α-st n)(∀ α-st m)ϕ(n, m) and fix α-finite n 0 such that (∀ α-st m)ϕ(n 0 , m). By Π α 1transfer, this implies (∀m)ϕ(n 0 , m) and hence (∃n)(∀m)ϕ(n, m).

Using pairing functions, we immediately obtain Stratified Σ α 2 and Π α 2 -transfer for formulas involving blocks of quantifiers. As for Σ α 1 -transfer, Σ α 2 -transfer as in [START_REF] Tait | Finitism[END_REF] expresses that a true Σ 2 -formula can be pushed down to its minimal context level 5.3. Transfer for Σ 3 and Π 3 -formulas. Here, we show that a certain transfer principle for Π 3 -formulas, called Π α 3 -TRANS, is sufficient to obtain Weak Stratified Transfer. We first introduce the former. Note that it is the natural extension of Σ α 2 and Π α 1 -transfer. 28. Axiom schema (Stratified Π 3 -transfer). For every quantifier-free formula ϕ of L α-st , not involving min, we have,

(∀ α-st n)(∃ α-st m)(∀ α-st k)ϕ(n, m, k) ↔ (∀n)(∃m)(∀k)ϕ(n, m, k). ( 30
)
We denote this schema by Π α 3 -TRANS. We now prove the main theorem of this section, namely that Π α 3 -transfer is sufficient to obtain Stratified Transfer. 29. Theorem. The theory ERNA A +Π α 3 -TRANS proves the Weak Stratified Transfer Principle.

Proof. Assume 0 α ≺ β and let f be as in the Weak Stratified Transfer Principle and assume that f (n, x) is α-infinite for all x and all α-infinite n. This implies that

(∀ x)(∀ α-st n)(∀ α ω)(f (ω, x) > n),
where the notation '(∀ α ω)' denotes 'for all α-infinite numbers ω'. Fixing x 0 and α-finite n 0 and applying underflow to the formula (∀ α ω)(f (ω, x 0 ) > n 0 ), yields the existence of an α-finite number k 0 such that (f (k 0 , x 0 ) > n 0 ). Hence,

(∀ x)(∀ α-st n)(∃ α-st m)(f (m, x) > n), (31)
and, by [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF]Theorem 58], there is a function g(n, x) which calculates the least m such that f (m, x) > n, for any x and α-finite n. Thus, (31) implies

(∀ α-st n)(∀ x)(f (g(n, x), x) > n), (32)
where g(n, x) is α-finite for α-finite n and any x. Now fix an α-infinite hypernatural ω 1 and define h(n) as max x ≤ω1 g(n, x). By definition, the function h(n) is α-finite for α-finite n. As f is weakly increasing in its first argument, (32) implies

(∀ α-st n)(∀ x)( x ≤ ω 1 → f (h(n), x) > n),
and also

(∀ α-st n)(∃m ≤ h(n))(∀ x)( x ≤ ω 1 → f (m, x) > n).
We previously showed that h(n) is α-finite for α-finite n. Thus,

(∀ α-st n)(∃ α-st m)(∀ x)( x ≤ ω 1 → f (m, x) > n),
and also

(∀ α-st n)(∃ α-st m)(∀ α-st x)(f (m, x) > n). (33)
By Π α 3 -transfer, this implies that

(∀ β-st n)(∃ β-st m)(∀ β-st x)(f (m, x) > n). (34)
Fixing appropriate β-finite n 0 and m 0 , and applying Π α 1 -transfer, yields

(∀ β-st n)(∃ β-st m)(∀ x)(f (m, x) > n).
This formula implies that f (k, x) is β-infinite for all x and all β-infinite k. The other implication in the Weak Stratified Transfer Principle is proved in the same way.

It is clear form the proof why the theorem fails for β such that 0 β ≺ α. Indeed, as f may contain ω α , we cannot apply Π α 3 -transfer to (33) for such β. Note that (Weak) Stratified Transfer is fundamentally different from the other transfer principles, as ≈ α can occur in the former, but not in the latter. In this respect, it is surprising that a 'regular' transfer principle such as Π α 3 -TRANS implies (Weak) Stratified Transfer.

However, if we consider things from the point of view of set theory, we can explain this remarkable correspondence between 'regular' and 'stratified' transfer. Internal set theory is an axiomatic approach to nonstandard mathematics (see [START_REF] Kanovei | Nonstandard analysis, axiomatically[END_REF] for details). Examples include Nelson's IST ( [START_REF] Nelson | Internal set theory: a new approach to nonstandard analysis[END_REF]), Kanovei's BST ( [START_REF] Kanovei | Nonstandard analysis, axiomatically[END_REF]), Péraire's RIST ( [START_REF] Péraire | Théorie relative des ensembles internes[END_REF]) and Hrbacek's FRIST * and GRIST ( [START_REF] Hrbacek | Stratified analysis?, The strength of nonstandard analysis[END_REF] and [START_REF]Relative set theory: internal view[END_REF]), which inspired parts of ERNA A . These set theories are extensions of ZFC and most have a so called 'Reduction Algorithm'. This effective procedure applies to certain general classes of formulas and removes any predicate not in the original ∈-language of ZFC. The resulting formula agrees with the original formula on standard objects. Thus, in GRIST, it is possible to remove the relative standardness predicate ' ' and hence transfer for formulas in the ∈--language follows from transfer for formulas in the ∈-language. Similarly, in theorem 19, we show that transfer for formulas involving the relative standardness predicate ≈ α can be reduced to a very specific instance, involving fewer predicates ≈ α . Later, in theorem 29, we prove that the remaining standardness predicates can be removed from the formula too, producing (33) and (34). Thus, we have reduced 'stratified' transfer to 'regular' transfer. In turn, it is surprising that a set-theoretical metatheorem such as the Reduction Algorithm appears in theories with strength far below ZFC.

Analysis in ERNA A

In this section, we obtain some basic theorems of analysis. We shall work in ERNA A + Π α 3 -TRANS, i.e. we may use the Stratified Transfer Principle. Most theorems can be proved in ERNA A , at the cost of adding extra technical conditions. This is usually mentioned in a corollary.

For the rest of this section, we assume that 0 ≺ α ≺ β, that a and b are α-finite and that the functions f and g do not involve the minimum operator min ϕ . 6.1. Continuity. Here, we define the notion of continuity in ERNA A and prove some fundamental theorems.

30. Definition. A function f is α-continuous at a point x 0 , if x ≈ α x 0 implies f (x) ≈ α f (x 0 ). A function is α-continuous over [a, b] if (∀x, y ∈ [a, b])(x ≈ α y → f (x) ≈ α f (y)).
As usual, we write 'continuous' instead of '0-continuous'. If f is α and βcontinuous for α = β, we say that f is 'α, β-continuous'

31. Theorem. If f is α-continuous over [a, b] and α-finite in one point of [a, b], it is α-finite for all x in [a, b].
Proof. Let f be as in the theorem, fix α-finite k 0 and consider

(∀x, y ∈ [a, b])(|x -y| ≤ 1/N ∧ x, y ≤ ω β → |f (x) -f (y)| < 1/k 0 ). ( 35
)
As f is α-continuous, this formula holds for all α-infinite N . By [12, Corollary 53], (35) is quantifier-free and applying underflow yields that it holds for all N ≥ N 0 , where N 0 is α-finite. Then let x 0 ∈ [a, b] be such that f (x 0 ) is α-finite. We may assume it satisfies x 0 ≤ ω β . Using (35) for N = N 0 , it easily follows that f (x) deviates at most (N 0 b -a )/k 0 from f (x 0 ) for x ≤ ω β . As the points

x n := a + n(b-a) ω β partition the interval [a, b] in α-infinitesimal subintervals, the theorem follows. 32. Corollary. If f ∈ L α-st is α-continuous over [a, b], it is α-finite for all x ∈ [a, b].
Proof. Let f (x, x) be the function f (x) from the corollary with all nonstandard numbers replaced with free variables. By [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF]Theorem 30], there is a k ∈ N such that f (x, x) ≤ 2

x, x k . Thus, f (x) is α-finite for α-finite x. Applying the theorem finishes the proof.

By Stratified Transfer, an α-continuous function of L α-st e.g. ERNA A 's cosine ωα n=0 (-1) n x 2n (2n)! is also β-continuous for all β α. Similar statements hold for integrability and differentiability. For the sake of brevity, we mostly do not explicitly mention these properties. 6.2. Differentiation. Here, we define the notion of differentiability in ERNA A and prove some fundamental theorems. To this end, we need some notation.

Notation.

(1) A nonzero number x is 'α-infinitesimal' or 'strict α-infinitesimal' (with respect to

β) if x ≈ α 0 ∧ x ≈ β 0. We denote this by x ≈ α 0. (2) We write 'a α b' instead of 'a < b ∧ a ≈ α b' and 'a β b' instead of 'a < b ∨ a ≈ β b'. (3) We write ∆ h (f )(x) instead of f (x+h)-f (x) h .
We use the following notion of differentiability.

Definition.

(

) A function f is 'α-differentiable at x 0 ' if ∆ ε f (x 0 ) ≈ α ∆ ε f (x 0 1
) for all nonzero ε, ε ≈ α 0 and both quotients are α-finite. (2) If f is α-differentiable at x 0 and ε ≈ α 0, then ∆ ε f (x 0 ) is called 'the derivative of f at x 0 ' and is denoted D α f (x 0 ). (3) A function f is called 'α-differentiable over (a, b)' if it is α-differentiable at every point a α x α b. (4) The concepts 'α-differentiable' and 'α-derivative' are defined by replacing, in the previous items, 'ε, ε ≈ α 0' by 'ε, ε ≈ α 0'. We use the same notation for the α-derivative as for the α-derivative.

The choice of ε is arbitrary and hence the derivative is only defined 'up to infinitesimals'. There seems to be no good way of defining it more 'precisely', i.e. not up to infinitesimals, without the presence of a 'standard part' function 'st α ' which maps α-finite numbers to their α-standard part.

35.

Theorem. If a function f is α-differentiable over (a, b), it is α-continuous at all a α x α b.

Proof. Immediate from the definition of differentiability. 36. Theorem. Let f (x) and g(x) be α-standard and α-differentiable over (a, b). Then f (x)g(x) is α-differentiable over (a, b) and

D α (f g)(x) ≈ α D α f (x) g(x) + f (x)D α g(x) (36)
for all a α x α b.

Proof. Assume f and g are α-differentiable over (a, b). Let ε be an α-infinitesimal and x such that a α x α b. Then,

D α (f g)(x) ≈ α 1 ε (f (x + ε)g(x + ε) -f (x)g(x)) = 1 ε (f (x + ε)g(x + ε) -f (x)g(x + ε) + f (x)g(x + ε) -f (x)g(x)) = 1 ε ((f (x + ε) -f (x))g(x + ε) + f (x)(g(x + ε) -g(x))) = f (x+ε)-f (x) ε g(x + ε) + f (x) g(x+ε)-g(x) ε ≈ α D α f (x)g(x + ε) + f (x)D α g(x) ≈ α D α f (x)g(x) + f (x)D α g(x).
The final two steps follow from theorem 35 and corollary 32. Hence f (x)g(x) is α-differentiable over (a, b) and (36) indeed holds.

By theorem 31, the requirement 'f, g ∈ L α-st ' in the previous theorem, can be dropped if we additionally require f g to be α-finite in one point of (a, b). In the following theorem, there is no such requirement. 37. Theorem (Chain rule). Let g be α-differentiable at a and let f be α-differentiable at g(a). Then f • g is α-differentiable at a and

D α (f • g)(a) ≈ α D α f (g(a)) D α g(a). (37)
Proof. Let f and g be as in the theorem and assume 0 = ε ≈ α 0. First of all, since g is α-differentiable at a, we have, that D α g(a) ≈ α g(a+ε)-g(a) ε

, which implies g(a + ε) = εD α g(a) + g(a) + εε for some ε ≈ α 0. Then ε = εD α g(a) + εε is also α-infinitesimal. If ε = 0, then, as f is α-differentiable at g(a), we have

D α f (g(a)) ≈ α f (g(a)+ε )-f (g(a)) ε . This implies f (g(a) + ε ) = ε D α f (g(a)) + f (g(a)) + ε ε
for some ε ≈ α 0. If ε = 0, then the previous formula holds trivially for the same ε . Note that ε ε ε ≈ α 0. Hence we have

∆ ε (f • g)(a) = f (g(a+ε))-f (g(a)) ε = f (g(a)+ε )-f (g(a)) ε = ε Dαf (g(a))+ε ε +f (g(a))-f (g(a)) ε ≈ α ε ε D α f (g(a)
). By definition, ε ε ≈ α D α g(a) and hence f • g is α-differentiable at a and (37) holds.

It is easily verified that the theorems of this section still hold if we replace 'αdifferentiable' with 'α-differentiable'. 6.3. Integration. Here, we define the notion of Riemann integral in ERNA A and prove some fundamental theorems.

In classical analysis, the Riemann-integral is defined as the limit of Riemann sums over ever finer partitions. In ERNA A , we adopt the following definition for the concept 'partition'. 38. Definition. A partition π of [a, b] is a vector (x 1 , . . . , x n , t 1 , . . . t n-1 ) such that x i ≤ t i ≤ x i+1 for all 1 ≤ i ≤ n -1 and a = x 1 and b = x n . The number δ = max 2≤i≤n (x i -x i-1 ) is called the 'mesh' of the partition π.

For the definition of integrability, we need to quantify over all partitions of an interval. In [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], it is proved that ERNA contains pairing functions, which can uniquely code vectors of numbers into numbers (and decode them back). As partitions are merely vectors, it is intuitively clear that quantifying over all partitions of an interval is possible in ERNA, and thus in ERNA A . Also, in [START_REF] Sanders | ERNA and Friedman's Reverse Mathematics[END_REF], the previous claim is proved explicitly. Incidentally, Riemann integration inside NQA + , the predecessor of ERNA, uses equidistant partitions.

Assume that ω is α-infinite and that a α b. Let n 0 be the least n such that (1) Given a partition (x 1 , . . . , x n , t 1 , . . . , t n-1 ) of [a, b], the Riemann sum corresponding to f is defined as Proof. The proof for α = 0 is given in [START_REF] Sanders | ERNA and Friedman's Reverse Mathematics[END_REF] and can easily be adapted to α 0. Proof. Fix ε ≈ α 0 and x such that a α x α b. We have

n i=2 f (t i-1 )(x i -x i-1 ). ( 2
F (x+ε)-F (x) ε = 1 ε x+ε a f (t)d(t, β) - x a f (t)d(t, β) ≈ β 1 ε x+ε x f (t)d(t, β), ( 38
)
as ε is not β-infinitesimal. Let ω 1 be β-infinite and define x i = x + iε ω1 . Let f (y 1 ) and f (y 2 ) be the least and the largest f

(x i ) for i ≤ ω 1 . As f is α,β-continuous, m := f (y 1 ) and M := f (y 2 ) are such that m β f (y) β M for y ∈ [x, x + ε] and m ≈ α M ≈ α f (x). This implies εm β x+ε x f (t)d(t, β) β εM, and hence m β 1 ε x+ε x f (t)d(t, β) β M, as ε is not β-infinitesimal. Thus, m ≈ α 1 ε x+ε x f (t)d(t, β) ≈ α M ≈ α f (x).
By (38), F is α-differentiable and the theorem follows.

. Let f ∈ L α-st be α-differentiable over (a, b) and such that D α f is β-continuous over [a, b]. For a α c α d α b, we have d c D α f (x) d(x, β) ≈ α f (d) -f (c).
Proof. Let c, d be as stated and let ε be strict α-infinitesimal. Note that d -c is α-finite. We have

d c D α f (x) d(x, β) ≈ α d c f (x+ε)-f (x) ε d(x, β) ≈ β 1 ε d c f (x + ε) d(x, β) - d c f (x) d(x, β) ≈ β 1 ε d+ε c+ε f (x) d(x, β) - d c f (x) d(x, β) ≈ β 1 ε d+ε d f (x) d(x, β) - c+ε c f (x) d(x, β) .
As in the proof of the second fundamental theorem, we have

d c f (x)D α g(x) d(x, β) ≈ α f (x)g(x) d c - d c D α f (x)g(x) d(x, β).
Proof. Immediate from the second fundamental theorem and theorem 36.

By theorem 35, we can drop the requirement 'f, g ∈ L α-st ' if we additionally require f g to be α-finite in one point of (a, b).

For simulating the Dirac Delta distribution, we need to introduce an extra level γ such that 0 ≺ γ ≺ α. We also need the function arctan. 48. Theorem. Define the (finite) constant π as 4 arctan(1).

(1) For all α-finite x, arctan(±|x|) + arctan

± 1 |x| ≈ α ±π/2. (2) We have arctan(±ω 3 α ) ≈ γ ±π/2.
Proof. The first item follows by calculating the α-derivative of arctan x+arctan 1/x using the chain rule and noting that the result is α-infinitesimally close to zero. Thus, there is a constant C such that arctan x + arctan 1/x ≈ α C, for all α-finite positive x. Substituting x = 1 yields C = π/2. The case x < 0 is treated in the same way. The second item follows from the previous item and the fact that arctan x is γ-continuous at zero.

Definition.

A function f ∈ L γ-st is said to have a 'compact support' if it is zero outside some interval [a, b] with a, b γ-finite.

50.

Theorem. Let f ∈ L γ-st be an γ-differentiable function with compact support such that D α f (x) is β-continuous for x ≈ γ 0. We have The product arctan(x/ε)f (x) satisfies all conditions for partial integration, implying in ERNA A , for α ≺ ξ ≺ β. We have introduced the function arctan x, because we needed its properties in theorem 50. The rest of the basic functions of analysis are easily defined and their well-known properties are almost immediate, thanks to Stratified Transfer.

1 π ωα -ωα d(x)f (x)d(x, β) ≈ γ f (0). Proof. Assume that f (x) is zero outside [a, b], with a, b γ-finite. First, we prove that b εα f (x)d(x) d(x, β) ≈ γ 0. As |x| ≥ ε α implies x 2 ≥ ε 2 α we have d(x) = ε ε 2 +x 2 ≤ ε x 2 ≤ ε εα 2 = ε 2 α < ε α . Hence the integral b εα |d(x)| |f (x)| d(x, β) is at most ε α b εα |f (x)| d(x, β). As f is γ-finite and γ-continuous on [a, b], we have b εα f (x)d(x) d(x, β) ≈ γ 0. In the same way, we have εα a f (x)d(x) d(x, β) ≈ γ 0 and εα -εα arctan(x/ε))D α f (x) d(x, β) ≈ γ 0. Hence we have ωα -ωα d(x)f (x)d(x, β) ≈ β b a d(x)f (x) d(x, β) ≈ γ εα -εα d(x)f (x) d(x, β).
In this section, we have shown that analysis can be developed inside ERNA A and its extensions in a concise and elegant way. We did not attempt to give an exhaustive treatment and have deliberately omitted large parts of analysis like e.g. higher order derivatives. It is interesting, however, to briefly consider the latter. In [START_REF] Hrbacek | Stratified analysis?, The strength of nonstandard analysis[END_REF], Hrbacek argues that stratified analysis yields a more elegant way of defining higher order derivatives than regular nonstandard analysis. In this way, a function D α f (x) is differentiable, if it is β-differentiable for β α and f (x) is defined as D β D α f (x). Thus, to manipulate an object such as D α f (x), which is not part of L α-st , we need to go to a higher level β, where D α f (x) is standard. The same principle is at the heart of most theorems in this section, in particular the first fundamental theorem (theorem 46). This principle is the essence of stratified analysis, and occurs in all of mathematics: to study a set of objects, we extend it and gain new insights (e.g. real versus complex analysis). Thanks to Stratified Transfer, all levels have the same standard properties and thus, the extension to a higher level is always uniform.

Towards a formal framework for physics

We have introduced ERNA A and proved its consistency inside PRA. We subsequently obtained several results of analysis using the elegant framework of stratified analysis. Thus, ERNA A is a good formal framework for doing finitistic analysis in a quantifier-free way, akin to the way mathematics is done in physics. As it turns out, Stratified Transfer gives us an even better framework. We sketch an example to illustrate this claim.

It seems only fair to say that physicists employ a lower standard of mathematical rigor than mathematicians (see [START_REF] Davey | Is mathematical rigor necessary in physics?[END_REF] for details). In this way, limits are usually pushed inside or outside integrals without a second thought. Moreover, a widely held 'rule of thumb' is that if, after performing a mathematically dubious manipulation, the result still makes physical and (to a lesser extent) mathematical sense, the manipulation was probably sound. As it turns out, stratified nonstandard analysis is a suitable formal framework for this sort of 'justification a posteriori'. We illustrate this with an example. The first step follows from Stratified Transfer. Indeed, as a finite summation can be pushed through a Riemann integral, a β-finite summation can be pushed through a β-Riemann integral. Thus, we can always obtain h(y) and if it is finite (the very least for it to be physically meaningful), we have h(y) ≈ g(y), thus justifying our 'rule of thumb'. 52. Remark. In [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], the authors introduce the transfer principle Π 1 -TRANS without stating whether standard parameters are allowed or not. Define Π 1 -TRANS (Π 1 -TRANS -) as schema 43 of [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] with (without) standard parameters in ϕ. The proof of theorem 44 in [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF] is obviously only correct for ERNA + Π 1 -TRANS -, as ERNA + Π 1 -TRANS interprets IΣ 1 , by theorem 45 in the same paper. In the rest of [START_REF] Impens | Transfer and a supremum principle for ERNA[END_REF], in particular §4 and §6, the schema Π 1 -TRANS is used. The authors hereby apologize for this oversight. Although the schemas Π α 1 -TRANS -and Π 1 -TRANS - originate from technical considerations, they turn out to play an important role in the context of Reverse Mathematics. We will explore this avenue of research in [START_REF]Levels of Reverse Mathematics[END_REF]. 53. Acknowledgement. The author thanks Professor Karel Hrbacek (City University of New York, City College) for his valuable advice.

0 . ( 7 )

 07 and finally c N 0 := b N 0 and d 0 := f D+1 (c N 0 ). The numbers b l 0 allow us to interpret ε α and ω α : val α (ω α1 ) := b 1 0 , val α (ω α2 ) := b 2 0 , . . . , val α (ω α N -1 ) := b N -1 0 (6) and val α (ε α1 ) := 1/b 1 0 , val α (ε α2 ) := 1/b 2 0 , . . . , val α (ε α N -1 ) := 1/b N -1 Hence we have an interpretation of all terms τ of depth zero such that |val α

nω

  > a and let n 1 be the least n such that n ω > b. Define a ω := n0 ω and b ω := n1-1 ω . Like the derivative, the Riemann integral can only be defined 'up to infinitesimals'. Hence, for α-Riemann integrable functions, it does not matter whether we use the interval [a, b] or the interval [a ω , b ω ] in its definition. From now on, we tacitly assume that a α b. 39. Definition (Riemann Integration). Let f be a function defined on [a, b].

2 . 40 .

 240 ) The function f is α-Riemann integrable on [a, b], if for all partitions of [a, b] with mesh ≈ α 0, the Riemann sums are α-finite and α-infinitely close. (3) If f is α-Riemann integrable on [a, b], then the integral of f over [a, b], denoted as b a f (x) d(x, α), is the Riemann sum corresponding to f of the equidistant partition of [a ω , b ω ] with mesh ε = 1 ω ≈ α 0 and points t i = xi+1+xi Theorem. A function f which is α-continuous and α-finite over [a, b], is α-Riemann integrable over [a, b].

  41. Theorem. Let f be α-continuous and α-finite over [a, b] and assume a α c α b. Hence, b a f (x) d(x, α) ≈ α c a f (x) d(x, α) + b c f (x) d(x, α).Proof. Immediate from the previous theorem and the definition of the Riemann integral. 42. Theorem. Let c be an α-finite positive constant such that c ≈ α 0 and let f be α-continuous and α-finite over [a, b + c]. We have b a f (x + c) d(x, α) ≈ α b+c a+c f (x) d(x, α). Proof. Immediate from theorem 40 and the definition of the Riemann integral. 43. Theorem (Second fundamental theorem). Let f ∈ L α-st be α-continuous on [a, b] and let F (x) be x a f (t)d(t, β). Then F (x) is α-differentiable over (a, b) and the equation D α F (x) ≈ α f (x) holds for all a α x α b.

44.

  Corollary. The condition 'f ∈ L α-st ' in the theorem can be dropped if we require f to be α, β-continuous over [a, b] and α-finite in one point of [a, b]. Proof. It is an easy verification that the proof of the theorem still goes through with these conditions. 45. Example. Define ε = ε 4 α . The function d(x) = ε ε 2 +x 2 is α, β-continuous for α-finite x and at most 1/ε 4 α . The function arctan x := x 0 d(t,β) 1+t 2 is α-differentiable in all α-finite x and we have D α arctan(x/ε) ≈ α ε ε 2 +x 2 for all α-finite x. 46. Theorem (First fundamental theorem)

f

  (x) d(x, β) ≈ α f (c) and d+ε d f (x) d(x, β) ≈ α f (d) and we are done. 47. Corollary (Partial Integration). Let f, g ∈ L α-st be α-differentiable over (a, b) and let D α f and D α g be β-continuous over [a, b]. For a α c α d α b,

If 0 ∈

 0 [a, b], then f (0) = 0 and the theorem follows. Otherwise, by example 45, the function d(x) is α-infinitesimally close to 1 π D α arctan(x/ε), yielding εα -εα d(x)f (x) d(x, β) ≈ α 1 π εα -εα D α (arctan(x/ε)) f (x) d(x, β).

D

  α (arctan(x/ε)) f (x) d(x, β)≈ α arctan (x/ε) f (x) εα -εα -εα -εα arctan(x/ε α )D α f (x)d(x, β) ≈ γ [arctan (x/ε) f (x)] εα -εα = arctan (ε α /ε) f (ε α ) -arctan (-ε α /ε) f (-ε α ) ≈ γ arctan(ω 3 α ) f (0) -arctan(-ω 3 α ) f (0) ≈ γ πf (0).The function d(x) has the typical 'Dirac Delta' shape: 'infinite at zero and zero everywhere else' and many functions like d(x) exist. Also, if we define H(x) = 1 π arctan(x/ε) + 1 2 , we have D α H(x) ≈ α d(x) and H(x) only differs from the 'usual' Heaviside function by an infinitesimal. In the same way as in the previous theorem, it is possible to prove statements like ωα -ωα D ξ d(x)f (x)d(x, β) ≈ γ -ωα -ωα d(x)D ξ f (x)d(x, β) ≈ γ -πD ξ f (0).

  51.Example. Let f i , a and b be standard objects. According to the previously mentioned 'rule of thumb', the following manipulation x, y) dx =:∞ i=0 g i (y) =: g(y)is considered valid in physics as long as the function g(y) is physically and/or mathematically meaningful. In stratified analysis, assuming 0 ≺ α ≺ β, the previous becomes b a ωα i=0 f i (x, y) d(x, β) ≈ ωα i=0 b a f i (x, y) d(x, β) =: ωα i=0 h i (y) =: h(y).

  and x ≤ x (4) if x and y are defined, x + y , x -y , xy and x/y are at most equal to (1 + x )(1 + y ), and xˆy is at most (1 + x )ˆ(1 + y ).