BRICS RS-03-12 Hernest & Kohlenbach: A Complexity Analysis of Functional Interpretations BRICS

Basic Research in Computer Science

A Complexity Analysis of Functional Interpretations

Mircea-Dan Hernest Ulrich Kohlenbach BRICS Report Series RS-03-12 ISSN 0909-0878 February 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Mircea-Dan Hernest & Ulrich Kohlenbach.

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/03/12/

A complexity analysis of functional interpretations

Mircea-Dan Hernest^{∗} and Ulrich Kohlenbach^{†}

February, 2003

Abstract

We give a quantitative analysis of Gödel’s functional interpretation and its monotone variant. The two have been used for the extraction of programs and numerical bounds as well as for conservation results. They apply both to (semi-)intuitionistic as well as (combined with negative translation) classical proofs. The proofs may be formalized in systems ranging from weak base systems to arithmetic and analysis (and numerous fragments of these). We give upper bounds in basic proof data on the depth, size, maximal type degree and maximal type arity of the extracted terms as well as on the depth of the verifying proof. In all cases terms of size linear in the size of the proof at input can be extracted and the corresponding extraction algorithms have cubic worst-time complexity. The verifying proofs have depth linear in the depth of the proof at input and the maximal size of a formula of this proof.

∗GKLI, Mathematisches Institut der Universität München, Theresienstr. 39, D-80333 München, Germany, \underline{danher@mathematik.uni-muenchen.de}; the first half of the work involved was carried at BRICS, Department of Computer Science, University of Aarhus; the second half of the work was supported by the “Deutsche Forschungsgemeinschaft” via the “Graduiertenkolleg Logik in der Informatik” (GKLI)

†BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade 540, DK-8000 Aarhus C, Denmark, \underline{kohlenb@brics.dk}; partly supported by the Danish Natural Science Research Council (Grant no. 21-02-0474)

Contents

1 Introduction 2 1.1 Outline of the main results . . . . . . . . . . . . . . . . . . . . 5 1.2 Notational conventions . . . . . . . . . . . . . . . . . . . . . . 9

2 The weak base system EIL^{ω} 9 2.1 The type structure FT . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Intuitionistic Equality Logic over FT (IEL^{ω}) . . . . . . . . . . 12 2.3 Extended Intuitionistic Equality Logic over FT (EIL^{ω}) . . . . . 17

3 A quantitative analysis of functional interpretation 22 3.1 Axiom extensions of EIL^{ω}. The system EIL_{+}^{ω}+AC+IP_{∀}+MK . . 25 3.2 The treatment of EIL^{ω} rules . . . . . . . . . . . . . . . . . . . 26 3.3 Bounds for realizing terms for EIL_{+}^{ω}+AC+IP_{∀}+MK axioms … 31 3.4 Better bounds on the size of extracted terms . . . . . . . . . . 39 3.5 Space and time complexity of the term extraction algorithm . 44

4 Immediate extensions of the quantitative analysis 45 4.1 Treatment of classical EIL^{ω}. The system ECL_{+}^{ω}+AC_{0}. . . . . . . 45 4.2 A quantitative analysis of monotone functional interpretation . 49

5 Extensions to Arithmetic and fragments of Analysis 54 5.1 Treatment of Primitive Recursive Arithmetic PRA^{ω} . . . . . . . 54 5.2 Extension to the analytical system PRA^{ω}+AC_{0}+WKL. . . . . . . 56 5.3 The case of Peano Arithmetic PA^{ω} and PA^{ω}+AC_{0}+WKL . . . . . 59

A Appendix 66

1 Introduction

This paper investigates the complexity of the extraction algorithms for effective data (such as programs and bounds) from proofs provided by Gödel’s functional (‘Dialectica’) interpretation and its monotone variant. The subject of extracting programs from proofs already has a long history. The techniques used can be roughly divided in two categories according to whether they are based on cut-elimination, normalization and related methods or on so-called proof interpretations. The latter typically make use of functionals of higher type. Prominent proof interpretations are realizability interpretations, particularly Kreisel’s [41] modified realizability (see [52] for a survey) and Gödel’s functional interpretation (first published in [21], see [3] for a survey). The no-counterexample interpretation (n.c.i.) due to Kreisel [39, 40] is sometimes viewed as a simplification of the functional interpretation (it uses only types of degree ≤ 2). In fact n.c.i. is not a real alternative since it has a bad behavior with respect to the modus ponens rule MP. This is overcome only if MP is interpreted by functional interpretation (see [34]).

Cut-elimination, normalization and the related ε-substitution method globally rebuild the given proof thereby increasing its length in a potentially non-elementary recursive way. In contrast, proof interpretations extract witnessing terms by recursion on the given proof tree which remains essentially unchanged in its structure. The latter techniques consequently enjoy full modularity: the global realizers of a proof can be computed from realizers of lemmas used in the proof. This suggests a radically lower complexity of the procedure and a radically smaller size of the extracted programs. Even though the latter would not be in normal form^{1} they can be used substantially in many ways without having to normalize them. One merely exploits properties which can be established inductively over their structure with the use of logical relations (like, e.g., Howard’s [24] notion of majorizability).

Both (modified) realizability and functional interpretations are applicable to a vast variety of formal systems and provide characterizations of their provably total programs. They had originally been applied to arithmetic in all finite types. They were subsequently adapted to various fragments thereof all the way down to weak systems of bounded arithmetic [10, 33, 45] or – more recently – the poly-time arithmetic of [5, 48]. They were extended to analysis [16, 42, 50], type theories [19] and fragments of set theory [8].

Realizability and functional interpretations cannot be directly applied to classical systems. A canonical manner of interpreting classical proofs would be by first translating them to intuitionistic proofs via a so-called negative translation and subsequently applying intuitionistic proof interpretations. However this fails for (modified) realizability since it extracts empty programs from negative formulas. The problem can be partly overcome by using an additional intermediate interpretation, the so-called Friedman-Dragalin A-translation [14, 17] and its variants [11] ^{2}. Unlike realizability interpretations, functional interpretations are sound for the so-called Markov principle and therefore feature extraction of programs from arbitrary proofs in fairly rich classical systems, like Peano arithmetic in all finite types PA^{ω} (see also Section 5.3). Hence the need for an intermediate translation is avoided when using functional interpretations. Moreover, monotone functional interpretation can extract programs from proofs T ⊢ ∀x^{ρ}∃y^{τ}Rec(x, y) in highly unconstructive systems T which contain, e.g., the binary König lemma. Here τ is an arbitrary finite type, ρ is a finite type of degree (aka level) at most 1 and Rec(x, y) is a specification which must^{3} be decidable if T is classical (we actually take it quantifier-free). This gives functional interpretations the ability of extracting programs and other effective data^{4} under certain conditions from ineffective proofs (proof mining). Monotone-functional-interpretation-based proof mining has already produced important results in computational analysis and has helped to obtain new results in mathematical analysis (see, e.g., [26, 28, 29, 31, 32, 35, 36, 37, 38]).

1Normalization would bring back the aforementioned complexities.

2See, e.g., [6, 44] for examples of program extractions using this approach. One draw-

A natural question that arises is whether such applications which were obtained ‘by hand’ could be automated or at least computer aided by implementing functional interpretations. In order to evaluate the feasibility of such a tool it is important to investigate the complexity aspects of functional interpretations. In the present paper we obtain upper bounds on the size of the terms which express the extracted programs. The interpretation algorithms only write down the extracted terms, proceeding by recursion on the input proof structure, see Section 3. It follows that their running time is proportional with the size of the extracted terms. Hence we obtain the time complexity of the extraction algorithms as a consequence of our quantitative analysis. Let n denote the size of the input proof P and m denote the maximal size of a formula of P. Due to the modularity of functional interpretations, these algorithms feature an almost linear time complexity, namely O(m^{2} · n) even for classical and analytical proofs. The almost refers to the fact that m is much smaller than n in most practical cases. In any case this time complexity is at most O(n^{3}), a result previously obtained by Alexi in [1] for an ad-hoc program-extraction technique for intuitionistic proofs only. Since the design of Alexi’s technique was driven by the optimal-time-overhead issue, cubic is probably the best worst-time-complexity one can expect from any program-extraction technique. We also give upper bounds on depths of the resulting verifying proofs – this is interesting for quantitative conservation results. In particular we obtain the feasibility of WKL–elimination for Π_{2}^{0}–sentences over primitive recursive arithmetic^{5} in all finite types by means of syntactic translations. Our technique is immediately implementable and in addition provides a term extraction procedure from analytical proofs.

back of this method is the limited modularity feature: only a restricted class of lemmas can be used in the proof at input. In contrast, functional-interpretations-based techniques feature full modularity: proofs at input may use arbitrary lemmas. See also [22] for applications of a form of recursive realizability.

3This restriction is generally unavoidable for classical proofs but is not necessary for intuitionistic proofs.

4Such as numerical bounds.

There exists a research line in extractive proof theory which is aimed at characterizing the classes of proofs from which programs belonging to certain complexity classes are extracted. Usually the feasible complexity classes are of interest, particularly poly-time, see for example [10, 48]. The issue of characterizing the complexity of provably total function(al)s of a theory is completely separate from the present paper’s topic. We are here concerned with the performance of the extraction algorithm and not with the one of the extracted programs.

The monotone variant of Gödel’s functional interpretation was developed by the second author in [26]. It takes into account that most applications of functional interpretation in recent years both to concrete proofs in numerical analysis and to conservation results do not actually use terms which realize the Gödel functional interpretation but terms which majorize^{6} (some) realizers. Monotone functional interpretation extracts majorizing terms which are simpler than the actual realizers produced by functional interpretation. This is due to the much simpler treatment of CT∧, see Proposition 3.22 and the paragraph following Definition 4.16. Also the treatment of induction axioms is much simpler, see Section 5. Moreover, the bound on verifying proof depth is better in the monotone case if the underlying logical system fairly supports monotone functional interpretation, see Remark 4.19.

1.1 Outline of the main results

We introduce the weak base system EIL^{ω}, a short for ‘(weakly extensional) extended intuitionistic equality logic in all finite types’. EIL^{ω} contains only the tools which are strictly necessary for carrying out the functional interpretation even for the most rudimentary intuitionistic systems.

5This was first shown in [2] for a second–order fragment with a formalized forcing technique.

6Majorization is understood in the sense of Howard [24] mentioned before.

We present upper bounds for the following quantitative measures of realizing/majorizing terms t extracted from proofs P in both semi-intuitionistic^{7} and classical systems based on EIL^{ω} up to the analytical system PA^{ω}+AC_{0}+WKL:

• the maximal degree (arity) of a subterm of t, denoted mdg (mar);

• the depth of t, denoted d (assuming a tree representation of the terms);

• the size of t, denoted S (number of all constants and variables used to build t).

We also give upper bounds on the depth^{8} of the verifying proof and time overhead of the extraction algorithm, here denoted ∂_{v} and θ respectively. For the extraction procedure we consider both the usual [21] and the monotone variant [26] of functional interpretation. We first consider a binarytree representation for terms, see also Footnote 32. Such a representation is more intuitive and therefore provides a better exposition of the bounds for mdg, mar. However it turns out that the same extracted terms have smaller size if represented in a more economic manner using pointers^{9}, see Section 3.4. Since their definition does not depend on the term representation, the bounds for mdg and mar still hold. From Section 3.4 on it is tacitly assumed that terms are represented in the economic manner. A representation for types becomes necessary only at the moment that we are interested in the space/time overhead of the extraction algorithm, see Section 3.5.

Let us denote by ∂ the depth and by S_{i}, S_{c}, S_{m} the size (in the sense of Definition 3.33) of P and for a formula A by

• vdg (var) the maximal degree (arity) of a variable occurring in A;

• id (fd, ld) the implication (forall, logical) depth of A, namely the maximal number of → (∀, all logical constants) on a path from root to leaves in the usual tree representation of A; by fid :≡ max{fd , id}; • qs the number of all quantifiers (including^{10} ∨) and free variables of A;

7Here semi-intuitionistic means intuitionistic plus a version of Markov’s principle MK and independence of premises for universal premises IP_{∀}, see Section 3.1 for details.

8Proofs are represented as trees, see also the last paragraph of Section 1.2.

9It would be possible to extract other terms which have the same smaller size in binarytree representation. However, the bounds for mdg, mar no longer hold in such a case, see also the remarks following Theorem 3.37.

• ls the number of all ∀, ∃, ∧, ∨, →, ⊥, = and free variables of A.

We prove that (relative to our underlying deductive framework EIL^{ω})

• mdg and mar do not depend on ∂; the difference between mdg (mar) and the maximal degree (arity) of a variable occurring in an axiom of P is linear (quadratic) in the maximal complexity of an axiom of P;

• d is linear in the maximal complexity of an axiom of P and ∂;

• S is linear in the size of P (here we use the economic representation of terms); also exponential in logarithm of the maximal complexity of an axiom of P and ∂ (this holds for the binary-tree representation of terms as well);

• ∂_{v} is linear in ∂ and the maximal complexity of an axiom of P.

More precisely, for semi-intuitionistic proofs P we have the following situation (below ‘FI’ means ‘functional interpretation’):

usual FI  monotone FI
mdg  O(1) + vdg_{0} + id_{0}  O(1) + vdg_{0} + id_{0}
mar  O(1) + var_{0} + qs_{0} · id_{0} O(1) + var_{0} + qs_{0} · id_{0}
d  O(ld_{1}) + qs_{0} · ∂  O(1) + qs_{0} · ∂
S  O(S_{i}) , O(ls_{1} · qs_{0}^{∂})  O(S_{m}) , O(qs_{0}^{∂})
∂_{v}  O(ld_{1} + ∂)  O(qs_{0} + ∂)
θ  O(qs_{0} · ls_{0} · S_{m})  O(qs_{0} · ls_{0} · S_{m})

where vdg_{0}, var_{0}, id_{0}, qs_{0}, ls_{0} are maxima taken over all the axioms of P ^{11} of vdg, var, id, qs and ls respectively and ld_{1}, ls_{1} are maxima of ld, ls taken over contractions A → A ∧ A of P.

10Since functional interpretation treats ∨ as an existential quantifier we count it as quantifier.

11In fact it is sufficient to consider only the axioms of the transformed proof P^{tr}, see Definition 3.8. Valid also for the subsequent definitions, including the classical case.

For classical proofs P there exists k ∈ IN constant (independent of P) such that (below ‘FI’ means ‘functional interpretation’):

usual FI  monotone FI
mdg  vdg_{0} + O(fid_{0})  vdg_{0} + O(fid_{0})
mar  var_{0} + O(qs_{0} · fid_{0})  var_{0} + O(qs_{0} · fid_{0})
d  O(ls_{0} · ∂)  O(qs_{0} · ∂)
S  O(S_{c}) , O(ls_{0} · qs_{0}^{k·∂})  O(S_{m}) , O(qs_{0}^{k·∂})
∂_{v}  O(ls_{0} + ∂)  O(qs_{0} + ∂)
θ  O(qs_{0} · ls_{0} · S_{m})  O(qs_{0} · ls_{0} · S_{m})

where vdg_{0}, var_{0}, qs_{0}, ls_{0} are maxima taken over all the axioms of P of vdg, var, qs and ls respectively and fid_{0} is the maximum of fid over all the formulas of P.

Since they are not produced by functional interpretation, we normally do not count the terms t_{1}, t_{2} which appear in prime formulas t_{1} = t_{2} of contractions A → A ∧ A and the quantifier axioms terms as part of the realizing terms. We rather consider them as “black boxes” and use their type and free variables information only (see Definition 3.10). From a programming perspective, they may be considered as subprograms residing in libraries and made accessible to the extracted program via references. The bounds for the usual functional interpretation actually hold also if we count in the terms mentioned above provided that instead of ld, ls one uses wd, respectively ws, where

• wd is the whole depth of A, assuming a tree representation of A where tree representations of the terms occurring in A are linked from the corresponding leaves of the usual tree representation of A;

• ws is the whole size of A, i.e., the number of all logical constants of A plus the number of all occurrences of variables and constants in A.

For mdg and mar also the maximal degree, respectively arity of constants occurring in contraction and quantifier axioms terms must be counted in. For more details see Remark 3.28.

1.2 Notational conventions

The symbols :≡ and ≡ belong to the meta-level and mean equal by definition to and is identical to respectively. The symbol = is used by abuse for equality in both meta-level and formal systems.

For a set M we let M^{≤ω}:≡ ∪_{n≤ω} M^{n}. The symbol IN denotes the set of natural numbers. For a function f : M′ ↦ IN and M ⊆ M′, M finite, we let

f(M) :≡ max{f(m) | m ∈ M}.

An enumeration S_{1}, …, S_{n} denotes an ordered tuple abbreviated \underline{S}; we denote by \{\underline{S}\} the set corresponding to \underline{S}, by |\underline{S}| the length of \underline{S} and by \underline{S′}, \underline{S′′} the concatenation of \underline{S′} and \underline{S′′}. If \{\underline{S}\} ⊆ M′ we abbreviate by f(\underline{S}) :≡ f(\{\underline{S}\}).

Let k_{0} ∈ IN be a sufficiently large constant (k_{0} ≡ 10 suffices for our purposes). For a labeled tree △ we denote by ∂(△) the depth of △ plus k_{0}, by ∂_{L}(△) the L depth of △, namely the maximal number of L labels on a path from root to leaves plus k_{0}, by Lv(△) the set of labels of leaves of △ and by V t(△) the set of labels of all vertices of △.

A (formal) proof in some logical system is a tree whose vertices are labeled with formulas, such that the leaves are labeled with axioms and assumptions and any parent vertex is labeled with the result of the application of an instance of some rule to the labels of its sons. The edges which connect the parent vertex with its sons are labeled with the name of the corresponding rule. We denote by L(·) the labeling function on vertices and edges. We call a proof complete if all its leaves are labeled with axioms only. Notice that an incomplete proof is complete in the system extended with its assumptions as axioms. We will denote proofs by ⊢ or , possibly with bounds on the depth attached, such as ⊢_{n} for a proof of depth at most n, n ∈ IN.

2 The weak base system EIL^{ω}

In the following we introduce the system EIL^{ω} ^{12} which forms in a sense a weak base system containing exactly the tools needed to carry out the functional interpretation. It extends intuitionistic logic in finite types with appropriate combinators^{13}, a cases operator D and some very basic arithmetic needed to define characteristic functionals for quantifier-free formulas.

12A short for ‘(weakly extensional) extended intuitionistic logic in all finite types’.

13These allow the definition of λ-terms, see Definition 2.12.

We also include C. Spector’s quantifier-free rule of extensionality ER_{0}. This allows an as extensional as possible treatment of higher type equality in the context of functional interpretation^{14}.

We first carry out a full quantitative analysis for the functional interpretation of an extension EIL_{+}^{ω}+AC+IP_{∀}+MK ^{15} of EIL^{ω} into the quantifierfree fragment of EIL^{ω}. Due to the modularity of functional interpretation this analysis immediately relativizes to further extensions of EIL^{ω} with certain axioms like, e.g., induction. Suppose that we consider an additional (closed) axiom A. Let us add to EIL^{ω} new constants \underline{c} of appropriate types and the axiom^{16} ∀\underline{y}A_{D}(\underline{c}, \underline{y}) expressing that \underline{c} satisfies the functional interpretation of A. The quantitative analysis for the functional interpretation of EIL_{+}^{ω}+AC+IP_{∀}+MK immediately relativizes to this extension. Functional interpretation now provides realizing terms \underline{t}[\underline{c}] built up out of the EIL^{ω}-material and \underline{c}. The complexity analysis for the extended theory is then completed by determining actual terms \underline{s} which satisfy the functional interpretation ∃\underline{x}∀\underline{y}A_{D}(\underline{x}, \underline{y}) of A and the complexity of the verifying proof ⊢ ∀\underline{y}A_{D}(\underline{s}, \underline{y}).

There are two possible ways of handling λ-abstraction in a system like EIL^{ω}. We could treat λ-abstraction either as a primitive concept or as defined by combinators. The treatment via combinators provides a finer complexity analysis and reflects more faithfully the actual functional interpretation of a Hilbert-style axiomatization^{17} of intuitionistic logic which we have – following Gödel’s original formulation – used for EIL^{ω}.

The combinators and projectors we use are more flexible than the usual Σ and Π first introduced by Schönfinkel in [47]. Our Σ provide in particular extensions of Schönfinkel Σ to tuples (see Definition 2.4) and our Π are extensions of Schönfinkel Π to tuples. This is natural since we use tuples of variables throughout our formulation of functional interpretation. The design of our Σ and Π is made according to the actual constructs required by functional interpretation while keeping the benefits of the usual Σ and Π. The latter allow to avoid any notion of bound variables in terms and are the most convenient in connection with logical relations^{18}. Our Σ and Π are in fact definable in terms of usual Σ and Π, though at the expense of a rather artificial increase in the length of the verifying proof. The upper bound on the size of the extracted terms would nevertheless still hold with such a definition, see Remark 3.30.

14Most applications of functional interpretation have been based on such an extensional variant. For sentences containing only variables of type 0 or 1 the use of full extensionality is admissible since the elimination-of-extensionality procedure from [42] is applicable.

15Here AC is the Axiom of Choice, IP_{∀} is Independence of Premises for universal premises and MK is a variant of Markov’s principle, see Section 3.1. For EIL_{+}^{ω} see Definition 3.10.

16Here ∃\underline{x}∀\underline{y}A_{D}(\underline{x}, \underline{y}) is the functional interpretation of A, see also Section 3.

17In a natural deduction context, it might be more natural to treat λ-abstraction as a primitive concept. Natural deduction formulations of functional interpretation are provided by Diller-Nahm [13] (see also [46, 51]) and Joergensen [25]. In the former all cases definitions for realizing terms of contractions are postponed to the end by collecting all candidates and making a single final global choice. In the latter choices are local and one has to apply a so-called ‘contraction lemma’ for each of them, i.e., whenever more than one copy of an assumption gets cancelled. In any case, the analysis carried out in the present paper can immediately be adapted to a system with λ-abstraction included as primitive construct, see Remark 3.30.

2.1 The type structure FT

The set FT of all finite types is inductively generated by the rules

(i) o ∈ FT

(ii) If σ, τ ∈ FT then (στ) ∈ FT.

Intuitively type o represents the set of natural numbers and (στ) represents the set of functions which map objects of type σ to objects of type τ. There are many alternative notations in the literature for (στ), such as τ(σ), (σ)τ, (σ → τ). We make the convention that concatenation of types is right associative and consequently omit unnecessary parenthesis, writing δστ instead of (δ(στ)). It can immediately be verified by induction over FT that each σ ∈ FT has the form σ_{1} … σ_{n}o with n ≥ 0. We abbreviate by:

• \underline{σ} the ordered tuple of types σ_{1}, …, σ_{n}

• \underline{σ}τ the type σ_{1} … σ_{n}τ.

If p is a permutation of \{1, …, n\}, \underline{σ}^{p} abbreviates the tuple σ_{p_{1}}, …, σ_{p_{n}}.

Definition 2.1 For a type we define:

• the arity by ar(o) :≡ 0, ar(στ) :≡ ar(τ) + 1;

• the degree by dg(o) :≡ 0, dg(στ) :≡ max{dg(σ) + 1 , dg(τ)} .

18One example of a logical relation is Howard’s majorizability which plays a key role in most applications of functional interpretation [3, 26, 27, 28, 30, 31, 33, 35, 38].

Let

\begin{aligned}dg(\underline{σ}) & :≡ & max\{dg(σ_{1}) , …, dg(σ_{n})\} \\ ar(\underline{σ}) & :≡ & max\{ar(σ_{1}) , …, ar(σ_{n})\} . \end{aligned}

The following hold:

dg(\underline{σ}τ) = max\{dg(\underline{σ}) + 1 , dg(τ)\}
ar(\underline{σ}τ) = ar(τ) + |\underline{σ}|

2.2 Intuitionistic Equality Logic over FT (IEL^{ω})

Our formalization of IEL^{ω} below is a slight modification of the axiomatic calculus for multisorted intuitionistic predicate logic used by Gödel in his original paper on functional interpretation [21]. The only differences are:

1. The syllogism and expansion are formulated as axioms instead of rules. Gödel’s formulation with rules was designed to ease the formulation of the soundness proof for the functional interpretation. Nevertheless for the quantitative analysis it is more convenient to use the axiom versions of

(a) the expansion rule

\frac{A → B}{C ∨ A → C ∨ B} ,

since the formula C may introduce realizing terms of arbitrary complexities; also the formula complexity of the conclusion is higher than the one of the premise;

(b) the syllogism rule

\frac{A → B , B → C}{A → C} ,

which would force us to consider the sum of quantitative measures of both premises when computing upper bounds for quantitative measures of the conclusion. We can immediately notice that the mere Modus Ponens

\frac{A , A → B}{B}

avoids such a situation, since the formula complexity of the premise A → B upper bounds that of the conclusion B.

2. The quantifier rules and axioms are formulated with tuples of variables since we use tuples throughout the functional interpretation.

The language of IEL^{ω}[C] contains, aside from the constants C, the following:

• denumerably many variables which we denote by letters x, y, z, u, v, w, possibly capitalized or adorned with subscripts; \underline{x}:≡ x_{1}, …, x_{n} denotes a tuple of variables; in the same context we use x as metavariable for an individual element of \underline{x}; each of the variables is associated a unique sort (mostly called type) which is an element of FT, such that there exist denumerably many variables for each sort; we possibly indicate the type of a variable by carrying it as a superscript, like x^{σ} and then \underline{x}\underline{σ}:≡ x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}.

• a binary predicate constant =_{o} for equality between objects of type o;

• logical constants ⊥, ∧, ∨, →, ∀x and ∃x (for each variable x).

Each of the constants in C is sorted as well, with the type possibly indicated as superscript. We often do not indicate C and write IEL^{ω} when the set of constants is either clear from the context or not relevant. We use l as metavariable for both variables and constants.

The terms of IEL^{ω} are sorted, with their types possibly indicated in superscripts and are inductively generated from variables and constants according to the rule that if t^{στ} and s^{σ} are terms then (ts)^{τ} is a term.

Terms are denoted by letters s, t, r, possibly adorned with subscripts; tuples of terms are denoted like \underline{t}:≡ t_{1}, …, t_{n}; in the same context we use t as metavariable for an individual element of \underline{t}.

We denote by V(t) the set of variables occurring in t and write t[\underline{x}] to indicate that \{\underline{x}\} ⊆ V(t). If V(t) = ∅ we say that t is a closed term.

We make the convention that concatenation of terms is left associative and consequently omit unnecessary parenthesis, writing rst instead of ((rs)t).

When writing down an expression it is always assumed that the terms are well-formed, i.e. the types are fitting.

For t^{σ} we denote by typ(t) :≡ σ and by

• ar(t) :≡ ar(σ) the arity of t;

• dg(t) :≡ dg(σ) the degree of t.

For a term we define

• the depth by d(l) :≡ 0, d(ts) :≡ max{d(t) , d(s)} + 1

• the size by S(l) :≡ 1, S(ts) :≡ S(t) + S(s).

The subterm relation is defined as the reflexive transitive closure of {(s, ts), (t, ts)}. We denote by s ≤ t the fact that s is a subterm of t. Obviously ≤ is a partial order relation. Let

\begin{aligned}mdg(t) & :≡ & max\{dg(s) | s ≤ t\} \\ mar(t) & :≡ & max\{ar(s) | s ≤ t\}. \end{aligned}

We notice that:

• dg(t) ≥ dg(ts), hence mdg(r) = max_{l≤r} dg(l)

• ar(t) ≥ ar(ts), hence mar(r) = max_{l≤r} ar(l)

We abbreviate by:

\begin{aligned}t(\underline{s}) & :≡ & t s_{1} … s_{m} \\ \underline{t}(\underline{s}) & :≡ & t_{1}(\underline{s}), …, t_{n}(\underline{s}) \end{aligned}

The formulas of IEL^{ω} are inductively generated from prime formulas s^{o} =_{o} t^{o} and ⊥ according to the rule that if A and B are formulas then (A ∧ B), (A ∨ B), (A → B), (∀xA) and (∃xA) are formulas.

Equality between terms s, t of type σ = σ_{1} … σ_{n}o (1 ≤ n) is an abbreviation for ∀x_{1}^{σ1} … x_{n}^{σ_{n}}(s x_{1} … x_{n} =_{o} t x_{1} … x_{n}), where the variables x_{1}, …, x_{n} do not occur in s, t. We abbreviate by \underline{s} = \underline{t} :≡ (s_{1} = t_{1}), …, (s_{n} = t_{n}) (hence a tuple of formulas).

∀\underline{x}, ∃\underline{x} abbreviate ∀x_{1} … ∀x_{n} and ∃x_{1} … ∃x_{n} respectively.

We abbreviate by A ↔ B:≡ ((A → B) ∧ (B → A)), ¬A:≡ (A → ⊥) and s ≠ t:≡ ¬(s = t). In order to avoid unnecessary parenthesis we make the convention that ∀x, ∃x, ¬, ∧, ∨, →, ↔ is the decreasing order of precedence and that → is right associative.

We denote formulas by letters A, B, C, possibly adorned with subscripts or superscripts. We call a formula quantifier-free if it does not contain ∀, ∃, ∨. The subscript 0 always indicates a quantifier-free formula, such as A_{0}, B_{0}, C_{0}.

We denote by V_{f}(A), V_{b}(A), V(A) the set of free, bounded, respectively all variables occurring in A and write A(\underline{x}) to indicate that \{\underline{x}\} ⊆ V_{f}(A). We denote by C(A) the set of constants occurring in A and by vdg(A) :≡ dg(V(A)),

var(A) :≡ ar(V(A)), cdg(A) :≡ dg(C(A)), car(A) :≡ ar(C(A)).

For S ⊆ {∀, ∃, ∧, ∨, →} we define d_{S}(·), the S-depth of a formula by

• d_{S}(s =_{o} t) :≡ d_{S}(⊥) :≡ k_{0} (see Section 1.2 for k_{0})

• For Q ∈ \{∀, ∃\}, d_{S}(Qx A) :≡ \{ \begin{matrix}d_{S}(A) + 1, & if Q ∈ S \\ d_{S}(A) , & if Q ∉ S \end{matrix}

• For □ ∈ \{∧, ∨, →\}, d_{S}(A□B) :≡ \{ \begin{matrix}max\{d_{S}(A) , d_{S}(B)\} + 1, & if □ ∈ S \\ max\{d_{S}(A) , d_{S}(B)\} , & if □ ∉ S \end{matrix}

For a formula A we define the following:

• the logical constants depth by ld(A) :≡ d_{∀,∃,∧,∨,→}(A);

• the whole depth by wd(A) :≡ d′_{∀,∃,∧,∨,→}(A); here d′ differs from d just in d′_{S}(s =_{o} t) :≡ k_{0} + max{d(s) , d(t)}

• the implication depth by id(A) :≡ d\underrightarrow{0}(A) and the forall depth by fd(A) :≡ d_{∀}^{0}(A); here d^{0} differs from d just in d_{S}^{0}(A_{0}) :≡ k_{0};

• the forall/implication depth by fid(A) :≡ max{fd(A) , id(A)};

• the quantifier size, denoted qs(A), is the number of quantifiers (including ∨) occurring in A, when A is a closed formula and the quantifier size of its universal closure in the general case;

• the logical constants size, denoted ls(A), is obtained by adding to qs(A) the number of ∧, →, ⊥, = occurring in A;

• the whole size, denoted ws(A), is obtained by adding to ls(A) the number of all occurrences of variables and constants in A.

We present below the rules and axioms of IEL^{ω}.

Logical rules

MP : A , A → B ⊢ B  (modus ponens)
EXP : A ∧ B → C ⊢ A → (B → C) (exportation)
IMP : A → (B → C) ⊢ A ∧ B → C  (importation)
\begin{matrix}QR∀ : \\ QR∃ : \end{matrix} \begin{matrix}B → A ⊢ B → ∀\underline{z}A \\ A → B ⊢ ∃\underline{z}A → B \end{matrix}  (quantifier rules)

We denote by QR :≡ QR∀ + QR∃. At QR, z is not free in B.

Logical axioms

\begin{matrix}CT∨ : \\ CT∧ : \end{matrix} \begin{matrix}A ∨ A → A \\ A → A ∧ A \end{matrix}  (contraction)
\begin{matrix}WK∨ : \\ WK∧ : \end{matrix} \begin{matrix}A → A ∨ B \\ A ∧ B → A \end{matrix}  (weakening)
\begin{matrix}PM∨ : \\ PM∧ : \end{matrix} \begin{matrix}A ∨ B → B ∨ A \\ A ∧ B → B ∧ A \end{matrix}  (permutation)
SYL : (A → B) ∧ (B → C) → (A → C) (syllogism)
EPN : (A → B) → (C ∨ A → C ∨ B)  (expansion)
EFQ : ⊥ → A  (ex falso quodlibet)
\begin{matrix}QA∀ : \\ QA∃ : \end{matrix} \begin{matrix}∀\underline{z}A(\underline{z}) → A(\underline{s}) \\ A(\underline{s}) → ∃\underline{z}A(\underline{z}) \end{matrix}  (quantifier axioms)

We denote by QA :≡ QA∀ + QA∃. At QA, s is free for z in A

and the substitution is simultaneous.

For instances B(\underline{s}) of QA which involve the constants \underline{s}, we define the • term depth of B(\underline{s}) by td(B) :≡ d(\underline{s});

• term size of B(\underline{s}) by ts(B) :≡ Σ_{s∈\underline{s}}S(s).

Equality axioms

REF : x =_{o} x  (reflexivity)
SYM : x =_{o} y → y =_{o} x  (symmetry)
TRZ : x =_{o} y ∧ y =_{o} z → x =_{o} z  (transitivity)

Remark 2.2 There exists k ∈ IN constant such that for all σ :

Higher-order equality

REF[σ] : IEL^{ω} ⊢_{k} x =_{σ} x  (reflexivity)
SYM[σ] : IEL^{ω} ⊢_{k} x =_{σ} y → y =_{σ} x  (symmetry)
TRZ[σ] : IEL^{ω} ⊢_{k} x =_{σ} y ∧ y =_{σ} z → x =_{σ} z  (transitivity)

Given a set of rules (axioms are comprised as rules with empty premise) Rl whose formulas contain the constants C, we denote by IEL^{ω}[Rl] the system IEL^{ω}[C] extended with the rules in Rl. We sometimes abbreviate IEL^{ω}[Rl] with a different denotation (like EIL^{ω} below) and then (IEL^{ω}[Rl])[Rl′] :≡ IEL^{ω}[Rl ∪ Rl′].

2.3 The system EIL^{ω}

Multisorted weakly extensional extended intuitionistic equality logic over FT, which we denote by EIL^{ω}, is obtained by extending IEL^{ω} with exactly the elements which are strictly necessary to carry out functional interpretation even for IEL^{ω}.

The language of EIL^{ω} contains the following constants:

• the zero constant 0 ≡ O_{o} of type o and for each type ρ ≡ \underline{σ}o, the zero constant O_{ρ} defined by the axiom

AxO : O_{ρ}(\underline{z}\underline{σ}) = 0

(hence for any type there exists at least one constant)

• the successor constant S of type oo defined by the axiom

AxS : \{ \begin{matrix}S x ≠ 0 \\ S x = S y → x = y \end{matrix}

• the boolean constants ν, I, E all of type ooo defined by the axioms

\begin{matrix}Axν : & (x = 0 ∧ y = 0) ↔ ν x y = 0 \\ AxI : & (x = 0 → y = 0) ↔ I x y = 0 \\ AxE : & x = y ↔ E x y = 0 \end{matrix}

• for each

– n, m ∈ IN, \underline{n}:≡ n_{0}, n_{1}, …, n_{m} ∈ IN, \overline{n}:≡ n^{1}, …, n^{m} ∈ IN with n_{0}, n_{1}, …, n_{m} ≤ n and n^{1}, …, n^{m} ≤ n,

– permutations \underline{p}:≡ p_{0}, p_{1}, …, p_{m} and \overline{p}:≡ p^{1}, …, p^{m} of \{1, …, n\} – types τ, \underline{σ} ≡ σ_{1}, …, σ_{n}, \underline{δ} ≡ δ_{1}, …, δ_{m}

the combinator constant Σ_{\underline{p},\overline{p},\underline{n},\overline{n}}^{\underline{σ},\underline{δ},τ,m} of type

– (\underline{σ_{0}} δ_{1} \underline{σ_{1}} … δ_{m} \underline{σ_{m}} τ) (\underline{σ}^{1} δ_{1}) … (\underline{σ}^{m} δ_{m}) \underline{σ} τ,

where – \underline{σ_{j}}:≡ σ_{(p_{j})_{1}}, …, σ_{(p_{j})_{n_{j}}} with j ∈ \overline{0, m} and

– \underline{σ}^{j}:≡ σ_{(p^{j})_{1}}, …, σ_{(p^{j})_{n^{j}}} with j ∈ \overline{1, m} defined by the axiom AxΣ : Σ_{\underline{p},\overline{p},\underline{n},\overline{n}}^{\underline{σ},\underline{δ},τ,m}(x, \underline{y}, \underline{z}) = x(\underline{z_{0}}, y_{1}(\underline{z}^{1}), \underline{z_{1}}, …, y_{m}(\underline{z}^{m}), \underline{z_{m}})

• for each n ∈ IN, permutation p of \{1, …, n\} and types τ, \underline{σ} ≡ σ_{1}, …, σ_{n}, the permutation constant P_{n,p}^{\underline{σ},τ} of type (\underline{σ}τ)\underline{σ}^{p}τ defined by the axiom AxP : P_{n,p}^{\underline{σ},τ}(x, \underline{z′}) = x(\underline{z})

• for each n, i ∈ IN, i ≤ n and types \underline{σ} ≡ σ_{1}, …, σ_{n}, the projector constant Π\underline{σ} ; i of type \underline{σ}σ_{i} defined by the axiom

AxΠ : Π\underline{σ} ; i(\underline{z}) = z_{i}

• for each n, i ∈ IN, i ≤ n and types \underline{σ} ≡ σ_{1}, …, σ_{n}, the decision constant D\underline{σ} ; i of type o\underline{σ} \underline{σ}σ_{i} defined by the axiom

AxD :  \{ \begin{matrix}x = 0 → D\underline{σ} ; i(x, \underline{z}, \underline{z′}) = z_{i} \\ x ≠ 0 → D\underline{σ} ; i(x, \underline{z}, \underline{z′}) = z′_{i} \end{matrix}  Here |\underline{z}| = |\underline{z′}|.

For simplicity we abbreviate by 1 :≡ S0. The system EIL^{ω} is finally obtained by adding the quantifier-free tertium non datur axiom

TND_{0} : x = 0 ∨ ¬(x = 0)

and the quantifier-free extensionality rule

ER_{0} : \frac{A_{0} → s_{1} = t_{1} , …, A_{0} → s_{n} = t_{n}}{A_{0} → B_{0}(\underline{s}) → B_{0}(\underline{t})} .

The formal proofs in the sequel will be in EIL^{ω} if not otherwise indicated.

Remark 2.3 The constants P and Π are definable in terms of Σ and also O_{\underline{σ}o} = Π_{1}^{o,\underline{σ}}0. We nevertheless chose to define them separately since they play a particular role.

Definition 2.4 As particular cases of Σ we distinguish the tuple-Schönfinkel combinators Σ_{(1_{n},1_{n}),(1_{n}),(n,0),(n)}^{\underline{σ},(δ),τ,1} with defining axioms of shape

Σ_{(1_{n},1_{n}),(1_{n}),(n,0),(n)}^{\underline{σ},(δ),τ,1}(x, y, \underline{z}) = x(\underline{z}, y(\underline{z})) .

These are generalizations of the usual^{19} Schönfinkel combinators Σ to tuples and will be used in the λ-abstraction Definition 2.12. The usual Schönfinkel combinators Σ are in fact particular cases of our Σ of shape Σ_{(1_{1},1_{1}),(1_{1}),(1,0),(1)}^{\underline{σ},(δ),τ,1}

with defining axioms Σ_{(1_{1},1_{1}),(1_{1}),(1,0),(1)}^{\underline{σ},(δ),τ,1}(x, y, z) = x(z, y(z)). Also the usual

Schönfinkel projectors Π are particular cases of our Π of shape Π_{1}^{(σ_{1},σ_{2})} with defining axioms Π_{1}^{(σ_{1},σ_{2})}(z_{1}, z_{2}) = z_{1}.

Remark 2.5 The quantifier-free tertium-non-datur TND_{0} becomes derivable in the presence of induction for propositional formulas. Moreover, in the presence of a modest amount of arithmetic, the constants D, I, ν, E are definable and their axioms derivable. Therefore these axioms are in fact redundant in any concrete application of functional interpretations, e.g., to HA^{ω} and fragments thereof. Examples of the latter are systems of bounded arithmetic like IPV^{ω} of [10] and the poly-time arithmetic LHA of [48] ^{20} .

19For the original definition of Schönfinkel Σ and Π see [47]. See also the last paragraph before Section 2.1.

20Even though LHA was designed in a modified realizability context, the outline of a similar functional-interpretation-generated system should be straightforward.

Remark 2.6 The extensionality axiom

EA[\underline{σ}] :  \underline{x}\underline{σ} = \underline{y}\underline{σ} → f^{\underline{σ}o} \underline{x} =_{o} f^{\underline{σ}o} \underline{y}  ( let EA :≡ ∪\underline{σ} EA[\underline{σ}] )

is derivable in EIL^{ω} for \underline{σ} ≡ o, …, o hence EIL^{ω} contains all equality axioms for type o. This no longer holds in general when \underline{σ} contains higher types (follows from [53](3.5.10) and [24]). On the other hand, ER_{0} is derivable from EA in EIL^{ω} ∖ ER_{0}, hence the rule is strictly weaker than the axiom, but only at higher types.

Remark 2.7 ⊢ ⊥ ↔ 1 = 0 and ⊢ x ≠ 0 ↔ Ix1 = 0.

Remark 2.8 There exists k ∈ IN constant such that for all \underline{s}, \underline{t}, r, r_{1}, r_{2}, B_{0}, the following hold:

\underline{s} = \underline{t} ⊢_{k} B_{0}(\underline{s}) → B_{0}(\underline{t})  (1)
\underline{s} = \underline{t} ⊢_{k} r[\underline{s}] = r[\underline{t}]
r_{1} = r_{2}, \underline{s} = \underline{t} ⊢_{k} r_{1}(\underline{s}) = r_{2}(\underline{t}).  (2)

Proposition 2.9

dg(Σ_{\underline{p},\overline{p},\underline{n},\overline{n}}^{\underline{σ},\underline{δ},τ,m}) = max\{dg(\underline{σ}, \underline{δ}) + 2 , dg(τ) + 1\}
dg(Π\underline{σ} ; i) = dg(\underline{σ}) + 1
dg(D\underline{σ} ; i) = dg(\underline{σ}) + 1
dg(P_{n,p}^{\underline{σ},τ}) = max\{dg(\underline{σ}) + 2 , dg(τ) + 1\}
ar(Σ_{\underline{p},\overline{p},\underline{n},\overline{n}}^{\underline{σ},\underline{δ},τ,m}) = ar(τ) + |\underline{σ}| + |\underline{δ}| + 1
ar(Π\underline{σ} ; i) = ar(σ_{i}) + |\underline{σ}|
ar(D\underline{σ} ; i) = ar(σ_{i}) + 2|\underline{σ}| + 1
ar(P_{n,p}^{\underline{σ},τ}) = ar(τ) + |\underline{σ}| + 1

□

In the proposition below we show how and at which cost in proof depth the quantifier-free formulas can be viewed as prime formulas.

Proposition 2.10 (Association of terms to quantifier-free formulas) There exists k ∈ IN constant and an association of terms to quantifier-free formulas A_{0} ↦ t_{A_{0}} such that for all A_{0},

⊢_{k·ld(A_{0})} A_{0}(\underline{a}) ↔ t_{A_{0}}[\underline{a}] = 0 .  (3)

Proof: The proof is by induction on the structure of A_{0}, making use of the boolean constants axioms. For prime formulas just take t_{⊥}:≡ 1, t_{t_{1}=t_{2}} :≡ Et_{1}t_{2} then recursively define t_{B_{0}∧C_{0}} :≡ νt_{B_{0}}t_{C_{0}}, t_{B_{0}→C_{0}} :≡ It_{B_{0}}t_{C_{0}}. □

Corollary 2.11 (TND and Stability for quantifier-free formulas) There exists k ∈ IN constant such that for all A_{0},

⊢_{k·ld(A_{0})} A_{0}(\underline{a}) ∨ ¬ A_{0}(\underline{a})  (4)
⊢_{k·ld(A_{0})} ¬¬ A_{0}(\underline{a}) → A_{0}(\underline{a}) .  (5)

Proof: The principle

STAB_{0} : ¬¬ x = 0 → x = 0

follows immediately with constant-depth proof from TND_{0}. Both (4) and (5) follow immediately from TND_{0} and STAB_{0} respectively by (3) and (1). □

Definition 2.12 (λ-abstraction) To every term t^{τ} one associates a term (λ\underline{x}\underline{σ}. t)^{\underline{σ}τ}, with V(λ\underline{x}. t) = V(t) − \{\underline{x}\}, recursively defined as follows:

λ\underline{x}. x_{i} :≡ Π\underline{σ} ; i
λ\underline{x}. t :≡ Π_{1}^{(τ,\underline{σ})}t, if \{\underline{x}\} ∩ V(t) = ∅
λ\underline{x}. (t^{δτ}s^{δ}) :≡ Σ_{(1_{n},1_{n}),(1_{n}),(n,0),(n)}^{\underline{σ},(δ),τ,1}(λ\underline{x}. t)(λ\underline{x}. s), if \{\underline{x}\} ∩ V(ts) ≠ ∅ (6)

Proposition 2.13 (β-reduction) There exists k ∈ IN constant such that for all t and \underline{r},

⊢_{k·d(t)} ( λ\underline{x}\underline{σ}. t[\underline{x}] ) \underline{r}\underline{σ} =_{τ} t[\underline{r}] .

Proof: By straightforward induction on d(t), using (2) when the induction step falls under (6). □

Proposition 2.14 The following hold:

d(λ\underline{x}. t) ≤ 2 · d(t)
S(λ\underline{x}. t) ≤ 3 · S(t)
mdg(λ\underline{x}. t) ≤ max\{dg(\underline{x}) + 1 , mdg(t)\} + 1
mar(λ\underline{x}. t) ≤ max\{mar(t) + 1 , ar(\underline{x})\} + |\underline{x}|

Proof: Structural induction on t, following Definition 2.12. □

Remark 2.15 In order to increase readability we will omit the adornments of Σ, P and Π from now on. We consider that this side information can be figured out from the context in a straightforward way. On the other hand its display would only complicate the exposition.

3 A quantitative analysis of functional interpretation

Gödel’s functional (Dialectica) interpretation, which assigns a formula A^{D} ≡ ∃\underline{x}∀\underline{y}A_{D}(\underline{x}; \underline{y}; \underline{a}) with A_{D} quantifier-free and \underline{x}, \underline{y} tuples of variables of finite type (s.t. \{\underline{x}, \underline{y}, \underline{a}\} = V_{f}(A_{D})) to each formula A(\underline{a}) (with \{\underline{a}\} = V_{f}(A)), was first introduced in [21] and is also presented in [42](4), [53](3.5.1).

For notational simplicity we will omit tuples of free variables of formulas but for the places where their presence is relevant. We shall denote by

\begin{aligned}B(\underline{a′})^{D} & ≡ & ∃\underline{u} ∀\underline{v} B_{D}(\underline{u}; \underline{v}; \underline{a′}) \\ C(\underline{a′′})^{D} & ≡ & ∃\underline{g} ∀\underline{h} C_{D}(\underline{g}; \underline{h}; \underline{a′′}). \end{aligned}

The interpretation is given by the following list of rules:

Definition 3.1 (Gödel’s functional interpretation)

A^{D} :≡ (A_{D} :≡ A) for prime formulas A
(A ∧ B)^{D} :≡ ∃\underline{x}, \underline{u} ∀\underline{y}, \underline{v} [(A ∧ B)_{D} :≡ A_{D}(\underline{x}; \underline{y}) ∧ B_{D}(\underline{u}; \underline{v})]
(∃zA(\underline{a}, z))^{D} :≡ ∃z, \underline{x} ∀\underline{y} [(∃zA(\underline{a}, z))_{D} :≡ A_{D}(\underline{x}; \underline{y}; \underline{a}, z)]
(∀zA(\underline{a}, z))^{D} :≡ ∃\underline{X} ∀z, \underline{y} (∀zA(\underline{a}, z))_{D}  (7)
(∀zA(\underline{a}, z))_{D} :≡ A_{D}(\underline{X}(z); \underline{y}; \underline{a}, z)
(A → B)^{D} :≡ ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{v} (A → B)_{D}  (8)

(A → B)_{D} :≡ A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{v})) → B_{D}(\underline{U}(\underline{x}); \underline{v})

(A ∨ B)^{D} :≡ ∃z^{o}, \underline{x}, \underline{u} ∀\underline{y}, \underline{v} (A ∨ B)_{D}

(A ∨ B)_{D} :≡ (z = 0 → A_{D}(\underline{x}; \underline{y})) ∧ (Iz1 = 0 → B_{D}(\underline{u}; \underline{v}))

Remark 3.2 For quantifier-free formulas A, A^{D} = A_{D} = A. The types and lengths of \underline{x} and \underline{y} depend only on the logical structure of A. Notice that V_{f}(A^{D}) = V_{f}(A) and V_{b}(A^{D}) = \{\underline{x}, \underline{y}\}.

Proposition 3.3 By induction on the structure of the formula A it can be easily proved that

qs(A^{D}) = |\underline{x}, \underline{y}, \underline{a}| = qs(A)  (9)

□

Lemma 3.4 The following hold:

dg(V_{b}(C^{D})) ≤ vdg(C) + id(C) − k_{0} + 1  (10)
ar(V_{b}(C^{D})) ≤ var(C) + qs(C) · (id(C) − k_{0} + 1)  (11)

Proof: The proof is by recursion on the structure of the formula C, following the Definition 3.1. We simply notice that

• dg(V_{b}(·^{D})) may increase only at (8), with the quantity 1; (7) forces us to start with 1 + vdg(C), since dg(X) = max{dg(x) , dg(z) + 1};

• ar(V_{b}(·^{D})) may increase with the quantity 1 at (7) and with at most |\underline{x}, \underline{v}| ≤ qs(A → B) ≤ qs(C) at (8), hence

ar(V_{b}(C^{D})) ≤ var(C) + fd(C) + qs(C) · (id(C) − k_{0}) .

□

Definition 3.5 Let Ax be an arbitrary but fixed^{21} set of axioms. For a set of closed terms Tm and a set of formulas Fm of EIL^{ω}[Ax] we define

• the prerealization relation by PR[Tm, Fm] :≡ \{(\underline{t}, A(\underline{a})) ⊆ Tm^{≤ω} × Fm | |\underline{t}| = |\underline{x}|, \{\underline{a}\} = V_{f}(A) and typ(\underline{t}(\underline{a})) = typ(\underline{x})\}. For (\underline{t}, A(\underline{a})) ∈ PR[Tm, Fm] we abbreviate by \{] \underline{t} , A [\}:≡ ∀\underline{y} A_{D}(\underline{t}(\underline{a}); \underline{y}; \underline{a}).

• the realization relation by

RR[Tm, Fm] :≡ \{ (\underline{t}, A) ∈ PR[Tm, Fm] | EIL^{ω}[Ax] ⊢ \{]\underline{t}, A[\} \}

• the set of realizing tuple selections RTS[Fm, Tm] as the set of those subsets of RR[Tm, Fm] which are functions from Fm to Tm^{≤ω}.

21See also Definition 3.10 and especially Remark 3.11.

We sometimes omit to specify Tm, Fm when they refer to all the closed terms, respectively formulas of EIL^{ω}[Ax]. The set Ax will be determined by the context. Whenever (\underline{t}, A) ∈ RR we denote this fact by \underline{t} Dr A and say that

• \underline{t} is a realizing tuple for A^{D};

• t is a realizing term for A^{D};

• A^{D} is realized by \underline{t} or t.

We call

• realizer any realizing tuple or term;

• realizer-free a formula A for which |\underline{x}| = 0.

Definition 3.6 We say that a proof P is realizer-free-normal if all realizerfree formulas of P are located at the leaf level.

Remark 3.7 Let P be a realizer-free-normal proof. There exists no instance of ER_{0} in P since the conclusion is quantifier-free and consequently realizerfree. Realizer-free formulas of P may label only leaves of P which are left premises of MP instances. Indeed, if the conclusion in any of the rules QR, EXP, IMP is non-realizer-free then also the premise must be non-realizer-free. For the MP rule, if the conclusion is non-realizer-free then also the A → B premise must be non-realizer-free.

Definition 3.8 To any proof P in some extension of EIL^{ω} we associate a realizer-free-normal proof P^{tr} which is obtained from P by removing its maximal subtrees rooted at vertices labeled with realizer-free formulas, yet keeping these roots (which become assumptions in P^{tr}). There is a fairly simple algorithm which transforms P to P^{tr} by recursion on proof structure.

Remark 3.9 The proofs we consider in the sequel are realizer-free-normal if not otherwise specified. See also Remark 3.32.

3.1 Axiom extensions of EIL^{ω}. The system

     EIL_{+}^{ω}+AC+IP_{∀}+MK

Instances of the following three schemata are formulas whose correspondents under functional interpretation can be realized by very simple terms, basically projectors Π. This makes them the first to be considered for axiom extensions of EIL^{ω} since by allowing them in proofs in the domain of functional interpretation causes no increase in complexity. Moreover the verifying proof is in EIL^{ω} and has a constant bound on its depth. The first two are logical axioms, i.e. they are valid in classical logic; the third axiom is non-logical.

1. a variant of Markov’s principle

MK : ¬¬ ∃\underline{x} A_{0}(\underline{x}) → ∃\underline{x} ¬¬ A_{0}(\underline{x}) ;

the usual^{22} formulation of Markov’s principle

MK′ : ¬¬∃\underline{x}A_{0}(\underline{x}) → ∃\underline{x}A_{0}(\underline{x})

can be deduced from MK with a proof which makes use of (5) and therefore has depth upper bounded by k ld(A_{0}) for some k ∈ IN constant; on the other hand the proof of MK from MK′ has constant depth;

2. Independence of Premises for universal premises

IP_{∀} : [ ∀\underline{x} A_{0}(\underline{x}) → ∃\underline{y} B(\underline{y}) ] → ∃\underline{y} [ ∀\underline{x} A_{0}(\underline{x}) → B(\underline{y}) ] ,

where \underline{y} ∉ V_{f}(∀\underline{x}A_{0}(\underline{x})) ;

3. the Axiom of Choice

AC : ∀\underline{x} ∃\underline{y} A(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x} A(\underline{x}, \underline{Y} (\underline{x})) .

Another simple axiom extension of EIL^{ω} is with realizer-free formulas since the quantitative analysis does not get affected in any way. There is a particular kind of such axiom extension which we consider in the sequel. Strictly, the terms t_{1}, t_{2} which appear in prime formulas t_{1} = t_{2} of contractions A → A ∧ A and terms \underline{s} involved in quantifier axioms A(\underline{s}) ≡ ∀\underline{z}B(\underline{z}) → B(\underline{s}) or A(\underline{s}) ≡ B(\underline{s}) → ∃\underline{z}B(\underline{z}) are part of the realizing term (see Section 3.3). However we do not count them in the quantitative analysis, but rather introduce new constants t̃_{1}, t̃_{2}, s̃ associated to terms t_{1}, t_{2}, s together with their defining axioms, such that any of the terms t_{1}, t_{2}, s contributes as much as a unit (plus the number of its free variables) of size to the realizing term. This is justified by the fact that we are merely interested in the complexity of functional interpretation itself; the terms t_{1}, t_{2}, s are not created by functional interpretation but are merely given as basic input data.

22We prefer the variant MK because the verifying proof of its functional interpretation is much simpler than for MK′. In the latter case the depth of the verifying proof is k ld(A_{0})

for some k ∈ IN constant.

Definition 3.10 Let Ax be an arbitrary but fixed set of axioms and Th_{rf} an arbitrary but fixed set of realizer-free theorems of EIL^{ω}[Ax]. We define below two extensions EIL_{+}^{ω} and EIL_{v}^{ω} of EIL^{ω}[Ax]. The system EIL_{+}^{ω} is obtained by simply adding Th_{rf} to the set of axioms of EIL^{ω}[Ax]. Let ˜ · be a map which uniquely associates constants t̃ to terms t[\underline{a}] of EIL^{ω}[Ax] such that

\begin{matrix}dg(t̃) & = & max\{dg(\underline{a}) + 1 , dg(t)\} \\ ar(t̃) & = & |\underline{a}| + ar(t) \end{matrix} \}  (12)

together with the defining axiom

Axt̃: t[\underline{a}] = t̃(\underline{a})

Let Tm be an arbitrary but fixed set of EIL^{ω}[Ax] terms. The system EIL_{v}^{ω} is obtained by extending EIL_{+}^{ω} with the defining axioms Axt̃ for the newly introduced constants t̃ associated to terms t ∈ Tm by (12).

Remark 3.11 All arbitrary but fixed items in the above definition are in fact context-dependent and will be in the subsequent concrete occurrences easy to figure out if not explicitly described.

3.2 The treatment of EIL^{ω} rules

Remark 3.12 Recall that the formal proofs below are by default in EIL^{ω}. See Definition 3.5 for the meaning of the relations PR, RR and RTS below.

Lemma 3.13 The following hold for any proof P:

qs(V t(P)) = qs(Lv(P)) and ls(V t(P)) = ls(Lv(P))  (13)
V(V t(P)) = V(Lv(P)) and C(V t(P)) = C(Lv(P))  (14)

Proof: The following (in)equalities are immediate:

\begin{matrix}qs(A → ∀\underline{z}B(\underline{z})) = qs(A → B(\underline{z})) & qs(∃\underline{z}A(\underline{z}) → B) = qs(A(\underline{z}) → B) \\ qs(A ∧ B → C) = qs(A → B → C) & qs(B) ≤ qs(A → B) \end{matrix}

It follows by structural induction on P that qs(A) ≤ qs(Lv(P)) for any formula A ∈ V t(P) and then qs(V t(P)) = qs(Lv(P)) is immediate. The argument for ls is identical and (14) has a similar proof, with ⊆ instead of ≤ . □

Lemma 3.14 (MP) There exists k ∈ IN constant and an algorithm which, given as input (\underline{t_{1}}, A(\underline{a})), (\underline{t_{2}}, \underline{t_{3}}, (A → B)(\underline{ã})) ∈ PR, produces as output (\underline{t_{4}}, B(\underline{a′})) ∈ PR and the following hold (below \{\underline{a_{1}}\}:≡ \{\underline{a}\} − \{\underline{a′}\} and \{\underline{ã}\} = \{\underline{a}\} ∪ \{\underline{a′}\}):

• t_{4} is obtained from t′_{4} :≡ Σ(t_{3}, \underline{t_{1}}, \underline{a_{1}}) = λ\underline{a′}. t_{3}(\underline{ã}, \underline{t_{1}}(\underline{a})) by replacing the variables in \underline{a_{1}} with constants O of appropriate type.

• \{] \underline{t_{1}} , A [\} , \{] \underline{t_{2}}, \underline{t_{3}} , A → B [\} ⊢_{k} \{] \underline{t_{4}} , B [\}

• d(\underline{t_{4}}) ≤ qs(A → B) + d(\underline{t_{1}}, \underline{t_{3}})  (15)

S(\underline{t_{4}}) ≤ 1 + qs(A → B) · S(\underline{t_{1}}, \underline{t_{3}})  (16)
dg(\underline{t_{4}}) ≤ dg(\underline{t_{3}}) and ar(\underline{t_{4}}) ≤ ar(\underline{t_{3}})
mdg(\underline{t_{4}}) ≤ max\{mdg(\underline{t_{1}}, \underline{t_{3}}) , dg(\underline{t_{3}}) + 1\}
mar(\underline{t_{4}}) ≤ max\{mar(\underline{t_{1}}, \underline{t_{3}}) , ar(\underline{t_{3}}) + 1 , ar(\underline{a_{1}})\}

Proof: There exists k ∈ IN constant such that for all (\underline{t_{1}}, A), (\underline{t_{2}}, \underline{t_{3}}, A → B) ∈ PR,

\underline{y}:≡ \underline{t_{2}}(\underline{ã}, \underline{t_{1}}(\underline{a}), \underline{v}) \frac{∀\underline{y} A_{D}(\underline{t_{1}}(\underline{a}); \underline{y})}{A_{D}(\underline{t_{1}}(\underline{a}); \underline{t_{2}}(\underline{ã}, \underline{t_{1}}(\underline{a}), \underline{v}))} k

\underline{x}:≡ \underline{t_{1}}(\underline{a}) \frac{∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{t_{2}}(\underline{ã}, \underline{x}, \underline{v})) → B_{D}(\underline{t_{3}}(\underline{ã}, \underline{x}); \underline{v}))}{A_{D}(\underline{t_{1}}(\underline{a}); \underline{t_{2}}(\underline{ã}, \underline{t_{1}}(\underline{a}), \underline{v})) → B_{D}(\underline{t_{3}}(\underline{ã}, \underline{t_{1}}(\underline{a})); \underline{v})} k

hence, by using MP once, we obtain that there exists k ∈ IN constant such that for all (\underline{t_{1}}, A), (\underline{t_{2}}, \underline{t_{3}}, A → B) ∈ PR,

\frac{∀\underline{y} A_{D}(\underline{t_{1}}(\underline{a}); \underline{y}) ∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{t_{2}}(\underline{ã}, \underline{x}, \underline{v})) → B_{D}(\underline{t_{3}}(\underline{ã}, \underline{x}); \underline{v}))}{B_{D}(\underline{t_{3}}(\underline{ã}, \underline{t_{1}}(\underline{a})); \underline{v})} k

Since by AxΣ there exists k ∈ IN constant such that for all (\underline{t_{1}}, A), (\underline{t_{2}}, \underline{t_{3}}, A → B) ∈ PR, ⊢_{k} t_{3}(\underline{ã}, \underline{t_{1}}(\underline{a})) = t′_{4}(\underline{a′}), and B_{D} is quantifier-free, by using (1) we obtain that there exists k ∈ IN constant such that for all (\underline{t_{1}}, A), (\underline{t_{2}}, \underline{t_{3}}, A → B) ∈ PR,

B_{D}(\underline{t_{3}}(\underline{ã}, \underline{t_{1}}(\underline{a})); \underline{v}) ⊢_{k} B_{D}(\underline{t′_{4}}(\underline{a′}); \underline{v})

and we conclude that there exists k ∈ IN constant such that for all (\underline{t_{1}}, A), (\underline{t_{2}}, \underline{t_{3}}, A → B) ∈ PR,

\frac{∀\underline{y} A_{D}(\underline{t_{1}}(\underline{a}); \underline{y}) ∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{t_{2}}(\underline{ã}, \underline{x}, \underline{v})) → B_{D}(\underline{t_{3}}(\underline{ã}, \underline{x}); \underline{v}))}{∀\underline{v} B_{D}(\underline{t′_{4}}(\underline{a′}); \underline{v})} k

We have that

\begin{aligned}d(\underline{t_{4}}) & ≤ & |\underline{t_{1}}, \underline{a_{1}}| + 1 + max\{d(\underline{t_{1}}) , d(\underline{t_{3}})\} \\ S(\underline{t_{4}}) & ≤ & 1 + (|\underline{t_{1}}, \underline{a_{1}}| + 1) · max\{S(\underline{t_{1}}) , S(\underline{t_{3}})\} . \end{aligned}

Inequalities (15) and (16) follow from

|\underline{t_{1}}, \underline{a_{1}}| + 1 ≤ qs(A) + 1 ≤ qs(A → B) ,

where for the last inequality we used that B is non-realizer-free. From

t_{3}(\underline{ã}, \underline{t_{1}}(\underline{a})) = t′_{4}(\underline{a′}) = Σ(t_{3}, \underline{t_{1}}, \underline{a_{1}}, \underline{a′})

we obtain that

\begin{aligned}dg(\underline{t_{4}}) & ≤ & dg(\underline{t_{3}}) & dg(\underline{a_{1}}) & ≤ & dg(Σ) = dg(t_{3}) + 1 \\ ar(\underline{t_{4}}) & ≤ & ar(\underline{t_{3}}) & ar(Σ) & = & ar(t_{3}) + 1 \end{aligned}

from which the remaining inequalities follow immediately. □

Lemma 3.15 (QR∀, QR∃) There exists k ∈ IN constant and an algorithm which, given as input (\underline{t_{1}}, \underline{t_{2}}, A(\underline{a}) → B(\underline{a′}, \underline{z})) ∈ PR, produces as output (\underline{t_{3}}, \underline{t_{4}}, A(\underline{a}) → ∀\underline{z} B(\underline{a′}, \underline{z})) ∈ PR and the following hold ( \{\underline{ã}\}:≡ \{\underline{a}\} ∪ \{\underline{a′}\} ):

• t_{3} :≡ P t_{1} = λ\underline{ã}, \underline{x}, \underline{z}. t_{1}(\underline{ã}, \underline{z}, \underline{x}) and t_{4} :≡ P t_{2} = λ\underline{ã}, \underline{x}, \underline{z}. t_{2}(\underline{ã}, \underline{z}, \underline{x})

• \{] \underline{t_{1}}, \underline{t_{2}} , A → B(\underline{z}) [\} ⊢_{k} \{] \underline{t_{3}}, \underline{t_{4}} , A → ∀\underline{z} B(\underline{z}) [\}

•

\begin{aligned}d(\underline{t_{3}}, \underline{t_{4}}) & ≤ & d(\underline{t_{1}}, \underline{t_{2}}) + 1 and dg(\underline{t_{3}}, \underline{t_{4}}) = dg(\underline{t_{1}}, \underline{t_{2}}) \\ S(\underline{t_{3}}, \underline{t_{4}}) & ≤ & S(\underline{t_{1}}, \underline{t_{2}}) + 1 and ar(\underline{t_{3}}, \underline{t_{4}}) = ar(\underline{t_{1}}, \underline{t_{2}}) \\ mdg(\underline{t_{3}}, \underline{t_{4}}) & ≤ & max\{mdg(\underline{t_{1}}, \underline{t_{2}}) , dg(\underline{t_{1}}, \underline{t_{2}}) + 1\} \\ mar(\underline{t_{3}}, \underline{t_{4}}) & ≤ & max\{mdg(\underline{t_{1}}, \underline{t_{2}}) , ar(\underline{t_{1}}, \underline{t_{2}}) + 1\} \end{aligned}

A corresponding statement holds for QR∃ as well, with the same bounds.

Proof: By definition,

\begin{aligned}(A → B(\underline{a′}, \underline{z}))^{D} & ≡ & ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{v} [A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{v})) → B_{D}(\underline{U}(\underline{x}); \underline{v}; \underline{a′}, \underline{z})] \\ (A → ∀\underline{z}B(\underline{a′}, \underline{z}))^{D} & ≡ & ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{z}, \underline{v} [A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{z}, \underline{v})) → B_{D}(\underline{U}(\underline{x}, \underline{z}); \underline{v}; \underline{a′}, \underline{z})] . \end{aligned}

By AxP , there exists k ∈ IN constant such that for all (\underline{t_{1}}, \underline{t_{2}}, A → B(\underline{z})) ∈ PR,

⊢_{k} t_{3}(\underline{ã}, \underline{x}, \underline{z}, \underline{v}) = t_{1}(\underline{ã}, \underline{z}, \underline{x}, \underline{v}) and ⊢_{k} t_{4}(\underline{ã}, \underline{x}, \underline{z}) = t_{2}(\underline{ã}, \underline{z}, \underline{x}) . Since A_{D}(\underline{x}; \underline{y}) → B_{D}(\underline{u}; \underline{v}; \underline{a′}, \underline{z}) is quantifier-free, by using (1) we obtain that there exists k ∈ IN constant such that for all (\underline{t_{1}}, \underline{t_{2}}, A → B(\underline{z})) ∈ PR,

\frac{A_{D}(\underline{x}; \underline{t_{1}}(\underline{ã}, \underline{z}, \underline{x}, \underline{v})) → B_{D}(\underline{t_{2}}(\underline{ã}, \underline{z}, \underline{x}); \underline{v}; \underline{a′}, \underline{z})}{A_{D}(\underline{x}; \underline{t_{3}}(\underline{ã}, \underline{x}, \underline{z}, \underline{v})) → B_{D}(\underline{t_{4}}(\underline{ã}, \underline{x}, \underline{z}); \underline{v}; \underline{a′}, \underline{z})} k .

Further, there exists k ∈ IN constant such that for all (\underline{t_{1}}, \underline{t_{2}}, A → B(\underline{z})) ∈ PR,

\frac{∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{t_{1}}(\underline{ã}, \underline{z}, \underline{x}, \underline{v})) → B_{D}(\underline{t_{2}}(\underline{ã}, \underline{z}, \underline{x}); \underline{v}; \underline{a′}, \underline{z}))}{∀\underline{x}, \underline{z}, \underline{v} (A_{D}(\underline{x}; \underline{t_{3}}(\underline{ã}, \underline{x}, \underline{z}, \underline{v})) → B_{D}(\underline{t_{4}}(\underline{ã}, \underline{x}, \underline{z}); \underline{v}; \underline{a′}, \underline{z}))} k .

Obviously, • dg(t_{3}) = dg(t_{1}), dg(t_{4}) = dg(t_{2}), hence dg(\underline{t_{3}}, \underline{t_{4}}) = dg(\underline{t_{1}}, \underline{t_{2}})

• ar(t_{3}) = ar(t_{1}), ar(t_{4}) = ar(t_{2}), hence ar(\underline{t_{3}}, \underline{t_{4}}) = ar(\underline{t_{1}}, \underline{t_{2}}) and the inequalities in the conclusion of this Lemma follow immediately. □

Lemma 3.16 (EXP, IMP) The following holds:

\{] \underline{t_{1}}, \underline{t_{2}}, \underline{t_{3}} , A → (B → C) [\} = \{] \underline{t_{1}}, \underline{t_{2}}, \underline{t_{3}} , A ∧ B → C [\}.

Proof: By definition,

(A ∧ B → C)^{D} ≡ ∃\underline{Y} , \underline{V} , \underline{G} ∀\underline{x}, \underline{u}, \underline{h}
[A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{u}, \underline{h})) ∧ B_{D}(\underline{u}; \underline{V} (\underline{x}, \underline{u}, \underline{h})) → C_{D}(\underline{G}(\underline{x}, \underline{u}); \underline{h})]
(A → B → C)^{D} ≡ ∃\underline{Y} , \underline{V} , \underline{G} ∀\underline{x}, \underline{u}, \underline{h}
[A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{u}, \underline{h})) → B_{D}(\underline{u}; \underline{V} (\underline{x}, \underline{u}, \underline{h})) → C_{D}(\underline{G}(\underline{x}, \underline{u}); \underline{h})] .

□ Theorem 3.17 There exists k ∈ IN constant and an algorithm 𝔄 which does the following. Let P be some proof of a formula A in EIL_{+}^{ω} and \underline{s}_{(·)} ∈ RTS[Lv(P)] a realizing tuple selection for the set of leaves of P. Let q_{0}:≡ max_{A∈Lv(P)} q(\underline{s}_{A}) for q ∈ \{d, S, dg, ar, mdg, mar\} and q_{0}:≡ q(Lv(P)) for q ∈ {qs, var}. Let^{23} ∂_{MP} :≡ ∂_{MP}(P), ∂_{QR} :≡ ∂_{QR}(P) and ∂:≡ ∂(P). Let ∂_{0} ∈ IN be a number such that for all A ∈ Lv(P), ⊢_{∂_{0}} \{]\underline{s}_{A}, A[\}. When 𝔄 is presented with P and \underline{s}_{(·)} at input, it produces as output (\underline{t}, A) ∈ RR and the following hold:

d(\underline{t}) ≤ d_{0} + ∂_{QR} + qs_{0} · (∂_{MP} − k_{0})  (17)
S(\underline{t}) ≤ (S_{0} + ∂_{QR} − k_{0} + 1) · qs_{0}^{(∂_{MP}−k_{0})}  (18)
dg(\underline{t}) ≤ dg_{0} and mdg(\underline{t}) ≤ mdg_{0} + 1  (19)
ar(\underline{t}) ≤ ar_{0} and mar(\underline{t}) ≤ max\{var_{0} , mar_{0} + 1\}  (20)
EIL_{+}^{ω} ⊢_{∂_{0}+k ∂} \{] \underline{t} , A [\}  (21)

Proof: The algorithm proceeds by recursion on the structure of P, using the algorithms in Lemmas 3.14 and 3.15 as subprocedures at the MP, respectively QR recursion steps; (21) follows immediately. We notice that dg and ar do not increase in the recursion, hence (19) and (20) are clear.

Let \underline{e} ≡ e_{1} … e_{n} denote paths from some leaf to the root of P, i.e., (e_{i})_{i∈\overline{1,n}} denote edges such that e_{1} is incident with a leaf and e_{n} is incident with the root of P. Let (d\underline{e} ; i , S\underline{e} ; i)_{i∈\overline{0,n}} be a sequence of pairs of natural numbers defined

by (d\underline{e} ; 0 , S\underline{e} ; 0) :≡ (d_{0} , S_{0}) and for i ∈ \overline{1, n},

(d\underline{e} ; i , S\underline{e} ; i) :≡ \{ \begin{matrix}(d\underline{e} ; i−1 + qs_{0} , qs_{0} · S\underline{e} ; i−1 + 1), & if L(e_{i}) = MP \\ (d\underline{e} ; i−1 + 1 , S\underline{e} ; i−1 + 1)  , & if L(e_{i}) ∈ QR \\ (d\underline{e} ; i−1 , S\underline{e} ; i−1)  , & otherwise \end{matrix} .

Using (13) it follows that max\underline{e} d\underline{e} ; n and max\underline{e} S\underline{e} ; n are upper bounds on d, S respectively. Inequalities (17) and (18) follow now immediately^{24} . □

Remark 3.18 Let us suppose that only unary (i.e., with n = 1) ER_{0} is allowed in the verifying proof. The n-ary ER_{0} can be obtained from unary ER_{0} with a proof of depth proportional with n. It follows that we can upper bound the depths of proofs of lemmas used in verifying MP and QR with quantities proportional with qs_{0}. In consequence, (21) becomes

EIL_{+}^{ω} ⊢_{∂_{0}+k·(qs_{0}+∂)} \{] \underline{t} , A [\} .

23 See Section 1.2 for the meaning of ∂_{MP}(P), ∂_{QR}(P) and ∂(P). Notice that QR∀, QR∃ and MP label edges in our EIL^{ω}-proof-trees P and QR cumulates both QR∀, QR∃ labels.

24At (18) an intermediate upper bound is (S_{0} + ∂_{QR} − k_{0}) · qs_{0}^{(∂_{MP}−k_{0})} + ∑_{i=0}^{(∂_{MP}−k_{0})−1} qs_{0}^{i} .

3.3 Bounds for realizing terms for EIL_{+}^{ω} +AC+IP_{∀} +MK axioms

Remark 3.19 Recall that the formal proofs below are by default in EIL^{ω}.

Proposition 3.20 There exists k ∈ IN constant such that for any instance A of CT∨, WK∨, WK∧, PM∨, PM∧, SYL, EPN, EFQ, TND_{0}, MK, IP_{∀}, AC, there exists a realizing tuple \underline{t} for A^{D} such that

d(\underline{t}) ≤ k  (22)
S(\underline{t}) ≤ k  (23)
mdg(\underline{t}) ≤ k + vdg(A) + id(A)  (24)
mar(\underline{t}) ≤ k + var(A) + qs(A) · (id(A) − k_{0} + 2)  (25)
EIL^{ω} ⊢_{k} \{] \underline{t} , A [\}  (26)

Proof: We treat here SYL as an example, since it is the most complex among the above listed axioms. The remaining axioms are treated in the Appendix.

We have

\begin{matrix}((A → B) ∧ (B → C) → (A → C))^{D} ≡ ∃\underline{X}, \underline{V} , \underline{U′}, \underline{H}, \underline{Y′}, \underline{G′} ∀\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′} \\ ( & \begin{aligned}( & \begin{matrix}A_{D}(\underline{X}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}); \underline{y}(\underline{X}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}), \underline{V} (\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}))) \\ → \\ B_{D}(\underline{u}(\underline{X}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′})); \underline{V} (\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′})) \end{matrix} & ) \\ & ⋀ \\ ( & \begin{matrix}B_{D}(\underline{U′}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}); \underline{v′}(\underline{U′}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}), \underline{H}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}))) \\ → \\ C_{D}(\underline{g}(\underline{U′}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′})); \underline{H}(\underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′})) \end{matrix} & ) \\ & ⟶ \\ ( & \begin{matrix}A_{D}(\underline{x′}; \underline{Y′}(\underline{y}, \underline{u}, \underline{v′}, \underline{g})(\underline{x′}, \underline{h′})) \\ → \\ C_{D}(\underline{G′}(\underline{y}, \underline{u}, \underline{v′}, \underline{g})(\underline{x′}); \underline{h′}) \end{matrix} & ) \end{aligned} & ) \end{matrix}

from

\begin{matrix}((A → B) ∧ (B → C))^{D} ≡ ∃\underline{Y} , \underline{U}, \underline{V′}, \underline{G} ∀\underline{x}, \underline{v}, \underline{u′}, \underline{h} \\ ((A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{v})) → B_{D}(\underline{U}(\underline{x}); \underline{v})) ∧ (B_{D}(\underline{u′}; \underline{V′}(\underline{u′}, \underline{h})) → C_{D}(\underline{G}(\underline{u′}); \underline{h}))) \end{matrix}

from

(A → B)^{D} ≡ ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{v})) → B_{D}(\underline{U}(\underline{x}); \underline{v}))
(B → C)^{D} ≡ ∃\underline{V′}, \underline{G} ∀\underline{u′}, \underline{h} (B_{D}(\underline{u′}; \underline{V′}(\underline{u′}, \underline{h})) → C_{D}(\underline{G}(\underline{u′}); \underline{h}))
(A → C)^{D} ≡ ∃\underline{Y′}, \underline{G′} ∀\underline{x′}, \underline{h′} (A_{D}(\underline{x′}; \underline{Y′}(\underline{x′}, \underline{h′})) → C_{D}(\underline{G′}(\underline{x′}); \underline{h′}))

and we can take (here \{\underline{a}\} = V_{f}((A → B) ∧ (B → C) → (A → C)))

\begin{aligned}t_{X} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}. x′ \\ t_{H} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}. h′ \\ t_{U′} & :≡ & P Σ = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}. u(\underline{x′}) \\ t_{V} & :≡ & P Σ = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}. v′(\underline{u}(\underline{x′})) \\ t_{Y′} & :≡ & P (Σ Σ) = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}, \underline{h′}. y(\underline{x′}, \underline{v′}(\underline{u}(\underline{x′}), \underline{h′})) \\ t_{G′} & :≡ & P Σ = λ\underline{a}, \underline{y}, \underline{u}, \underline{v′}, \underline{g}, \underline{x′}. g(\underline{u}(\underline{x′})) \end{aligned}

The proofs of (22) and (23) are immediate, for (24) and (25) we use the results in Proposition 2.9 plus (10), respectively (9, 11) and for (26) we use AxΣ, AxP, AxΠ, AxD and (1). □

Proposition 2.10 gives us an algorithm for associating terms t_{A_{D}} to formulas A such that ⊢ A_{D} ↔ t_{A_{D}} = 0. Since V(t_{A_{D}}) = V_{f}(A_{D}) these t_{A_{D}} are generally not closed, whereas we want to produce closed realizing terms for contractions A → A ∧ A. We could, of course, close these t_{A_{D}} via the λ-abstraction algorithm of Definition 2.12, however there is a more efficient way to achieve what we need.

Proposition 3.21 (Association of closed terms to all EIL_{+}^{ω} formulas) There exists k ∈ IN constant and an association of terms to EIL_{+}^{ω} formulas A ↦ t_{A}^{D} such that for all A (with \{\underline{a}\} = V_{f}(A))

d(t_{A}^{D}) ≤ k · ld(A)  (27)
S(t_{A}^{D}) ≤ k · ls(A)  (28)
mdg(t_{A}^{D}) ≤ k + vdg(A) + id(A)  (29)
mar(t_{A}^{D}) ≤ k + var(A) + qs(A) · (id(A) − k_{0} + 2)  (30)
EIL_{v}^{ω} ⊢_{k·ld(A)} A_{D}(\underline{x}; \underline{y}; \underline{a}) ↔ t_{A}^{D}(\underline{x}, \underline{y}, \underline{a}) = 0 .  (31)

The ˜ · constants in (31) are only those corresponding to terms occuring in A.

Proof: Induction on the structure of A. For prime formulas just take t_{⊥}^{D} :≡ 1 and (below \{\underline{a_{1}}\} = V(t_{1}), \{\underline{a_{2}}\} = V(t_{2}), and \{\underline{a}\} = V_{f}(t_{1} = t_{2}))

t_{t_{1}=t_{2}}^{D} :≡ Σ E t̃_{1} t̃_{2} = λ\underline{a}. E t̃_{1}(\underline{a_{1}}) t̃_{2}(\underline{a_{2}})

and otherwise define (below \{\underline{ã}\} = \{\underline{a}\} ∪ \{\underline{a′}\})

t_{A∧B}^{D} :≡ Σ ν t_{A}^{D} t_{B}^{D} = λ\underline{x}, \underline{u}, \underline{y}, \underline{v}, \underline{ã}. ν t_{A}^{D}(\underline{x}, \underline{y}, \underline{a}) t_{B}^{D}(\underline{u}, \underline{v}, \underline{a′})
t_{∃zA(\underline{a},z)}^{D} :≡ P t_{A(\underline{a},z)}^{D} = λz, \underline{x}, \underline{y}, \underline{a}. t_{A(\underline{a},z)}^{D}(\underline{x}, \underline{y}, \underline{a}, z)
t_{∀zA(\underline{a},z)}^{D} :≡ Σ t_{A(\underline{a},z)}^{D} = λ\underline{X}, z, \underline{y}, \underline{a}. t_{A(\underline{a},z)}^{D}(\underline{X}(z), \underline{y}, \underline{a}, z)
t_{A→B}^{D} :≡ Σ Σ I t_{A}^{D} t_{B}^{D} = λ\underline{Y} , \underline{U}, \underline{x}, \underline{v}, \underline{ã}. I t_{A}^{D}(\underline{x}, \underline{Y} (\underline{x}, \underline{v}), \underline{a}) t_{B}^{D}(\underline{U}(\underline{x}), \underline{v}, \underline{a′})
t_{A∨B}^{D} :≡ Σ Σ ν I t_{A}^{D} t_{B}^{D} I 1 =

= λz, \underline{x}, \underline{u}, \underline{y}, \underline{v}, \underline{ã}. ν (I z t_{A}^{D}(\underline{x}, \underline{y}, \underline{a})) (I (I z 1) t_{B}^{D}(\underline{u}, \underline{v}, \underline{a′}))

The inequalities (27) and (28) are immediate, (29) and (30) follow from (10), respectively (9, 11) and (31) follows using the axioms AxΣ, AxI, Axν, AxE. □

Proposition 3.22 There exists k ∈ IN constant such that for any instance A of CT∧ there exists a realizing tuple \underline{t} for A^{D} such that

d(\underline{t}) ≤ k · ld(A)
S(\underline{t}) ≤ k · ls(A)
mdg(\underline{t}) ≤ k + vdg(A) + id(A)
mar(\underline{t}) ≤ k + var(A) + qs(A) · (id(A) − k_{0} + 3)
EIL_{v}^{ω} ⊢_{k·ld(A)} \{] \underline{t} , A [\} .  (32)

The ˜ · constants in (32) are only those corresponding to terms occurring in A.

Proof: We have

\begin{aligned}(A ≡ B → B ∧ B)^{D} & ≡ & ∃\underline{Y} , \underline{X′}, \underline{X′′} ∀\underline{x}, \underline{y′}, \underline{y′′} \\ & [ B_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{y′}, \underline{y′′})) → B_{D}(\underline{X′}(\underline{x}); \underline{y′}) ∧ B_{D}(\underline{X′′}(\underline{x}); \underline{y′′}) ] \end{aligned}

and we can take (here \{\underline{a}\} = V_{f}(A) = V_{f}(B))

\begin{aligned}t_{X′} & :≡ & t_{X′′}:≡ Π = λ\underline{a}, \underline{x}. x \\ t_{Y} & :≡ & Σ D t_{B}^{D} = λ\underline{a}, \underline{x}, \underline{y′}, \underline{y′′}. D(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′}) \end{aligned}

The proof of (32) is as follows: By AxD, there exists k ∈ IN constant such that for all B,

\{ \begin{matrix}⊢_{k} & t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) = 0 → D(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′}) = y′′ \\ ⊢_{k} & I t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) 1 = 0 → D(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′}) = y′ \end{matrix}

and by using ER_{0}, there exists k ∈ IN constant such that for all B,

\{ \begin{matrix}⊢_{k} & t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) = 0 → B_{D}(\underline{x}; \underline{D}(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′})) → B_{D}(\underline{x}; \underline{y′′}) \\ ⊢_{k} & I t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) 1 = 0 → B_{D}(\underline{x}; \underline{D}(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′})) → B_{D}(\underline{x}; \underline{y′}) . \end{matrix}

By TND_{0} and AxI, there exists k ∈ IN constant such that for all B,

⊢_{k} t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) = 0 ∨ I t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) 1 = 0 .

¿From (31), there exists k ∈ IN constant such that for all B,

EIL_{v}^{ω} ⊢_{k·ld(B)} B_{D}(\underline{x}; \underline{y′}) ↔ t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}) = 0,

hence there exists k ∈ IN constant such that for all B,

\{ \begin{matrix}EIL_{v}^{ω} & ⊢_{k·ld(B)} & B_{D}(\underline{x}; \underline{y′}) → B_{D}(\underline{x}; \underline{D}(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′})) → B_{D}(\underline{x}; \underline{y′′}) \\ EIL_{v}^{ω} & ⊢_{k·ld(B)} & ¬B_{D}(\underline{x}; \underline{y′}) → B_{D}(\underline{x}; \underline{D}(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′})) → B_{D}(\underline{x}; \underline{y′}) . \end{matrix}

Since there exists k ∈ IN constant such that for all A, B, C,

\frac{A ∨ ¬A , A → B → C , ¬A → B → A}{B → A ∧ C} k,

we finally obtain that there exists k ∈ IN constant such that for all B,

EIL_{v}^{ω} ⊢_{k·ld(B)} B_{D}(\underline{x}; \underline{D}(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′})) → B_{D}(\underline{x}; \underline{y′}) ∧ B_{D}(\underline{x}; \underline{y′′}) .

Since there exists k ∈ IN constant such that for all B,

\begin{matrix}⊢_{k} & t_{Y} (\underline{a}, \underline{x}, \underline{y′}, \underline{y′′}) = D(t_{B}^{D}(\underline{x}, \underline{y′}, \underline{a}), \underline{y′′}, \underline{y′}) \\ ⊢_{k} & t_{X′}(\underline{a}, \underline{x}) = x \\ ⊢_{k} & t_{X′′}(\underline{a}, \underline{x}) = x , \end{matrix}

by (1) we obtain that there exists k ∈ IN constant such that

EIL_{v}^{ω} ⊢_{k·ld(B)} B_{D}(\underline{x}; \underline{t_{Y}} (\underline{a}, \underline{x}, \underline{y′}, \underline{y′′})) → B_{D}(\underline{t_{X′}}(\underline{a}, \underline{x}); \underline{y′′}) ∧ B_{D}(\underline{t_{X′′}}(\underline{a}, \underline{x}); \underline{y′})

which gives (32). The other inequalities follow immediately from Proposition 3.21. □

Proposition 3.23 There exists k ∈ IN constant such that for any instance A(\underline{s}) of QA∀, QA∃, there exists a realizing tuple \underline{t} for A^{D} such that

d(\underline{t}) ≤ k + fd(A), when A(\underline{s}) ∈ QA∀ and  (33)
d(\underline{t}) ≤ k, when A(\underline{s}) ∈ QA∃
S(\underline{t}) ≤ k + fd(A), when A(\underline{s}) ∈ QA∀ and  (34)
S(\underline{t}) ≤ k, when A(\underline{s}) ∈ QA∃
mdg(\underline{t}) ≤ k + vdg(A) + id(A)  (35)
mar(\underline{t}) ≤ k + var(A) + qs(A) · (id(A) − k_{0} + 2)  (36)
EIL_{v}^{ω} ⊢_{k} \{] \underline{t} , A [\}  (37)

The ˜ · constants in (37) are only those corresponding to terms occurring in A.

Proof: Let A(\underline{s}) ≡ ∀\underline{z}B(\underline{z}, \underline{a′′}) → B(\underline{s}, \underline{a′′}) be an instance of QA∀, s free for z in B. Let \underline{a′}:≡ V(\underline{s}) and \underline{a}:≡ \underline{a′}, \underline{a′′} = V_{f}(A(\underline{s})). Also \underline{s} ≡ s_{1}, …, s_{n} and let \underline{a_{i}}:≡ V(s_{i}) for i ∈ \overline{1, n}. We have

\begin{matrix}(∀\underline{z}B(\underline{z}) → B(\underline{s}))^{D} ≡ ∃\underline{Z}, \underline{Y} , \underline{X} ∀\underline{x}, \underline{y} \\ [ B_{D}(\underline{x}(\underline{Z}(\underline{x}, \underline{y})); \underline{Y} (\underline{x}, \underline{y}); \underline{Z}(\underline{x}, \underline{y})) → B_{D}(\underline{X}(\underline{x}); \underline{y}; \underline{s}) ] \end{matrix}

and we can take (recall from Definition 3.10 that s̃_{i}(\underline{a_{i}}) = s_{i})

t_{Z_{i}} :≡ Σ′ s̃_{i} = [λu_{i}, \underline{a}, \underline{x}, \underline{y}. u_{i}(\underline{a_{i}})]s̃_{i} = λ\underline{a}, \underline{x}, \underline{y}. s̃_{i}(\underline{a_{i}})
t_{Y} :≡ Π = λ\underline{a}, \underline{x}, \underline{y}. y
t_{X} :≡ P Σ \underline{s̃} = [λ\underline{u}, \underline{a}, \underline{x}. x(u_{1}(\underline{a_{1}}), …, u_{n}(\underline{a_{n}}))] \underline{s̃}
= λ\underline{a}, \underline{x}. x(s̃_{1}(\underline{a_{1}}), …, s̃_{n}(\underline{a_{n}}))

¿From Proposition 2.9, typ(u_{i}) = typ(s̃_{i}) and (12) it immediately follows that

\begin{aligned}dg(Σ′) & ≤ & 2 + max\{dg(\underline{a}, \underline{x}, \underline{y}) , dg(s_{i})\} \\ ar(Σ′) & ≤ & 1 + |\underline{a}, \underline{x}, \underline{y}| + ar(s_{i}) \\ dg(Π) & ≤ & 1 + dg(\underline{a}, \underline{x}, \underline{y}) \\ ar(Π) & ≤ & |\underline{a}, \underline{x}, \underline{y}| + ar(y) \\ dg(P) & ≤ & 1 + dg(Σ) ≤ 3 + max\{dg(\underline{a}, \underline{x}) , dg(\underline{s})\} \\ ar(P) & ≤ & 1 + ar(Σ) ≤ 2 + |\underline{a}, \underline{x}| + |\underline{s}| + ar(x) \end{aligned}

and (35), (36) now follow immediately from (10), respectively (9, 11), also using that |\underline{z}| = |\underline{s}| and typ(z_{i}) = typ(s_{i}).

The inequalities (33) and (34) are immediate from |\underline{s}| ≤ fd(A).

The proof of (37) uses the fact (which follows from (1)) that there exists k ∈ IN constant such that for all A(\underline{s}),

⊢_{k} B_{D}( \underline{x}(s̃_{1}(\underline{a_{1}})...s̃_{n}(\underline{a_{n}})) ; \underline{y}; s̃_{1}(\underline{a_{1}})...s̃_{n}(\underline{a_{n}}) ) → B_{D}( \underline{x}(s̃_{1}(\underline{a_{1}})...s̃_{n}(\underline{a_{n}})) ; \underline{y}; \underline{s}) .

Let A(\underline{s}) ≡ B(\underline{s}, \underline{a′′}) → ∃\underline{z}B(\underline{z}, \underline{a′′}) be an instance of QA∃, s free for z in B. The tuples \underline{a′}, \underline{a} and \underline{a_{i}} below are defined like in the QA∀ case above. We have

(B(\underline{s}) → ∃\underline{z}B(\underline{z}))^{D} ≡ ∃\underline{Y} , \underline{Z}, \underline{X} ∀\underline{x}, \underline{y} [ B_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{y}); \underline{s}) → B_{D}(\underline{X}(\underline{x}); \underline{y}; \underline{Z}(\underline{x})) ]

and we can take (recall from Definition 3.10 that s̃_{i}(\underline{a_{i}}) = s_{i})

\begin{aligned}t_{Y} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y}. y \\ t_{Z_{i}} & :≡ & Σ s̃_{i} = (λu_{i}, \underline{a}, \underline{x}. u_{i}(\underline{a_{i}}))s̃_{i} = λ\underline{a}, \underline{x}. s̃_{i}(\underline{a_{i}}) \\ t_{X} & :≡ & Π = λ\underline{a}, \underline{x}. x \end{aligned}

The inequalities (33) and (34) are trivial, (35), (36) follow with an argument similar to the one in the QA∀ case. For (37) we use the fact (which follows from (1)) that there exists k ∈ IN constant such that for all A(\underline{s}),

⊢_{k} B_{D}( \underline{x}; \underline{y}; s_{1}, …, s_{n}) → B_{D}( \underline{x}; \underline{y}; s̃_{1}( \underline{a_{1}}), …, s̃_{n}(\underline{a_{n}}) ) .

□

Notation 3.24 We will denote by qs_{0}(P) :≡ max{2 , qs(Lv(P))} and

\begin{aligned}vdg_{0}(P) & :≡ & vdg(Lv(P)) & var_{0}(P) & :≡ & var(Lv(P)) \\ fd_{1}(P) & :≡ & fd(QA∀ ∩ Lv(P)) & id_{0}(P) & :≡ & id(Lv(P)) \\ ld_{1}(P) & :≡ & ld(CT∧ ∩ Lv(P)) & ls_{1}(P) & :≡ & ls(CT∧ ∩ Lv(P)) \\ fid_{0}(P) & :≡ & fid(V t(P)) & ls_{0}(P) & :≡ & ls(Lv(P)) \end{aligned}

We will omit P when this will be clear from the context.

Theorem 3.25 There exists k ∈ IN constant such that for any proof P in EIL_{+}^{ω}+AC+IP_{∀}+MK and any non-realizer-free A ∈ Lv(P) there exists \underline{t}_{A} such that \underline{t}_{A} Dr A and the following hold:

• if A is not an instance of (CT∧, QA∀) then

\begin{matrix}d(\underline{t}_{A}) & ≤ & k \\ S(\underline{t}_{A}) & ≤ & k \\ mdg(\underline{t}_{A}) & ≤ & k + vdg_{0} + id_{0} \\ mar(\underline{t}_{A}) & ≤ & k + var_{0} + qs_{0} · id_{0} \\ EIL_{v}^{ω} ⊢_{k} \{] \underline{t}_{A} , A [\} \end{matrix} \}  (38)

• if A is an instance of CT∧, (38) holds except that

\begin{aligned}d(\underline{t}_{A}) & ≤ & k · ld_{1} \\ S(\underline{t}_{A}) & ≤ & k · ls_{1} \\ EIL_{v}^{ω} & ⊢_{k·ld_{1}} & \{] \underline{t}_{A} , A [\} \end{aligned}

• if A is an instance of QA∀, (38) holds except that

\begin{aligned}d(\underline{t}_{A}) & ≤ & k + fd_{1} \\ S(\underline{t}_{A}) & ≤ & k + fd_{1} \end{aligned}

The ˜ · constants of EIL_{v}^{ω} above^{25} are only those required by the terms \underline{t}_{A} and hence are limited to those corresponding to terms occurring in A.

Proof: Follows immediately from Propositions 3.20, 3.22, 3.23 and k_{0} ≥ 10. □

Theorem 3.26 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A in EIL_{+}^{ω}+AC+IP_{∀}+MK it produces as output \underline{t} such that \underline{t} Dr A and, with the notations 3.24 and abbreviations^{26} ∂_{MP} :≡ ∂_{MP}(P), ∂_{QR} :≡ ∂_{QR}(P) and ∂:≡ ∂(P), the following hold:

d(\underline{t}) ≤ k · ld_{1} + ∂_{QR} + qs_{0} · ∂_{MP}  (39)
S(\underline{t}) ≤ (k · ls_{1} + ∂_{QR}) · qs_{0}^{∂_{MP}}  (40)
mdg(\underline{t}) ≤ k + vdg_{0} + id_{0}  (41)
mar(\underline{t}) ≤ k + var_{0} + qs_{0} · id_{0}  (42)
EIL_{v}^{ω} ⊢_{k·(ld_{1}+∂)} \{] \underline{t} , A [\}  (43)

25See also Definition 3.10 and Remark 3.11.

26See Footnote 23 for the meaning of ∂_{MP}(P), ∂_{QR}(P) and ∂(P).

The ˜ · constants of EIL_{v}^{ω} in (43) are among those corresponding to terms occurring in the leaves of P.

Proof: Just a synthesis of the results in Theorems 3.17 and 3.25. For (39) and (40) we use that fd_{1} ≤ qs_{0} and k_{0} ≥ 10, hence

max{k · ld_{1} , k + fd_{1}} + ∂_{QR} + qs_{0} · (∂_{MP} − k_{0}) ≤ k · ld_{1} + ∂_{QR} + qs_{0} · ∂_{MP}

(max{k · ls_{1} , k + fd_{1}} + qs_{0} + ∂_{QR} − k_{0} + 1) · qs_{0}^{(∂_{MP}−k_{0})} ≤ (k · ls_{1} + ∂_{QR}) · qs_{0}^{∂_{MP}}

□

Notation 3.27 We will denote by

wd_{1}(P) :≡ max{wd(CT∧ ∩ Lv(P)) , td(QA ∩ Lv(P))}
ws_{1}(P) :≡ max{ws(CT∧ ∩ Lv(P)) , ts(QA ∩ Lv(P))}
cdg_{1}(P) :≡ cdg((CT∧ ∪ QA) ∩ Lv(P))
car_{1}(P) :≡ car((CT∧ ∪ QA) ∩ Lv(P))

We will omit P when this will be clear from the context.

Remark 3.28 Theorem 3.26 holds also when the terms t_{1}, t_{2} which build prime formulas t_{1} = t_{2} of contractions CT∧ and the quantifier axioms terms \underline{s} are counted as components of the global realizer (instead of just taking the associated constants t̃_{1}, t̃_{2}, s̃). We only need to use wd_{1}, ws_{1} instead of ld_{1}, ls_{1} and (41), (42) must be replaced with

\begin{aligned}mdg(\underline{t}) & ≤ & max\{k + vdg_{0} + id_{0} , cdg_{1}\} \\ mar(\underline{t}) & ≤ & max\{k + var_{0} + qs_{0} · id_{0} , car_{1}\} \end{aligned}

Corollary 3.29 There exists k′ ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A ≡ ∀\underline{x} ∃\underline{y} B(\underline{x}, \underline{y}) with \{\underline{x}, \underline{y}\} = V_{f}(B) in EIL_{+}^{ω}+AC+IP_{∀}+MK it produces as output \underline{t_{Y}} such that

EIL_{v}^{ω}+AC+IP_{∀}+MK ⊢_{k′·max\{ld_{1}+∂ , ld(B)\}} ∀\underline{x} B(\underline{x}, \underline{t_{Y}} (\underline{x}))

Proof: In this case we have A^{D} ≡ ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{v} B_{D}(\underline{U}(\underline{x}); \underline{v}; \underline{x}, \underline{Y} (\underline{x})), hence EIL_{v}^{ω} ⊢_{k·(ld_{1}+∂)} ∀\underline{v} B_{D}(\underline{t_{U}}(\underline{x}); \underline{v}; \underline{x}, \underline{t_{Y}} (\underline{x})) by Theorem 3.26 and further

EIL_{v}^{ω} ⊢_{k·(ld_{1}+∂)} ∃\underline{u} ∀\underline{v} B_{D}(\underline{u}; \underline{v}; \underline{x}, \underline{t_{Y}} (\underline{x})) [ ≡ B^{D}(\underline{x}, \underline{t_{Y}} (\underline{x})) ]  (44)

It can be easily proved by induction on ld(B) that there exists k′′ ∈ IN such that for all formulas B,

EIL^{ω}+AC+IP_{∀}+MK ⊢_{k′′· ld(B)} B ↔ B^{D}  (45)

The conclusion now follows immediately by combining (44) and (45). □

Remark 3.30 If λ-abstraction were treated as primitive and Σ, P, Π were defined in terms of it then (40) would still hold. E.g., for Σ defined as λx, \underline{y}, \underline{z}. x(\underline{z_{0}}, y_{1}(\underline{z}^{1}), \underline{z_{1}}, …, y_{m}(\underline{z}^{m}), \underline{z_{m}}) we would have S(Σ) ≤ 2 · |x, \underline{y}, \underline{z}|^{2} and on the other hand |x, \underline{y}, \underline{z}| ≤ qs_{0} for all Σ which appear in \underline{t}. Similarly (40) would still hold if only Schönfinkel Σ and Π were allowed^{27}. This follows from the λ-abstraction Definition 2.12. There exists k ∈ IN constant such that at most k · |x, \underline{y}, \underline{z}|^{2} ≤ k · qs_{0}^{2} tuple-Schönfinkel Σ and Π are needed to simulate our Σ and any of these tuple-Schönfinkel Σ and Π can be defined^{28} in terms of at most k · |x, \underline{y}, \underline{z}| ≤ k · qs_{0} usual Schönfinkel Σ and Π.

Remark 3.31 If we allow only unary (see Remark 3.18) ER_{0} in the verifying proof then (43) becomes

EIL_{v}^{ω} ⊢_{k·(ld_{1}+qs_{0}+∂)} \{] \underline{t} , A [\}

Remark 3.32 The algorithm of Theorem 3.26 can be applied to complete proofs P in EIL_{+}^{ω}+AC+IP_{∀}+MK after a preprocessing phase to P^{tr} via the procedure of Definition 3.8. Since IEL^{ω} ⊢ A ↔ A^{D} for any realizer-free assumption A produced by the realizer-free-elimination procedure, the verifying proof can use the same assumptions as P^{tr}. A complete verifying proof in EIL_{v}^{ω} can be produced by (re)including the parts of P which were eliminated in the preprocessing phase.

3.4 Better bounds on the size of extracted terms

Smaller terms can be extracted if we use a simplification provided by the definitional equation of Σ. The size of the extracted terms becomes linear in the size of the proof at input. Nevertheless the use of extra Σ’s brings an increase in type complexity. This can be avoided by using a more economical representation of the realizing tuples by means of pointers to parts which are shared by all members of a tuple. In such a setting all inequalities of Theorem 3.26 remain valid.

27See Definition 2.4 for the notions of “tuple-Schönfinkel” and “Schönfinkel” combinators Σ. Also for “Schönfinkel” projectors Π.

28For Σ the proof is by induction on |\underline{z}| of Definition 2.4. We have Σ x y z \underline{z′} = x z \underline{z′} (y z \underline{z′}) = Σ′ (xz) (yz) \underline{z′} hence Σ = λx, y, z. Σ′ (xz) (yz). For Π we can use the iterated λ-abstraction λz_{1}. (… λz_{n}. z_{i}).

The simplification is based on the observation that all terms t_{4} produced by MP (see Lemma 3.14) contain a common part. Namely \underline{t_{1}}, \underline{O}, which is somehow redundant to count for all t_{4} in \underline{t_{4}} - and this is what we have done by now. We give below a small example. Consider the following proof of C from A, A → B and B → C :

\frac{\frac{A , A → B}{B} , B → C}{C}

Let \underline{t_{1}} Dr A, (\underline{t_{2}}, \underline{t_{3}}) Dr (A → B) and (\underline{t_{5}}, \underline{t_{6}}) Dr (B → C). The algorithm in Lemma 3.14 first produces \underline{t_{4}} Dr B defined as t_{4} ≡ Σ(t_{3}, \underline{t_{1}}, \underline{O}) and then produces the realizing tuple for C, namely \underline{t_{7}} Dr C defined as

\begin{aligned}t_{7} & ≡ & Σ(t_{6}, \underline{t_{4}}, \underline{O′}) \\ & ≡ & Σ(t_{6}, Σ(t_{3}^{1}, \underline{t_{1}}, \underline{O}), …, Σ(t_{3}^{|\underline{t_{3}}|}, \underline{t_{1}}, \underline{O}), \underline{O′}) \end{aligned}

We immediately notice that the tuple \underline{t_{1}}, \underline{O} is common to all terms t_{4} ∈ \underline{t_{4}} and is multiply included in t_{7}. We describe below how it is possible to extract realizing terms such that the common parts which were previously multiply included are now counted only once for all the terms of a tuple.

Definition 3.33 For a proof P we define three size measures, denoted S_{i}(P), S_{c}(P), S_{m}(P), to be used in the semi-intuitionistic (i.e., what we have already described), the classical and in the monotone case respectively. The measure S_{m}(P) will be used also for the time upper bounds (see Section 3.5) in all cases. All three size measures are obtained by adding the following to the sum of qs(A → B) for all MP-right-premises A → B plus the sum of qs(C) for all QR-conclusions qs(C) (below A are non-realizer-free leaves):

S_{i}(P): the sum of qs(A) for non-CT∧ A plus the sum of ls(A) for CT∧ A;

S_{c}(P): the sum of ls(A) for all non-realizer-free leaves A;

S_{m}(P): the sum of qs(A) for all non-realizer-free leaves A.

Obviously S_{m}(P) ≤ S_{i}(P) ≤ S_{c}(P).

Definition 3.34 For the tuples \underline{t} ≡ t_{1}, …, t_{n} extracted by the algorithm of Theorem 3.26 we define a size measure, denoted Sz′(\underline{t}) in the following way. There exists m ≥ 0 and a tuple \underline{t′} such that each t_{i} ∈ \underline{t} is either of shape t_{i} ≡ P_{1}^{i}(… P_{m}^{i}(t^{i})) or of shape t_{i} ≡ P_{1}^{i}(… P_{m}^{i}(t^{i}(\underline{t′}))) where \{P_{j}^{i}\}_{j=1}^{m} and t^{i} are characteristic to t_{i} and \underline{t′} is common to all t_{i} in the corresponding subset of \underline{t}. It is possible that m = 0 and/or the aforementioned subset is ∅. We define

Sz′(\underline{t}) :≡ m · |\underline{t}| + Σ_{t′∈\underline{t′}} S(t′) + Σ_{i=1}^{n} S(t^{i}) .

Lemma 3.35 There exists k ∈ IN constant such that for any term P_{1}(P_{2} x) with P_{1}, P_{2} permutations there exists a permutation P_{3} such that ⊢_{k} P_{1}(P_{2} x) = P_{3} x.

Proof: By AxP for P_{1} we get (P_{1}(P_{2} x))(\underline{z^{p}}) = P_{2}(x, \underline{z}). We can now apply AxP for P_{2} and we distinguish two cases:

• \underline{z} ≡ \underline{u^{p′}}, \underline{v} and P_{2}(x, \underline{u^{p′}}) = x(\underline{u}) hence P_{2}(x, \underline{z}) = x(\underline{u}, \underline{v}) ≡ x(\underline{z^{p′′}}) and the last term is equal to P_{3}(x, \underline{z^{p}}) via a definitional equation for P_{3}.

• \underline{z}, \underline{y} ≡ \underline{u^{p′}} and P_{2}(x, \underline{u^{p′}}) = x(\underline{u}) hence (P_{1}(P_{2} x))(\underline{z^{p}}, \underline{y}) = x(\underline{u}) and the last term is equal to P_{3}(x, \underline{z^{p}}, \underline{y}) via a definitional equation for P_{3}.

□

Lemma 3.36 There exists k ∈ IN constant such that for any term P_{1}(… (P_{m} x)) with P_{1}, …, P_{m} permutations there exists a permutation P_{0} such that ⊢_{k·m} P_{1}(… (P_{m} x)) = P_{0} x.

Proof: Repeated applications of Lemma 3.35 and transitivity of equality. □

Theorem 3.37 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A in EIL_{+}^{ω}+AC+IP_{∀}+MK it produces as output \underline{t} such that \underline{t} Dr A with (43) and (below #_{MP} denotes the number of MP instances in P)

Sz′(\underline{t}) ≤ k · S_{i}(P)  (46)
3 #_{MP} ≤ d(\underline{t})  (47)
∂_{MP} − k_{0} ≤ mdg(\underline{t})  (48)
3 #_{MP} ≤ mar(\underline{t})  (49)

Proof: The proof of (46) is by structural induction on P. For axioms A we use the same realizing terms as before. When A is not an instance of CT∧ or QA∀, (46) follows from |\underline{t}| ≤ qs(A). If A ≡ B → B ∧ B then we notice that t_{B}^{D} of Proposition 3.22 is common to all realizing t_{Y} , hence using (9) and (28),

Sz′(\underline{t_{X′}}, \underline{t_{X′′}}, \underline{t_{Y}}) ≤ k′ ·|\underline{Y} , \underline{X′}, \underline{X′′}|+S(t_{B}^{D}) ≤ k′ ·qs(A)+k′′ ·ls(A) ≤ k ·ls(A) .

If A ≡ ∀\underline{z}B(\underline{z}, \underline{a′′}) → B(\underline{s}, \underline{a′′}) then the tuple \underline{s̃} of Proposition 3.23 is common to all realizing t_{X}, hence

Sz′(\underline{t_{Z}}, \underline{t_{Y}} , \underline{t_{X}}) ≤ k′ · |\underline{Z}, \underline{Y} , \underline{X}| + |\underline{s̃}| ≤ k · qs(A) .

Nothing to prove for EXP and IMP instances, see Lemma 3.16.

For QR instances the proof is trivial using Lemma 3.15.

For MP instances we use Lemma 3.14 and further improve the result by applying a number of Σ definitional equations. The algorithm in Lemma 3.14 is presented with the tuples \underline{t_{3}} and \underline{t_{1}}, represented ^{29} as

\begin{matrix}t_{3} & ≡ & P′_{1}(… P′_{m′}(t_{0}(\underline{t′}))) & = & P′(t_{0}(\underline{t′})) \\ t_{1}^{i} & ≡ & P_{1}^{i}(… P_{m}^{i}(t^{i}(\underline{t}))) & = & P_{i}(t^{i}(\underline{t})) \end{matrix} \} Using Lemma 3.36

and it produces (we assumed without loss of generality that 1 ≤ m′, m)

t_{4} ≡ Σ_{1}(P′(t_{0}(\underline{t′})), P_{1}(t^{1}(\underline{t})), …, P_{n}(t^{n}(\underline{t})), \underline{O}) =
= Σ_{2}(Σ_{1}, P′, P_{1}, …, P_{n}, t_{0}(\underline{t′}), t^{1}(\underline{t}), …, t^{n}(\underline{t}), \underline{O}) =
= Σ_{3}(Σ_{2}, t_{0}, t^{1}, …, t^{n}, \underline{t′}, \underline{t}, P′, P_{1}, …, P_{n}, Σ_{1}, \underline{O}) =
= P (Σ_{3}, Σ_{2}, P′, t_{0}, t^{1}, …, t^{n}, \underline{t′}, \underline{t}, P_{1}, …, P_{n}, Σ_{1}, \underline{O})

hence we can actually take

t_{4} ≡ (P Σ_{3} Σ_{2} P′ t_{0})(t^{1}, …, t^{n}, \underline{t′}, \underline{t}, P_{1}, …, P_{n}, Σ_{1}, \underline{O})  (50)

29In the case when \underline{t_{3}} or \underline{t_{1}} comes from a (sub)proof which involved CT∧ or QA∀ and no MP then we have an exception in the sense that only a part of the terms in the tuple share a common tuple, see also Definition 3.34. The reason should be obvious from the above treatment of CT∧ and QA∀. The final shape of the term t_{4} in (50) below is nevertheless not affected by this technical exception. After an MP all terms of the realizing tuple share a common tuple.

where t^{1}, …, t^{n}, \underline{t′}, \underline{t}, P_{1}, …, P_{n}, Σ_{1}, \underline{O} is common to all t_{4} ∈ \underline{t_{4}}. Hence

\begin{aligned}Sz′(\underline{t_{4}}) & ≤ & |P, Σ_{3}, Σ_{2}| · |\underline{t_{4}}| + |Σ_{1}, \underline{O}| + Sz′(\underline{t_{3}}) + Sz′(\underline{t_{1}}) \\ & ≤ & 3 · qs(A → B) + Sz′(\underline{t_{3}}) + Sz′(\underline{t_{1}}), \end{aligned}

where for the last inequality we used that |\underline{t_{4}}| + max\{1 , |\underline{O}|\} ≤ qs(A → B).

In order to prove the remaining inequalities it is useful to denote by cp(\underline{t}) the common tuple in the canonical representation of the tuple \underline{t} (i.e., \underline{t′}). We have |cp(\underline{t_{1}})| + |cp(\underline{t_{3}})| + 1 ≤ |cp(\underline{t_{4}})| because at least the constant Σ_{1} appears new at each MP application. It follows that for the final extracted tuple \underline{t} we have #_{MP} ≤ |cp(\underline{t})|. Now (47) and (49) are immediate because |cp(\underline{t})| ≤ d(\underline{t}) and |cp(\underline{t})| ≤ mar(\underline{t}). Also (48) is immediate once we notice that dg(cp(\underline{t})) increases by at least 1 at each MP application; this is due to the fact that t^{i} enters cp(\underline{t_{4}}) and dg(t^{i}) ≥ dg(\underline{t}) + 1.

The proof that (43) still holds is by straightforward computations. □ We notice that the price to pay for having smaller realizing terms is an

increase in type complexity. This is unavoidable with the actual representation of terms. The maximal degree of the realizing term increases by at least 1 at each MP application. This is due to the fact that subterms from the private part, which have degree greater by at least 1 than the maximal degree of the common part now enter the new common part.

We can avoid the increase in type complexity only by modifying the term representation such that the terms in the common part are multiply pointed from each member of the realizing tuple. In this way Σ_{3} is no longer needed for feeding the common part to each member of the realizing tuple. The increase in degree was due exactly to these Σ_{3}’s. We can now state the following theorem, where Sz is defined in the new pointer setting similarly to Sz′, i.e., counting common parts only once.

Theorem 3.38 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A in EIL_{+}^{ω}+AC+IP_{∀}+MK it produces as output \underline{t} such that \underline{t} Dr A, Sz(\underline{t}) ≤ k · S_{i}(P) and the inequalities of Theorem 3.26 all hold. □

Remark 3.39 The following inequalities are immediate:

\begin{aligned}S(t) & ≤ & Sz(\underline{t}) \\ S_{i}(P) & ≤ & (ls_{1}(P) + qs_{0}(P)) · 2^{∂(P)} ≤ 3 · ls_{1}(P) · qs_{0}(P)^{∂(P)} . \end{aligned}

They just express the fact that the new bounds on size are indeed better.

Remark 3.40 We will tacitly assume in the sequel that terms are represented with pointers in the manner described above.

3.5 Space and time complexity of the functional interpretation algorithm

In a real-world implementation of the algorithm of Theorem 3.26 we ought to count also the size of types associated to the EIL^{ω}-constants as part of the size of the realizing terms. This real-size of the extracted terms actually gives also the time complexity of the algorithm^{30} since what this does is only spelling down the extracted terms.

In order to compute the real-size we need to decide upon some representation of types. It turns out that the most efficient is to use dags ^{31}. We choose dags instead of normal binary trees^{32} because dags allow the reuse of existent types via pointers. Hence given the input proof P we start with the types of all variables and constants which appear in P and build the types of constants which are produced by functional interpretation. We therefore need to count for the real-size only the number of new type-nodes which are created in order to represent the type of a newly created constant c. By straightforward computations it follows that there exists k′ ∈ IN constant such that for any formula C, the number of new type-nodes required by V_{b}(C^{D}) is at most k′ · qs(C)^{2} · ls(C). Hence the number of new type-nodes required by the new variables created in the interpretation of the leaves, right MP–premises and QR–conclusions of P is at most k′ · qs_{0} · ls_{0} · S_{m}(P). Then we can immediately see that whenever a new constant c of type \underline{σ}τ is created by the algorithm of Theorem 3.26, the types \underline{σ}, τ are immediately available from the existent terms or functional-interpretation-created variables. There exists k′′ ∈ IN constant such that for any such new constant c created at a leaf C, MP–instance of right–premise C or QR–instance of conclusion C of P, at most k′′ · |\underline{σ}|^{2} ≤ k′′ · qs(C)^{2} new type-nodes are necessary to represent the type of c. Hence overall we have at most k′′ · qs_{0} · ls_{0} · S_{m}(P) newly created type-nodes in this category. We can now state the following theorem.

30The space complexity follows immediately by the principle that the space overhead of an algorithm is always less than its time overhead.

31Here “dag” is the usual acronym for “directed acyclic graph”.

32The representation with binary trees is in fact equivalent to the usual parenthesizedstrings representation.

Theorem 3.41 There exists k ∈ IN constant such that the time overhead of the algorithm in Theorem 3.38 is upper bounded by k · qs_{0} · ls_{0} · S_{m}(P). □

4 Immediate extensions of the quantitative analysis

4.1 Treatment of classical EIL^{ω}. The system ECL_{+}^{ω}+AC_{0}.

So far we have considered only semi-intuitionistic systems. We describe in the sequel how our complexity analysis can easily be adapted to classical logic (and theories) as well by applying it to the image of the classical system under a suitable negative translation. The so-called ‘negative’ or ‘double-negation’ translations have all in common the fact that the image of a formula is (intuitionistically equivalent to) a negative formula ^{33}. Negative translations were initially produced by Gödel [20], Gentzen, Kolmogorov, Glivenko. We use below a variant due to Kuroda of Gödel’s translation which we further adapt such as to handle blocks of universal quantifiers.

Definition 4.1 (Kuroda’s N-translation) To a formula A one associates A^{N} ≡ ¬¬A^{∗}, where A^{∗} is defined by structural induction on A as follows:

• A^{∗}:≡ A, if A is a prime formula;

• (A□B)^{∗}:≡ A^{∗}□B^{∗}, where □ ∈ {∧, ∨, →}

• (∃xA(x))^{∗}:≡ ∃x(A(x))^{∗}

• (∀\underline{x}A(\underline{x}))^{∗}:≡ ∀\underline{x}¬¬(A(\underline{x}))^{∗}, where A(\underline{x}) ≢ ∀yB(y, \underline{x})

Remark 4.2 A^{N} is realizer-free iff A is realizer-free.

33By definition, a formula is called negative, respectively existential-free if it is built up from negated prime, respectively prime formulas by means of ⊥, ∧, → and ∀ only. In our system negative formulas are trivially existential-free. On the other hand, EIL^{ω} ⊢ s =_{o} t ↔ ¬¬(s =_{o} t) for any prime formula s =_{o} t and hence also every existentialfree formula is equivalent to a negative formula.

N-translation followed by functional interpretation gives a proof interpretation for theories based on classical logic ^{34}. Remark 4.2 implies that given a (complete) proof P in some classical system the following are equivalent:

• carry out the composed^{35} interpretation to P^{tr};

• first do the N-translation of P, then apply the realizer-free-elimination algorithm of Definition 3.8 and finally carry out the functional interpretation of (P^{N})^{tr}.

The former approach is obviously more efficient: one does not carry out the N-translation of parts which subsequently get eliminated.

Let ECL^{ω}, ECL_{+}^{ω} be the classical versions^{36} of EIL^{ω}, EIL_{+}^{ω} respectively, obtained by replacing TND_{0} with the full tertium-non-datur schema A ∨ ¬A. Let

AC_{0} : ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x} A_{0}(\underline{x}, \underline{Y} (\underline{x}))

be the quantifier-free axiom-of-choice (with \underline{x} and \underline{y} of arbitrary types).

Remark 4.3 The proof–size measure S_{c} is introduced in Definition 3.33.

Proposition 4.4 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A in ECL_{+}^{ω}+AC_{0} it produces as output a proof P^{N} of A^{N} in EIL_{+}^{ω}+AC_{0}+MK and the following hold:

• ∂(P^{N}) ≤ k · ∂(P) and S_{i}(P^{N}) ≤ k · S_{c}(P);

•

\begin{matrix}qs_{0}(P^{N}) ≤ qs(V t(P^{N})) ≤ k · qs(V t(P)) & =^{(13)} & k · qs_{0}(P) \\ ld_{1}(P^{N}) ≤ ls_{1}(P^{N}) ≤ ls(V t(P^{N})) ≤ k · ls(V t(P)) & =^{(13)} & k · ls_{0}(P) \end{matrix}

• id_{0}(P^{N}) ≤ k · fid_{0}(P); we must use fid_{0}(P) because in the N-translation a ∀ brings two ¬, hence in fact two → due to our treatment of negation; • no new variable or constant appears in P^{N}, hence (using (14))

34Details of the use of negative translation in combination with functional interpretation may be found, e.g., in [3, 27, 42].

35In fact parts which are produced by N-translation also need to be transformed.

36Below EIL_{+}^{ω}-based systems will appear for verifying the functional interpretation of proofs in ECL_{+}^{ω}-based systems. In virtue of Remark 4.2 it should be obvious that A is a realizer-free axiom from Th_{rf} of ECL_{+}^{ω} (see Definition 3.10) if and only if A^{N} is a realizer-free axiom from Th_{rf} of EIL_{+}^{ω}.

vdg(V t(P^{N})) ≤ vdg(V t(P)) = vdg(Lv(P))
var(V t(P^{N})) ≤ var(V t(P)) = var(Lv(P))
cdg(V t(P^{N})) ≤ cdg(V t(P)) = cdg(Lv(P))
car(V t(P^{N})) ≤ car(V t(P)) = car(Lv(P))

Proof: The algorithm proceeds by recursion on the structure of P, see [27] for details. The proof of its correctness makes use of the following schemata of intuitionistic logic:

¬¬(A → B) ↔ (A → ¬¬B) ↔ (¬¬A → ¬¬B)  (51)
¬¬∀\underline{x}¬¬A(\underline{x}) ↔ ∀\underline{x}¬¬A(\underline{x})  (52)
A → ¬¬A  (53)

These schemata have proofs in which the axiom instances and intermediate formulas have size (depth) at most linear in the size (depth) of the formula to be proved. We only need to further notice that there exists k′ ∈ IN constant such that the following hold:

• the N-translation of any non-realizer-free axiom B of ECL_{+}^{ω}+AC_{0} is a theorem in EIL_{+}^{ω}+AC_{0}+MK whose proof P′ has the same structure for all instances of B, in particular the same depth; all formulas which appear in P′ have size (depth) upper bounded by k′ times the maximal size (depth) of B;

• any rule A_{1} [, A_{2}] ⊢ B of ECL_{+}^{ω}+AC_{0} is interpreted under N-translation to a proof P′ of B^{N} from A_{1}^{N} [, A_{2}^{N}]; P′ has the same structure for all instances of the rule, in particular the same depth; all formulas which appear in P′ have size (depth) upper bounded by k′ times the maximal size (depth) of A_{1} [, A_{2}].

As an example we prove the above claim for AC_{0} and QR∀. The other axioms and rules are even easier. \underline{Case AC_{0}}: We prove that there exists k′ ∈ IN constant such that for all A_{0},

EIL_{+}^{ω}+AC_{0}+MK ⊢_{k′} [ ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x} A_{0}(\underline{x}, \underline{Y} (\underline{x})) ]^{N}  (54)

By (53), the conclusion of (54) is implied by

∀\underline{x} ¬¬ ∃\underline{y} A_{0}(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x} ¬¬ A_{0}(\underline{x}, \underline{Y} (\underline{x})) .

This follows from MK and AC_{0} with a IEL^{ω}–proof of constant depth. \underline{Case QR∀}: B → A ⊢ B → ∀\underline{z}A. By induction hypothesis we have a proof of ¬¬(B^{∗} → A^{∗}). Then we use (51) and MP to get B^{∗} → ¬¬A^{∗} and by QR∀, B^{∗} → ∀\underline{z}¬¬A^{∗}. If A ≢ ∀yC then ∀\underline{z}¬¬A^{∗} ≡ (∀\underline{z}A)^{∗}. If A ≡ ∀\underline{x}A′ with A′ ≢ ∀yC then A^{∗} ≡ ∀\underline{x}¬¬A′^{∗} and using (52) we get B^{∗} → ∀\underline{z}, \underline{x}¬¬A′^{∗} with ∀\underline{z}, \underline{x}¬¬A′^{∗} ≡ (∀\underline{z}A)^{∗}. In any case we obtain ¬¬(B → ∀\underline{z}A)^{∗} (also using (53)). Hence overall the deduction of (B → ∀\underline{z}A)^{N} from (B → A)^{N} has constant depth. □

Remark 4.5 The new quantifier axioms of P^{N} are of shape ∀\underline{z}B(\underline{z}) → B(\underline{z}) and these can be realized with simple projectors Π instead of the terms t_{Z} of Proposition 3.23.

Remark 4.6 Except for those triggered by (A → A ∧ A)^{N}, the contractions CT∧ of P^{N} are required by the N-translations of A ∨ ¬A, QA∀ and QR∃. In the last two cases the verifying CT∧ is brought by the critical implication

(¬¬A → ¬¬B) → ¬¬(A → B)  (55)

of (51). The use of (55) can be avoided in the case of IMP, EXP by using axiom versions of these rules^{37}, the non-critical converse of (55) and MP.

Remark 4.7 ((P^{tr})^{N})^{tr} = (P^{N})^{tr} .

We are now able to describe an efficient algorithm for extracting realizing terms from (complete) proofs P in ECL_{+}^{ω}+AC_{0}. First P is transformed to P^{tr} and then to (P^{tr})^{N} via the algorithm of Theorem 4.4. In a second phase (P^{tr})^{N} is transformed^{38} to ((P^{tr})^{N})^{tr} and the algorithm of Theorem 3.26 is applied to it. Using Proposition 4.4, Theorems 3.38 and 3.41, Notation 3.24 and the abbreviations ∂:≡ ∂(P), S_{c} :≡ S_{c}(P) and S_{m} :≡ S_{m}(P) we can state the following theorem.

37The axiom versions of IMP and EXP are simply realized with projectors Π. This follows immediately from the fact that ( A → (B → C) )^{D} ≡ ( A ∧ B → C)^{D}. See also Lemma 3.16 and the comment before the cases MK, IP_{∀}, AC in the proof of Proposition A.1.

38Here only the parts produced by N-translation need to be transformed.

Theorem 4.8 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of a formula A in ECL_{+}^{ω}+AC_{0} it produces as output \underline{t} such that \underline{t} Dr A^{N} and the following hold:

d(\underline{t}) ≤ k · (ls_{0} + qs_{0} · ∂)  (56)
S(\underline{t}) ≤ Sz(\underline{t}) ≤ k · S_{c} ≤ k · (ls_{0} + ∂) · (k · qs_{0})^{k·∂}  (57)
mdg(\underline{t}) ≤ vdg_{0} + k · fid_{0}  (58)
mar(\underline{t}) ≤ var_{0} + k · qs_{0} · fid_{0}  (59)
EIL_{v}^{ω} ⊢_{k·(ls_{0}+∂)} \{] \underline{t} , A^{N} [\} .  (60)

The time overhead of the algorithm is upper bounded by k · qs_{0} · ls_{0} · S_{m}. The ˜ ·constants of EIL_{v}^{ω} in (60) are among those corresponding to terms occurring in the leaves of P^{N}. □

Remark 4.9 In the above theorem we use the more general quantity ∂ instead of the more detailed ones ∂_{QR} and ∂_{MP} which appear in Theorem 3.26. We do so because the N-translations of QR∀, QR∃, EXP and IMP trigger new MP instances in P^{N}. Hence ∂_{MP}(P^{N}) ≥ ∂(P) already.

Corollary 4.10 Let A ≡ ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) with A_{0} quantifier-free and V_{f}(A_{0}) = \{\underline{x}, \underline{y}\}. The theorem above holds also with A instead of A^{N}, i.e., \underline{t} Dr A with EIL_{v}^{ω} ⊢_{k·(ls_{0}+∂)} ∀\underline{x} A_{0}(\underline{x}, \underline{t}(\underline{x})) and (56), (57), (58), (59).

Proof: There exists k′ ∈ IN constant such that, using (52) and (5),

EIL_{+}^{ω}+MK ⊢_{k′· ld(A_{0})} (∀\underline{x}∃\underline{y}A_{0}(\underline{x}, \underline{y}))^{N} → ∀\underline{x}∃\underline{y}A_{0}(\underline{x}, \underline{y}) .

¿From (13) it follows that the quantity ld(A_{0}) gets absorbed into ls_{0}. □

4.2 A quantitative analysis of monotone functional interpretation

The second author realized in [26] that a much simpler extraction procedure applies if the goal is to extract majorizing functionals \underline{t^{∗}} for the realizing terms \underline{t} of A^{D} , i.e., terms \underline{t^{∗}} such that

M : ∃\underline{x} [ \underline{t}^{∗} maj \underline{x} ∧ ∀\underline{a}, \underline{y} A_{D}(\underline{x}(\underline{a}), \underline{y}, \underline{a})] .

Here maj is W.A. Howard’s majorization relation (see [24]) and \underline{y} maj \underline{x} :≡ ∧ (y maj x). This is of significance since \underline{t^{∗}} suffices for many (if not most) applications of functional interpretation. These range from conservation results (e.g., for weak König’s lemma [30]) to the proof mining of concrete proofs [28, 31, 32, 35]. We noticed in Section 3 that the contraction A → A ∧ A is by far the most complicated axiom in the usual functional interpretation. Monotone functional interpretation features a very simple treatment of A → A ∧ A and therefore the extraction process for \underline{t^{∗}} becomes much simpler than the one for \underline{t}.

Definition 4.11 Let EIL_{M}^{ω} be an extension of EIL^{ω} with the following:

• An inequality relation ≥_{o} for type-o-objects with the usual axioms plus

1 ≥_{o} I x^{o} y^{o} 1 ≥_{o} ν x^{o} y^{o} 1 ≥_{o} E x^{o} y^{o} .

Inequality for higher types is defined extensionally by

x ≥_{\underline{σ}o} y :≡ ∀\underline{z}\underline{σ} ( x \underline{z} ≥_{o} x \underline{z} ) .

The majorization relation is defined by maj_{o} :≡ ≥_{o} and

x^{∗} maj_{\underline{σ}o} x :≡ ∀\underline{z}\underline{σ}, \underline{y}\underline{σ} ( \underline{z} maj \underline{σ} \underline{y} → x^{∗} \underline{z} maj_{o} x \underline{y} ) ,

where \underline{z} maj \underline{σ} \underline{y} is an abbreviation for ∧_{σ∈\underline{σ}}(z maj_{σ} y) .

• A maximum constant M_{o} of type ooo with the axioms

AxM : M_{o} x y ≥_{o} x M_{o} x y ≥_{o} y M_{o} maj M_{o} .

Maximum constants for higher types are defined by

M_{\underline{σ}o}:≡ Σ M_{o} = λx^{\underline{σ}o}, y^{\underline{σ}o}, \underline{z}\underline{σ}. M_{o} (x \underline{z}) (y \underline{z}) .

• A schema of explicit definability for arbitrary quantifier-free formulas:

ED[A_{0}] : ∃Y ∀\underline{a} [ (1 ≥_{o} Y (\underline{a})) ∧ (A_{0}(\underline{a}) ↔ Y (\underline{a}) =_{o} 0) ] .

• Axioms S maj S and O maj O.

Remark 4.12 In the presence of a minimal amount of arithmetic S maj S and O maj O are immediately provable. Also the constants ≥_{o}, ν, I, E and M_{o} can be defined such that the remaining axioms of Definition 4.11 become provable (see also Remark 2.5).

Remark 4.13 The formulas Σ maj Σ, Π maj Π and P maj P hold in EIL_{M}^{ω} with proofs of depths proportional with the arities of Σ, Π and P respectively. Then M_{ρ} maj M_{ρ} holds for arbitrary ρ with a formal proof of depth proportional with ar(ρ) + 1.

Lemma 4.14 There exists k ∈ IN constant such that for any tuple of terms \underline{s} of EIL_{M}^{ω} (with V(\underline{s}) = \{\underline{x}\}) there exist corresponding terms \underline{s^{∗}} of EIL_{M}^{ω} (with V(\underline{s^{∗}}) = \{\underline{x^{∗}}\}) such that

EIL_{M}^{ω} ⊢ \underline{x^{∗}} maj \underline{x} → \underline{s^{∗}} maj \underline{s} .  (61)

Proof: The constants O and S trivially majorize themselves by the last clause of Definition 4.11. On the other hand, Σ M = λz, \underline{x}, \underline{x′}. M x x′ majorizes D and Π 1 = λx^{o}, y^{o}. 1 majorizes I, ν and E. Using Remark 4.13 we have that Σ, Π, P and M majorize themselves. The conclusion follows immediately by induction on d(\underline{s}). □

Corollary 4.15 Let s̃, s̃^{∗} be constants associated to terms s, s^{∗} like in Definition 3.10. ¿From (61) it immediately follows that

⊢ \underline{s̃^{∗}} maj \underline{s̃}  (62)

Definition 4.16 We denote by EIL_{M,+}^{ω} the system (EIL_{M}^{ω})_{+} where “+” includes all formulas \underline{s̃^{∗}} maj \underline{s̃} as axioms. We take them as axioms because we consider that the (formal) proof in (62) is not created by monotone functional interpretation. Also let EIL_{M,v}^{ω} be the corresponding (EIL_{M}^{ω})_{v}.

In [26] realizing terms are presented for the monotone functional interpretation of all axioms of EIL_{M}^{ω}+AC+IP_{∀}+MK. They are the same as for the usual functional interpretation, except that

• A → A ∧ A is realized by terms ΣM = λ\underline{a}, \underline{x}, \underline{y′}, \underline{y′′}. M y′ y′′ and Π = λ\underline{a}, \underline{x}. x; compare this with the results of Proposition 3.22;

• A ∨ A → A is realized by ΣM = λ\underline{a}, z, \underline{x}, \underline{x′}. M x x′ and Π;

• A ∨ B → B ∨ A is realized by terms Π and Π 1;

• the schema ED itself is trivially realized by Π 1 = λ\underline{a}. 1; • ∀\underline{z}A(\underline{z}) → A(\underline{s}) is realized by terms obtained from the realizing terms

of the usual functional interpretation by replacing the constants s̃ with the corresponding s̃^{∗} where \underline{s^{∗}} are given by Lemma 4.14.

Using Remark 4.13 it follows that there exists k ∈ IN constant such that the verifying proof for some axiom A of EIL_{M}^{ω}+AC+IP_{∀}+MK has depth upper bounded by k · qs(A). The verifying proof for CT∧ makes use of ED.

Remark 4.17 The proof–size measure S_{m} is introduced in Definition 3.33. The proof–depth measures ∂_{MP}, ∂_{QR} and ∂ are introduced in Section 1.2. In the following theorem we will abbreviate by ∂_{MP} :≡ ∂_{MP}(P), ∂_{QR} :≡ ∂_{QR}(P), ∂:≡ ∂(P) and S_{m} :≡ S_{m}(P).

Since monotone functional interpretation uses the same algorithm as the usual functional interpretation for producing realizing terms for conclusions given the realizing terms for premises, the following analogue of Theorem 3.38 holds.

Theorem 4.18 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of A in EIL_{M,+}^{ω}+AC+IP_{∀}+MK it produces as output \underline{t^{∗}} such that, with the notations 3.24, the following hold:

d(\underline{t}) ≤ k + ∂_{QR} + qs_{0} · ∂_{MP}
S(\underline{t}) ≤ Sz(\underline{t}) ≤ min\{k · S_{m} , k · ∂_{QR} · qs_{0}^{∂_{MP}}\} ≤ k · qs_{0}^{∂}  (63)
mdg(\underline{t}) ≤ k + vdg_{0} + id_{0}
mar(\underline{t}) ≤ k + var_{0} + qs_{0} · id_{0}
EIL_{M,v}^{ω} ⊢_{k·(qs_{0}+∂)} ∃\underline{x} (\underline{t^{∗}} maj \underline{x} ∧ ∀\underline{a}, \underline{y} A_{D}(\underline{x}(\underline{a}), \underline{y}, \underline{a}))  (64)

The time overhead of the algorithm is upper bounded by k · qs_{0} · ls_{0} · S_{m}. The ˜ · constants of EIL_{M,v}^{ω} in (64) are among those corresponding to terms occurring in the leaves of P.

Proof: The rightmost inequality of (63) follows from a suitable adaptation of Remark 3.39 to the monotone case. We now only need to comment on (64). In order to build the verifying proof for MP we need to use the following lemma:

(\underline{y_{1}} maj \underline{x_{1}}) ∧ (\underline{y_{3}} maj \underline{x_{3}}) → ∧ [ Σ(y_{3}, \underline{y_{1}}, \underline{O}) maj Σ(x_{3}, \underline{x_{1}}, \underline{O}) ] (65)

Using Remark 4.13 it follows that there exists k′ ∈ IN such that for all its instances, lemma (65) has a proof of depth at most k′ · |y_{3}, \underline{y_{1}}, \underline{O}|. When used for verifying MP, |y_{3}, \underline{y_{1}}, \underline{O}| ≤ qs_{0} hence (64) follows immediately. □

Remark 4.19 If (65) were taken as axiom, the depth of verifying MP would be upper bounded by a constant, just like in the case of usual functional interpretation. On the other hand (65), Σ maj Σ, Π maj Π, P maj P and M maj M would have constant-depth proofs in EIL_{M}^{ω} if the underlying logical system handled tuples of conjunctions more smoothly. In such a case (64) could be replaced with

EIL_{M,v}^{ω} ⊢_{k·∂} ∃\underline{x} (\underline{t^{∗}} maj \underline{x} ∧ ∀\underline{a}, \underline{y} A_{D}(\underline{x}(\underline{a}), \underline{y}, \underline{a}))

Hence the bound on verifying proof depth would be better than in the usual functional interpretation case, see (43). The smoother treatment of tuples of conjunctions would actually be normal in our context with free use of tuples in both quantifier axioms/rules and the extensionality rule ER_{0}.

Let ECL_{M,+}^{ω} be the classical variant of EIL_{M,+}^{ω}. Combined with N-translation, monotone functional interpretation carries over to ECL_{M,+}^{ω}+AC_{0} and the upper bounds on size and proof depth are smaller than in the functional interpretation case. The following analogue of Theorem 4.8 + Corollary 4.10 holds.

Theorem 4.20 There exists k ∈ IN constant and an algorithm which does the following. Given as input a proof P of A in ECL_{M,+}^{ω}+AC_{0}, it produces as output \underline{t^{∗}} such that, with the notations 3.24 and the abbreviations ∂:≡ ∂(P) and S_{m} :≡ S_{m}(P) the following hold:

d(\underline{t^{∗}}) ≤ k · qs_{0} · ∂
S(\underline{t^{∗}}) ≤ Sz(\underline{t^{∗}}) ≤ k · S_{m} ≤ (k · qs_{0})^{k·∂}
mdg(\underline{t^{∗}}) ≤ vdg_{0} + k · fid_{0}
mar(\underline{t^{∗}}) ≤ var_{0} + k · qs_{0} · fid_{0}
EIL_{M,v}^{ω} ⊢_{k·(qs_{0}+∂)} ∃\underline{x} [ \underline{t^{∗}} maj \underline{x} ∧ ∀\underline{a}, \underline{y} (A^{N})_{D}(\underline{x}(\underline{a}), \underline{y}, \underline{a}) ]  (66)

For A ≡ ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) with A_{0} quantifier-free and \{\underline{x}, \underline{y}\} = V_{f}(A_{0}), (66) can be replaced with

EIL_{M,v}^{ω} ⊢_{k·(ld(A_{0})+qs_{0}+∂)} ∃\underline{Y} [ \underline{t^{∗}} maj \underline{Y} ∧ ∀\underline{x} A_{0}(\underline{x}, \underline{Y} (\underline{x})) ]  (67)

The time overhead of the algorithm is upper bounded by k · qs_{0} · ls_{0} · S_{m}. The ˜ · constants of EIL_{M,v}^{ω} in (66, 67) are among those corresponding to terms occurring in the leaves of P^{N}. □

In concrete applications of monotone functional interpretation, EIL_{M}^{ω} will be extended by certain arithmetical (and even analytical) principles (see Section 5 below).

In the presence of a modest amount of arithmetic we can make use of t^{∗} extracted by monotone functional interpretation in the following way. Let \underline{x}, \underline{y} be of type o. Then (67) implies ∀\underline{x}∃\underline{y} ≤ \underline{t^{∗}}(\underline{x}) A_{0}(\underline{x}, \underline{y}) and therefore, using bounded search applied to \underline{t^{∗}} and a characteristic term t_{A_{0}} for A_{0} one easily constructs \underline{t} such that ∀\underline{x}A_{0}(\underline{x}, \underline{t}(\underline{x})). This also works for \underline{x} of type 1 using the construction x^{M}(i) :≡ max_{j≤i} x(j) since x^{M} maj x. Moreover, for sentences of the form ∀x^{1} ∀z ≤_{1} s ∃y^{o} A_{0}(x, z, y) with s closed term one can easily obtain a type-2-term t̂from t^{∗} such that ⊢ ∀x^{1} ∀z ≤_{1} s ∃y ≤_{o} t̂(x) A_{0}(x, z, y) by taking t̂(x) :≡ t^{∗}(x^{M}, s^{∗}) where s^{∗} is a majorizing term for s. The term t̂ provides a uniform bound on y which is independent from z. See [30] for more details. This feature of monotone functional interpretation is of crucial importance in applications to numerical analysis [31, 32, 26, 28, 35, 38] where {z | z ≤_{1} s} is used to represent compact Polish spaces. Since A_{0}(x, z, y) is monotone (i.e., A_{0}(x, z, y_{1}) ∧ y_{2} ≥ y_{1} → A_{0}(x, z, y_{2})) in most applications, the term t̂will not only be a bound but actually a realizer for ∃y.

Hence in this context monotone functional interpretation even provides a realizer which is independent from z and of simpler structure than realizers produced by the usual functional interpretation (see [26] for more on this).

5 Extensions to Arithmetic and fragments of Analysis

Both Gödel’s functional interpretation and the monotone functional interpretation apply to intuitionistic and, via the negative translation, also classical arithmetic [21, 33, 53] (even in finite types) and fragments thereof [10, 33, 45].

5.1 Treatment of Primitive Recursive Arithmetic PRA^{ω}

Let us first consider Feferman’s system [16] PRA^{ω} (and its intuitionistic variant PRA_{i}^{ω}) of primitive recursive arithmetic in all finite types, where only quantifier-free induction and ordinary Kleene-primitive recursive functionals are included.

Definition 5.1 Let PRA_{i}^{ω} be an extension of EIL^{ω} with the following:

• Kleene recursor^{39} constants R̂_{ρ} with axioms

AxR̂ : \{ \begin{matrix}R̂_{ρ}(0, y, z, \underline{v}) & =_{o} & z(\underline{v}) \\ R̂_{ρ}(Sx, y, z, \underline{v}) & =_{o} & y(R̂_{ρ}(x, y, z, \underline{v}), x, \underline{v}) \end{matrix} .

• Axioms (the usual primitive recursive +, ∗, \overline{sg}, | · | are defined by R̂_{o})

\begin{matrix}x =_{o} y ↔ |x − y| =_{o} 0 \\ x =_{o} 0 ∧ y =_{o} 0 ↔ x + y =_{o} 0 \\ x =_{o} 0 ∨ y =_{o} 0 ↔ x ∗ y =_{o} 0 \\ (x =_{o} 0 → y =_{o} 0) ↔ \overline{sg}(x) ∗ y =_{o} 0 \\ x ≠_{o} 0 ↔ \overline{sg}(x) =_{o} 0 \end{matrix} \}  (68)

• An axiom of quantifier-free-induction (below “y < x” is the usual primitive recursively definable strict order relation on natural numbers)

IA′_{0} : ∀f^{1}, x^{o}(f(0) =_{o} 0 ∧ ∀y < x(f(y) =_{o} 0 → f(Sy) =_{o} 0) → f(x) =_{o} 0) .

The EIL^{ω}-constants ν, I and E are immediately definable in PRA_{i}^{ω} from (68). Also the (here primitive-recursive) closed terms associated to quantifierfree-formulas A_{0} (which here may also contain ∨) like in Proposition 3.21 are immediately provided in PRA_{i}^{ω} with PRA_{i}^{ω} ⊢ t_{A_{0}}(\underline{a}) =_{o} 0 ↔ A_{0}(\underline{a}). Because of this, IA′_{0} implies the following schema of quantifier-free-induction (below A_{0} are quantifier-free-formulas which here may contain ∨):

IA_{0} : A_{0}(0) ∧ ∀x(A_{0}(x) → A_{0}(Sx)) → ∀xA_{0}(x) .

The EIL^{ω}-axiom TND_{0} : x =_{o} 0 ∨ x ≠_{o} 0 can be immediately derived from IA_{0}. The EIL^{ω}-constant D can now easily be defined from R̂ in PRA_{i}^{ω}.

The axioms AxR̂ and (68) are realizer-free except for the implication x · y =_{o} 0 → ( x =_{o} 0 ∨ y =_{o} 0 ) whose functional interpretation is realized by Π = λx, y. x. It follows that functional interpretation is immediately available for PRA_{i}^{ω} once realizing terms are provided for IA′_{0}. Such terms of constant size can be built using Kleene recursors R̂ and are equivalent to

λf, x. min _{y<x} t_{[ f(0)=0 ∧ ( f(y)=0 → f(Sy)=0 ) → f(x)=0 ]}(f, x, y) .

39For all ρ the recursor R̂_{ρ} can be defined from R̂_{o} using λ-abstraction and hence the EIL^{ω} combinators in view of Definition 2.12. This property no longer holds for Gödel recursor R_{ρ} to be introduced in Section 5.3. See also Footnote 10 of [3].

Since ≥ and M are PRA_{i}^{ω}-definable as well, the axioms added to EIL^{ω} in Definition 4.11 become derivable in PRA_{i}^{ω}. It follows that also monotone functional interpretation is available for PRA_{i}^{ω}. In this case IA′_{0} is much simpler realized by projectors Π = λf, x. x (no recursors are needed).

Theorem 5.2 All the quantitative results proved above for EIL^{ω} in Theorem 3.26 and EIL_{M}^{ω} in Theorem 4.18 carry on to PRA_{i}^{ω} in the obvious way. □

5.2 Extension to the analytical system PRA^{ω}+AC_{0}+WKL.

The analogue of Theorem 5.2 for the classical system PRA^{ω}+AC_{0} holds as well. The system PRA^{ω}+AC_{0} allows to derive the schemas of Σ_{1}^{0}-induction and Δ_{1}^{0}-comprehension (see [30]) and therefore contains the system RCA_{0} known from reverse mathematics (see [49]).

Let us denote by WKL the binary König’s lemma. This important^{40} analytical principle simply asserts that every infinite binary tree has an infinite path. The second author has proved in [30] by means of a combination of functional interpretation and majorizability (a precursor of monotone functional interpretation) that PRA^{ω}+AC_{0}+WKL (which contains Friedman’s system^{41} WKL_{0} of [18, 49]) is Π_{2}^{0}-conservative over PRA_{i}^{ω}. Moreover, a witnessing term can be provided. We give below a quantitative version of this result. We follow closely the proof in Section 7 of [3] which is a simplification of the more general method of [30].

Let PRA^{ω} be formulated over ECL_{M}^{ω}. We use the following convenient formulations of the binary König’s lemma:

WKL : ∀f [ ∀k ¬Bnd(BTr(f), k) → ∃b ∀ k (InSeg(Bin(b), k) ∈ BTr(f)) ]
WKL′ : ∀f ∃b ∀ k [ ¬Bnd(BTr(f), k) → InSeg(Bin(b), k) ∈ BTr(f) ]

where (see Section 7 of [3] for full details)

• Bin and BTr are primitive recursive functionals which transform their argument to a binary function, respectively a binary tree; • InSeg is a primitive recursive functional which produces the length k

40See [49] for a comprehensive discussion of the vast mathematical applicability of WKL.

41Theorem I.10.3 of [49] gives a summary of important mathematical statements which are theorems of WKL_{0}. We only mention here the Heine-Borel covering lemma, the maximum principle, the separable Hahn-Banach theorem and Brouwer’s fixed point theorem.

initial segment of the binary function Bin(b);

• Bnd is a primitive recursive predicate which expresses that the given binary tree BTr(f) has depth at most k.

Remark 5.3 Below A_{0} is quantifier-free, \underline{x}, \underline{y} are type o and \{\underline{x}, \underline{y}\} = V_{f}(A_{0}).

The following theorem expresses the fact that the WKL–elimination and term extraction procedure from WKL–based proofs as developed in [30] is feasible both w.r.t. the size of the extracted terms and the depth of the verifying WKL–free proof. Although the feasibility of WKL–elimination was first shown (for a fragment of second-order arithmetic) in [2], the forcing technique used there does not provide any term extraction.

Theorem 5.4 There exists k ∈ IN constant and a functional-interpretation-based algorithm which does the following. Given as input a proof

P : PRA^{ω}+AC_{0} ⊢_{∂} WKL → ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y})

it produces at output realizing terms \underline{t} such that Sz(\underline{t}) ≤ k · S_{c}(P) and

PRA_{i}^{ω} ⊢_{k·(ls_{0}+∂)} ∀\underline{x} A_{0}(\underline{x}, \underline{t}(\underline{x})) .  (69)

The time overhead of the algorithm is upper bounded by k · qs_{0} · ls_{0} · S_{m}(P).

Proof:

The first step is to transform P : PRA^{ω}+AC_{0} ⊢_{∂} WKL → ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) to P^{N} : PRA_{i}^{ω}+AC_{0}+MK ⊢_{k′·(ld(A_{0})+∂)} WKL′ → ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) such that all statements on P^{N} in Proposition 4.4 hold. Here P^{N} is obtained by a slight transformation within PRA_{i}^{ω}+MK of the output from the N-translation algorithm carried on P. There exist fixed proofs (hence with constant complexity) in PRA_{i}^{ω} of WKL′ → WKL and WKL → WKL^{N}. See also Lemmas 7.3.1 and 7.3.3 of [3].

The second step is to transform P^{N} to the proof in (69) via a technique based on functional interpretation and majorization. This technique is described in Lemmas 7.4.1 and 7.4.2 of [3] and is an adaptation of the more general technique of [30]. The elimination of WKL′ is achieved by weakening WKL′ to a formula which is provable in PRA_{i}^{ω}. Since we are here interested also in the realizing term for ∃\underline{y} and not only in the WKL–conservation, we use a (tuple-extended) variant of [3]–Lemma 7.4.1 where a realizer for ∃y is provided as well. □

Corollary 5.5 (quantitative WKL-conservation) There exists an algorithm which transforms proofs

P : PRA^{ω}+AC_{0} ⊢_{∂} WKL → ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y})

into proofs

P′ : PRA_{i}^{ω} ⊢_{k·(ls_{0}+∂)} ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y})

Remark 5.6 We could alternatively use a monotone functional interpretation – version of [3]–Lemma 7.4.1 in the lines of Theorem 4.20. Then we would first obtain a majorizing tuple \underline{t^{∗}} for ∃ \underline{y} and we could produce a realizer by bounded search (up to \underline{t^{∗}}(\underline{x})) along the predicate t_{A_{0}}(\underline{x}, \underline{y}) = 0. In such a case Theorem 5.4 would hold with (69) replaced by

PRA_{i}^{ω} ⊢_{k·(ld(A_{0})+qs_{0}+∂)} ∀\underline{x} A_{0}(\underline{x}, \underline{t}(\underline{x})) .

In many cases A_{0} is monotone in \underline{y} and therefore bounded search is actually not needed^{42}. In such a case we would obtain terms \underline{t} with Sz(\underline{t}) ≤ k · S_{m}(P), time overhead at most k · fid_{0} · qs_{0} · S_{m}(P) and

PRA_{i}^{ω} ⊢_{k·(qs_{0}+∂)} ∀\underline{x} A_{0}(\underline{x}, \underline{t}(\underline{x}))  (70)

hence a full better performance than the algorithm of Theorem 5.4.

Remark 5.7 There are three ways to produce a variant of Theorem 5.4 where the input proof is P : PRA^{ω}+AC_{0}+WKL ⊢_{∂} ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}). One way to overcome the failure of the deduction theorem for weakly extensional PRA^{ω} is via the elimination-of-extensionality procedure from [42]. This applies only when P contains just^{43} variables of type 0 or 1, but in fact this is the case in most applications. We conjecture that the aforementioned procedure is feasible and hence the overall term extraction and WKLconservation is still a feasible process. However if we are mainly interested in the term extraction rather than the WKL-conservation we can state a monotone-functional-interpretation-based variant of Theorem 5.4 with the verifying proof in PRA_{i}^{ω}+{ \atop WKL} and of the same depth as (70), where { \atop WKL}: ∃B ∀f ∀ k [ ¬Bnd(BTr(f), k) → InSeg(Bin(B(f)), k) ∈ BTr(f) ]

42See also the remarks following Theorem 4.20.

43Under this type restriction we can allow the use of (full) extensionality axiom EA, see also Remark 2.6. Hence in this setting we work with (fully) extensional PRA^{ω} which features the deduction theorem.

is a strengthening of WKL′. If we are satisfied with a partial WKL-conservation then we can use the fact that premises of ER_{0} are realizer-free and hence any WKL instance used in the proof of such a ER_{0}-premise gets discarded in the preprocessing phase of the (monotone) functional-interpretation-algorithm. We can thus consider that the input proof is in PRA^{ω}+AC_{0}⊕WKL (see [30], p. 1246 for the meaning of ⊕ in this context). For this system the deduction theorem holds w.r.t. ⊕ and we obtain (69) with PRA_{i}^{ω} extended with the Ntranslations of conclusions of those ER_{0} instances in P whose sub-proof-trees use WKL. See also Remark 3.32.

Remark 5.8 Even though the term extraction procedure of Theorem 5.4 is extremely feasible, the normalization of the extracted terms into ordinary primitive recursive functions and the verification in (plain) primitive recursive arithmetic would however trigger a non-elementary recursive complexity.

5.3 The case of Peano Arithmetic PA^{ω} and PA^{ω}+AC_{0}+WKL

Already Gödel showed that the functional interpretation of full induction can be realized by his impredicative recursors R for (simultaneous^{44}) primitive recursion in finite types, where (below i ∈ \overline{1, |\underline{σ}|} with |\underline{σ}| the length of \underline{σ})

AxR : \{ \begin{matrix}Ri ; \underline{σ}(\underline{x}, \underline{y}, 0) & =_{σ_{i}} & x_{i} \\ Ri ; \underline{σ}(\underline{x}, \underline{y}, Sz) & =_{σ_{i}} & y_{i}(R1 ; \underline{σ}(\underline{x}, \underline{y}, z), …, R|\underline{σ}| ; \underline{σ}(\underline{x}, \underline{y}, z), z) \end{matrix} .

Gödel’s objective was to reduce the consistency of Peano arithmetic PA to that of a quantifier-free calculus (called T) based on these R. In order to achieve this he had to give a verifying proof for the functional interpretation of induction which used only quantifier-free induction. For the applied purpose of program extraction this is not required. We may use full induction in the verifying proof as well. This simplifies matters substantially as was already observed in [53](3.5.5.(iii)). Things are particularly simple if induction is formulated as a rule

IR : \frac{A(0) , A(z) → A(Sz)}{A(z)}

[53].

44Simultaneous primitive recursion even in higher types can be reduced to ordinary primitive recursion in higher types. This is particularly simple in the presence of ER_{0}, see

which nevertheless allows to derive the axiom schema of induction

IA : A(0) ∧ ∀z ( A(z) → A(Sz) ) → ∀zA(z) .

The treatment of IR under functional interpretation is fairly similar to that of modus ponens MP. Recursors R have to be used in addition to Σ. Given that \underline{t_{1}} Dr A(z, \underline{a}) and (\underline{t_{2}}, \underline{t_{3}}) Dr (A(z, \underline{a}) → A(Sz, \underline{a})) one can prove^{45} in a constant number of steps that \underline{t_{4}} Dr ∀zA(z, \underline{a}). Here t_{4} ≡ Σ R \underline{t_{1}} (P t_{3}^{1}) … (P t_{3}^{|\underline{t_{3}}|}) . The monotone functional interpretation of IR is much the same as the usual one if we use recursors R^{∗} which can easily be defined from R by a minor modification (see also [24] for similar R^{+} recursors). Negative translation applies to IR just as it did for MP. Let Peano arithmetic in all finite types PA^{ω} be formulated over ECL^{ω} plus IR and recursors R. The remarks above imply that we can state the following consequence of (Corollary 4.10) of Theorem 4.8.

Theorem 5.9 There exists k ∈ IN constant and a functional-interpretation-based algorithm which does the following. Given as input a proof P : PA^{ω}+AC_{0} ⊢_{∂} ∀\underline{x} ∃\underline{y} A_{0}(\underline{x}, \underline{y}) it produces a realizing tuple \underline{t} such that PA_{i}^{ω} ⊢_{k·(ls_{0}+∂)} ∀\underline{x} A_{0}(\underline{x}, \underline{t}(\underline{x})) and Sz(\underline{t}) ≤ k · S_{c}(P). The time overhead of the algorithm is upper bounded by k · qs_{0} · ls_{0} · S_{m}(P). □

In contrast to IR, the treatment of IA under usual functional interpretation results in complexity issues similar to those of CT∧ in Proposition 3.22. This is hinted by the fact that the derivation of IA from IR apparently needs contraction A → A ∧ A. Let A be the induction formula; in order to realize IA we need bounded search along the predicate t_{A_{D}}(\underline{x}, y) =_{o} 0. Here t_{A_{D}} is a characteristic term for A_{D}, see [45]. The monotone functional interpretation of IA avoids this altogether (like before in the case of A → A ∧ A). Now only a majorizing term for μy ≤ z [ t_{A_{D}}(\underline{x}, y) =_{o} 0 ] needs to be constructed and we can simply use t^{∗}:≡ Π = λ\underline{x}, z. z. Let PA^{ω} be formulated over ECL_{M}^{ω} plus IA and the recursors R. The remarks above imply that we can state the following result.

Theorem 5.10 All the quantitative results of Theorem 5.4 and the subsequent considerations carry on to the corresponding PA^{ω}-based systems in the obvious way. □

45Obviously using IR.

Acknowledgements: The authors are grateful to Paulo Oliva, Philipp Gerhardy and Daniele Varacca for their comments and suggestions on an earlier draft of this work. We also thank Prof. Helmut Schwichtenberg for useful comments.

References

[1] W. Alexi. Extraction and verification of programs by analysis of formal proofs. Theoretical Computer Science, 61:225–258, 1988.

[2] J. Avigad. Formalizing forcing arguments in subsystems of second-order arithmetic. Annals of Pure and Applied Logic, 82:165–191, 1996.

[3] J. Avigad and S. Feferman. Gödel’s functional (‘Dialectica’) interpretation. In [9], pages 337–405.

[4] J. Barwise, editor. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, New York, Oxford, 1977.

[5] S. Bellantoni and H. Schwichtenberg. Feasible computation with higher types. Marktoberdorf 2001 volume.

[6] U. Berger, W. Buchholz, and H. Schwichtenberg. Refined program extraction from classical proofs. Annals of Pure and Applied Logic, 114:3– 25, 2002.

[7] J. Blanck and al., editors. Proceedings Fourth Workshop on Computability and Complexity in Analysis (CCA 2000), volume 2064 of Springer LNCS. Springer, 2001.

[8] W. Burr. Functional interpretation of Aczel’s constructive set theory. Ann. Pure Applied Logic, 104:31–75, 2000.

[9] S.R. Buss, editor. Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1998.

[10] S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arithmetic. Ann. Pure Applied Logic, 63:103–200, 1993.

[11] T. Coquand and M. Hofmann. A new method for establishing conservativity of classical systems over their intuitionistic version. Math. Structures Comput. Sci., 9(4):323–333, 1999.

[12] J.C.E. Dekker, editor. Recursive function theory, Symposia in Pure Mathematics, volume 5, 1962.

[13] J. Diller and W. Nahm. Eine Variante zur Dialectica Interpretation der Heyting Arithmetik endlicher Typen. Archive für Mathematische Logik und Grundlagenforschung, 16:49–66, 1974.

[14] A.G. Dragalin. New kinds of realisability and the Markov rule. Dokl. Akad. Nauk. SSSR, 251:534–537, 1980. Russian, English Translation [15].

[15] A.G. Dragalin. New kinds of realisability and the Markov rule. Soviet Math. Dokl., 21:461–464, 1980.

[16] S. Feferman. Theories of finite type related to mathematical practice. In [4], pages 913–972.

[17] H. Friedman. Classical and intuitionistically provably recursive functions. In [43], pages 21–27.

[18] H. Friedman. Systems of second order arithmetic with restricted induction, I, II (abstracts). Journal of Symbolic Logic, 41:557–559, 1976.

[19] J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérior. PhD thesis, Université de Paris VII, 1972.

[20] K. Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, 4:34–38, 1933.

[21] K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280–287, 1958.

[22] S. Hayashi and H. Nakano. PX: A Computational Logic. MIT Press, 1988.

[23] W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors. Logic: from Foundations to Applications. European Logic Colloquium, Keele, 1993. Oxford University Press, 1996.

[24] W.A. Howard. Hereditarily majorizable functionals of finite type. In [53], pages 454–461.

[25] K.F. Joergensen. Finite type arithmetic. Master’s thesis, University of Roskilde, Departments of Mathematics and Philosophy, 2001.

[26] U. Kohlenbach. Analysing proofs in analysis. In [23], pages 225–260.

[27] U. Kohlenbach. Lecture Course: Proof Interpretations and the Computational Content of Proofs. Updated version at http://www.brics.dk/ kohlenb.

[28] U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In [7], pages 119–145.

[29] U. Kohlenbach. Uniform asymptotic regularity for Mann iterates. To appear in J. Math. Anal. Appl.

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

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

[32] U. Kohlenbach. 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:581–606, 1993.

[33] U. Kohlenbach. Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Arch. Math. Logic, 36:31–71, 1996.

[34] U. Kohlenbach. On the no-counterexample interpretation. Journal of Symbolic Logic, 64:1491–1511, 1999.

[35] U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numer. Funct. Anal. and Optimiz., 22:641–656, 2001.

[36] U. Kohlenbach and L. Leuştean. Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. To appear in Abstr. Appl. Anal.

[37] U. Kohlenbach and P. Oliva. Proof mining: a systematic way of analysing proofs in Mathematics. To appear in Proc. Steklov Inst. Math.

[38] U. Kohlenbach and P. Oliva. Proof mining in L_{1}-approximation. To appear in Ann. Pure Appl. Logic.

[39] G. Kreisel. On the interpretation of non-finitist proofs, part I. Journal of Symbolic Logic, 16:241–267, 1951.

[40] G. Kreisel. On the interpretation of non-finitist proofs, part II: Interpretation of number theory. Journal of Symbolic Logic, 17:43–58, 1952.

[41] G. Kreisel. On weak completeness of intuitionistic predicate logic. J. Symbolic Logic, 27:139–158, 1962.

[42] H. Luckhardt. Extensional Gödel Functional Interpretation. Springer LNM, 306, 1973.

[43] G.H. Müller and D.S. Scott, editors. Higher Set Theory, volume 669 of Lecture Notes in Mathematics. Springer, 1978.

[44] C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990.

[45] C. Parsons. On n-quantifier induction. J. Symbolic Logic, 37:466–482, 1972.

[46] P. Rath. Eine verallgemeinerte Funktionalinterpretation der Heyting Arithmetik endlicher Typen. PhD thesis, Universität Münster, 1978.

[47] M. Schönfinkel. Über die Bausteine der mathematischen Logik. Math. Annalen, 92:305–316, 1924.

[48] H. Schwichtenberg. An arithmetic for polynomial-time computation. Submitted. Available at http://www.mathematik.uni-muenchen.de/ schwicht.

[49] S.G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999.

[50] C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In [12], pages 1–27.

[51] M. Stein. Interpretation der Heyting-Arithmetik endlicher Typen. PhD thesis, Universität Münster, 1976.

[52] A.S. Troelstra. Realisability. In [9], pages 407–473.

[53] A.S. Troelstra, editor. Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, Berlin - Heidelberg - New York, 1973.

A Appendix

Below we complete the proof of Proposition 3.20. We first recall its statement.

Proposition A.1 There exists k ∈ IN constant such that for any instance A of CT∨, WK∨, WK∧, PM∨, PM∧, SYL, EPN, EFQ, TND_{0}, MK, IP_{∀}, AC, there exists a realizing tuple for A^{D} such that

d(\underline{t}) ≤ k  (71)
S(\underline{t}) ≤ k  (72)
mdg(\underline{t}) ≤ k + vdg(A) + id(A)  (73)
mar(\underline{t}) ≤ k + var(A) + qs(A) (id(A) − k_{0} + 2)  (74)
⊢_{k} \{] \underline{t} , A [\}  (75)

Proof: Only SYL was treated in the proof of Proposition 3.20. Below we treat the remaining axioms, where \{\underline{a}\} ≡ V_{f}(the corresp. axiom instance).

CT∨ : By definition,

\begin{matrix}(A ∨ A → A)^{D} ≡ ∃\underline{Y} , \underline{Y′}, \underline{X′′} ∀z, \underline{x}, \underline{x′}, \underline{y′′} \\ ( & \begin{aligned}( & \begin{matrix}z = 0 → A_{D}(\underline{x}; \underline{Y} (z, \underline{x}, \underline{x′}, \underline{y′′})) \\ ∧ \\ z ≠ 0 → A_{D}(\underline{x′}; \underline{Y′}(z, \underline{x}, \underline{x′}, \underline{y′′})) \end{matrix} & ) \\ & ⟶ \\ & A_{D}(\underline{X′′}(z, \underline{x}, \underline{x′}); \underline{y′′}) \end{aligned} & ) \end{matrix}

and we can take \{ \begin{matrix}t_{Y} & :≡ & t_{Y′}:≡ Π = λ\underline{a}, z, \underline{x}, \underline{x′}, \underline{y′′}. y′′ \\ t_{X′′} & :≡ & Π D = λ\underline{a}. D \end{matrix}

WK∨ : By definition,

\begin{matrix}(A → A ∨ B)^{D} ≡ ∃\underline{Y} , Z, \underline{X′}, \underline{U} ∀\underline{x}, \underline{y′}, \underline{v} \\ ( & \begin{aligned}& A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{y′}, \underline{v})) \\ & ⟶ \\ ( & \begin{matrix}Z(\underline{x}) = 0 → A_{D}(\underline{X′}(\underline{x}); \underline{y′}) \\ ∧ \\ Z(\underline{x}) ≠ 0 → B_{D}(\underline{U}(\underline{x}); \underline{v}) \end{matrix} & ) \end{aligned} & ) \end{matrix}

and we can take \{ \begin{matrix}t_{Y} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y′}, \underline{v}. y′ \\ t_{Z} & :≡ & O = λ\underline{a}, \underline{x}. 0 \\ t_{X′} & :≡ & Π = λ\underline{a}, \underline{x}. x \\ t_{U} & :≡ & O \end{matrix}

WK∧ : By definition,

\begin{aligned}& (A ∧ B → A)^{D} ≡ ∃\underline{Y} , \underline{V} , \underline{X′} ∀\underline{x}, \underline{u}, \underline{y′} \\ ( & \begin{matrix}A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{u}, \underline{y′})) ∧ B_{D}(\underline{u}; \underline{V} (\underline{x}, \underline{u}, \underline{y′})) \\ ⟶ \\ A_{D}(\underline{X′}(\underline{x}, \underline{u}); \underline{y′}) \end{matrix} & ) \end{aligned}

and we can take \{ \begin{matrix}t_{Y} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}, \underline{y′}. y′ \\ t_{V} & :≡ & O \\ t_{X′} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}. x \end{matrix}

PM∨ : By definition,

\begin{matrix}(A ∨ B → B ∨ A)^{D} ≡ ∃\underline{Y} , \underline{V} , Z′, \underline{U′}, \underline{X′} ∀z, \underline{x}, \underline{u}, \underline{v′}, \underline{y′} \\ ( & \begin{aligned}( & \begin{matrix}z = 0 → A_{D}(\underline{x}; \underline{Y} (z, \underline{x}, \underline{u}, \underline{v′}, \underline{y′})) \\ ∧ \\ z ≠ 0 → B_{D}(\underline{u}; \underline{V} (z, \underline{x}, \underline{u}, \underline{v′}, \underline{y′})) \end{matrix} & ) \\ & ⟶ \\ ( & \begin{matrix}\underline{Z′}(z, \underline{x}, \underline{u}) = 0 → B_{D}(\underline{U′}(z, \underline{x}, \underline{u}); \underline{v′}) \\ ∧ \\ \underline{Z′}(z, \underline{x}, \underline{u}) ≠ 0 → A_{D}(\underline{X′}(z, \underline{x}, \underline{u}); \underline{y′}) \end{matrix} & ) \end{aligned} & ) \end{matrix}

and we can take \{ \begin{matrix}t_{Y} & :≡ & Π = λ\underline{a}, z, \underline{x}, \underline{u}, \underline{v′}, \underline{y′}. y′ \\ t_{V} & :≡ & Π = λ\underline{a}, z, \underline{x}, \underline{u}, \underline{v′}, \underline{y′}. v′ \\ t_{Z′} & :≡ & Σ (Σ (Π I) Π) (Π 1) = λ\underline{a}, z, \underline{x}, \underline{u}. (I z 1) \\ t_{U′} & :≡ & Π = λ\underline{a}, z, \underline{x}, \underline{u}. u \\ t_{X′} & :≡ & Π = λ\underline{a}, z, \underline{x}, \underline{u}. x \end{matrix}

PM∧ : By definition,

\begin{matrix}(A ∧ B → B ∧ A)^{D} ≡ ∃\underline{Y} , \underline{V} , \underline{U′}, \underline{X′} ∀\underline{x}, \underline{u}, \underline{y′}, \underline{v′} \\ ( & \begin{matrix}A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{u}, \underline{y′}, \underline{v′})) ∧ B_{D}(\underline{u}; \underline{V} (\underline{x}, \underline{u}, \underline{y′}, \underline{v′})) \\ → \\ B_{D}(\underline{U′}(\underline{x}, \underline{u}); \underline{v′}) ∧ A_{D}(\underline{X′}(\underline{x}, \underline{u}); \underline{y′}) \end{matrix} & ) \end{matrix}

and we can take \{ \begin{matrix}t_{Y} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}, \underline{y′}, \underline{v′}. y′ \\ t_{V} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}, \underline{y′}, \underline{v′}. v′ \\ t_{U′} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}. u \\ t_{X′} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{u}. x \end{matrix}

EFQ : By definition,

(1 = 0 → A)^{D} ≡ ∃\underline{x} ∀\underline{y} (1 = 0 → A_{D}(\underline{x}; \underline{y}))

and we can take t_{x}:≡ O. □ EPN : By definition,

(A → B)^{D} ≡ ∃\underline{Y} , \underline{U} ∀\underline{x}, \underline{v} (A_{D}(\underline{x}; \underline{Y} (\underline{x}, \underline{v})) → B_{D}(\underline{U}(\underline{x}); \underline{v}))
(C ∨ A)^{D} ≡ ∃z, \underline{g}, \underline{x} ∀\underline{h}, \underline{y} ((z = 0 → C_{D}(\underline{g}; \underline{h})) ∧ (z ≠ 0 → A_{D}(\underline{x}; \underline{y})))
(C ∨ B)^{D} ≡ ∃z′, \underline{g′}, \underline{u} ∀\underline{h′}, \underline{v} ((z′ = 0 → C_{D}(\underline{g′}; \underline{h′})) ∧ (z′ ≠ 0 → B_{D}(\underline{u}; \underline{v})))

hence

\begin{matrix}(C ∨ A → C ∨ B)^{D} ≡ ∃\underline{H}, \underline{Y} , Z′, \underline{G′}, \underline{U′} ∀z, \underline{g}, \underline{x}, \underline{h′}, \underline{v} \\ ( & \begin{aligned}( & \begin{matrix}z = 0 → C_{D}(\underline{g}; \underline{H}(z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})) \\ ∧ \\ z ≠ 0 → A_{D}(\underline{x}; \underline{Y} (z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})) \end{matrix} & ) \\ & ⟶ \\ ( & \begin{matrix}Z′(z, \underline{g}, \underline{x}) = 0 → C_{D}(\underline{G′}(z, \underline{g}, \underline{x}); h′) \\ ∧ \\ Z′(z, \underline{g}, \underline{x}) ≠ 0 → B_{D}(\underline{U′}(z, \underline{g}, \underline{x}); \underline{v}) \end{matrix} & ) \end{aligned} & ) \end{matrix}

and further

\begin{matrix}((A → B) → (C ∨ A → C ∨ B))^{D} ≡ ∃\underline{X}, \underline{V} , \underline{H}, \underline{Y} , Z′, \underline{G′}, \underline{U′} ∀\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v} \\ ( & \begin{aligned}( & \begin{matrix}A_{D}(\underline{X}(\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}); \underline{y}(\underline{X}(\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}), \underline{V} (\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}))) \\ → \\ B_{D}(\underline{u}(\underline{X}(\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})); \underline{V} (\underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})) \end{matrix} & ) \\ & ⟶ \\ ( & \begin{matrix}z = 0 → C_{D}(\underline{g}; \underline{H}(\underline{y}, \underline{u})(z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})) \\ ∧ \\ z ≠ 0 → A_{D}(\underline{x}; \underline{Y} (\underline{y}, \underline{u})(z, \underline{g}, \underline{x}, \underline{h′}, \underline{v})) \end{matrix} & ) \\ & ⟶ \\ ( & \begin{matrix}Z′(\underline{y}, \underline{u})(z, \underline{g}, \underline{x}) = 0 → C_{D}(\underline{G′}(\underline{y}, \underline{u})(z, \underline{g}, \underline{x}); \underline{h′}) \\ ∧ \\ Z′(\underline{y}, \underline{u})(z, \underline{g}, \underline{x}) ≠ 0 → B_{D}(\underline{U′}(\underline{y}, \underline{u})(z, \underline{g}, \underline{x}); \underline{v}) \end{matrix} & ) \end{aligned} & ) \end{matrix}

and we can take \{ \begin{matrix}t_{X} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}. x \\ t_{V} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}. v \\ t_{H} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}. h′ \\ t_{Z′} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}. z \\ t_{Y} & :≡ & P Σ = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}. y(\underline{x}) \\ t_{G′} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}, \underline{x}, \underline{h′}, \underline{v}. g \\ t_{U′} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, z, \underline{g}. u \end{matrix}

TND_{0} : By definition,

[ x = 0 ∨ ¬(x = 0) ]^{D} ≡ ∃z [ (z = 0 → x = 0) ∧ (Iz1 = 0 → ¬(x = 0)) ] and we can take t_{z}:≡ λx. x. The remaining axioms are of shape A → B such that A^{D} ≡ B^{D} and therefore are immediately seen to be realized with projectors Π. For the reader’s convenience we nevertheless give below the full details. MK: We have [ ¬¬ ∃\underline{x} A_{0}(\underline{x}) ]^{D} ≡ ∃\underline{x} ¬¬ A_{0}(\underline{x}) hence

[ ¬¬ ∃\underline{x} A_{0}(\underline{x}) → ∃\underline{x} ¬¬ A_{0}(\underline{x}) ]^{D} ≡ ∃\underline{X} ∀\underline{x} [ ¬¬ A_{0}(\underline{x}) → ¬¬ A_{0}(\underline{X}(\underline{x})) ] and we can take t_{X} :≡ Π = λ\underline{a}, \underline{x}. x. IP_{∀}: We have

\begin{aligned}[ ∀\underline{x} A_{0}(\underline{x}) → ∃\underline{y} B(\underline{y}) ]^{D} & ≡ & ∃\underline{X}, \underline{y}, \underline{u} ∀\underline{v} [ A_{0}(\underline{X}(\underline{v})) → B_{D}(\underline{u}; \underline{v}; \underline{y}) ] \\ ( ∃\underline{y} [ ∀\underline{x} A_{0}(\underline{x}) → B(\underline{y}) ] )^{D} & ≡ & ∃\underline{y}, \underline{X}, \underline{u} ∀\underline{v} [ A_{0}(\underline{X}(\underline{v})) → B_{D}(\underline{u}; \underline{v}; \underline{y}) ] \end{aligned}

hence ( [ ∀\underline{x} A_{0}(\underline{x}) → ∃\underline{y} B(\underline{y}) ] → ∃\underline{y} [ ∀\underline{x} A_{0}(\underline{x}) → B(\underline{y}) ] )^{D} is

\begin{aligned}& ∃V, Y, X, U ∀x, y, u, v \\ ( & \begin{matrix}A_{0}(x(V (x, y, u, v))) → B_{D}(\underline{u}; V (x, y, u, v); y) \\ ⟶ \\ A_{0}(X(x, y, u, v)) → B_{D}(U(x, y, u); v; Y (x, y, u)) \end{matrix} & ) \end{aligned}

and we can take \{ \begin{matrix}t_{V} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y}, \underline{u}, \underline{v}. v \\ t_{Y} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y}, \underline{u}. y \\ t_{X} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y}, \underline{u}. x \\ t_{U} & :≡ & Π = λ\underline{a}, \underline{x}, \underline{y}, \underline{u}. u \end{matrix}

AC: We have [ ∀x ∃y B(\underline{x}, \underline{y}) ]^{D} ≡ ∃Y, \underline{U} ∀x, v B_{D}(\underline{U}(x); v; x, Y (x)) ≡ [ ∃Y ∀x B(x, Y (x)) ]^{D} hence [ ∀\underline{x} ∃\underline{y} B(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x} B(\underline{x}, \underline{Y} (\underline{x})) ]^{D} is

\begin{aligned}& ∃X, V, Y, U ∀y, u, x, v \\ ( & \begin{matrix}B_{D}(u(X(y, u, x, v)); V (y, u, x, v); X(y, u, x, v), y(X(y, u, x, v))) \\ ⟶ \\ B_{D}(U(y, u, x); v; x, Y (y, u, x)) \end{matrix} & ) \end{aligned}

and we can take \{ \begin{matrix}t_{X} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, \underline{x}, \underline{v}. x \\ t_{V} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}, \underline{x}, \underline{v}. v \\ t_{Y} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}. y \\ t_{U} & :≡ & Π = λ\underline{a}, \underline{y}, \underline{u}. u \end{matrix}

Recent BRICS Report Series Publications

RS-03-12 Mircea-Dan Hernest and Ulrich Kohlenbach. A Complexity Analysis of Functional Interpretations. February 2003. 70 pp.

RS-03-11 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. February 2003. 14 pp.

RS-03-10 Federico Crazzolara and Giuseppe Milicia. Wireless Authentication in χ-Spaces. February 2003. 20 pp.

RS-03-9 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average and Worst Case Error Estimates. February 2003.

RS-03-8 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. Efficient Algorithms for gcd and Cubic Residuosity in the Ring of Eisenstein Integers. February 2003.

RS-03-7 Claus Brabrand, Michael I. Schwartzbach, and Mads Vanggaard. The METAFRONT System: Extensible Parsing and Transformation. February 2003. 24 pp.

RS-03-6 Giuseppe Milicia and Vladimiro Sassone. Jeeg: Temporal Constraints for the Synchronization of Concurrent Objects. February 2003. 41 pp. Short version appears in Fox and Getov, editors, Joint ACM-ISCOPE Conference on Java Grande, JGI ’02 Proceedings, 2002, pages 212–221.

RS-03-5 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise Analysis of String Expressions. February 2003. 15 pp.

RS-03-4 Marco Carbone and Mogens Nielsen. Towards a Formal Model for Trust. January 2003.

RS-03-3 Claude Crépeau, Paul Dumais, Dominic Mayers, and Louis Salvail. On the Computational Collapse of Quantum Information. January 2003. 31 pp.

RS-03-2 Olivier Danvy and Pablo E. Martínez López. Tagging, Encoding, and Jones Optimality. January 2003. To appear in Degano, editor, Programming Languages and Systems: Twelfth European Symposium on Programming, ESOP ’03 Proceedings, LNCS, 2003.