BRICS RS-97-30 U. Kohlenbach: Proof Theory and Computational Analysis BRICS

Basic Research in Computer Science

Proof Theory and Computational Analysis

Ulrich Kohlenbach BRICS Report Series RS-97-30 ISSN 0909-0878 November 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/30/

Proof theory and computational analysis

Ulrich Kohlenbach

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade, Bldg. 540 DK-8000 Aarhus C, Denmark kohlenb@brics.dk

November 1997

Abstract

In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effective uniform bounds and rates of convergence) from non-constructive proofs in numerical analysis.

We focus on the case where the extractability of polynomial bounds is guaranteed. This leads to the concept of hereditarily polynomial bounded analysis PBA. We indicate the mathematical range of PBA which turns out to be surprisingly large.

Finally we discuss the relationship between PBA and so-called feasible analysis FA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs.

In a sequel of appendices to this paper we indicate the expressive power of PBA.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

1 Uniform bounds in analysis

There are (at least) two major challenges in computational analysis:

1) to find algorithms for the computation of basic analytical concepts like e.g. the Riemann integral ∫_{0}^{1} f(x)dx (as well as more general integrals), the supremum sup_{x∈[0,1]} f(x) etc. for functions f ∈ C[0, 1] which are efficient at least under

additional assumptions on f which are satisfied in many practical applications. Sometimes additional assumptions are needed to ensure at all the computability of the concept in question, e.g. in the problem of finding roots etc.

2) to get a-priori bounds on the stopping problems for certain algorithmic procedures, e.g. the rate of convergence of some iterative algorithm. Typically such algorithms compute solutions x_{ε} of ε-weakenings A_{ε}(x) of an equation or a property A(x) (e.g. ε-best approximations instead of best approximations in Chebycheff approximation theory) where

(1) (∀ε > 0A_{ε}(x)) ↔ A(x)

and

(2) ∀x ∈ K, ε, ε̃ > 0(ε < ε̃∧ A_{ε}(x) → Aε̃(x)).

In general a solution x_{ε} for A_{ε}(x) need not to be close to any actual solution of A(x). If x varies over some compact metric space (K, d) and A(x) is ‘ε-continuous’ in the sense

(3) ∀x ∈ K∀ε > 0∃δ > 0∀x̃ ∈ K(d(x, x̃) < δ ∧ A_{ε}(x̃) → A_{2ε}(x))

and if (x_{n})_{n∈IN} ⊂ K with A_{\frac{1}{n}} (x_{n}) for all n ∈ IN, then an easy compactness argument shows that there exists a subsequence of (x_{\frac{1}{n}})_{n∈IN} which converges to a solution of A(x). Example: A(x) :≡ (F (x) =_{IR} 0), where F : K → IR is continuous, and A_{ε}(x) :≡ (|F (x)| ≤_{IR} ε).

Moreover if there exists exactly one solution x_{0} of A(x) in K, then the sequence (x_{\frac{1}{n}})_{n∈IN} itself converges to this solution

(4) n → ∞ ⇒ d(x_{n}, x_{0}) → 0,

but what is the rate of convergence?

Whereas it seems doubtful whether proof theory is able to contribute to 1) (in a narrow sense) it is a potentially useful tool for 2) as is witnessed e.g. in the area of (Chebycheff) approximation theory where new mathematical results on strong unicity and a new quantitative version of the so-called alternation theorem were obtained by proof-theoretic analysis of well-known (non-constructive) uniqueness proof (see [11],[12],[13]).

Let us discuss this further considering (4) again: The uniqueness of x_{0}, i.e.

(5) ∀x_{1}, x_{2} ∈ K(A(x_{1}) ∧ A(x_{2}) → x_{1} = x_{2})

can – using (1), (2) – be written as^{1}

(6) ∀x_{1}, x_{2} ∈ K∀k ∈ IN∃n ∈ IN( \underbrace{A_{\frac{1}{n}} (x_{1}) ∧ A_{\frac{1}{n}} (x_{2}) → d(x_{1}, x_{2}) <_{IR} \frac{1}{k}}_{B(x_{1},x_{2},k,n)} ).

Typically (using a suitable representation of analytical objects like x ∈ K and y ∈ IR) A_{ε}(x) can be written as a Π_{1}^{0}-formula (as in our example above) and so B ∈ Σ_{1}^{0}.^{2} The convergence problem is solved quantitatively if we can construct a uniform witness for ∃n which does not depend on x_{1}, x_{2} ∈ K, i.e.

(7) ∀x_{1}, x_{2} ∈ K∀k ∈ IN(A_{\frac{1}{Φk}} (x_{1}) ∧ A_{\frac{1}{Φk}} (x_{2}) → d(x_{1}, x_{2}) < \frac{1}{k}).

One then immediately concludes that

(8) ∀k ∈ IN(d(x_{Φk}, x_{0}) < \frac{1}{k})

and even (using (2) above)

(9) ∀k ∈ IN∀m ≥ Φk(d(x_{m}, x_{0}) < \frac{1}{k}),

where (x_{n})_{n∈IN} ⊂ K such that A_{\frac{1}{n}} (x_{n}) for all n ≥ 1 and x_{0} ∈ K such that A(x_{0}).

1For simplicity we tacitly assume here that k, n ≥ 1 in order to avoid the need to replace \frac{1}{k} , \frac{1}{n} by \frac{1}{k+1}, \frac{1}{n+1}.

2In the systems we are considering real numbers are represented as (certain) sequences of rational numbers with fixed rate of convergence. Hence =_{IR}, ≤_{IR}∈ Π_{1}^{0} and <_{IR}∈ Σ_{1}^{0} (for details see appendix A1,2).

It is an easy observation (using (2) again) that (6) is monotone w.r.t. ‘∃n’. Hence any uniform bound (not depending on x_{1}, x_{2} ∈ K) provides already a uniform witness. So the whole question comes down to the problem:

How to construct a uniform bound

(10) ∀x_{1}, x_{2} ∈ K∀k ∈ IN∃n ≤ Φk B(x_{1}, x_{2}, k, n)

if

(11) ∀x_{1}, x_{2} ∈ K∀k ∈ IN∃n ∈ IN B(x_{1}, x_{2}, k, n)

holds, where B ∈ Σ_{1}^{0}?

Using a suitable representation of the compact space K, (11) (when formalized in a system in the language of arithmetic in all finite types) has the form

(12) ∀x_{1}, x_{2} ≤_{1} s∀k^{0}∃n^{0}B(x_{1}, x_{2}, k, n)

where ≤_{ρ} is pointwise defined and s is a specific function (given by a closed term of the respective system).

Slightly more general we consider sentences

(13) ∀x^{1}∀k^{0}∀y ≤_{ρ} sxk∃n^{0}B(x, k, y, n),

where B(x, k, y, n) ∈ Σ_{1}^{0} and contains only x, k, y, n as free variables.

Remark 1.1 In (13) above we may have tuples \underline{x} of variables x_{1}^{δ_{1}}, …, x_{m}^{δ_{m}} with deg(δ_{i}) ≤ 1 for i = 1, …, m. Furthermore n may have a type τ with deg(τ) ≤ 2 (we may even have a tuple of such variables) and B may be a formula ∃\underline{v}B_{0}, where B_{0} is quantifier-free and the variables \underline{v} are of arbitrary types. Also we may have tuples \underline{y} of variables y_{i} ≤_{ρ} sxk. For notational simplicity we restrict ourselves to variables n, \underline{v} of type 0. Note that then without loss of generality we may assume B to be quantifier-free.

Our goal is now to construct a computable functional Φ^{0(0)(1)} such that

(14) ∀x^{1}∀k^{0}∀y ≤_{ρ} sxk∃n ≤_{0} Φxk B(x, y, k, n).

Usually and in particular if (13) has been proved non-constructively (both by the use of classical logic as well as by using non-constructive function existence principles like the binary König’s lemma WKL) one cannot directly read of a bound Φ from the proof of (13) and it is here where proof theory comes into the picture. The applicability of proof theory in this area of course depends on various requirements to be satisfied:

1) The extraction of the bound Φ from a proof of (13) must be relatively simple and should leave the original structure of the proof essentially unchanged (in particular it should not cause an enormous increase of the length of the given proof), i.e. it should have a nice behaviour w.r.t. modus ponens (‘modularity’).

2) The proof-theoretic method should be applicable to systems formulated in a rich and flexible language which makes it easy to formalize the analytical concepts used in the proof avoiding complicated coding devices and at the same time allows to formalize many interesting theorems in analysis in the form (13) (i.e. the quantifier-free part of the system should already have a great expressive power).

3) It should be able to treat a variety of genuine analytical principles without increasing the complexity of the extraction procedure or the bound extracted.

4) It should faithfully reflect the numerical content w.r.t. bounds of the given proof and provide bounds of low growth (relative to the growth of the terms used in the proof) if no complicated instances of induction are used in the proof.

Condition 1) rules out methods based on cut-elimination or normalization of proofs. Condition 2) makes it desirable to have a method which applies to systems formulated in a language of all finite types instead of second-order languages. Condition 3) rules out the usual Gödel functional interpretation (with a negative translation on top of it). Moreover it provides an additional obstacle to a combination of negative translation followed by the Friedman/Dragalin A-translation and modified realizability interpretation, since the A-translation does not capture the negative translation of the axiom of quantifier-free choice (this will be discussed in a paper under preparation).

A method which we believe fulfils these requirements is the monotone functional interpretation which was developed in [13],[15] (the technique used in [10] can be viewed of as a precursor of this method). Monotone functional interpretation is a variant of Gödel’s functional interpretation [6] and extracts majorizing functionals (in the sense of Howard [8]) of functionals satisfying the usual Gödel functional interpretation. These majorizing functionals keep control through all finite types of the growth rates involved in a given proof without any normalization. The method applies to (sub-)systems of classical arithmetic in all finite types extended by the axiom schema of quantifier-free choice

AC^{ρ,τ}-qf : ∀x^{ρ}∃y^{τ}A_{0}(x, y) → ∃Y^{τ(ρ)}∀x^{ρ}A_{0}(x, Y x), AC-qf := ⋃_{ρ,τ∈T}{AC^{ρ,τ}-qf },

where A_{0} is a quantifier-free formula,^{3} but also to various (mostly non-constructive) analytical axioms Δ covering a great deal of classical analysis (see section 3 below). Furthermore the method can be combined with the elimination of Skolem function procedure from [16] and this combination is able to deal also with principles which go beyond WKL and cannot be treated by the monotone functional interpretation in a direct way.

A case of particular mathematical and computational interest is when Φ is guaranteed to be a polynomial in k and (in some sense also in) x. This has led to the study of hereditarily polynomial bounded analysis which has to be carefully distinguished from so-called feasible analysis as we are going to discuss now.

2 Hereditarily polynomial bounded analysis versus feasible analysis

By hereditarily polynomial bounded analysis we mean subsystems PBA of analysis 𝔄 whose provably recursive functions (and in some sense explained below also functionals) can be bounded by polynomials p ∈ IN[k]. More specific (restricting ourselves for the moment to the special case of (13) where ∀x^{1} is not present) the following rule is supposed to hold:

(15) \{ \begin{matrix}PBA ⊢ ∀k^{0}∀y ≤_{ρ} sk∃z^{0}A_{0}(k, y, z) \\ ⇒ one can extract a polynomial p(k) ∈ IN[k] such that \\ PBA^{∗} ⊢ ∀k^{0}∀y ≤_{ρ} sk∃z ≤_{0} p(k) A_{0}(k, y, z), \end{matrix}

where PBA^{∗} is a system closely related to PBA (here s is a closed term of PBA and A_{0}(k, y, z) contains only k, y, z as free variables).

3Throughout this paper A_{0}, B_{0}, C_{0}, … denote quantifier-free formulas. We allow bounded number quantifiers ∀x ≤_{0} t, ∃x ≤_{0} t to occur in A_{0}, B_{0}, C_{0}, … since they can be expressed in a quantifier-free way using the bounded search-functional μ_{b} which is included to all systems we are considering. T denotes the set of all finite types.

If the statement ∀k^{0}∀y ≤_{ρ} sk∃z^{0}A_{0}(k, y, z) is monotone w.r.t. ‘∃z’, as is typically the case because of the very way in which sentences of this type arise in analysis (namely as ∀ε > 0∃δ > 0-statements, see section 4 below), then the uniform bound p(k) realizes the quantifier

(16) PBA^{∗} ⊢ ∀k^{0}∀y ≤_{ρ} sk A_{0}(k, y, p(k)).

Feasible analysis – FA for short – in the sense of e.g. [4] in contrast to PBA refers to subsystems of analysis with feasible (poly-time) Skolem functions for provable Π_{2}^{0}- sentences, i.e.

(17) \{ \begin{matrix}FA ⊢ ∀k^{0}∃z^{0}A_{0}(k, z) \\ ⇒ ∃f ∈ P olytime \\ FA^{∗} ⊢ ∀k^{0}A_{0}(k, f(k)). \end{matrix}

Ferreira introduced in [4] a system of FA in the language of second-order arithmetic which includes a suitable version of the binary König’s lemma WKL. He in particular proved (17) for his system (where FA^{∗} := FA minus WKL).

Both approaches are incomparable:

1) The existence of a bound p(k) ∈ IN[k] of course yields a bound in P olytime^{4}, namely p, but not a poly-time witness function (not even when A_{0} is poly-time decidable which typically will not be the case in PBA) since P olytime is not closed under bounded search (but only under sharply bounded search).

2) The existence of a poly-time Skolem function f in (17) does not imply the existence of a bound p(k) ∈ IN[k] since not every poly-time function is bounded by a polynomial, e.g. f(k) := k^{logk} is poly-time but growths faster than every polynomial.

So in short: hereditarily polynomial bounded analysis guarantees the extractability of uniform polynomial bounds whereas feasible analysis guarantees the existence (or when treated proof-theoretically the extractability) of poly-time algorithms. Although the latter approach may yield applications e.g. in the area of analytical number theory, many existential statement in analysis are monotone and therefore the restriction to bounds is no restriction at all here but has tremendous benefits: it allows to incorporate many analytical constructions and principles which are known to be unfeasible (unless the polynomial hierarchy collapses). E.g. the work of H. Friedman and K.-I. Ko (see [9]) shows that almost all basic concepts in analysis, e.g. the Riemann integral, the supremum sup_{x∈[0,1]} f(x) and many others are not feasible (in

4P olytime here denotes the set of all poly-time computable n-ary number-theoretic functions.

general). So to a great extend one can say that there is no such thing as feasible analysis. On the other hand hereditarily polynomial bounded analysis is amazingly rich both w.r.t. to the size of the fragment of analysis which can be carried out in a suitable system for PBA and w.r.t. to the great variety of theorems which can be expressed in the form (13) which is due to the fact that e.g. ∫_{0}^{1} f(x)dx and sup_{x∈[0,1]} f(x)

can be defined explicitly in PBA by certain functionals of type level 2 (see appendix A4 below).

3 The range of hereditarily polynomial analysis

In [14],[15] we proposed a system G_{2}A^{ω}+ AC-qf +Δ for PBA. Here G_{2}A^{ω} is the second system in a hierarchy of subsystems (G_{n}A^{ω})_{n∈IN} of arithmetic in all finite types. The definable type-1-objects of G_{n}A^{ω} correspond to the well-known Grzegorczyk hierarchy. Moreover G_{n}A^{ω} contains various functionals of higher type, a rule of quantifier-free extensionality in higher types where s =_{ρ} t is an abbreviation for ∀\underline{x}(s\underline{x} =_{0} t\underline{x}), and all true universal axioms ∀\underline{x}A_{0}(\underline{x}) where A_{0} is a quantifier-free formula and \underline{x} is a tuple of variables of types ≤ 2. Here ‘true’ refers to validity in the full set-theoretic type structure S^{ω}. In particular these universal axioms capture the schema of quantifier-free induction (since bounded quantification can be expressed in a quantifier-free way in G_{n}A^{ω} using a bounded search functional). The reason for including all true universal axioms of the type above as axioms instead of using only the schema of quantifier-free induction is that axioms of this form have a trivial (monotone) functional interpretation and therefore do not contribute to the extractable bounds by their proofs but only by the terms used in their formulation. Of course in specific proofs only finitely many of them are used.

In the special case of G_{2}A^{ω} we have the Π_{ρ,τ}, Σ_{δ,ρ,τ}-combinators for all types (which allow the definition of λ-abstraction), constants 0^{0} (zero), S^{00} (successor), min_{0} and max_{0} (minimum and maximum of pairs of numbers), + (addition), · (multiplication), bounded predicative recursor constants R̃_{ρ}, a bounded search functional μ_{b}, a bounded maximum functional Φ_{max}fx (= max_{0}(f0, …, fx) and a bounded sum functional

Φ_{Σ}fx (= ∑_{i=0}^{x} fi).

Δ is a set of axioms having the logical form

(18) ∀x^{δ}∃y ≤_{ρ} sx∀z^{τ}A_{0}(x, y, z),

where A_{0} is quantifier-free (containing only x, y, z as free variables), s is a closed term of G_{n}A^{ω} and δ, ρ, τ are arbitrary finite types. It turns out that many non-constructive analytical theorems can be formalized as axioms (18). Nevertheless one of the main features of monotone functional interpretation is that axioms (18) can be seen not to contribute to the bound extracted (or to the complexity of the extraction procedure) by their proofs but only by majorizing functionals (in the sense of [8]) for the terms s. Hence we can treat them as axioms as well. However we want to keep track of their use (and therefore do not include them in the definition of G_{n}A^{ω}) since at some places we need to replace them by certain ε-weakenings. The reason for this is that we want to make use also of a certain non-standard axiom

(19) F^{−} :≡ ∀Φ^{2(0)}, y^{1(0)}∃y_{0} ≤_{1(0)} y∀k^{0}, z^{1}, n^{0}( ⋀_{i<_{0}n}(zi ≤_{0} yki) → Φk(\overline{z, n}) ≤_{0} Φk(y_{0}k)),

(where, for z^{ρ0}, (\overline{z, n})(k^{0}) :=_{ρ} zk, if k <_{0} n and := 0^{ρ}, otherwise). F^{−} is not true in S^{ω} since it implies that every functional Φ^{2} is bounded on all functions \overline{1, n} for all n ∈ IN. However to construct a counterexample to F^{−} one has to use arithmetical comprehension over functions which is not available in our systems. In fact we are able to reduce F^{−} (which has the logical form of an axiom Δ!) in proofs of sentences (13) (relative to G_{n}A^{ω} + Δ+ AC-qf) to its ε-weakening which is true in S^{ω} and even provable in G_{3}A^{ω}. Combined with AC^{1,0}-qf, F^{−} proves a strong principle of uniform boundedness which allows to give very short proves of various non-constructive analytical principles including a strong version of WKL (for details on this see [15],[17]).

Definition 3.1 A term t[x^{1}, k^{0}] of type 0 is called a polynomial in x, k if it is built up from 0^{0}, S, +, ·, x, k only by application.

Notation 3.2 1) For f^{1} we define f^{M} := Φ_{max}f.

2) Δ̃ := {∃V ≤_{δγ} t∀u^{γ}, w^{τ}G_{0}(u, V u, w) : ∀u^{γ}∃v ≤_{δ} tu∀w^{τ}G_{0}(u, v, w) ∈ Δ}.

3) G_{n}A_{i}^{ω} denotes the intuitionistic variant of G_{n}A^{ω}.

4) E-G_{n}A^{ω} is the extension of G_{n}A^{ω} obtained by adding the extensionality implication for all types.

Theorem 3.3 ([14],[15]) Let A_{1}(x^{1}, k^{0}, y^{1}, z^{0}) be a Σ_{1}^{0}-formula which contains only x, k, y, z as free variables and let s be a closed term of G_{n}A^{ω}. Furthermore let Δ be a set of closed axioms of the form ∀u^{γ}∃u ≤_{δ} ∀w^{τ}G_{0}(u, v, w) with deg(δ) ≤ 1. Then the following rule holds

(20) \{ \begin{matrix}E-G_{2}A^{ω}+ AC^{1,0}-qf + AC^{0,1}-qf + Δ + F^{−} ⊢ ∀x^{1}∀k^{0}∀y ≤_{1} sxk∃z^{0}A_{1}(x, k, y, z) \\ ⇒ one can extract a polynomial Φ[x, k] in x, k such that \\ G_{3}A_{i}^{ω} + Δ̃ ⊢ ∀x^{1}∀k^{0}∀y ≤_{1} sxk∃z ≤_{0} Φ[x^{M}, k] A_{1}(x, k, y, z). \end{matrix}

Remark 3.4 1) Note that in the theorem above we extract a polynomial bound whereas its verification uses an (exponential) coding functional Φ_{⟨⟩}fx := ⟨f0, …, f(x − 1)⟩ which is definable in G_{3}A^{ω} but not in G_{2}A^{ω}.

2) For G_{2}A^{ω} instead of E-G_{2}A^{ω} and ⊕F^{−} instead of +F^{−} one^{5} may have full quantifier-free choice AC-qf and y^{ρ} for arbitrary type ρ in the theorem above. In this case we also can allow δ in Δ to be an arbitrary finite type. In this form theorem 3.3 is proved in [15]. The present formulation follows by the well-known extensionality elimination procedure, see [15](proof of cor.3.1.4).

The extraction of a bound Ψ in the theorem above which is built up only from Π_{ρ,τ}, Σ_{δ,ρ,τ} (for certain types δ, ρ, τ), S, +, · is obtained by monotone functional interpretation without any normalization involved. It is only if one wants to write Ψxk as a polynomial Φ[x, k] that one has to use logical normalization (i.e. normalization w.r.t. Π,Σ-reductions).

Theorem 3.3 remains true if we add new function symbols φ^{ρ} (deg(ρ) ≤ 1) to G_{n}A^{ω} together with certain universal axioms ∀x^{τ}A_{0}(x) (deg(τ) ≤ 2) about them including an axiom of the form t ≥_{ρ} φ for some closed term t of G_{n}A^{ω} (see theorem 3.2.8 of [15]). If these axioms are true in S^{ω} for say the intended interpretation of φ, then S^{ω} is a model also for this extension of G_{n}A^{ω} and since such extensions don’t have any impact on extractable bounds we are free to use them and will do so in appendix B and still denote the resulting system by G_{n}A^{ω}.

5Here ⊕ means that F^{−} must not be used in the proof of the premise of an application of the quantifier–free rule of extensionality QF–ER. G_{n}A^{ω} satisfies the deduction theorem w.r.t ⊕ but not w.r.t +.

Theorem 3.5 ([14],[15],[17]) For suitable axioms Δ of the form ∀u^{1}∃v ≤_{1} tu∀w^{1}G_{0}(u, v, w), E-G_{2}A^{ω}+ AC^{1,0}-qf + AC^{0,1}-qf +Δ + F^{−} contains a substantial part of analysis including:

1) Basic properties of the operations +, −, ·, (·)^{−1}, | · |, max, min and the relations =, ≤, < for rational numbers and real numbers (which are given by Cauchy sequences of rationals with fixed Cauchy rate of convergence).

2) Basic properties of maximum and sum for sequences of real numbers of variable length.

3) Basic properties of uniformly continuous functions f : [a, b]^{d} → IR, sup_{x∈[a,b]} f(x)

and ∫_{a}^{x} f(x)dx for f ∈ C[a, b] where a < b and x ∈ [0, 1].

4) The Leibniz criterion, the quotient criterion, the comparison test for series of real numbers. The convergence of the geometric series together with its sum formula. The non-convergence of the harmonic series. (But not: The Cauchy property of bounded monotone sequences in IR or the Bolzano–Weierstraß property for bounded sequences in IR).

5) Characteristic properties of the trigonometric functions sin, cos, tan, arcsin, arccos, arctan and of the restrictions exp_{k} and ln_{k} of exp, ln to [−k, k] for every fixed number k.

6) Fundamental theorem of calculus.

7) Fejér’s theorem on uniform approximation of 2π–periodic uniformly continuous functions f : IR → IR by trigonometric polynomials.

8) Equivalence (local and global) of sequential continuity and ε–δ–continuity for

f : IR → IR.

9) Mean value theorem of differentiation.

10) Mean value theorem for integrals.

11) Cauchy–Peano existence theorem.

12) Brouwer’s fixed point theorem for uniformly continuous functions f : [a, b]^{d} → [a, b]^{d}.

13) Attainment of the maximum of f ∈ C([a, b]^{d}, IR) on [a, b]^{d}.

14) Uniform continuity (together with the existence of a modulus of uniform continuity) of pointwise continuous functions f : [a, b]^{d} → IR.

15) Sequential form of the Heine–Borel covering property of [a, b]^{d} ⊂ IR^{d}.

16) Dini’s theorem: Every sequence (G_{n}) of pointwise continuous functions G_{n} : [a, b]^{d} → IR which increases pointwise to a pointwise continuous function G : [a, b]^{d} → IR converges uniformly on [a, b]^{d} to G and there exists a modulus of uniform convergence.

17) Every strictly increasing pointwise continuous function G : [a, b] → IR possesses a uniformly continuous strictly increasing inverse function G^{−1} : [Ga, Gb] → [a, b].

18) a higher type formulation of König’s lemma WKL_{seq}^{2} for sequences of binary trees.^{6}

Remark 3.6 The reason for assuming f to be uniformly continuous in some of the principles 1)-13) mentioned in the theorem, although we can weaken this to pointwise continuity in view of 14), is to make explicit the use of the non-standard axiom F^{−} which is used only for 14)-18).

Let us denote from now on E-G_{2}A^{ω}+ AC^{1,0}-qf + AC^{0,1}-qf +Δ + F^{−} by PBA (for a set of axioms Δ sufficient for theorem 3.5).

Theorem 3.5 is proved in [14]. Various parts of it are published: In [15] we showed that PBA (even for Δ = ∅) proves 18). In [17] it is shown that PBA proves (again with Δ = ∅) 13)–17). 9) easily follows from 13). It is an easy exercise that 8) is provable in G_{2}A^{ω}+ AC^{0,1}-qf. Using a suitable representation of C([a, b]^{d}, IR) which is developed in [14] one can show that 10)-12) can be written directly as axioms Δ. 6) and 7) follow from suitable quantitative versions which can be expressed as universal axioms. 1) is carried out in detail in [18]. In an appendix to this paper we show 2),3) and 4).

6See [15] for details. The usual formulation of WKL cannot be written down in G_{2}A^{ω} since it requires the coding functional Φ_{⟨⟩}fx := ⟨f0, …, f(x − 1)⟩. In G_{3}A^{ω} one can show that WKL_{seq}^{2} implies WKL.

Theorems 3.3,3.5 can also be viewed as a vast extension of a result by Parikh [19]: Parikh considered a fragment PB of Peano arithmetic PA which contains the schema of induction only for bounded formulas. He shows that if a sentence ∀x∃y A(x, y) (A(x, y) being a bounded formula) is provable in PB then there exists a polynomial p such that PB proves ∀x∃y ≤ p(x) A(x, y). So PB can be considered as a (very weak) system of polynomially bounded arithmetic.

4 The expressive power of sentences ∀x^{1}∀k^{0}∀y ≤_{1} sxk∃z^{0}A_{1} in G_{2}A^{ω}

For the applicability of theorems 3.3,3.5 it is of relevance what kind of analytical theorems are formalizable in G_{2}A^{ω} as sentences

(21) ∀x^{1}∀k^{0}∀y ≤_{1} sxk∃z^{0}A_{1}(x, k, y, z),

where A_{1} ∈ Σ_{1}^{0}. Sentences (21) typically arise as follows: Let X be a complete separable metric space, K a compact metric space and F, G : X × K → IR constructively definable (and therefore continuous) functions. Many interesting theorems in analysis (e.g. a large class of uniqueness theorems, see [11]) can be written in the form

(22) ∀x ∈ X∀y ∈ K(F (x, y) = 0 → G(x, y) = 0)

and thus

(23) ∀x ∈ X∀y ∈ K∀k ∈ IN∃n ∈ IN(|F (x, y)| ≤ \frac{1}{n + 1} → |G(x, y)| < \frac{1}{k + 1}).

In order to formalize (23) as a sentence (21) in G_{2}A^{ω} one has to represent quantification over X (resp. over K) by quantification of the form ‘∀x^{1}(A_{X}(x) → …)’ (resp. ‘∀y ≤_{1} s(A_{K}(y) → …)’ for a closed term s of G_{2}A^{ω}) where A_{X}, A_{K} ∈ Π_{1}^{0} and F, G are definable in G_{2}A^{ω} (and provably extensional w.r.t. =_{X×K}, =_{IR}) by functionals Φ_{F}^{1(1)(1)}, Φ_{G}^{1(1)(1)} (given by closed terms of G_{2}A^{ω}). Then (23) has the form

(24) ∀x^{1}∀y ≤_{1} s∀k^{0}∃n^{0}(A_{X}(x)∧A_{K}(y)∧|Φ_{F} (x, y)| ≤_{IR} \frac{1}{n + 1} → |Φ_{G}(x, y)| <_{IR} \frac{1}{k + 1}),

where ‘( …)’ can be prenexed into a Σ_{1}^{0}-formula.

In finite type systems of the sort we are considering many spaces X, K can be represented even in such a way that the predicates A_{X}, A_{K} do not occur (see e.g.[1],[11]). In [14] we have shown that e.g. the spaces IR^{d}, C([a, b]^{d}, IR) and the compact space [a_{1}, b_{1}]×… [a_{d}, b_{d}] can be represented in this way already in G_{2}A^{ω} (for d = 1 we show this in the appendix A2,3 to this paper). Whereas the fact that one can get rid of A_{X}, A_{K} is crucial in recognizing that certain (non-constructive) analytical tools (e.g. Brouwer’s fixed point theorem) can be written as axioms Δ, it is not necessary for the formalization of (23) in the form (24) which allows very simple representations. E.g. (using the representation of rational numbers and reals from [18]) continuous functions F ∈ C[0, 1] can be represented simply as pairs (f^{1(0)}, ω_{f}^{1}) where f represents a function [0, 1] ∩ Q → IR and ω_{f} a modulus of uniform continuity of f, i.e.

(25) ∀x^{0}, y^{0}, k^{0}(0 ≤Q x, y ≤Q 1 ∧ |x −Q y| ≤Q \frac{1}{ω(k) + 1} → |fx −_{IR} fy| ≤_{IR} \frac{1}{k + 1}).

Note that (25) ∈ Π_{1}^{0}.

The expressive power of sentences (22) crucially depends on what functions F, G are definable in G_{2}A^{ω}. In appendix A4 we show that e.g. F : C[0, 1] → IR, F (f) := sup_{x∈[0,1]} f(x) and G : C[0, 1] → IR, G(f) := ∫_{0}^{1} f(x)dx are definable in G_{2}A^{ω}. So in

our sentences (22) we are free to use these functions although they are not feasible and are still able to extract polynomial (and hence poly-time) bounds from proofs in PBA. The definability of F, G in G_{2}A^{ω} is due to the fact that we have the functionals Φ_{max}, Φ_{Σ} available. Both functionals are not feasible (and therefore not allowed in FA) but don’t cause any problems in the framework of PBA since they can be majorized (in the sense of Howard [8]) by λf, x.f(x) resp. λf, x.(x + 1) · f(x).

References

[1] Beeson, M., Foundations of Constructive Mathematics. Springer Ergebnisse der Mathematik und ihrer Grenzgebiete 3. Folge, Band 6. Springer Berlin Heidelberg New York Tokyo 1985.

[2] Bishop, E.– Bridges, D. , Constructive analysis. Springer Grundlehren der mathematischen Wissenschaften vol.279, Berlin 1985.

[3] Brown, D.K.– Simpson, S.G., Which set existence axioms are needed to prove the separable Hahn–Banach theorem? Ann. Pure Appl. Logic 31, pp. 123–144 (1986).

[4] Ferreira, F., A feasible theory for analysis. J. Smybolic Logic 59, pp. 1001–1011 (1994).

[5] Forster, O., Analysis 1. Vieweg, Braunschweig/Wiesbaden (1976).

[6] Gödel, K., Über eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes. Dialectica 12, pp. 280–287 (1958).

[7] Heuser, H., Lehrbuch der Analysis: Teil 1. Teubner, Stuttgart (1980).

[8] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (1973).

[9] Ko, K.–I., Complexity theory of real functions. Birkhäuser; Boston, Basel, Berlin (1991).

[10] Kohlenbach, U., Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symbolic Logic 57, pp. 1239–1273 (1992).

[11] Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Ann. Pure Appl. Logic 64, pp. 27–94 (1993).

[12] Kohlenbach, U., New effective moduli of uniqueness and uniform a–priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numer. Funct. Anal. and Optimiz. 14, pp. 581–606 (1993).

[13] Kohlenbach, U., Analysing proofs in analysis. In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225–260, Oxford University Press (1996).

[14] Kohlenbach, U., Real growth in standard parts of analysis. Habilitationsschrift, pp. xv+166, Frankfurt (1995).

[15] Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of provably recursive functionals. Arch. Math. Logic 36, pp. 31–71 (1996).

[16] Kohlenbach, U., Elimination of Skolem functions for monotone formulas. To appear in: Archive for Mathematical Logic.

[17] Kohlenbach, U., The use of a logical principle of uniform boundedness in analysis. To appear in: Proc. ‘Logic in Florence 1995’.

[18] Kohlenbach, U., Arithmetizing proofs in analysis. To appear in: Proc. Logic Colloquium 96 (San Sebastian).

[19] Parikh, R.J. Existence and feasibility in arithmetic. J. Symbolic Logic 36, pp.494–508 (1971).

[20] Troelstra, A.S. (ed.) Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics 344 (1973).

[21] Troelstra, A.S. – van Dalen, D., Constructivism in mathematics: An introduction. Vol. I,II. North–Holland, Amsterdam (1988).

In the following two appendices we present some technical details about the representability of basic analytical concepts in G_{2}A^{ω} from [14] which have been unpublished hitherto but which are of relevance for the material presented in this paper. We assume some familiarity with notions introduced in [15]. G_{n}R^{ω} denotes the set of all closed terms of G_{n}A^{ω}. For the treatment of higher non-constructive analytical principles (mentioned in this article) see [15],[17],[18].

A C[0, 1], sup_{x∈[0,1]} f(x) and ∫_{0}^{1} f(x)dx in G_{2}A^{ω}

A.1 Real numbers in G_{2}A^{ω}

We recall the representation of real numbers used in [18] on which the representation of continuous functions developed in the next section is based. We have to start with the representation of Q: Rational numbers are represented as codes j(n, m) of pairs (n, m) of natural numbers n, m. j(n, m) represents

the rational number \frac{\frac{n}{2}}{m + 1}, if n is even, and the negative rational − \frac{\frac{n+1}{2}}{m + 1} if n is odd.

Here j ∈ G_{2}R^{ω} is the surjective pairing function j(x, y) := \frac{1}{2}((x + y)^{2} + 3x + y). On the codes of Q, i.e. on IN, we have an equivalence relation by

n_{1} =Q n_{2} :≡ \frac{\frac{j_{1}n_{1}}{2}}{j_{2}n_{1} + 1} = \frac{\frac{j_{1}n_{2}}{2}}{j_{2}n_{2} + 1} if j_{1}n_{1}, j_{1}n_{2} both are even

and analogously in the remaining cases, where \frac{a}{b} = \frac{c}{d} is defined to hold iff ad =_{0} cb (for bd > 0). On IN one easily defines functions |·|Q, +Q, −Q, ·Q :Q, maxQ, minQ ∈ G_{2}R^{ω} and (quantifier– free) relations) <Q, ≤Q which represent the corresponding functions and relations on Q. We sometimes omit the index Q if this does not cause any confusion.

Notational convention: For better readability we often write e.g. \frac{1}{k+1} instead of its code

j(2, k) in IN. So e.g. we write x^{0} ≤Q \frac{1}{k+1} for x ≤Q j(2, k).

By the coding of rational numbers as natural numbers, sequences of rationals are just functions f^{1} (and every function f^{1} can be conceived as a sequence of rational numbers in a unique way). So real numbers can be represented by functions f^{1} modulo this coding. We now show that every function can be conceived as an representative of a uniquely determined Cauchy sequence of rationals with modulus 1/(k + 1) and therefore can be conceived as an representative of a uniquely determined real number.

Definition A.1.1 The functional λf^{1}.f̂ ∈ G_{2}R^{ω} is defined such that

f̂n = \{ \begin{matrix}fn, if ∀k, m, m̃ ≤_{0} n(m, m̃ ≥_{0} k → |fm −Q fm̃| ≤Q \frac{1}{k+1}) \\ f(n_{0} − 1) for n_{0} := min l ≤_{0} n[∃k, m, m̃ ≤_{0} l(m, m̃ ≥_{0} k ∧ |fm −Q fm̃| >Q \frac{1}{k+1})], \\ otherwise. \end{matrix}

It is clear that (provable in G_{2}A^{ω})

1) if f^{1} represents a Cauchy sequence of rational numbers with modulus 1/(k + 1), then ∀n^{0}(fn =_{0} f̂n),

2) for every f^{1} the function f̂ represents a Cauchy sequence of rational numbers with modulus 1/(k + 1).

Hence every function f gives a uniquely determined real number, namely that number which is represented by f̂. Quantification ∀x ∈ IR A(x) (∃x ∈ IR A(x)) so reduces to the quantification ∀f^{1}A(f̂) (∃f^{1}A(f̂)) for properties A which are extensional w.r.t. =_{IR} below (i.e. which are really properties of real numbers). Operations Φ : IR → IR are given by functionals Φ^{1(1)} (which are extensional w.r.t.=_{1}). A real function : IR → IR is given by a functional Φ^{1(1)} which (in addition) is extensional w.r.t. =_{IR} . For convenience we often write (x_{n}) instead of fn and (x̂_{n}) instead of f̂n. One easily defines in G_{2}A^{ω} the usual relations and operations of IR on the representatives of the reals:

Definition A.1.2 1) (x_{n}) =_{IR} (x̃_{n}) :≡ ∀k^{0}(|x̂_{k} −Q ˆ x̃_{k}| ≤Q \frac{3}{k+1});

2) (x_{n}) <_{IR} (x̃_{n}) :≡ ∃k^{0}(ˆx̃_{k} − x̂_{k} >Q \frac{3}{k+1});

3) (x_{n}) ≤_{IR} (x̃_{n}) :≡ ¬(ˆx̃_{n}) <_{IR} (x̂_{n});

4) (x_{n}) +_{IR} (x̃_{n}) := (x̂_{2n+1} +Q ˆ x̃_{2n+1});

5) (x_{n}) −_{IR} (x̃_{n}) := (x̂_{2n+1} −Q ˆ x̃_{2n+1});

6) |(x_{n})|_{IR} := (|x̂_{n}|Q);

7) (x_{n}) ·_{IR} (x̃_{n}) := (x̂_{2(n+1)k} ·Q ˆ x̃_{2(n+1)k}), where k := ⌈maxQ(|x_{0}|Q + 1, |x̃_{0}|Q + 1)⌉;

8) For (x_{n}) and l^{0} we define

(x_{n})^{−1} := \{ \begin{matrix}(maxQ(x̂_{(n+1)(l+1)^{2}}, \frac{1}{l+1})^{−1}), if x̂_{2(l+1)} >Q 0 \\ (minQ(x̂_{(n+1)(l+1)^{2}}, \frac{−1}{l+1})^{−1}), otherwise; \end{matrix}

9) max_{IR} ((x_{n}), (x̃_{n})) := ( maxQ(x̂_{n}, ˆ x̃_{n})), min_{IR} ((x_{n}), (x̃_{n})) := ( minQ(x̂_{n}, ˆ x̃_{n})).

G_{2}A^{ω} suffices to prove the usual properties of the relations and operations represented above (see [18] for details).

Notational convention: For notational simplicity we often omit the embedding Q ↪ IR, e.g. x^{1} ≤_{IR} y^{0} stands for x ≤_{IR} λn.y^{0}. From the type of the objects it will be always clear what is meant.

If (f_{n})_{n∈IN} of type 1(0) represents a \frac{1}{k+1}–Cauchy sequence of real numbers, then (provably

in G_{2}A^{ω}) f(n) := f̂_{3(n+1)}(3(n+1)) represents the limit of this sequence, i.e. ∀k(|f_{k}−_{IR}f| ≤_{IR}

\frac{1}{k+1}).

A.2 Representation of [0,1]⊂ IR in G_{2}A^{ω}

Every element of [0, 1] can be represented already by a bounded function f ∈ {f : f ≤_{1} M}, where M is a fixed function from G_{2}R^{ω} and that every function from this set can be conceived as an (representative of an) element in [0,1]: Define a function q ∈ G_{2}R^{ω} by

q(n) := \{ \begin{matrix}min l ≤_{0} n[l =Q n], if 0 ≤Q n ≤Q 1 \\ 0^{0}, otherwise. \end{matrix}

Every rational number ∈ [0, 1] ∩ Q has a unique code by a number ∈ q(IN) and ∀n^{0}(q(q(n)) =_{0} q(n)). Also every such number codes an element of ∈ [0, 1] ∩ Q. We may conceive every number n as a representative of a rational number ∈ [0, 1] ∩ Q, namely of the rational coded by q(n). In contrast to IR we can restrict the set of representing functions for [0,1] to the compact (in the sense of the Baire space) set f ∈ {f : f ≤_{1} M}, where M(n) := j(6(n + 1), 3(n + 1) − 1): Each fraction r having the form \frac{i}{3(n+1)} (with i ≤ 3(n + 1)) is represented by a number k ≤ M(n), i.e. k ≤ M(n) ∧ q(k) codes r. Thus {k : k ≤ M(n)} contains (modulo this coding) an \frac{1}{3(n+1)}–net for [0,1]. Let λf.f̃ ∈ G_{2}R^{ω} be such that

f̃(k) = q(i_{0}),

where i_{0} = μi ≤_{0} M(k)[∀j ≤_{0} M(k)(|f̂(3(k + 1)) −Q q(j)| ≥Q |f̂(3(k + 1)) −Q q(i)|)].

f̃ has (provably in G_{2}A^{ω}) the following properties:

1) ∀f^{1}(f̃ ≤_{1} M).

2) ∀f^{1}(ˆf̃ =_{1} f̃).

3) ∀f^{1}(0 ≤_{IR} f̃ ≤_{IR} 1).

4) ∀f^{1}(0 ≤_{IR} f ≤_{IR} 1 → f =_{IR} f̃).

5) ∀f^{1}(˜f̃ =_{IR} f̃).

Using this construction we can reduce quantification ∀x ∈ [0, 1] A(x) and ∃x ∈ [0, 1] A(x) to quantification of the form ∀f ≤_{1} M A(f̃) and ∃f ≤_{1} M A(f̃) for properties A which are =_{IR}–extensional (for f_{1}, f_{2} such that 0 ≤_{IR} f_{1}, f_{2} ≤_{IR} 1), where M ∈ G_{2}R^{ω} . Analogously one can define a representation of [a, b] for variable a^{1}, b^{1} such that a <_{IR} b by bounded functions {f^{1} : f ≤_{1} M(a, b)}. However one can easily reduce the quantification over [a, b] to quantification over [0, 1] using the convex combination a(1−x)+bx where x varies over [0, 1] so that we do not need this generalization. But on some occasions it is convenient to have an explicit representation for [−k, k] for all natural numbers k. This representation is analogous to the representation of [0, 1] except that we now define M_{k}(n) := j(6k(n + 1), 3(n + 1) − 1) as the bounding function. The construction corresponding to λf.f̃ is also denoted by f̃ since it will be always clear from the context what interval we have in mind.

A.3 Representation of continuous functions f : [0, 1] → IR by number theoretic functions

Functions f : [a, b] → IR (a, b ∈ IR, a < b) are represented in G_{n}A^{ω} by functionals Φ^{1(1)} which are =_{IR}–extensional:

∀x^{1}, y^{1}(a^{1} ≤_{IR} x, y ≤_{IR} b^{1} ∧ x =_{IR} y → Φx =_{IR} Φy).

Let f : [a, b] → IR be a pointwise continuous function. Then (classically) f is uniformly continuous and possesses a modulus ω : IN → IN of uniform continuity, i.e.

∀x, y ∈ [a, b], k ∈ IN(|x − y| ≤ \frac{1}{ω(k) + 1} → |fx − fy| ≤ \frac{1}{k + 1}).

In G_{n}A^{ω} this reads as follows

(+) ∀x^{1}, y^{1}, k^{0}(a^{1} ≤_{IR} x, y ≤_{IR} b ∧ |x −_{IR} y| ≤_{IR} \frac{1}{ω(k) + 1} → |Φx −_{IR} Φy| ≤_{IR} \frac{1}{k + 1}).

Thus quantification over continuous functions : [a, b] → IR corresponds in G_{n}A^{ω} to quantification over all Φ^{1(1)}, ω^{1} which fulfil (+). In the following we show how this quantification over objects of type level 2 can be reduced to type–1–quantification and how the condition (+) can be eliminated so that quantification over continuous functions on [a, b] corresponds exactly to (unrestricted) quantification over f^{1}. We do this first for a = 0, b = 1 and reduce the general case to this situation. For a generalization of our treatment to functions on [0, 1]^{d} (and [a_{1}, b_{1}] × … × [a_{d}, b_{d}]) see [14].

Let f : [0, 1] → IR be a uniformly continuous function with modulus of uniform continuity ω_{f}. f is already uniquely determined by its restriction to [0, 1] ∩ Q. Thus continuous functions f : [0, 1] → IR can be conceived as a pair (f_{r}, ω_{f}) of functions f_{r} : [0, 1] ∩ Q → IR, ω_{f} : IN → IN which satisfy

(∗) ∀k ∈ IN, x, y ∈ [0, 1] ∩ Q(|x − y| ≤ \frac{1}{ω_{f}(k) + 1} → |f_{r}x − f_{r}y| ≤ \frac{1}{k + 1})

(See also [21] and [2]).

Remark A.3.1 To represent a continuous function f ∈ C[0, 1] as a pair including a modulus of uniform continuity is a numerical enrichment of the given data which we use here for reasons which are similar to the endowment of real numbers with a Cauchy modulus: As we will see below quantification over C[0, 1] so reduces to quantification over functions of type 1. Furthermore many functions on C[0, 1] as e.g. ∫_{0}^{1} f(x)dx or sup_{x∈[0,1]} f(x) are given by functionals ∈ G_{2}R^{ω} in these data (see below). This has as a consequence that many important theorems on continuous functions have the logical form of axioms Δ in theorem 3.3. Also many sentences ∀f ∈ C[0, 1]∀x ∈ IR∀y ∈ [0, 1]∃z ∈ IN A(f, x, y, z) have the logical form ∀f^{1}, x^{1}∀y ≤_{1} M∃z^{0} Ã(f, x, y, z) with Ã ∈ Σ_{1}^{0} so that theorem 3.5 applies yielding bounds on ∃z which depend only on f, x (if f is represented with a modulus of continuity). In the presence of the axiom F^{−} it follows that every pointwise continuous function f : [0, 1] → IR is uniformly continuous and possesses a modulus of uniform continuity (see [17]). Hence under F^{−} the enrichment by such a modulus does not imply a restriction on the class of functions.

Modulo our representation of Q and IR, f_{r} is an object of type 1(0) (i.e. a sequence of number theoretic functions). Quantification over continuous functions on [0,1] reduces to quantification over all pairs (f^{1(0)}, ω^{1}) (and therefore by suitable coding to quantification over all functions of type 1) which satisfy (∗) by substituting λx^{1}.f(x)_{IR} for (f, ω) in the matrix where f(x)_{IR} := lim_{k→∞} f(x̃(ω(k))) (λk^{0}.f(x̃(ω(k))) is a Cauchy sequence of real num-

bers with modulus \frac{1}{k+1} and so its limit is definable in G_{2}A^{ω}). For the applicability of the axioms Δ in theorem 3.5 it is of importance to be able to eliminate the implicative premise (∗): Let us consider the theorem of the attainment of the maximum of a continuous function on [0,1]

∀f ∈ C[0, 1]∃x_{0} ∈ [0, 1]∀x ∈ [0, 1](f(x_{0}) ≥ fx).

Without the need of the implicative premise (∗) on (f, ω) this theorem would have (using our representation) the logical form

∀f^{1}∃x_{0} ≤_{1} M∀x^{1} A(f, x_{0}, x),

where A ∈ Π_{1}^{0}, i.e. the logical form of an axiom Δ in theorems 3.5. Similarly many other important non–constructive theorems would have the logical form of an axiom Δ and thus do not contribute to the rate of growth of the uniform bounds extracted from proofs which use these theorems. In fact below we will show that the premise (∗) can be eliminated by constructing functionals Ψ̃_{1}, Ψ̃_{2} ∈ G_{2}R^{ω} such that the following holds

1) If (f^{1(0)}, ω^{1}) fulfils (∗), then f =_{1(0)} Ψ̃_{1}fω and Ψ̃_{2}fω is also a modulus of uniform continuity for f.

2) For every pair (f^{1(0)}, ω^{1}) the pair (Ψ̃_{1}fω, Ψ̃_{2}fω) satisfies (∗).

By this construction the quantification

∀(f^{1(0)}, ω^{1})((∗) → A(f, ω))

reduces to

∀(f^{1(0)}, ω^{1}) A(Ψ̃_{1}fω, Ψ̃_{2}fω)

(and likewise for ∃) for properties A which are extensional in the sense of =_{C[0,1]}.

In the following we write more suggestively f_{ω}, ω_{f} for Ψ̃_{1}fω, Ψ̃_{2}fω.

The underlying intuition for the following definition is roughly as follows: If f is uniformly continuous with modulus ω, then f_{ω}(n) := f(n). In the case that the continuity property is violated at the first time at a point n, then we define f_{ω} as a simple polygon using the f–values on the previous points:

Definition A.3.2 For f^{1(0)}, ω^{1} we define f_{ω}, ω_{f} as follows:

f_{ω}(n) :=_{1} \{ \begin{matrix}f(n), if A_{0}(f, ω, n) :≡ ∀m, m̃ ≤_{0} Φ_{ω}(3n)∀k ≤_{0} n^{2} \\ (|q(m) −Q q(m̃)| ≤ \frac{1}{ω̃(k)+1} → | ˆ (f(qm))k −Q ˆ (f(qm̃))k| ≤ \frac{3}{k+1}) \\ p_{n_{0},f}(n), for n_{0} ≤_{0} n minimal such that ¬A_{0}(f, ω, n_{0}), otherwise, \end{matrix}

\overline{ω}_{f}(n) :=_{0}

ω̃(3n), if A_{0}(f, ω, n)

max_{0} ((max_{0} \{⌈  ˆ|\frac{f(qi)−_{IR}f(qj)}{qi−Qqj} |(1)⌉ + 1 : i, j ≤_{0} Φ_{ω}(3n_{0}), q(i) ≠ q(j)\}) · (n + 1), ω̃(n))
for n_{0} ≤_{0} n minimal such that ¬A_{0}(f, ω, n_{0}), otherwise,

(here | … |(1) is the value of the sequence | … | at 1) where p_{n_{0},f} is the polygon defined by f(q0), …, f(q(Φ_{ω}(3(n_{0} − · 1)))), ω̃(k) :=_{0} max_{0}(k, 1)^{2} · ( max_{i≤k} ω(i) + 1), ω_{f}(n) := \overline{ω}_{f}(5(n + 1)) and Φ_{ω}(n) :=_{0} j(2(ω̃(n) + 1), ω̃(n) + 1) (Note that 0, 1 are coded by 0, j(2, 0) ≤_{0} Φ_{ω}(3(n_{0} − · 1))).

Remark A.3.3 f_{ω} and ω_{f} are definable in G_{2}R^{ω} (as functionals in f, ω) since A_{0} can be expressed quantifier–free and p_{n_{0},f} can be written as

p_{n_{0},f}(n) =_{1} f(qi) +_{IR} \frac{f(qi) −_{IR} f(qj)}{qi −Q qj} ·_{IR} (qn −Q qi),

where i, j ≤_{0} Φ_{ω}(3(n_{0} − · 1)) are such that qi ≤Q qn ∧ (|qi −Q qn| minimal) ∧ qj >Q qn ∧ (|qj −Q qn| minimal) (If q(n) =Q 1, then p_{n_{0},f}(n) =_{1} f(q(n))).

Lemma A.3.4 1) k_{1} ≥_{0} k_{2} → ω̃(k_{1}) ≥_{0} ω̃(k_{2}).

2) ω̃(k) ≥_{0} k and ω̃(k) ≥_{0} ω(k).

3) ω̃(3 · k) ≥_{0} 3 · ω̃(k) + 3 for k ≥ 1.

Proof: 1) and 2) follow immediately from the definition of ω̃.

3) ω̃(3k) ≥^{k≥1} 9k^{2} · ( max_{i≤k} ω(i) + 1) ≥ 3k^{2} · ( max_{i≤k} ω(i) + 1) + 6k^{2}

≥^{k≥1} 3k^{2}( max_{i≤k} ω(i) + 1) + 3 = 3 · ω̃(k) + 3.

Lemma A.3.5 If f^{1(0)} represents a uniformly continuous function F : [0, 1] → IR with a modulus ω^{1} of uniform continuity, i.e. ∀m, m̃, k(|qm −Q qm̃| ≤Q \frac{1}{ω(k)+1} → |f(qm) −_{IR} f(qm̃)| ≤_{IR} \frac{1}{k+1}), then f_{ω} =_{1(0)} f and ω_{f} is also a modulus of uniform continuity for F.

Proof: The first part of the lemma follows from the definition of f_{ω} observing that the case ‘otherwise’ never occurs because of the assumption, since

|qm −Q qm̃| ≤ \frac{1}{ω̃(k) + 1} ≤^{l.A.3.4} \frac{1}{ω(k) + 1}

implies that

| ˆ (f(qm))k −Q ˆ (f(qm̃))k| ≤ |f(qm) −_{IR} f(qm̃)| + \frac{2}{k + 1} ≤ \frac{3}{k + 1}.

Furthermore \overline{ω}_{f}(n) = ω̃(3n) ≥_{0}^{l.A.3.4} ω(n). Hence together with ω also \overline{ω}_{f} and thus a fortiori ω_{f} is a modulus of uniform continuity.

Lemma A.3.6 For every pair (f^{1(0)}, ω^{1}) the following holds: f_{ω} represents a uniformly continuous function : [0, 1] ∩ Q → IR and ω_{f} is a modulus of uniform continuity for this function, i.e.

∀m, m̃, k(|qm −Q qm̃| ≤ \frac{1}{ω_{f}(k) + 1} → |f_{ω}(qm) −_{IR} f_{ω}(qm̃)| ≤ \frac{1}{k + 1}).

Proof: Let m, m̃, k ∈ IN be such that |qm −Q qm̃| ≤ \frac{1}{\overline{ω}_{f} (k)+1}. We may assume that qm >_{0} qm̃. \underline{Case} 1: A_{0}(f, ω, qm). Then also A_{0}(f, ω, qm̃) since the monotonicity of Φ_{ω}(3n) and n^{2} implies

n_{1} ≥_{0} n_{2} ∧ A_{0}(f, ω, n_{1}) → A_{0}(f, ω, n_{2}).

Hence f(qm) =_{IR} f_{ω}(qm) and f(qm̃) =_{IR} f_{ω}(qm̃). By \overline{ω}_{f}(k) ≥_{0} ω̃(k), k the assumption on m, m̃, k yields

(+) |qm −Q qm̃| ≤ \frac{1}{ω̃(k) + 1} and (++) |qm −Q qm̃| ≤ \frac{1}{k + 1}.

(++) implies that k ≤_{0} (qm)^{2} (Because of j_{2}(qm), j_{2}(qm̃) <_{0} qm, the (distinct) fractions coded by qm, qm̃ have denominators a, b ≤_{0} qm. Thus |\frac{i}{a} − \frac{j}{b}| ≥ \frac{1}{ab} ≥ \frac{1}{(qm)^{2}} ). Furthermore qm, qm̃ ≤_{0} Φ_{ω}(3(qm)). Hence (+) and A_{0}(f, ω, qm) yield (using ∀x^{0}(q(qx) =_{0} qx))

|(f̂(qm))k −Q (f̂(qm̃))k| ≤ \frac{3}{k + 1}

and therefore

|f_{ω}(qm) −_{IR} f_{ω}(qm̃)| =_{IR} |f(qm) −_{IR} f(qm̃)| ≤ \frac{5}{k + 1}.

\underline{Case} 2: ¬A_{0}(f, ω, qm). 2.1 k ≥_{0} n_{0} := min n ≤_{0} qm¬A_{0}(f, ω, n): In this case we have f_{ω}(qm) =_{IR} p_{n_{0},f}(qm) and f_{ω}(qm̃) =_{IR} p_{n_{0},f}(qm̃) (In the case A_{0}(f, ω, qm̃) we have qm̃ < n_{0} ≤ Φ_{ω}(3(n_{0} − 1)) and so f_{ω}(qm̃) = f(qm̃) is one of the f–values used in defining p_{n_{0},f}). Since \overline{ω}_{f} is a modulus of uniform continuity for p_{n_{0},f} for k ≥ n_{0}, the assumption on m, m̃ implies

|f_{ω}(qm) −_{IR} f_{ω}(qm̃)| ≤ \frac{1}{k + 1}.

2.2 1 ≤_{0} k <_{0} n_{0}: Then A_{0}(f, ω, k) and therefore \overline{ω}_{f}(k) = ω̃(3k). Since all fractions \frac{i}{ω̃(3(n_{0}−1))+1} with i ≤_{0} ω̃(3(n_{0} − 1)) + 1 have a code ≤_{0} Φ_{ω}(3(n_{0} − 1)), the maximal distance between two adjacent breaking points of p_{n_{0},f} is ≤ \frac{1}{ω̃(3(n_{0}−1))+1}. Hence there are m^{∗}, m̃^{∗} ≤_{0} Φ_{ω}(3(n_{0} − 1)) (i.e. ’breaking points’ of the polygon p_{n_{0},f} next to m, m̃ satisfying (2) below) such that

(1) \{ \begin{matrix}|qm^{∗} −Q qm̃^{∗}| ≤ \frac{1}{\overline{ω}_{f} (k)+1} + \frac{2}{ω̃(3(n_{0}−1))+1} ≤^{l.A.3.4} \frac{3}{ω̃(3k)+1} ≤^{l.A.3.4} \frac{3}{3ω̃(k)+3+1} \\ ≤ \frac{1}{ω̃(k)+1} \end{matrix}

and

(2) | \underbrace{p_{n_{0},f}(qm̃^{∗})}_{=_{IR}f(qm̃^{∗})} −_{IR} \underbrace{p_{n_{0},f}(qm^{∗})}_{=_{IR}f(qm^{∗})} | ≥_{IR} | \underbrace{p_{n_{0},f}(qm̃)}_{=_{IR}f_{ω}(qm̃)} −_{IR} \underbrace{p_{n_{0},f}(qm)}_{=_{IR}f_{ω}(qm)} |.

Since A_{0}(f, ω, n_{0} − 1) and k ≤_{0} (n_{0} − 1)^{2}, (1) and (2) imply

\begin{matrix}|f_{ω}(qm) −_{IR} f_{ω}(qm̃)| ≤^{(2)} |f(qm^{∗}) −_{IR} f(qm̃^{∗})| ≤ |(f̂(qm^{∗}))k −Q (f̂(qm̃^{∗}))k| + \frac{2}{k+1} \\ ≤^{(1)} \frac{3}{k+1} + \frac{2}{k+1} = \frac{5}{k+1}. \end{matrix}

Put together we have shown that in both cases (for k ≥ 1)

|qm −Q qm̃| ≤ \frac{1}{\overline{ω}_{f}(k) + 1} → |f_{ω}(qm) −_{IR} f_{ω}(qm̃)| ≤ \frac{5}{k + 1}.

Hence ω_{f} is a modulus of uniform continuity for f_{ω}.

Since every pair (f^{1(0)}, ω^{1}) can be conceived now as a representation of a uniformly continuous function [0, 1] ∩ Q → IR, namely that function which is represented by (Ψ̃_{1}fω, Ψ̃_{2}fω) (where Ψ̃_{1}fω := f_{ω} ∘ q, Ψ̃_{2}fω := ω_{f}).^{7} And every function g^{1} can be conceived as a pair (f, ω) by g ↦ (λk^{0}, n^{0}.(j_{1}g)(j(k, n)), j_{2}g) (where j_{i}g := λx^{0}.j_{i}(gx)), so g^{1} represents the continuous function (Ψ_{1}g, Ψ_{2}g), where Ψ_{1}g := Ψ̃_{1}(λk^{0}, n^{0}.(j_{1}g)(j(k, n)), j_{2}g) and Ψ_{2}g := Ψ̃_{2}(λk^{0}, n^{0}.(j_{1}g)(j(k, n)), j_{2}g). Since every pair (f, ω) can be coded by a function g, every uniformly continuous function [0, 1] ∩ Q → IR is represented by some function g. Together with Ψ̃_{i} also the Ψ_{i} are in G_{2}R^{ω}. Now we define the continuation on full [0, 1]:

Definition A.3.7 The functional λg^{1}, x^{1}.g(x)_{IR} ∈ G_{2}R^{ω} is defined by (g(x)_{IR})(k^{0}) :=_{0} Ψ̂_{1}g(x̃(Ψ_{2}g(3(k + 1))))(3(k + 1)), x̃ is the construction used in our representation of [0, 1].

Remark A.3.8 g(x)_{IR} represents the value of the function ∈ C[0, 1], which is represented by g, applied to the real ∈ [0, 1], which is represented by x. Notation: If a function ∈ C[0, 1] is given as a pair (f^{1(0)}, ω^{1}) we also use the notation f(x)_{IR} in order to avoid the need of spelling out the coding (f, ω) ↦ g^{1}.

Remark A.3.9 Quantification over C[a, b] (where a < b) reduces to quantification over C[0, 1] by f ∈ C[a, b] ↦ g := λx.f(a(1 − x) + bx) ∈ C[0, 1] and g ∈ C[0, 1] ↦ f := λx.g(\frac{x−a}{b−a}) ∈ C[a, b].

7By switching from f_{ω} to f_{ω} ∘ q we can formulate the continuity of Ψ̃_{1}fω now as ∀m, m̃(0 ≤Q m, m̃ ≤Q 1 ∧ |m −Q m̃| ≤ \frac{1}{ω_{f} (k)+1} → |(Ψ̃_{1}fω)(m) −_{IR} |(Ψ̃_{1}fω)(m̃)| ≤ \frac{1}{k+1}), i.e. without mentioning q anymore.

In [11] we used a different representation of the space C[0, 1] (following [3] ) based on the Weierstraß approximation theorem: A function f ∈ C[0, 1] was represented as a Cauchy sequence w.r.t. ∥ · ∥_{∞} (with modulus 1/(k + 1)) of polynomials with rational coefficients. Then we applied a construction, similarly to f̂ used in our representation of IR above, to ensure that every function f^{1} could be conceived as such a Cauchy sequence. However this representation is not convenient for our theory G_{2}A^{ω} since the coding of an arbitrary sequence of polynomials requires the coding of finite sequences of natural numbers (the codes of the coefficients) of variable length which can be carried out in G_{3}A^{ω} but not in G_{2}A^{ω}. Furthermore in practice the computation of an approximating sequence of polynomials to a given function is quite complicated (and even more when one deals with functions in several variables) whereas for most functions occurring in mathematics a modulus of continuity can be written down directly. Hence it is much more useful to extract bounds which require as a function input only the function endowed with a modulus of uniform continuity than an approximating sequence of polynomials. In our applications to approximation theory we always obtained bounds in functions with a modulus of continuity. Because of this we conjectured in [11] that this will always hold for extractions of bounds from concrete proofs. By our new representation of C[0, 1] this conjecture is theoretically justified: From a proof of a sentence

∀f ∈ C[0, 1]∃y^{0} A(f, y), where A ∈ Σ_{1}^{0}

we obtain a bound on y in a representative of f in our sense, i.e. in f endowed with a modulus of uniform continuity.

The construction of f_{ω}, ω_{f} looks quite complicated. However if f is already given with a modulus ω (as in concrete applications) then f_{ω} does not change anything and ω_{f}(n) is just a slight modification of ω and the proof of this (A.3.5 ) is almost trivial. The complicated clause in the definition of f_{ω}, ω_{f} is needed only to ensure that an arbitrary given pair (f, ω) is transformed into a continuous function. The quite complicated proof of lemma A.3.6 is not relevant for the extraction process since the statement of this lemma is a purely universal sentence and therefore an axiom of G_{2}A^{ω}.

A.4 The functionals max_{IR}, +_{IR} for sequences of variable length and

sup_{x∈[a,b]} fx , b ; ∫ ; a f(x)dx in G_{2}A^{ω}

For the computation of sup_{x∈[a,b]} fx and ∫_{a}^{b} f(x)dx for f ∈ C[a, b] we need the maximum and

the sum of a sequence of real numbers of variable length, i.e. max_{IR} {f(r_{i}) : i ≤ k} and f(r_{0}) +_{IR} … +_{IR} f(r_{k}) for a sequence of rational numbers r_{i}. For the construction of such operations in G_{2}R^{ω} we need a special form of our representation of real numbers: The computation of the addition of a sequence of x real numbers a_{0}, …, a_{x} requires the addition of corresponding sequences of the n–th rational approximations â_{0}(n), …, â_{x}(n) of these real numbers (for all n). For this we need the computation of a common divisor of â_{0}(n), …, â_{x}(n). However the size of such a common divisor will (in general) have an exponential growth in x and therefore is not definable in G_{2}R^{ω} but only in G_{3}R^{ω}. This difficulty is avoided by modifying representatives f of real numbers to representatives f′ such that f =_{IR} f′ and the n–th rational approximation f′n of f′ is a (code of a) fraction with a fixed denominator. We choose 3(n + 1) + 1 as this denominator in order to ensure the right rate of convergence such that f̂′ =_{1} f′. For the computation of max_{IR}(a_{0}, …, a_{x}) this modification is (although not necessary) very convenient.

Definition A.4.1

f̌n :=_{0}

min k ≤_{0} j_{1}(f̂(3(n + 1))) · (3(n + 1) + 1)[\frac{\frac{k}{2}}{3(n+1)+1} ≤Q f̂(3(n + 1)) <Q \frac{\frac{k}{2} +1}{3(n+1)+1}

∧k even ] if it exists and j_{1}(f̂(3(n + 1))) is even

min k ≤_{0} (j_{1}(f̂(3(n + 1))) + 1) · (3(n + 1) + 1)[\frac{− \frac{k+1}{2}}{3(n+1)+1} ≤Q f̂(3(n + 1)) <Q \frac{− \frac{k+1}{2} +1}{3(n+1)+1}

∧k odd ] if it exists and j_{1}(f̂(3(n + 1))) is odd

0^{0}, otherwise.

f′(n) := j(f̌n, 3(n + 1)).

Remark A.4.2 Together with λf.f̂ also λf.f̌ and therefore λf.f′ are definable in G_{2}R^{ω}.

Lemma A.4.3 G_{2}A^{ω} ⊢ ∀f^{1}(f′ =_{IR} f).

Definition A.4.4 χ^{1}, ψ^{1(1)} ∈ G_{2}R^{ω} are defined such that (provably in G_{2}A^{ω})

χn^{0} =_{0} \{ \begin{matrix}1, if ∃m ≤_{0} n(n =_{0} 2m) \\ 0, otherwise. \end{matrix}

and

ψg^{1}k^{0} =_{0} \{ \begin{matrix}max_{i≤k} (g(i) · χ(gi)), if ∃i ≤_{0} k(χ(gi) =_{0} 1) \\ min_{i≤k} g(i), otherwise. \end{matrix}

Definition A.4.5 Φ_{max_{IR}} ∈ G_{2}R^{ω} is defined by Φ_{max_{IR}} := λf^{1(0)}, k^{0}, n^{0}.j(ψ(λi^{0}.j_{1}((fi)′n), k), 3(n + 1)).

Lemma A.4.6

G_{2}A^{ω} ⊢ ∀k^{0}, f^{1(0)}(Φ_{max_{IR}}f0 =_{IR} f0 ∧ Φ_{max_{IR}}f(k + 1) =_{IR} max_{IR}(Φ_{max_{IR}}fk, f(k + 1))).

Lemma A.4.7 1) G_{2}A^{ω} ⊢ ∀f^{1(0)}, m^{0}, m̃^{0}(m ≥_{0} m̃ → Φ_{max_{IR}}fm ≥_{IR} Φ_{max_{IR}}fm̃, fm̃).

2) G_{2}A^{ω}+AC^{0,0}–qf ⊢ ∀f^{1(0)}, m^{0}∃k ≤_{0} m(fk =_{IR} Φ_{max_{IR}}fm).

Remark A.4.8 1) The elementary but tedious proofs for the two lemmas above (which we don’t carry out here) have no impact on the extraction of bounds: Lemma A.4.6 and A.4.7 1) are purely universal sentences. Since one can verify their truth they are treated as axioms. Lemma A.4.7 2) (although not being universal) has the logical form ∀x∃y ≤ sx∀zA_{0} of an axiom ∈ Δ and therefore is treated as an axiom by our monotone (but not by the usual) functional interpretation. The same is true for the next lemma.

2) Φ_{min_{IR}}fm can be defined from Φ_{max_{IR}}fm by := −_{IR}Φ_{max_{IR}}(λk.(−_{IR}fk), m).

Using Φ_{max_{IR}} we are able to define sup_{x∈[0,1]} f(x) for f ∈ C[0, 1]:

Definition A.4.9 Φ_{sup_{[0,1]}}^{1(1)} ∈ G_{2}R^{ω} is defined as follows

Φ_{sup_{[0,1]}}^{1(1)} := λf^{1}, n^{0}.Φ_{max_{IR}}(Ψ_{1}f, h(Ψ_{2}f(3(n + 1))))(3(n + 1)),

where hn := j(2n, n) and Ψ_{1}, Ψ_{2} ∈ G_{2}R^{ω} are the functionals used in the representation of C[0, 1].

Lemma A.4.10

G_{2}A^{ω} ⊢ ∀f ∈ C[0, 1](∀x ∈ [0, 1](Φ_{sup_{[0,1]}}f ≥_{IR} fx)∧∀k^{0}∃x ∈ [0, 1](Φ_{sup_{[0,1]}}f−_{IR}fx ≤ \frac{1}{k + 1})).

From now on we make liberal use of the usual mathematical expressions ‘ sup_{x∈[0,1]} fx’ and

‘f ∈ C[0, 1]’ and go back to the details of the actual representation of these notions in G_{2}A^{ω} only when this is needed to determine the logical form of a sentence which involves these notions. For a function f ∈ C[a, b] we can express sup_{x∈[a,b]} fx as sup_{x∈[0,1]} f̃x, where f̃x := f((1−x)a+xb).

For the definition of the sum of a sequence of real numbers of length x we need the following constructions.

Definition A.4.11 The functionals ζ, \overline{ζ}, ξ ∈ G_{2}R^{ω} are defined such that

ζn^{0} =_{0} \{ \begin{matrix}n, if ∃m ≤ n(n = 2m) \\ 0, otherwise. \end{matrix}

\overline{ζ}n^{0} =_{0} \{ \begin{matrix}n + 1, if ∃m ≤ n(n = 2m + 1) \\ 0, otherwise. \end{matrix}

ξn^{0}m^{0} =_{0} \{ \begin{matrix}n − · m, if n ≥ m \\ m − · n − · 1, otherwise. \end{matrix}

Using these functions we are now able to define a variable summation: Definition A.4.12 Φ_{Σ_{IR}} ∈ G_{2}R^{ω} is defined as

Φ_{Σ_{IR}} := λf^{1(0)}, k^{0}, n^{0}.j(ξ( ∑_{i=0}^{k} ζ(j_{1}[(fi)′(α(k, n))]), ∑_{i=0}^{k} \overline{ζ}(j_{1}[(fi)′(α(k, n))])), 3(α(k, n) + 1)),

where α(k, n) := 2(k + 1)(n + 1).

Lemma A.4.13 G_{2}A^{ω} ⊢ ∀f^{1(0)}, k^{0}(Φ_{Σ_{IR}}f0 =_{IR} f0∧Φ_{Σ_{IR}}f(k +1) =_{IR} Φ_{Σ_{IR}}fk +_{IR} f(k +1)).

Using Φ_{Σ_{IR}} we now define the Riemann integral ∫_{0}^{1} f(x)dx for f ∈ C[0, 1]: Let S_{n} := \frac{1}{ω_{f} (n)+1} · ∑_{i=0}^{ω_{f} (n)} f(\frac{i}{ω_{f} (n)+1}) denote the n–th Riemann sum (where ω_{f} is the modulus of uniform continuity from the representation of f). One easily follows from the usual proof of the convergence of the sequence of Riemann sums that (S_{n})_{n∈IN} is a Cauchy sequence with Cauchy modulus 2/(n + 1) (which converges to ∫_{0}^{1} f(x)dx). Therefore we define: Definition A.4.14 1) Φ_{S} ∈ G_{2}R^{ω} is defined as

Φ_{S} := λf^{1}, n^{0}.j(2, Ψ_{2}fn) ·_{IR} Φ_{Σ_{IR}}(λi.(Ψ_{1}f)(j(2i, Ψ_{2}fn)), Ψ_{2}fn).

2) Φ_{I} ∈ G_{2}R^{ω} is defined as Φ_{I} := λf^{1}, n^{0}.[Φ_{S}f(2(3(n + 1)) + 1)](3(n + 1)).

Proposition A.4.15 Φ_{I}f^{1} represents the real number ∫_{0}^{1} F (x)dx, where F is the function ∈ C[0, 1] which is represented by f.

Proof: Since j(2i, Ψ_{2}fn) codes \frac{i}{Ψ_{2}fn+1} and Ψ_{2} is a modulus of uniform continuity for the function : [0, 1] ∩ Q → IR which is represented by Ψ_{1}, Φ_{S} is just the n–th Riemann sum for the function represented by f. As we have mentioned already above, these Riemann sums S_{n} form a Cauchy sequence with modulus 2/(n + 1). Hence (S_{2n+1})_{n∈IN} is a Cauchy sequence with modulus 1/(n + 1). Φ_{I}f represents the limit of this sequence.

In the following we use the usual notation ∫_{0}^{1} f(x)dx instead of Φ_{I}.

Proposition A.4.16 The following properties of ∫_{0}^{1} are provable in G_{2}A^{ω} (f, f_{n}, g ∈ C[0, 1], λ ∈ IR):

1) ∫_{0}^{1}(f + g)(x)dx = ∫_{0}^{1} f(x)dx + ∫_{0}^{1} g(x)dx.

2) ∫_{0}^{1}(λ · f)(x)dx = λ ∫_{0}^{1} f(x)dx.

3) f ≤ g → ∫_{0}^{1} f(x)dx ≤ ∫_{0}^{1} g(x)dx.

4) |∫_{0}^{1} f(x)dx| ≤ ∫_{0}^{1} |f|(x)dx ≤ ∥f∥_{∞}.

5) f_{n} →^{∥·∥_{∞}} f ⇒ ∫_{0}^{1} f_{n}(x)dx → ∫_{0}^{1} f(x)dx.

Proof: It is clear from the usual proofs in analysis that 1)–5) are true. Since 1),2) and 4) are purely universal, they are axioms of G_{2}A^{ω}. 3) can be transformed into a purely universal sentence

3)′ ∫_{0}^{1} f(x)dx ≤ ∫_{0}^{1} max(f, g)(x)dx.

The proof of the equivalence of 3) and 3)’ uses the extensionality of ∫_{0}^{1}, which follows immediately from 4) and thus is also provable in G_{2}A^{ω}. 5) follows from 1),2) and 4).

Our definition of ∫_{0}^{1} easily generalizes to ∫_{a}^{b} F (x)dx for F ∈ C[a, b] (a < b). Let F be given as a pair (Ψ^{1(1)}, ω), where Ψ represents a function : [a, b] → IR which has the modulus of uniform continuity ω. Then a representative of ∫_{a}^{b} F (x)dx can be computed in Ψ, ω, a, b by a functional in G_{2}R^{ω}. For this one has to replace the partition

\frac{0}{ω(n) + 1}, …, \frac{ω(n) + 1}{ω(n) + 1}

of [0,1] by the partition

a_{0}, …, a_{k(ω(n)+1)}, where a_{i} := a +_{IR} i(b − a) ·_{IR} \frac{1}{k(ω(n) + 1)} and IN ∋ k ≥ b − a,

of [a, b] which also has mesh ≤ 1/(ω(n) + 1).

We can define also a functional Φ_{I_{a}^{x}} ∈ G_{2}R^{ω} such that Φ_{I_{a}^{x}}(x^{1}, a^{1}, Ψ^{1(1)}, ω^{1}) represents the integral ∫_{a}^{x} Ψxdx if Ψ represents a function [a, b] → IR (a < b), which is uniformly continuous with modulus ω, and x ∈ [a, b]:

Φ_{I_{a}^{x}}(x^{1}, a^{1}, Ψ^{1(1)}, ω^{1}) := lim_{n→∞} S_{n}(x, a, Ψ, ω),

where

S_{n}(= S_{n}(x, a, Ψ, ω)) := \frac{x −_{IR} a}{n + 1} ·_{IR} Φ_{Σ}(λi.Ψ(a +_{IR} i(x −_{IR} a) ·_{IR} \frac{1}{n + 1}), n + 1).

From our reasoning above it is clear that (S_{n}) is a Cauchy sequence which converges to ∫_{a}^{x} Ψxdx. In order to be able to define lim_{n→∞} S_{n} in G_{2}R^{ω} we have to construct a Cauchy modulus for this sequence in G_{2}R^{ω}. This however is possible since

|S_{k(ω(n)+1)} − ∫_{a}^{x} Ψxdx| ≤ \frac{k}{n + 1},

where k ∈ IN such that k ≥ x − a.

The formula

∫_{a}^{c} f(x)dx + ∫_{c}^{b} f(x)dx = ∫_{a}^{b} f(x)dx for a < c < b

is purely universal and hence an axiom of G_{2}A^{ω}.

B Trigonometric functions in G_{2}A^{ω}: Moduli and universal properties

B.1 The functions sin, cos and tan in G_{2}A^{ω}

In the following we introduce the functions sin , cos axiomatically by adding to G_{2}A^{ω} new function constants Φ_{sin}, Φ_{cos} of type 1(0) which represent the restriction of sin and cos to Q. Then the Lipschitz continuity of sin, cos is used to continue these functions to IR (If we would introduce sin, cos directly as functions on IR, this would require new constants for functionals of type 1(1). In order to express their extensionality by universal axioms we also would have to make use of the Lipschitz continuity, since uniform continuity is just a uniform quantitative version of extensionality).

The following purely universal assertions on the function constants Φ_{sin}, Φ_{cos} express true propositions on sin, cos and are therefore taken as axioms in G_{2}A^{ω} ∪ {Φ_{sin}, Φ_{cos}} (which we also denote by G_{2}A^{ω}):

1) ∀x^{0}( ˆ (Φ_{sin}x) =_{1} Φ_{sin}x ≤_{1} M ∧ ˆ (Φ_{cos}x) =_{1} Φ_{cos}x ≤_{1} M ∧ −1 ≤_{IR} Φ_{sin}x, Φ_{cos}x ≤_{IR} 1), where M^{1} ∈ G_{2}R^{ω} is the boundedness function from the representation of [−1, 1] (one may take M := λn^{0}.j(6(n + 1), 3(n + 1) − 1) see [0, 1]).

2) ∀x^{0}, y^{0}, q^{0}(|x −Q y| ≤Q q → |Φ_{sin}x −_{IR} Φ_{sin}y| ≤_{IR} q ∧ |Φ_{cos}x −_{IR} Φ_{cos}y| ≤_{IR} q). (2) (together with 1)) asserts that Φ_{sin} and Φ_{cos} represent functions : Q → [−1, 1] which are Lipschitz continuous on Q with Lipschitz constant λ = 1).

3) ∀x^{0}(Φ_{sin}(−Qx) =_{IR} −_{IR}Φ_{sin}x ∧ Φ_{cos}(−Qx) =_{IR} Φ_{cos}x), Φ_{cos}0 =_{IR} 1.

4) ∀x^{0}, y^{0}(Φ_{sin}(x +Q y) =_{IR} (Φ_{sin}x) ·_{IR} (Φ_{cos}y) +_{IR} (Φ_{cos}x) ·_{IR} (Φ_{sin}y) ∧

Φ_{cos}(x +Q y) =_{IR} (Φ_{cos}x) ·_{IR} (Φ_{cos}y) −_{IR} (Φ_{sin}x) ·_{IR} (Φ_{sin}y)). ∀x^{0}, y^{0}(Φ_{sin}x −_{IR} Φ_{sin}y = 2 · Φ_{cos}(\frac{x+Qy}{2} ) ·_{IR} Φ_{sin}(\frac{x−Qy}{2} ) ∧

Φ_{cos}x −_{IR} Φ_{cos}y = −2 · Φ_{sin}(\frac{x+Qy}{2} ) ·_{IR} Φ_{sin}(\frac{x−Qy}{2} )).

5) ∀x^{0}(0 <Q |x| → |\frac{Φ_{sin}x}{x} −_{IR} 1| ≤_{IR} \frac{|x|^{2}}{6} ).

This proposition on sin (which is proved e.g. in [5] ) provides a quantitative version of the proposition \frac{sin x}{x} →^{x→0} 1. Only by this quantitative strengthening the proposition becomes purely universal (and therefore an axiom of G_{2}A^{ω}).

Because of axiom 2) there are unique continuous extensions of the functions : Q → IR, which are represented by Φ_{sin}, Φ_{cos}, to the whole space IR. These extensions are represented by

Φ̃_{sin}^{1(1)}x^{1} := λk^{0}.Φ_{sin}(x̂(3(k + 1)))(3(k + 1)),
Φ̃_{cos}^{1(1)}x^{1} := λk^{0}.Φ_{cos}(x̂(3(k + 1)))(3(k + 1)).

Remark B.1.1 1) It is well–known that 2)–5) already characterize sin, cos (see e.g. [7]).

2) By the axioms 1) Φ_{sin} and Φ_{cos} are majorizable by λx^{0}, n^{0}.j(6(n + 1), 3(n + 1) − 1) ∈ G_{2}R_{−}^{ω}. Hence theorem 3.2.8 from [15] applies.

3) In G_{3}A^{ω} we can define constants Φ′_{sin}, Φ′_{cos} which satisfy (provable in G_{3}A^{ω}) −1 ≤ Φ′_{sin}x, Φ′_{cos}x ≤ 1 and 2)–5) above using the usual definition via the Taylor expansion of sin and cos. If we now define Φ_{sin}x := ˜ (Φ′_{sin}x) and Φ_{cos}x := ˜ (Φ′_{cos}x) (where λy^{1}.ỹ ∈ G_{2}R^{ω} is the construction corresponding to our representation of [−1, 1] such that ỹ ≤_{1} M, y =_{IR} ỹ if −1 ≤_{IR} y ≤_{IR} 1, and −1 ≤_{IR} ỹ ≤_{IR} 1 for all y^{1}), then these functionals satisfy 1)–5).

In the following we will write Φ_{sin},Φ_{cos} also for Φ̃_{sin}, Φ̃_{cos} since from the type of the argument it will always be clear whether Φ_{sin},Φ_{cos} or their extensions Φ̃_{sin}, Φ̃_{cos} are meant.

In the following we will introduce \frac{π}{2} (and thus π) as the uniquely determined zero of the function cos on [0, 2]. This is possible since Φ_{cos}0 =_{IR} 1, Φ_{cos}2 ≤_{IR} −\frac{1}{3} and

(∗) ∀x^{0}, y^{0}(0 ≤Q y ≤Q x ≤Q 2 → Φ_{cos}x −_{IR} Φ_{cos}y ≤_{IR} −\frac{(x −Q y)^{2}}{18} )

are true purely universal assertions on cos (see below for the verification of (∗)) and hence axioms of G_{2}A^{ω}. (∗) is a uniform quantitative version of the strict monotonicity of cos on [0, 2]. This strict monotonicity implies the uniqueness and hence (by a general meta–theorem from [11] ) the effectivity of the uniquely determined zero of cos [0, 2]. This can be seen also directly as follows: The quantitative monotonicity (∗) immediately yields a modulus of uniqueness (in the sense of [11] ) ω ∈ G_{2}R^{ω}, namely ω(n) := \frac{1}{36(n+1)^{2}} and thus the computability of the

zero of cos in G_{2}R^{ω} ∪ Φ_{cos}: Let x_{m}, xm̃ ∈ [0, 2] be such that

| cos x_{m}|, | cos xm̃| < \frac{1}{36(n + 1)^{2}} and therefore | cos x_{m} − cos xm̃| < \frac{1}{18(n + 1)^{2}} .

Then –by (∗)– |x_{m} − xm̃| < \frac{1}{n+1}, i.e. ω is a modulus of uniqueness. We define a partition of [0, 2] by

x_{i} := \frac{i}{3 · 36(n + 1)^{2}} for i = 0, …, 6 · 36(n + 1)^{2}

and compute for each i a rational 1/(6 · 36(n + 1)^{2})–approximation y_{i} of | cos x_{i}|. Next we compute an i_{n} such that

|y_{i_{n}}| = min {|y_{i}| : i = 0, …, 6 · 36(n + 1)^{2}} .

It follows

| cos(x_{i_{n}})| ≤ min_{i≤6·36(n+1)^{2}} | cos x_{i}|+\frac{1}{3 · 36(n + 1)^{2}} ≤ inf_{x∈[0,2]} | cos x|+\frac{2}{3 · 36(n + 1)^{2}} < \frac{1}{36(n + 1)^{2}} .

Hence (x_{i_{n}}) is a Cauchy sequence in [0, 2] with Cauchy modulus 1/(n + 1). (x_{i_{n}}) can be computed by a term t^{1} in G_{2}R^{ω} ∪ Φ_{cos}. Therefore we may define π :=_{1} 2 ·_{IR} t.

The following propositions on π, Φ_{sin}, Φ_{cos} are purely universal and therefore axioms of G_{2}A^{ω}:

1) 2 ≤_{IR} π ≤_{IR} 4, Φ_{cos}(\frac{π}{2} ) =_{IR} 0.

2) ∀x^{1}(Φ_{cos}(x +_{IR} 2π) =_{IR} Φ_{cos}x ∧ Φ_{sin}(x +_{IR} 2π) =_{IR} Φ_{sin}x ∧ Φ_{cos}(x +_{IR} π) =_{IR} −Φ_{cos}x ∧ Φ_{sin}(x +_{IR} π) =_{IR} −Φ_{sin}x ∧ Φ_{cos}x =_{IR} Φ_{sin}(\frac{π}{2} −_{IR} x) ∧ Φ_{sin}x =_{IR} Φ_{cos}(\frac{π}{2} −_{IR} x)).

3) Uniform quantitative strict monotonicity:

∀x^{0}, y^{0}((0 ≤Q y ≤Q x ≤Q 4 → Φ_{cos}(x̃) −_{IR} Φ_{cos}(ỹ) ≤_{IR} −\frac{(x̃−_{IR}ỹ)^{2}}{18} ) ∧

( − 2 ≤Q y ≤Q x ≤Q 2 → Φ_{sin}(x̌) −_{IR} Φ_{sin}(ŷ) ≥_{IR} \frac{(x̌−_{IR}ŷ)^{2}}{18} )),

where z̃:= min_{IR}(z, π), ž:= min_{IR}(z, π/2) and ẑ:= max_{IR}(z, −π/2).

3) implies (together with 1) and the continuity of cos, sin):

3)’ ∀x^{1}, y^{1}((0 ≤_{IR} y ≤_{IR} x ≤_{IR} π → Φ_{cos}(x) −_{IR} Φ_{cos}(y) ≤_{IR} −\frac{(x−_{IR}y)^{2}}{18} )∧
( − \frac{π}{2} ≤_{IR} y ≤_{IR} x ≤_{IR} \frac{π}{2} → Φ_{sin}(x) −_{IR} Φ_{sin}(y) ≥_{IR} \frac{(x−_{IR}y)^{2}}{18} )).

The reason for our somewhat complicated formulation 3) instead of 3)’ is that 3) is in Π_{1}^{0} (in contrast to 3)’). Proof of 3)’ (and hence of 3) and (∗) above): Since sin z ≥ \frac{z}{3} for all z ∈ [0, 2] (see e.g. [5]), we obtain for all x, y such that 0 ≤ y ≤ x ≤ \frac{π}{2} :

cos x − cos y = −2 sin(\frac{x + y}{2} ) sin(\frac{x − y}{2} ) ≤ −2(\frac{x + y}{6} )(\frac{x − y}{6} ) ≤ −\frac{(x − y)^{2}}{18} .

Because of cos x = − cos(π − x), the claim follows for x, y ∈ [0, \frac{π}{2} ] and x, y ∈ [\frac{π}{2} , π]. Now assume that x ≥ \frac{π}{2} ∧ y ≤ \frac{π}{2} : Then

cos x − cos y = cos x − cos \frac{π}{2} + cos \frac{π}{2} − cos y ≤ −2(\frac{x^{2}−y^{2}}{36} ) ≤ −\frac{(x−y)^{2}}{18} . Put together this yields the claim for [0, π]. By sin x = − cos(\frac{π}{2} + x) the corresponding claim for sin follows.

Remark B.1.2 The proof of 3)’ above can be conceived as an instance of theorem 3.3 (of course a very simple one): When formalized within G_{2}A^{ω}, the strict monotonicity of cos has (modulo a suitable prenexation) the logical form

(+) ∀x, y ≤_{1} M_{π}, k^{0}∃n^{0}( \underbrace{x ≥_{IR} y + \frac{1}{k + 1} → Φ_{cos}x − Φ_{cos}y <_{IR} −\frac{1}{n + 1}}_{≡:A∈Σ_{1}^{0}(modulo prenexation)} ).

Since (+) is provable in G_{2}A^{ω}, theorem 3.3 implies the extractability of a polynomial pk providing a bound on n which does not depend on x, y. Since A is monotone w.r.t. n, this bound in fact realizes ‘∃n’, i.e.

G_{2}A^{ω} ⊢ ∀x, y ∈ [0, π], k^{0}(x ≥_{IR} y + \frac{1}{k + 1} → Φ_{cos}x − Φ_{cos}y <_{IR} −\frac{1}{pk + 1}).

Our proof of 3)’ yields pk := 18(k + 1)^{2}. The majorization used in this proof to eliminate the dependence on x, y is simply the inequality

(x + y)(x − y) ≥ (x − y)^{2} ≥ \frac{1}{(k + 1)^{2}} for x ≥ y + \frac{1}{k + 1} ≥ \frac{1}{k + 1}.

The tangent function tan x := \frac{sin x}{cos x} is represented by a term Φ_{tan}^{1(0)(1)} ∈ G_{2}R^{ω} ∪ \{Φ_{sin}, Φ_{cos}\} such that

∀x^{1}, n^{0}( − \frac{π}{2} + \frac{1}{n + 1} ≤_{IR} x ≤_{IR} \frac{π}{2} − \frac{1}{n + 1} → Φ_{tan}xn =_{IR} \frac{Φ_{sin}x}{Φ_{cos}x}).

B.2 The functions arcsin, arccos and arctan in G_{2}A^{ω}

As we have seen above, sin x is strictly monotone on [−\frac{π}{2} , \frac{π}{2} ] with the ‘modulus of uniform strict monotonicity’ ω(ε) := \frac{ε^{2}}{18}. Since sin x has the Lipschitz constant λ = 1, ∀y ∈ [−1, 1]∃x ∈ [−\frac{π}{2} , \frac{π}{2} ](sin x = y) implies

(∗) ∀y ∈ [−1, 1], n ∈ IN∃r_{n} ∈ \{q_{1}, …, q_{l_{n}}\}(| sin r_{n} − y| ≤ \frac{1}{n + 1}),

where \{q_{1}, …, q_{l_{n}}\} ⊂ [−\frac{π}{2} , \frac{π}{2} ]∩Q is a 1/(n+1)–net for [−\frac{π}{2} , \frac{π}{2} ]. Similarly to the function M used in our representation of [0, 1] one constructs a function M_{π} ∈ G_{2}R^{ω} such that {i : i ≤_{0} M_{π}n} contains (modulo our coding of Q) such a 1/(n + 1)–net (e.g. M_{π}n := j(8(n + 1), n)). (∗) implies

∀y ≤_{1} M, n^{0}∃q ≤_{0} M_{π}n( ˆ (−\frac{π}{2} )(n)+\frac{1}{n + 1} ≤Q q ≤Q ( ˆ\frac{π}{2} )(n)−\frac{1}{n + 1}∧|Φ_{sin}q−_{IR}ỹ| ≤_{IR} \frac{3}{n + 1})^{8}

and therefore

∀y ≤_{1} M, n^{0}∃q ≤_{0} M_{π}n

( ˆ(−\frac{π}{2} )(n) + \frac{1}{n+1} ≤Q q ≤Q (_{\frac{π}{2}})(n) − \frac{1}{n+1} ∧ |(Φ_{sin}q)(n) −Q ỹ(n)| ≤Q \frac{5}{n+1}).

8Here again λy^{1}.ỹ ∈ G_{2}R^{ω} is the construction corresponding to our representation of [−1, 1] such that ỹ ≤_{1} M, y =_{IR} ỹ if −1 ≤_{IR} y ≤_{IR} 1, and −1 ≤_{IR} ỹ ≤_{IR} 1 for all y^{1}.

Bounded μ–search provides a functional Ψ̃^{1(1)} ∈ G_{2}R^{ω} ∪ {Φ_{sin}} such that

∀y ≤_{1} M, n^{0}

( ˆ(−\frac{π}{2} )(n) + \frac{1}{n+1} ≤Q Ψ̃yn ≤Q (_{\frac{π}{2}})(n) − \frac{1}{n+1} ∧ |Φ_{sin}(Ψ̃yn))(n) −Q ỹ(n)| ≤Q \frac{5}{n+1})

and therefore

∀y ≤_{1} M, n^{0}( ˆ (−\frac{π}{2} )(n) + \frac{1}{n + 1} ≤Q Ψ̃yn ≤Q ( ˆ\frac{π}{2} )(n) − \frac{1}{n + 1} ∧ |Φ_{sin}(Ψ̃yn) −_{IR} ỹ| ≤_{IR} \frac{7}{n + 1})

Hence for Ψyn := Ψ̃y(7 · 36(n + 1)^{2})

∀y ∈ [−1, 1], n ∈ IN(|Φ_{sin}(Ψyn) −_{IR} ỹ| < \frac{1}{36(n + 1)^{2}} ).

From the fact that ω(ε) is a modulus of strict monotonicity for sin we obtain that (Ψyn)_{n∈IN} is a Cauchy sequence in [−\frac{π}{2} , \frac{π}{2} ] with Cauchy modulus 1/(n + 1): Suppose that m, m̃ ≥_{0} n, then

|Φ_{sin}(Ψym) − Φ_{sin}(Ψym̃)| ≤ |Φ_{sin}(Ψym) − ỹ| + |ỹ − Φ_{sin}(Ψym̃)| < \frac{1}{18(n + 1)^{2}}

and therefore |Ψym −Q Ψym̃| < \frac{1}{n+1}. Hence Φ_{arcsin}y := Ψỹ represents the inverse function of sin on [−\frac{π}{2} , \frac{π}{2} ] and is uniformly continuous on [−1, 1] with ω as a modulus of uniform continuity. The inverse arccos of cos on [0, π] is defined analogously. Similarly to arcsin, arccos one can finally define arctan in G_{2}A^{ω}.

B.3 The exponential functions exp_{n} and exp in G_{2}A^{ω} and G_{3}A^{ω}

Since all terms t^{1} ∈ G_{2}R^{ω} are bounded by a polynomial (see [15],prop.2.2.29) it is clear that exp can neither be defined in G_{2}A^{ω} nor can exp be represented by a new function constant which is majorized by a term from G_{2}R^{ω}. However for every fixed number n ≥_{0} 1 we can introduce the restriction of exp to [−n, n](⊂ IR) by such a constant. This means that we can deal locally with exp in G_{2}A^{ω} and e.g. may use exp for the solution of ordinary differential equations etc.

We add to G_{2}A^{ω} a function constant Φ_{exp_{n}}^{1(0)} which is intended to represent the restriction of exp on [−n, n] ∩ Q. Since exp is Lipschitz continuous on [−n, n] with a Lipschitz constant e.g. λ := 3^{n}, we have the following universal axioms on Φ_{exp_{n}}^{1(0)} in G_{2}A^{ω}^{9}

(1) ∀x^{0}(Φ̂_{exp_{n}}x =_{1} Φ_{exp_{n}}x ≤_{1} M_{n} ∧ 0 ≤_{IR} Φ_{exp_{n}}x ≤_{IR} 3^{n}),

where M_{n} is the boundedness function used in the representation of [0, 3^{n}] (e.g. M_{n}(k) := j(6 · 3^{n}(k + 1), 3(k + 1) − 1)).^{10}

(2) ∀x^{0}, y^{0}, q^{0}( − n ≤Q x, y ≤Q n ∧ |x −Q y| ≤Q \frac{q}{3^{n}} → |Φ_{exp_{n}}x −_{IR} Φ_{exp_{n}}y| ≤_{IR} q).

As in the case of Φ_{sin}, by (2) we can extend Φ_{exp_{n}} to a constant Φ̃_{exp_{n}}^{1(1)} ∈ G_{2}R^{ω} which represents the continuation of the function represented by Φ_{exp_{n}} to [−n, n]. As for Φ_{sin} we will denote this extension also by Φ_{exp_{n}}. The most important properties of exp (restricted on [−n, n]) can be expressed by purely universal sentences and thus are axioms of G_{2}A^{ω}:

(3) ∀x^{0}, y^{0}( − n ≤Q y ≤Q x ≤Q n → ∫_{y}^{x}(Φ_{exp_{n}}t)dt =_{IR} Φ_{exp_{n}}x −_{IR} Φ_{exp_{n}}y), Φ_{exp_{n}}0 =_{IR} 1,

(4) ∀x^{0}, y^{0}( − n ≤Q x, y, x +Q y ≤Q n → Φ_{exp_{n}}(x +Q y) =_{IR} Φ_{exp_{n}}(x) ·_{IR} Φ_{exp_{n}}(y)).

By the continuity of Φ_{exp_{n}}, (3) and (4) immediately generalize to real arguments. Furthermore by the theorem that the derivative of ∫_{0}^{x} f(x)dx is f (which can be expressed as a universal axiom in G_{2}A^{ω}), (3) implies

(3)’ ∀x^{1}(−n ≤_{IR} x ≤_{IR} n → Φ′_{exp_{n}}x =_{IR} Φ_{exp_{n}}x), where ′ denotes the derivative.

In contrast to G_{2}A^{ω} we can define the unrestricted exponential function in G_{3}A^{ω} as usual via the exponential series:^{11} one easily defines the sequence of partial sums of this series for rational arguments. From the quotient criterion one gets the convergence of this series together with a modulus of convergence. By the continuity of this series in x ∈ IR with the modulus ω(x, n) := 3^{⌈|_{x}(0)|+1⌉} · (n + 1) we can continue it on IR.

Analogously to the definition of arcsin we can define the inverse function ln_{n} of exp_{n} using the fact that e.g. ω(ε) := ε · 3^{−n} is a modulus of strict monotonicity for exp_{n} on [−n, n].

9As in the case of Φ_{sin} and Φ_{cos} we denote (according to the discussion in connection with theorem 3.2.8 in [15]) G_{2}A^{ω} ∪ {Φ_{exp_{n}}^{1(0)}} also by G_{2}A^{ω}

10For notational simplicity we identify in the following the natural number n with its code j(2n, 0)

as a rational number, e.g. we write x^{0} ≤Q n instead of x^{0} ≤Q j(2n, 0) in order to express that the rational number which is coded by x is ≤ the natural number n.

11In particular we can define a term Φ_{exp_{n}} in G_{3}A^{ω} which satisfies (provably) (1)–(4).

In this appendix we have seen that sin, cos can be introduced relatively to G_{2}A^{ω} via new

constants Φ_{sin}^{1(0)}, Φ_{cos}^{1(0)} and purely universal axioms which express the usual (characterizing) properties of sin, cos. tan and the inverse functions arcsin, arccos, arctan of sin, cos, tan as well as π can be defined in G_{2}A^{ω} using Φ_{sin}, Φ_{cos}. Furthermore for each fixed n ∈ IN the restriction exp_{n} of the exponential function exp to [−n, n] can be introduced relatively to

G_{2}A^{ω} via a new constant Φ_{exp_{n}}^{1(0)} and its characterizing properties can be expressed as universal axioms. Thus by theorem 3.2.8 from [15] the use of sin, cos, tan, arcsin, arccos, arctan, π and the local use of exp only contributes to the growth of provably functionals by majorants

∈ G_{2}R^{ω} for the constants Φ_{sin}^{1(0)}, Φ_{cos}^{1(0)}, Φ_{exp_{n}}^{1(0)} and the terms used in the formulation of their universal axioms and in the definition of π, arcsin, arccos, arctan.

Recent BRICS Report Series Publications

RS-97-30 Ulrich Kohlenbach. Proof Theory and Computational Analysis. November 1997. 38 pp.

RS-97-29 Luca Aceto, Augusto Burgueño, and Kim G. Larsen. Model Checking via Reachability Testing for Timed Automata. November 1997. 29 pp.

RS-97-28 Ronald Cramer, Ivan B. Damgård, and Ueli Maurer. Span Programs and General Secure Multi-Party Computation. November 1997. 27 pp.

RS-97-27 Ronald Cramer and Ivan B. Damgård. Zero-Knowledge Proofs for Finite Field Arithmetic or: Can Zero-Knowledge be for Free? November 1997. 33 pp.

RS-97-26 Luca Aceto and Anna Ingólfsdóttir. A Characterization of Finitary Bisimulation. October 1997. 9 pp. To appear in Information Processing Letters.

RS-97-25 David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. Searching Constant Width Mazes Captures the AC^{0} Hierarchy. September 1997. 20 pp. To appear in STACS ’98: 15th Annual Symposium on Theoretical Aspects of Computer Science Proceedings, LNCS, 1998.

RS-97-24 Søren B. Lassen. Relational Reasoning about Contexts. September 1997. 45 pp. To appear as a chapter in the book Higher Order Operational Techniques in Semantics, eds. Andrew D. Gordon and Andrew M. Pitts, Cambridge University Press.

RS-97-23 Ulrich Kohlenbach. On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. August 1997. 35 pp.

RS-97-22 Carsten Butz. Syntax and Semantics of the logic L_{ωω}^{λ}. July 1997. 14 pp.

RS-97-21 Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp.

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.