BRICS LS-98-1 U. Kohlenbach: Proof Interpretations BRICS

Basic Research in Computer Science

Proof Interpretations

Ulrich Kohlenbach BRICS Lecture Series LS-98-1 ISSN 1395-2048 June 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, 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 Lecture 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 LS/98/1/

Proof Interpretations

Ulrich Kohlenbach

Ulrich Kohlenbach

kohlenb@brics.dk

BRICS^{1}

Department of Computer Science

University of Aarhus

Ny Munkegade DK-8000 Aarhus C, Denmark

June 1998

1Basic Research In Computer Science, Centre of the Danish National Research Foundation.

Preface

These lecture notes are a polished version of notes from a BRICS PhD course which I gave in the spring term 1998.

Their purpose is to give an introduction to two major proof theoretic techniques: functional interpretation and (modified) realizability. We focus on the possible use of these methods to extract programs, bounds and other effective data from given proofs.

Both methods are developed in the framework of intuitionistic arithmetic in higher types.

We also discuss applications to systems based on classical logic. We show that the combination of functional interpretation with the so-called negative translation, which allows to embed various classical theories into their intuitionistic counterparts, can be used to unwind non-constructive proofs.

Instead of combining functional interpretation with negative translation one can also use in some circumstances a combination of modified realizability with negative translation if one inserts the so-called A-translation (due to H. Friedman) as an intermediate step.

Acknowledment: I am grateful to the participants of my BRICS PhD course for helpful and clarifying comments. vi

Contents

Preface v 1 Introduction: Unwinding proofs 1 2 Intuitionistic logic and arithmetic in all finite types 17 3 Modified realizability 25 4 Majorizability and the fan rule 33 5 Gödel’s functional (‘Dialectica-’)interpretation 38 6 Negative translation and its use combined with functional

interpretation 50 7 The Friedman A-translation 59 8 Final comments 62

Bibliography 64 viii

Chapter 1

Introduction: Unwinding proofs

Proof interpretations of the kind we are going to study in these lectures are tools to extract constructive (computational) data from given proofs by recursion on the proof. Such data quite often cannot directly be read off from a proof but are hidden behind the use of quantifiers. G. Kreisel was the first to formulate the program of unwinding proofs under the general question:

‘What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?’

What do we mean by ‘constructive data’? E.g.

1) Realizing terms from a proof of an existential theorem A ≡ ∃x B(x) (closed).

A weaker requirement is to construct a list of terms t_{1}, …, t_{n} which are candidates for A, i.e. such that B(t_{1}) ∨ … ∨ B(t_{n}) holds.

More general: If A ≡ ∀x∃y B(x, y), then one can ask for an algorithm p such that ∀x B(x, p(x)) holds (or – weaker– for a bounding function b such that ∀x∃y ≤ b(x) B(x, y), if e.g. y ranges over the natural numbers).

Chapter 1. Unwinding Proofs

2) weakening of the assumptions used in the proof: e.g. replacing general assumptions by specific instances of them.

What type of information one can expect (in general) depends of course on the structure of the theorem A to be proved and the principles used in its proof. A first VERY ROUGH division of the structure of a sentence^{1} A can be made according to the quantifier complexity of A:

1) A purely universal, i.e. A ≡ ∀xA_{0}(x), where A_{0} is quantifier-free.^{2} Such sentences A, sometimes called complete, don’t ask for any witnessing data. So the problem of extracting data is empty here.

2) A purely existential, i.e. A ≡ ∃x A_{0}(x). We treat this as a special case of

3) A ≡ ∀x∃y A_{0}(x, y). Lets consider the case where x, y ∈ IN and A_{0} ∈ L(PA) (here PA denotes first-order Peano arithmetic which we assume to contain all primitive recursive functions). A_{0} is decidable (Exercise: A_{0}(\underline{x}) ∈ L(PA), then one can construct a primitive recursive function term t such that PA ⊢ ∀\underline{x}(t\underline{x} = 0 ↔ A_{0}(\underline{x}))) and therefore defines a partial recursive function f, namely

f(x) := \{ \begin{matrix}min y[A_{0}(x, y)], if ∃y A_{0}(x, y) \\ undefined, otherwise. \end{matrix}

A just says that f is total recursive.

Questions: How to extract a non-trivial program for f (different from simple unbounded search) from a proof of A? What is the complexity and the rate of growth of f if A is proved in a certain theory T ?

Theorems expressing that a set {y ∈ IN : A(y)} ⊆ IN is infinite have the form ∀x ∈ IN∃y ≥ x A(y). Quite often A can be expressed in a quantifier-free way A_{0} in PA, so that this falls under the general form ∀x∃y B_{0}(x, y), where B_{0}(x, y) :≡ (y ≥ x ∧ A_{0}(y)).

1As usual a sentence is a closed formula.

2From now on A_{0}, B_{0}, C_{0}, … always denote quantifier-free formulas. Instead of a single variable we may have (here and in the following) also a tuple \underline{x} = x_{1}, …, x_{n} of variables.

As an example consider the following Proposition 1.1 There are infinitely many prime numbers. The predicate P (x) :≡ ‘x is a prime number’ can be expressed in a quantifierfree way as a primitive recursive predicate (see e.g. [27],[68]).

Proof 1 (Euclid): Define a := 1 + ∏_{{p≤x \atop p prime}} p. a cannot be divided by any

prime number p ≤ x. By the decomposition of every number into prime factors it follows that a contains a prime factor q ≤ a with q > x. □

¿From this proof one immediately gets the bound g(x) := 1 + x! (≥ 1 + ∏_{{p≤x \atop p prime}} p). By the Stirling formula we obtain

g(x) ∼ 1 + (2πx)^{\frac{1}{2}} (\frac{x}{e})^{x} = 1 + \sqrt{2π} · e^{x log x−x+ \frac{1}{2} log x} and hence g(x) ≤ e^{x log x} for sufficiently large x.

Proof 2 (Euler): Suppose that there are only finitely many prime numbers p_{0}, …, p_{r} (listed in increasing order). One has

∑_{0≤α_{0},...,α_{r}≤n} \frac{1}{p_{0}^{α_{0}}·...·p_{r}^{αr}} = ( ∑_{i=0}^{n} \frac{1}{p_{0}^{i}} ) · . . . · ( ∑_{i=0}^{n} \frac{1}{p_{r}^{i}} )

< _{\frac{1}{1− \frac{1}{p_{0}}}} · . . . · _{\frac{1}{1− \frac{1}{pr}}} = \frac{p_{0}}{p_{0}−1} · . . . · \frac{p_{r}}{p_{r}−1}

≤ \frac{2}{1} · \frac{3}{2} · \frac{4}{3} · . . . · \frac{p_{r}}{p_{r}−1} = p_{r}

(note that this holds for all n ∈ IN). It follows (using the decomposition into prime numbers) that for all n ∈ IN

∑_{i=1}^{n} \frac{1}{i} ≤ p_{r}.

But this contradicts the fact that ∑_{i=1}^{∞} \frac{1}{i} = ∞. □

Quantitative analysis of Euler’s proof:

We need a quantitative version of ‘ ∑_{i=1}^{n} \frac{1}{i} →^{n→∞} ∞’, more precisely we need a

bound on ∃n( ∑_{i=1}^{n} \frac{1}{i} > p_{r}). It is known that ∑_{i=1}^{n} \frac{1}{i} − ln(n) ↘ C, where C ≈

0.5772... is the so-called Euler-Mascheroni constant. Hence for n_{r} := ⌈e^{p_{r}−C}⌉

we have ∑_{i=1}^{n_{r}} \frac{1}{i} > p_{r} (and this is essentially optimal). From the proof above it

follows that for all n ∈ IN

∑_{0≤α_{0},...,α_{r}≤n} \frac{1}{p_{0}^{α_{0}} · . . . · p_{r}^{α_{r}}} ≤ p_{r}.

Hence there must be an i (1 ≤ i ≤ n_{r}) which contains a prime factor p with p_{r} < p ≤ i ≤ n_{r}. So put together

∃p(p prime ∧ p_{r} < p ≤ ⌈e^{p_{r}−C}⌉).

Applying this argument to all prime numbers p_{0} < … < p_{r_{x}} ≤ x we obtain

∀x∃p(p prime ∧ x < p ≤ ⌈e^{x−C}⌉).

So we can take g(x) := ⌈e^{x−C}⌉ (or an appropriate upper bound of this to make it computable).

Conclusion: Euler slightly better than Euclid!

Proof 3: Let p_{1}, …, p_{j} be the first j primes and define N(x) := {n ≤ x : n is not divisible by any prime p > p_{j} } . We can express n ∈ N(x) in the form n = n_{1}^{2}m where m is ‘squarefree’, i.e. is not divisible by a square of any prime. We have m = p_{1}^{b_{1}} · p_{2}^{b_{2}} · . . . · p_{j}^{b_{j}}, where b_{i} ∈ {0, 1} . There are 2^{j} possible exponents and consequently at most 2^{j} different values of m. Also, because of n_{1} ≤ \sqrt{n} ≤ \sqrt{x}, there are not more than \sqrt{x} different values of n_{1}. Hence |N(x)| ≤ 2^{j}\sqrt{x}. Now if there were only finitely many primes p_{1}, …, p_{j}, then |N(x)| = x for every x and so 2^{j}\sqrt{x} ≥ x for all x which is a contradiction.

¿From this proof one gets a bound as follows: Let p_{1}, …, p_{j} be the first j primes. Define x := (2^{j})^{2} + 1 = 2^{2j} + 1. Then 2^{j}\sqrt{x} < x. Hence ∃n ≤ x(n is divisible by some prime p > p_{j}) and so ∃p(p prime ∧ p_{j} < p ≤ 2^{2j} + 1). So we get a bound g(j) := 2^{2j} + 1 which is exponential in j (and no longer in x ≥ p_{j}) which (for large enough j) is a significant improvement (e.g. from this bound one easily gets the lower bound \frac{log x}{2 log 2} (for x ≥ 1) for the Euler π-function π(x) := | {p : p prime ∧ p ≤ x} | whereas the bound from Euclid’s proof only yields log log x (for x ≥ 2) as a lower bound, see [23] for details).

For still another proof (in fact a variant of proof 3) see the exercise 1.

Discussion:

1) All three proofs provide more information than the mere fact that ‘there are infinitely many primes’ is true. By making their quantitative content explicit one can compare them with respect to their numerical quality.

2) The unwindings of the proofs 1)-3) were straightforward and didn’t require any tools from logic as guiding principles. However there are more complicated proofs where the use of proof-theoretic tools turned out to be decisive in practice(see e.g. [14],[53],[31],[32]). The final verification of the data extracted will always be again an ordinary mathematical proof (obtained by a proof-theoretic transformation of the original proof) which does not rely on any logical meta-theorems (in contrast to the verification of the general procedure of transformation). This differs from many model theoretic applications to mathematics where the provability or the truth in some model of the conclusion is established without exhibiting a proof which doesn’t rely on model theoretic theorems.

3) Already the a-priori information, provided by a general meta-theorem, that e.g. a certain computable bound must be extractable from a given proof which is formalizable in a certain system T can be an important step in actually finding such a bound even if the latter is carried out by ad hoc methods and doesn’t follow closely any proof-theoretic procedure.

Remark 1.2 If A does not have the form ∀x∃y A_{0}(x, y) right away it may have so after some logical transformations, e.g.

A :≡ (∃x∀y A_{0}(x, y) → ∀u∃v B_{0}(u, v))

is logically equivalent to the prenex normal form

A^{pr} :≡ ∀u, x∃v, y(A_{0}(x, y) → B_{0}(u, v))

so that the reasoning above applies to the A^{pr}.

4) A ≡ ∃x∀y A_{0}(x, y): From a proof of A (even in PL) one cannot (in general) obtain a realization ∀y A_{0}(t, y) nor a list of candidates such that

⋁_{i=1}^{n} ∀y A_{0}(t_{i}, y) (t, t_{1}, …, t_{n} not containing y) holds:

Proposition 1.3 There exists a Σ_{2}^{0}-sentence A ≡ ∃x∀y A_{0}(x, y) ∈ L(PA) in the language of Peano arithmetic PA such that there is no list of closed terms t_{1}, …, t_{k} ∈ L(PA) such that

PA ⊢ ⋁_{i=1}^{k} ∀y A_{0}(t_{i}, y).

Proof: Take P x :≡ P rov_{P A}(x, \overline{0} = \overline{1}) and A_{0}(x, y) :≡ P x ∨ ¬P y (here ‘P rov_{P A}(x, \overline{0} = \overline{1})’ expresses primitive recursively ‘x is the Gödel number of a PA-proof of 0 = 1’ (see e.g. [27]). Suppose there are closed terms t_{1}, …, t_{k} such that

(1) PA ⊢ ⋁_{i=1}^{k} ∀y A_{0}(t_{i}, y).

Within PA each t_{i} can be computed to a numeral \overline{n}_{i}:

(2) PA ⊢ t_{i} = \overline{n}_{i} for 1 ≤ i ≤ k.

By (1) and (2) we have

(3) PA ⊢ ⋁_{i=1}^{k} ∀y A_{0}(\overline{n}_{i}, y).

By the consistency of PA we know that

(4) IN ⊧ ⋀_{i=1}^{k} ¬P \overline{n}_{i}.

Hence by the numeralwise representability of primitive recursive predicates in PA we have

(5) PA ⊢ ⋀_{i=1}^{k} ¬P \overline{n}_{i}.

But (3) and (5) imply

(6) PA ⊢ ∀y¬P rov_{P A}(y, \overline{0} = \overline{1}),

which contradicts Gödel’s second incompleteness theorem. □

However, although PA is not able to verify ⋁_{i=1}^{k} ∀y A_{0}(t_{i}, y) for some terms t_{i}

we can (assuming the consistency of PA). In fact for any term t, e.g. for 0, we know that A_{0}(t) is true in IN simply because IN ⊧ ∀y¬P rov_{P A}(y, \overline{0} = \overline{1}).

But there are other examples where –in general– even this is not possible, e.g. take

A_{e} :≡ ∃x∀y(T (\overline{e}, \overline{e}, x) ∨ ¬T (\overline{e}, \overline{e}, y)),

where T is the (primitive recursive) Kleene-T-predicate, i.e. T xyz :≡ ‘the Turing machine with Gödel number x applied to the input y terminates with a computation whose Gödel number is z’ (see e.g. [68]). In general we are not able to determine closed terms t_{1}, …, t_{k} such that

IN ⊧ ⋁_{i=1}^{k} ∀y(T (\overline{e}, \overline{e}, t_{i}) ∨ ¬T (\overline{e}, \overline{e}, y)),

Chapter 1. Unwinding Proofs

since this would allow us to decide whether ∃xT (\overline{e}, \overline{e}, x) or not (simply check whether ⋁_{i=1}^{k} T (\overline{e}, \overline{e}, t_{i}) is true or not). In fact for

A :≡ ∀x∃y∀z(T xxy ∨ ¬T xxz)

A is provable in PA (using only the logical axioms and rules), but there is no computable bound g on ‘∃y’, i.e. no computable g such that

∀x∃y ≤ gx∀z(T xxy ∨ ¬T xxz)

since this would make the (special) halting problem {x ∈ IN : ∃y ∈ IN(T xxy)} decidable by the then computable function

fx := \{ \begin{matrix}0, if ∃y ≤ gx(T xxy) \\ 1, otherwise. \end{matrix}

Two examples of non-constructive proofs from number theory: Proposition 1.4 ∃a, b ∈ IR \underbrace{(a, b irrational ∧ a^{b} rational )}_{(sightly more complex than Π_{1}^{0})} .

Proof: Case 1: \sqrt{2}^{\sqrt{2}} is rational. Put a := b := \sqrt{2}. Case 2: \sqrt{2}^{\sqrt{2}} irrational. Put a := \sqrt{2}^{\sqrt{2}}, b := \sqrt{2}. □ ¿From this proof we get two candidates for (a, b), namely (\sqrt{2}, \sqrt{2}) and (\sqrt{2}^{\sqrt{2}}, \sqrt{2}) but no decision which one satisfies the proposition. Remark 1.5 ¿From a deep result of Gelfand and Schneider, stating that if a, b are algebraic, a ≠ 0, 1 and b irrational, then a^{b} is transcendental, it follows that \sqrt{2}^{\sqrt{2}} is transcendental and therefore irrational. So it is the pair (\sqrt{2}^{\sqrt{2}}, \sqrt{2}) which satisfies the proposition.

Here is an example (communicated by H. Friedman) of a simple non-construc-tive PA-proof in number theory of a disjunction where none of the two disjuncts is known to be true up to now:

Proposition 1.6 PA ⊢ (e − π is irrational) or (e + π is irrational).

Proof: One easily formalizes the proof of the irrationality of e as given e.g. in [23] in PA. If both e − π and e + π were rational, then also their sum 2e and therefore e would be rational which is a contradiction. □

We have seen that already for Σ_{2}^{0}, Π_{3}^{0}-sentences A it is not possible in general to compute witnesses resp. bounds. However one can obtain such witness candidates and bounds (and even realizing function(al)s) for a weakened version of A, namely its so-called Herbrand normal form A^{H}:

Definition 1.7 A ≡ (∀y_{0})∃x_{1}∀y_{1} … ∃x_{n}∀y_{n}A_{0}(y_{0}, x_{1}, y_{1}, …, x_{n}, y_{n}). Then the Herbrand normal form of A is defined as

A^{H} :≡ ∃x_{1}, …, x_{n}A_{0}(y_{0}, x_{1}, f_{1}x_{1}, …, x_{n}, f_{n}x_{1} … x_{n}),

where f_{1}, …, f_{n} are new function symbols, called index functions.

Remark 1.8 In theories with function variables and function quantifiers we take the Herbrand normal form of A to be

A^{H} :≡ ∀(y_{0}), f_{1}, …, f_{n}∃x_{1}, …, x_{n}A_{0}(y_{0}, x_{1}, f_{1}x_{1}, …, x_{n}, f_{n}x_{1} … x_{n}).

A and A^{H} are equivalent with respect to logical validity, i.e.

⊧ A ⇔⊧ A^{H},

but are not logically equivalent since in general

PL ⊢ / A^{H} → A

However the converse implication holds

PL ⊢ A → A^{H}.

Let PL^{2} denote the extension of PL obtained by the addition of n-ary function variables (for every n) and function quantifiers. Let furthermore AC denote the schema of choice

AC : ∀\underline{x}∃y A(\underline{x}, y) → ∃f∀\underline{x} A(\underline{x}, f\underline{x}) (\underline{x} = x_{1} … x_{n}),

then it is an easy exercise to show that

PL^{2} + AC ⊢ A ↔ A^{H}.

We now consider again the sentence

A ≡ ∀x∃y∀z(P xy ∨ ¬P xz),

where P is some predicate symbol. In contrast to A, the Herbrand normal form A^{H} of A

A^{H} ≡ ∃y(P (x, y) ∨ ¬P (x, gy))

allows an interpretation in form of a list of candidates (uniformly in x, g) for ‘∃y’, namely (x, gx) and also (c, gc) for any constant c does the job since the disjunction

A^{H,D} :≡ (P (x, c) ∨ ¬P (x, gc)) ∨ (P (x, gc) ∨ ¬P (x, g(g(c))))

is a tautology. A tautology remains a tautology if we replace all occurrences of a term s by a variable y: Replace gc by y and g(g(c)) by z. Then A^{H,D} becomes

A^{D} :≡ (P (x, c) ∨ ¬P (x, y)) ∨ (P (x, y) ∨ ¬P (x, z)),

which still is a tautology. From A^{D} we can derive A by a so-called direct proof (which uses only appropriate quantifier introduction rules, the shift of quantifiers over ∨ and contraction):

P (x, c) ∨ ¬P (x, y) ∨ P (x, y) ∨ ¬P (x, z)

⇓ (∀-introduction) P (x, c) ∨ ¬P (x, y) ∨ ∀z(P (x, y) ∨ ¬P (x, z)) ⇓ (∃-introduction) P (x, c) ∨ ¬P (x, y) ∨ ∃y∀z(P (x, y) ∨ ¬P (x, z)) ⇓ (∀-introduction) ∀y(P (x, c) ∨ ¬P (x, y)) ∨ ∃y∀z(P (x, y) ∨ ¬P (x, z)) ⇓ (∃-introduction) ∃u∀y(P (x, c) ∨ ¬P (x, y)) ∨ ∃y∀z(P (x, y) ∨ ¬P (x, z)) ⇓ ( contraction) ∃y∀z(P (x, y) ∨ ¬P (x, z)) ⇓ (∀-introduction) ∀x∃y∀z(P (x, y) ∨ ¬P (x, z))

Definition 1.9 A formula A in the language of first-order predicate logic with equality (PL_{=}) is called a quasi-tautology if it is a tautological consequence of instances of =-axioms. Theorem 1.10 (Herbrand’s Theorem) Let A ≡ ∃x_{1}∀y_{1} … ∃x_{n}∀y_{n}A_{0}(x_{1}, y_{1}, …, x_{n}, y_{n}). Then the following holds: PL ⊢ A iff there are terms t_{1,1}, …, t_{1,k_{1}}, …, t_{n,1}, …, t_{n,k_{n}} (built up out of the constants and variables of A and the index functions used for the formation of A^{H}) such that

A^{H,D} :≡ ⋁_{j_{1}=1}^{k_{1}} … ⋁_{j_{n}=1}^{k_{n}} A_{0}(t_{1,j_{1}}, f_{1}(t_{1,j_{1}}), …, t_{n,j_{n}}, f_{n}(t_{1,j_{1}}, …, t_{n,j_{n}}))

is a tautology.

The terms t_{i,j} can be extracted constructively from a given PL-proof of A and conversely one can construct a PL-proof for A out of a given tautology A^{H,D}. The theorem holds for PL_{=} if ‘tautology’ is replaced by ‘quasi-tautology’.

Proof: See e.g. [60]. □

The most difficult part of the proof of Herbrand’s theorem is the construction of the Herbrand terms t_{i,j}. The reverse direction for PL follows similar to the special case treated above: the terms f_{i}-terms in A^{H,D} are replaced by new variables (starting from terms of maximal size) yielding an index-function-free Herbrand disjunction A^{D}. From this A is derived by a direct proof. For PL_{=} the reverse direction is more complicated to establish since also instances of equality axioms \underline{x} = \underline{y} → f_{i}\underline{x} = f_{i}\underline{y} are now allowed in the proof of A^{H,D}.

In applications, the Herbrand disjunction A^{D} without index function has been particular useful (see [47],[53]). Although it is quite complicated to write down the general form of such a disjunction it is easy for Π_{3}^{0}-sentences (which is sufficient for many applications in mathematics):

For sentences A ≡ ∀x∃y∀z A_{0}(x, y, z), A^{D} can always be written in the form

A_{0}(x, t_{1}, b_{1}) ∨ A_{0}(x, t_{2}, b_{2}) ∨ … ∨ A_{0}(x, t_{k}, b_{k}),

where the b_{i} are new variables and t_{i} does not contain any b_{j} with i ≤ j (see [47]).

Herbrand’s theorem immediately extends to so-called open theories, i.e. firstorder theories T whose non-logical axioms G_{1}, …, G_{n} are all purely universal (G_{i} ≡ ∀a_{i}G_{0}^{i}(a_{i})), if ‘(quasi-)tautology’ is replaced by ‘tautological consequence of instances of equality axioms and the non-logical axioms’.

Proof: Apply Herbrand’s theorem for logic to

Ã :≡ ∃x_{1}∀y_{1} … ∃x_{n}∀y_{n}∃a_{1}, …, a_{m}( ⋀_{i=1}^{n} G_{0}^{i}(a_{i}) → A_{0}(x_{1}, y_{1}, …, x_{n}, y_{n})).

□ Warning: For the extension of Herbrand’s theorem to open theories T it is important that the index function used in defining A^{H} are new and do not occur in the non-logical axioms. In particular if we have a schema of purely universal axioms then in the statement of Herbrand’s theorem this schema is always understood with respect to the original language (without the index functions). Otherwise the reverse direction in Herbrand’s theorem in general would fail (see [29] for a discussion of this and related matters thereby pointing out errors in the literature).

In general Herbrand’s theorem in the form stated above does not hold for theories which are not open, e.g. it fails for PA. However there are ways to extend the general idea behind Herbrand’s theorem to theories like PA and beyond: in these lectures we will discuss Gödel’s functional interpretation and the so-called no-counterexample interpretation (due to G. Kreisel [42],[43]). We conclude the first lecture by motivating the latter:

Lets consider again the example

A ≡ ∀x∃y∀z(P (x, y) ∨ ¬P (x, z)).

If P is formulated in some theory like PA with decidable prime formulas, e.g. if P (x, y) ≡ T (x, x, y), then we can realize the Herbrand normal form A^{H} of A instead of using a disjunction also by a computable functional of type level 2 which is defined by cases:

Φ(x, g) := \{ \begin{matrix}x if ¬T (x, x, gx) \\ gx otherwise. \end{matrix}

¿From this definition it easily follows that

∀x, g(T (x, x, Φxg) ∨ ¬T (x, x, g(Φxg)).

If A is not provable in PL but e.g. in PA we no longer can expect that functionals as simple as Φ above will be sufficient. In addition to the use of definition by cases we also have to allow certain recursive definitions whose complexity depends on the strength of the theory in which A is proved. In these lectures we will characterize in the case of PA (and subsystems) what functionals are needed.

Definition 1.11 Let A ≡ ∃x_{1}∀y_{1} … ∃x_{n}∀y_{n}A_{0}(x_{1}, y_{1}, …, x_{n}, y_{n}). If a tuple of functionals Φ_{1}, …, Φ_{n} realizes the Herbrand normal form A^{H} of A, i.e. if

∀\underline{f}A_{0}(Φ_{1}\underline{f}, f_{1}(Φ_{1}\underline{f}), …, Φ_{n}\underline{f}, f_{n}(Φ_{1}\underline{f}, …, Φ_{n}\underline{f}))

is true (where \underline{f} = f_{1}, …, f_{n}), then we say that \underline{Φ}(= Φ_{1}, …, Φ_{n}) satisfies the no-counterexample interpretation of A (short: \underline{Φ} n.c.i. A). If A starts with a universal quantifier ∀y_{0} then y_{0} is considered as a 0-place index function and Φ_{i} now depends on y_{0} and \underline{f}.

Motivation for the name ‘no-counterexample interpretation’:

Let A be as above. Then ¬A is equivalent to

∀x_{1}∃y_{1} … ∀x_{n}∃y_{n}¬A_{0}(x_{1}, y_{1}, …, x_{n}, y_{n}).

So a counterexample to A is given by functions f_{1}, …, f_{n} such that

(+) ∀\underline{x}¬A_{0}(x_{1}, f_{1}(x_{1}), …, x_{n}, f_{n}(x_{1}, …, x_{n}))

holds. Hence functionals \underline{Φ} satisfying the n.c.i. of A produce a counterexample to (+) i.e. to the existence of counterexample functions f_{1}, …, f_{n}.

Definition 1.12 A functional F of type level ≤ 2 is called primitive recursive in the sense of Kleene if it can be defined by the following schemas (\underline{x} = x_{0}, …, x_{p−1} is a list of number variables and \underline{f} = f_{0}, …, f_{q−1} is a list of function variables):

(i) (Identity) F (\underline{x}, \underline{f}) = x_{i} (for i < p),

(ii) (Function application) F (\underline{x}, \underline{f}) = f_{i}(x_{j_{0}}, …, n_{j_{l−1}}) (for i < q and j_{0}, …, j_{l−1} < p),

(iii) (Successor) F (\underline{x}, \underline{f}) = x_{i} + 1 (for i < p), (iv) (Substitution)

F (\underline{x}, \underline{f}) = G(H_{0}(\underline{x}, \underline{f}), …, H_{l−1}(\underline{x}, \underline{f}), λy.K_{0}(y, \underline{x}, \underline{f}), …, λy.K_{j−1}(y, \underline{x}, \underline{f})),

(v) (Primitive recursion) F (0, \underline{x}, \underline{f}) = G(\underline{x}, \underline{f}), F (y + 1, \underline{x}, \underline{f}) = H(F (y, \underline{x}, \underline{f}), y, \underline{x}, \underline{f}).

Exercises:

1) Consider Ψ(x) := |{n ∈ IN : 1 ≤ n ≤ x ∧ n is not divisible by any square number ≠ 1 }|. Show that Ψ(x) ≥ x − ∑_{{p prime \atop p≤x}}[\frac{x}{p^{2}} ] and use this to show that there are

infinitely many primes. Use this proof to obtain an upper bound g(j) for the next prime p_{j+1} as in the 3. proof of this statement above. Can you improve the bound we obtained from the latter (see Hacks [22])?

2) Let (a_{n})_{n∈IN} be a sequence of rational numbers in [0, 1] with ∀n ∈ IN(a_{n+1} ≤ a_{n}). Since rational numbers can be coded by natural numbers one can consider (a_{n}) as a number theoretic function. The order relation ≤ and the usual arithmetical operations between rational numbers are primitive recursive in their codes. Construct a primitive recursive functional Φ which satisfies (uniformly in (a_{n})) the n.c.i. of the theorem

∀x ∈ IN∃y ∈ IN∀z ∈ IN (z > y → a_{y} − a_{z} ≤ \frac{1}{x + 1}).

3) Construct primitive recursive functionals \underline{Φ} which satisfy the n.c.i. of (some prenex normal form of) the second-order axiom of Σ_{1}^{0}-induction:

∀f(∃y(f0y = 0)∧∀x(∃y(fxy = 0) → ∃y(fx′y = 0)) → ∀x∃y(fxy = 0))

uniformly as a functional in f and the index functions.

Suggested further reading 1) On the general program of unwinding proofs: [47],[48],[49].

2) On Herbrand’s theorem: [8],[14],[29],[47],[60].

3) On the no-counterexample interpretation: [14],[40],[42],[43].

Intuitionistic logic and arithmetic in all finite types

In the following we formulate an axiomatic system for intuitionistic firstorder predicate logic IL. The particular axiomatization we choose is due to [17] and particular suited to carry out proof interpretations inductively over the proof tree.

Intuitionistic first-order predicate logic IL

I. The language L(IL) of IL:

As logical constants we use ∧, ∨, →, ⊥ (absurdity of ‘falsum’), ∃, ∀. L(IL) contains variables x, y, z, … (which can be free or bound). Furthermore we have function constants f_{1}, f_{2}, f_{3}, … and predicate constants P_{1}, P_{2}, P_{3}, … (both n-ary for every n).

Abbreviations:

¬A :≡ A → ⊥, A ↔ B :≡ (A → B) ∧ (B → A).

II. Axioms of IL:

(i) A ∨ A → A, A → A ∧ A (axioms of contraction)

(ii) A → A ∨ B, A ∧ B → A (axioms of weakening)

Chapter 2. Intuitionistic Arithmetic

(iii) A ∨ B → B ∨ A, A ∧ B → B ∧ A (axioms of permutation) (iv) ⊥ → A (ex falso quodlibet)

(v) ∀x A(x) → A(t), A(t) → ∃x A(x), where t is free for x in A (quantifier axioms).

1) Rules of IL:

(i)

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

(modus ponens and syllogism) (ii)

\frac{A ∧ B → C}{A → (B → C)}, \frac{A → (B → C)}{A ∧ B → C}

(exportation and importation) (iii)

\frac{A → B}{C ∨ A → C ∨ B} (expansion)

(iv)

\frac{B → A(x)}{B → ∀x A(x)}, \frac{A(x) → B}{∃x A(x) → B} , where x is not free in B

(quantifier rules).

The Brouwer-Heyting-Kolmogorov (‘BHK’) proof interpretation of the intuitionistic logical constants^{1}

This interpretation is an informal attempt to explain the meaning of the logical constants of IL in terms of proof constructions:^{2} (i) There is no proof for ⊥.

1Our exposition makes use of [58].

2‘Proof’ is understood here as ‘verification by a construction’ and not as a formal proof in some fixed deductive framework like HA below.

(ii) A proof of A ∧ B is a pair (q, r) of proofs, where q is a proof of A and r is a proof of B.

(iii) A proof of A ∨ B is a pair (n, q) consisting of an integer n and a proof q which proves A if n = 0 and resp. B if n = 1.

(iv) A proof p of A → B is a construction which transforms any hypothetical proof q of A into a proof p(q) of B.

(v) A proof of ∀x A(x) is a construction which produces for every construction c_{d} of an element d of the domain a proof p(c_{d}) of A(d).

(vi) A proof p of ∃x A(x) is a pair (c_{d}, q), where c_{d} is the construction of an element d of the domain and q is a proof of A(d).

Exercise 2.1 1) Convince yourself that the axioms and rules of IL are sound under this interpretation.

2) Convince yourself that ¬¬A → A in general is not valid under this interpretation.

Discussion: There is one problem with the BHK-interpretation: from a strictly constructive point of view one would like to have a constructive verification of ‘p is a proof of A’ in case this is true, i.e. one would like to recognize a proof if one sees it. For (i), (ii), (iii), (vi) there is no problem with this requirement. But for the universal statements in (iv), (v) one would need an additional clause as suggested by Kreisel in [46]:

(iv)’ A proof p of A → B is a pair (r, q), where q is a construction which transforms any hypothetical proof s of A into a proof q(s) of B and r is a proof which verifies that q is such a construction.

(v)’ A proof p of ∀x A(x) is a pair (r, q) where q is a construction which produces for every construction c_{d} of an element d of the domain a proof q(c_{d}) of A(d) and r is a proof of the fact that q is such a construction.

Remark 2.2 There are various ways to formalize the idea behind the BHKinterpreta-tion which give rise to various forms of so-called realizability interpretations. The first version of realizability, the so-called recursive realizability, was introduced by Kleene in [26]. In these lectures we will focus on a typed variant of Kleene’s type-free interpretation which is called ‘modified realizability’ and is due to Kreisel [44],[45].

Intuitionistic (‘Heyting’-)arithmetic HA

L(HA) contains the logical constants of L(IL), number variables x, y, z, …, a constant 0 (zero), a unary function constant S (successor), function constants for all primitive recursive functions (more precisely for all derivations of primitive recursive functions) and a single binary predicate =.

Axioms and rules of HA:

(i) axioms and rules of IL (based on L(HA))

(ii) =-axioms: x = x, x = y → y = x, x = y ∧ y = z → x = z, \underline{x} = \underline{y} → f(\underline{x}) = f(\underline{y}) for every n-ary function constant f (\underline{x} = x_{1}, …, x_{n}, \underline{y} = y_{1}, …, y_{n})

(iii) successor axioms:

\{ \begin{matrix}Sx ≠ 0, \\ Sx = Sy → x = y \end{matrix}

(iv) defining equations for the primitive recursive functions

(v) axiom schema of complete induction

IA : A(0) ∧ ∀x(A(x) → A(Sx)) → ∀x A(x)

for every formula A ∈ L(HA)

Convention: We often write x′ or x + 1 for Sx.

Remark 2.3 In HA we may identify ⊥ with 0 = 1.

Instead of the axiom schema IA we could have formulated HA equivalently using the rule of induction

IR: \frac{A(0) , A(x) → A(Sx)}{A(x)}.

Exercise 2.4 Show that IA is derivable from IR. Compare the complexity of the induction formula Ã(x) of the IR-instance needed to prove an IA-instance with induction formula A(x) with that of A(x).

Extensional intuitionistic (‘Heyting’-) arithmetic E-HA^{ω} in all finite types

The set T of all finite types is generated inductively by the clauses

(i) 0 ∈ T, (ii) ρ, τ ∈ T ⇒ τ(ρ) ∈ T.

The type 0 is the type natural numbers. Objects of type τ(ρ) are functions which map objects of type ρ to objects of type τ (some authors write (ρ)τ or ρ → τ instead of τ(ρ). We often omit brackets which are uniquely determined and write e.g. 0(00) instead of 0(0(0)).

The set P ⊂ T of pure types is defined by

(i) 0 ∈ P, (ii) ρ ∈ P ⇒ 0(ρ) ∈ P.

Pure types are often denoted by natural numbers: 0(n) := n + 1 (e.g. 00 = 1, 0(00) = 2). The type level or degree deg(ρ) of a type ρ is defined as

deg(0) := 0, deg(τ(ρ)) := max(deg(τ), deg(ρ) + 1)

(note that for pure types ρ, deg(ρ) is just the number which denotes ρ).

Objects of type ρ with deg(ρ) > 1 are usually called functionals. The language L(E-HA^{ω}) of E-HA^{ω} is based on a many-sorted version IL^{ω} of IL which contains variables x^{ρ}, y^{ρ}, z^{ρ}, … and quantifiers ∀x^{ρ}, ∃y^{ρ} for every type ρ. As constants E-HA^{ω} contains 0^{0} (zero), S^{00} (successor), Π_{ρ,τ}^{ρτρ} (projector), Σ_{δ,ρ,τ} (combinator of type τδ(ρδ)(τρδ)) and recursor constants R_{ρ} of type ρ(ρ0ρ)ρ0 for all δ, ρ, τ ∈ T. Furthermore L(E-HA^{ω}) contains a binary predicate constant =_{0} for equality between object of type 0. Terms of E-HA^{ω} are built up by

(i) constants c^{ρ} and variables x^{ρ} of type ρ are terms of type ρ (ii) if t^{τρ} is a terms of type τρ and s^{ρ} is a term of type ρ, then (st) is a

term of type τ. Formulas of E-HA^{ω} are built up by

(i) prime formulas (also called ‘atomic formulas’) s =_{0} t are formulas (where s^{0}, t^{0} are terms of type 0)

(ii) if A, B are formulas, then also A ∧ B, A ∨ B and A → B are formulas (iii) if A(x^{ρ}) is a formula, then also ∀x^{ρ}A(x) and ∃x^{ρ}A(x) are formulas. Abbreviations:

1) Higher type equations s =_{ρ} t between terms s, t of type ρ = 0(ρ_{k}) … (ρ_{1})

(where k ≥ 1) are abbreviations for

∀y_{1}^{ρ_{1}}, …, y_{k}^{ρ_{k}}(sy_{1} … y_{k} =_{0} ty_{1} … y_{k}),

where y_{1}, …, y_{k} are variables which don’t occur in s, t.

2) As before: ¬A :≡ A → ⊥, where ⊥ :≡ (0 = 1).

A ↔ B :≡ (A → B) ∧ (B → A). Axioms and rules of E-HA^{ω}

(i) all axioms and rules of IL^{ω}

Chapter 2. Intuitionistic Arithmetic

(ii) equality axioms for =_{0} (iii) higher type extensionality:

E_{ρ} : ∀z^{ρ}, x_{1}^{ρ_{1}}, y_{1}^{ρ_{1}}, …, x_{k}^{ρ_{k}}, y_{k}^{ρ_{k}}( ⋀_{i=1}^{k}(x_{i} =_{ρ_{i}} y_{i}) → z\underline{x} =_{0} z\underline{y}),

where ρ = 0ρ_{k} … ρ_{1} (iv) successor axioms

(v) induction schema

IA: A(0) ∧ ∀x^{0}(A(x) → A(Sx)) → ∀x^{0}A(x),

where A(x^{0}) is an arbitrary formula of E-HA^{ω} (vi) axioms for Π_{ρ,τ}, Σ_{δ,ρ,τ} and R_{ρ}:

(Π) : Π_{ρ,τ}x^{ρ}y^{τ} =_{ρ} x^{ρ},

(Σ) : Σ_{δ,ρ,τ}xyz =_{τ} xz(yz) (x^{τρδ}, y^{ρδ}, z^{δ}),

(R) : \{ \begin{matrix}R_{ρ}0yz =_{ρ} y \\ R_{ρ}(Sx^{0})yz =_{ρ} z(R_{ρ}xyz)x (y^{ρ}, z^{ρ0ρ}). \end{matrix}

Definition 2.5 Later on we will need also a variant WE-HA^{ω} of E-HA^{ω}, where the extensionality axioms E_{ρ} are weakened to a quantifier-free rule of extensionality

QF-ER: \frac{A_{0} → s =_{ρ} t}{A_{0} → r[s] =_{τ} r[t]},

where s^{ρ}, t^{ρ}, r[x^{ρ}]^{τ} are terms of WE-HA^{ω} (ρ, τ ∈ T arbitrary). Warning: WE-HA^{ω} does not satisfy the deduction theorem. WE-HA^{ω} allows the definition of λ-abstraction in the following sense:

Chapter 2. Intuitionistic Arithmetic

Lemma 2.6 For every term t[x^{ρ}]^{τ} one can construct in WE-HA^{ω} a term λx^{ρ}.t[x] of type τρ (with FV(λx^{ρ}.t[x]) = FV(t[x]) \ {x})^{3} such that

WE-HA^{ω} ⊢ (λx^{ρ}.t[x])(s^{ρ}) =_{τ} t[s].

Proof: Define

λx.x := ΣΠΠ,
λx.t := Πt, if x ∉ FV(t)
λx.(ts) := Σ(λx.t)(λx.s), if x ∈ FV(ts)

(here Π, Σ of suitable types). □ Exercise: It is known that the function α(x, y) defined by the equations

(∗) \{ \begin{matrix}α(0, y) = y′ \\ α(x′, 0) = α(x, 1) \\ α(x′, y′) = α(x, α(x′, y)) \end{matrix}

is not primitive recursive (in the sense of Kleene). In fact α is a variant due to R. Peter of the well-known Ackermann function. Show that α is definable in in WE-HA^{ω} by a closed term t^{0(0)(0)} (i.e. WE-HA^{ω} proves the equations (∗) for t). Suggested further reading: See [64] for further information on the BHK-interpretation. For more information on (W)E-HA^{ω} and its variants see [65].

3FV(t) (FV(A)) denotes the set of all free variables of t (A).

Modified realizability

Definition 3.1 (modified realizability) For each formula A of E-HA^{ω} we define a formula \underline{x} mr A (in words: ‘\underline{x} modified realizes A’) of E-HA^{ω} whose free variables are contained in that of A and \underline{x}, where \underline{x} is a – possibly empty – tuple of variables which do not occur free in A. The length of \underline{x} and the types of these variables are determined by the logical structure of A, since the definition of \underline{x} mr A proceeds by induction over the logical structure of A:

(i) \underline{x} mr A :≡ A with the empty tuple \underline{x}, if A is a prime formula.

(ii) \underline{x}, \underline{y} mr (A ∧ B) :≡ \underline{x} mr A ∧ \underline{y} mr B.

(iii) z^{0}, \underline{x}, \underline{y} mr (A ∨ B) :≡ [(z = 0 → \underline{x} mr A) ∧ (z ≠ 0 → \underline{y} mr B)].

(iv) \underline{y} mr (A → B) :≡ ∀\underline{x}(\underline{x} mr A → \underline{y} \underline{x} mr B).

(v) \underline{x} mr (∀y^{ρ}A(y)) :≡ ∀y^{ρ}(\underline{x}y mr A(y)).

(vi) z^{ρ}, \underline{x} mr (∃y^{ρ}A(y)) :≡ \underline{x} mr A(z).

Definition 3.2 1) A formula A ∈ L(E-HA)^{ω} is called ∃-free if it is built up from prime formulas by means of ∧, → and ∀ only.

2) A formula A ∈ L(E-HA)^{ω} is called negative if it is built up from negated prime formulas by means of ∧, → and ∀ only.

Chapter 3. Modified Realizability

Remark 3.3 In WE-HA^{ω} all prime formulas P are decidable and therefore ¬¬P ↔ P is provable in WE-HA^{ω}. Hence every ∃-free formula is equivalent to a negative formula in WE-HA^{ω}.

Remark 3.4 1) For ∃-free formulas A we have (\underline{x} mr A) ≡ A with \underline{x} being the empty tuple.

2) (\underline{x} mr A) is always an ∃-free formula.

We will also need a variant ‘modified realizability with truth’ mrt of mr:

Definition 3.5 \underline{x} mrt A is defined analogously to \underline{x} mr A except that clause (iv) is replaced by

(iv)′ \underline{y} mrt (A → B) :≡ ∀\underline{x}(\underline{x} mrt A → \underline{y} \underline{x} mrt B) ∧ (A → B).

The name ‘modified realizability with truth’ is motivated by the following

Lemma 3.6 WE-HA^{ω} ⊢ (\underline{x} mrt A) → A, for every formula A.

Proof: Straightforward. □

Exercise 3.7 WE-HA^{ω} ⊢ (\underline{x} mrt ¬A) ↔ ¬A for every formula A.

The schema of choice AC:= ⋃_{ρ,τ∈T}{ AC^{ρ,τ}} is given by

AC^{ρ,τ} : ∀x^{ρ}∃y^{τ}A(x, y) → ∃Y^{τρ}∀x^{ρ}A(x, Y x),

where A is an arbitrary formula of E-HA^{ω}.

The independence-of-premise-schema IP_{ef}^{ω} := ⋃_{ρ∈T}{IP_{ef}^{ρ}} for ∃-free formulas

is given by

IP_{ef}^{ρ} : (A → ∃x^{ρ}B(x)) → ∃x^{ρ}(A → B(x)),

where A is ∃-free and doesn’t contain x free.

Theorem 3.8 (soundness for mr) Let A be an arbitrary formula in L(E-HA^{ω}). Then the following rule holds

E-HA^{ω} + AC + IP_{ef}^{ω} ⊢ A ⇒ E-HA^{ω} ⊢ \underline{t} mr A,

where \underline{t} is a suitable tuple of terms of E-HA^{ω} with F V (\underline{t}) ⊆ F V (A) which can be extracted from a given proof of A. Proof: Induction on the length of the derivation of A:

1) Axioms. A ∨ A → A: If z^{0}, \underline{x}, \underline{y} mr (A ∨ A), then \underline{t}z^{0}\underline{x} \underline{y} mr A, where \underline{t}

such that \underline{t}z^{0}\underline{x} \underline{y} := \{ \begin{matrix}\underline{x}, if z = 0 \\ \underline{y}, if z ≠ 0 \end{matrix}

(t_{i} can easily be defined using R_{0}: exercise!). Hence \underline{t} mr (A ∨ A → A). A → A ∧ A is realized by λ\underline{x}.(\underline{x}, \underline{x}). A → A ∨ B: Let \underline{x} mr A, then (0, \underline{x}, \underline{O}) mr (A ∨ B) and hence λ\underline{x}.[0, \underline{x}, \underline{O}] mr (A → A ∨ B) (here \underline{O} is a suitable tuple O_{1}^{ρ_{1}}, …, O_{k}^{ρ_{k}} with suitable types ρ_{i} so that \underline{O} mr B is syntactically correct^{1}). A ∧ B → A: if (\underline{x}, \underline{y}) mr A ∧ B, then \underline{x} mr A. Hence λ\underline{x}, \underline{y}.\underline{x} mr (A ∧ B → A). ⊥ → A is realized by \underline{O} mr(⊥ → A) such that \underline{O} mr A is syntactically correct. A ∨ B → B ∨ A is realized by λz^{0}, \underline{y}, \underline{x}.[\overline{sg}(z), \underline{x}, \underline{y}], where

\overline{sg}(z) := \{ \begin{matrix}0^{0}, if z ≠ 0 \\ 1^{0}, otherwise. \end{matrix}

A ∧ B → B ∧ A is realized by λ\underline{y}, \underline{x}.\underline{x}, \underline{y}. ∀x^{ρ}A(x) → A(t^{ρ}): Let \underline{y} mr ∀x A(x). Then \underline{y}(t) mr A(t). Hence λ\underline{y}.\underline{y}(t) mr (∀x A(x) → A(t)). A(t^{ρ}) → ∃x^{ρ}A(x) is realized by λ\underline{y}.[t, \underline{y}], where \underline{y} is a tuple of variables such that \underline{y} mr A(t) is well-formed.

2) Rules. \frac{A , A→B}{B}: Assume \underline{t} mr A and \underline{s} mr (A → B). Let \underline{r} be the terms which result from \underline{t}(\underline{s}) be replacing all free variables \underline{a} which occur in A but not in B by \underline{O}. Then \underline{r} mr B.

1Here for ρ = 0(ρ_{k}) … (ρ_{1}), O^{ρ} := λx_{1}^{ρ_{1}}, …, x_{k}^{ρ_{k}}.0^{0}.

\frac{A→B , B→C}{A→C} : \underline{s} mr (A → B), \underline{t} mr (B → C). If \underline{x} mr A, then \underline{s} \underline{x} mr B and hence \underline{t}(\underline{s} \underline{x}) mr C. Thus λ\underline{x}.\underline{t}(\underline{s} \underline{x}) mr (A → C) (if necessary replace free variables which don’t occur in A → C by O). \frac{A∧B→C}{A→(B→C)} and \frac{A→(B→C)}{A∧B→C} are trivially satisfied: use the terms from the premise for the conclusion. \frac{A→B}{C∨A→C∨B} : Assume \underline{t} mr (A → B) and z^{0}, \underline{x}, \underline{y} mr (C ∨ A). Then either z = 0, \underline{x} mr C or z ≠ 0, \underline{y} mr A. In the second case we have \underline{t} \underline{y} mr B. Hence λz^{0}, \underline{x}, \underline{y}.[z^{0}, \underline{x}, \underline{t} \underline{y}] mr (C ∨ A → C ∨ B). \frac{B→A(x^{ρ})}{B→∀x^{ρ}A(x)} : Assume \underline{t}[x] mr (B → A(x)) and \underline{z} mr B. Then λx.(\underline{t}[x]\underline{z}) mr ∀x A(x) and therefore λ\underline{z}, x.(\underline{t}[x]\underline{z}) mr (B → ∀x A(x)). \frac{A(x^{ρ})→B}{∃x^{ρ}A(x)→B} : Assume \underline{t}[x] mr (A(x) → B) and x, \underline{z} mr ∃x A(x). Then \underline{z} mr A(x) and therefore \underline{t}[x]\underline{z} mr B. Thus λx, \underline{z}.(\underline{t}[x]\underline{z}) mr (∃x A(x) → B).

3) Axioms for =_{0}, S, Π, Σ, R and E_{ρ}: These axioms are all ∃-free and therefore realized by themselves.

4) The induction schema: Let \underline{x} mr A(0) and \underline{y} mr ∀z^{0}(A(z) → A(z+1)). Define \underline{t} by simultaneous primitive recursion in higher types (which can be reduced to ordinary primitive recursion in higher types, exercise!) such that

\{ \begin{matrix}\underline{t} \underline{x} \underline{y}0 = \underline{x} \\ \underline{t} \underline{x} \underline{y}(z + 1) = \underline{y}z(\underline{t} \underline{x} \underline{y}z). \end{matrix}

By induction on z^{0} one shows that \underline{t} \underline{x} \underline{y}z mr A(z) and hence \underline{t} \underline{x} \underline{y} mr ∀z A(z).

5) The interpretations for AC and IP_{ef}^{ω} are trivial (note that AC and IP_{ef}^{ω} are not needed to verify their mr-interpretation). □

Definition 3.9 ([65]) The subset Γ_{1} of formulas ∈ L(E-HA^{ω}) is defined inductively by

1) Prime formulas are in Γ_{1}.^{2}

2) A, B ∈ Γ_{1} ⇒ A ∧ B, A ∨ B, ∀x A(x), ∃x A(x) ∈ Γ_{1}.

2Note that in our theories quantifier–free formulas can be written as prime formulas s =_{0} t.

3) If A is ∃–free and B ∈ Γ_{1}, then (∃\underline{x}A → B) ∈ Γ_{1}.

Lemma 3.10 For A ∈ Γ_{1} we have

E-HA^{ω} ⊢ (\underline{x} mr A) → A.

Proof: Straightforward induction on the generation of Γ_{1}. □

Corollary 3.11 E-HA^{ω}+ AC + IP_{ef}^{ω} is conservative over E-HA^{ω} with respect to formulas A ∈ Γ_{1}. In particular E-HA^{ω}+ AC + IP_{ef}^{ω} is consistent relative to E-HA^{ω} since (0 = 1) ∈ Γ_{1}.

Remark 3.12 One can show by much more complicated methods that E-HA^{ω}+ AC is conservative over HA. For a ‘neutral’ version of E-HA^{ω} without extensionality this is due to [19],[20],[21] (see also [54],[57]). The extension to E-HA^{ω} is due to [2]. In contrast to corollaries 3.11 and 3.14 (below), this result does not relativize to subsystems with restricted induction (see [39]).

Theorem 3.13 (soundness for mrt) Let H^{ω} := E-HA^{ω} {+ \atop −} AC {+ \atop −} IP_{ef}^{ω} and A be an arbitrary formula in L(E-HA^{ω}). The following rule holds

H^{ω} ⊢ A ⇒ H^{ω} ⊢ \underline{t} mrt A,

where \underline{t} is a suitable tuple of terms of E-HA^{ω} with F V (\underline{t}) ⊆ F V (A) which can be extracted from a given proof of A.

Proof: The treatment of the logical axioms is analogous to the one for the mr-interpretation in the proof of of theorem 3.8. The same applies for the modus ponens. For the remaining rules the new second clause in the mrt-interpretation of the conclusion follows from the corresponding second clause(s) of the premise(s) using the same rule. Only in the case of the →-introduction rule one has to be a bit more careful because of the nested implications: By induction hypothesis we have terms \underline{s} such that

\underline{s} mrt (A ∧ B → C).

Chapter 3. Modified Realizability

Hence

∀\underline{x}, \underline{y}(\underline{x} mrt A ∧ \underline{y} mrt B → \underline{s} \underline{x} \underline{y} C) ∧ (A ∧ B → C),

which is equivalent to

∀\underline{x}(\underline{x} mrt A → ∀\underline{y}(\underline{y} mrt B → \underline{s} \underline{x} \underline{y} mrt C)) ∧ (A → (B → C)). By lemma 3.6 we have (\underline{x} mrt A) → A. Hence ∀\underline{x}(\underline{x} mrt A → ∀\underline{y}(\underline{y} mrt B → \underline{s} \underline{x} \underline{y} mrt C) ∧ (B → C)) ∧ (A → (B → C)) and hence

∀\underline{x}(\underline{x} mrt A → \underline{s} \underline{x} mrt (B → C)) ∧ (A → (B → C)),

i.e.

\underline{s} mrt A → (B → C).

We leave it as an exercise to the reader to adopt the mr-interpretation of the non-logical axioms and rules from the proof of theorem 3.8 to the mrtinterpretation. □ Corollary 3.14 Let H^{ω} := E-HA^{ω} {+ \atop −} AC {+ \atop −} IP_{ef}^{ω}. Then the following rules hold:

1)

H^{ω} ⊢ A ∨ B ⇒ H^{ω} ⊢ A or H^{ω} ⊢ B,

for closed formulas A ∨ B (disjunction property DP) 2)

H^{ω} ⊢ ∃x^{ρ}A(x) ⇒ H^{ω} ⊢ A(t),

for a suitable term t^{ρ} of H^{ω} with F V (t) ⊆ F V (A) \ {x^{ρ}} (the special case of this property for closed formulas ∃x^{ρ}A(x) is called existence property EP)

3)

H^{ω} ⊢ ∀x^{ρ}∃y^{τ}A(x, y) ⇒ H^{ω} ⊢ ∃Y^{τρ}∀x^{ρ}A(x, Y x)

(closure of H^{ω} under the rule of choice ACR).

4)

H^{ω} ⊢ (A → ∃x^{ρ}B(x)) ⇒ H^{ω} ⊢ ∃x^{ρ}(A → B(x^{ρ})),

where A is ∃-free and doesn’t contain x free (closure of H^{ω} under the rule of independence of premise for ∃-free formulas IPR_{ef}^{ω}).

Proof: 1) Suppose that H^{ω} ⊢ A ∨ B for a closed formula A ∨ B. By theorem 3.13 one finds closed terms t^{0}, \underline{s}, \underline{r} such that

H^{ω} ⊢ (t =_{0} 0 → \underline{s} mrt A) ∧ (t ≠ 0 → \underline{r} mrt B).

In E-HA^{ω} the closed number term t^{0} can be reduced (computed) to a numeral \overline{n} and so

H^{ω} ⊢ t =_{0} \overline{n}.

The conclusion now follows from the fact that

H^{ω} ⊢ \overline{n} = 0 or H^{ω} ⊢ \overline{n} ≠ 0

and lemma 3.6.

2) By theorem 3.13 the assumptions yields terms t^{ρ}, \underline{s} with F V (t, \underline{s}) ⊆ F V (A) \ {x} such that

H^{ω} ⊢ \underline{s} mrt A(t).

The claim now follows using lemma 3.6.

3) By 2) applied to the open formula ∃y^{τ}A(x^{ρ}, y^{τ}) we get a term t[x^{ρ}]^{τ} such that

H^{ω} ⊢ A(x, t[x]).

The conclusion follows by taking Y := λx^{ρ}.t[x^{ρ}].

4) Theorem 3.13 applied to

H^{ω} ⊢ A → ∃x^{ρ}B(x)

yields terms t^{ρ}, \underline{s} such that (using that (\underline{x} mrt A) ↔ A with the empty tuple \underline{x} for ∃-free formulas A)

H^{ω} ⊢ A → \underline{s} mrt B(t)

and hence (by lemma 3.6)

H^{ω} ⊢ A → B(t)

and so

H^{ω} ⊢ ∃x(A → B(x)),

where x is not free in A. □

Proposition 3.15 For all formulas A of E-HA^{ω} one has

E-HA^{ω} + AC + IP_{ef}^{ω} ⊢ (\underline{x} mr A) ↔ A.

This also holds for mrt instead of mr.

Proof: Straightforward induction on the logical structure of A. □

Exercise:

The so-called Markov Principle in all finite types is the schema

MP^{ω} : ¬¬∃\underline{x} A_{0}(\underline{x}) → ∃\underline{x} A_{0}(\underline{x}),

where A_{0} is an arbitrary quantifier-free formula of WE-HA^{ω} and \underline{x} is a tuple of variables of arbitrary types.

Show, using modified realizability, that already for \underline{x} = x^{0}, MP^{ω} is not derivable in E-HA^{ω}+AC+IP_{ef}.

Suggested further reading: [65] (chapter III, section 4) provides a very concise and detailed treatment of modified realizability interpretation. For a general survey on various forms of realizability interpretations see [67]. For an application of modified realizability to the extraction of a program from a specific proof see [3].

Majorizability and the fan rule

In this lecture we investigate an interesting structural property of the functionals which are definable by the closed terms of E-HA^{ω}, namely their majorizability. We will indicate the far-reaching use one can make out of this observation by showing the closure of E-HA^{ω} {+ \atop −}AC {+ \atop −} IP_{ef} under the so-called fan rule:

Definition 4.1 For arbitrary ρ ∈ T we define the relation x_{1} ≥_{ρ} x_{2} between functionals x_{1}, x_{2} of type ρ by induction on ρ:

x_{1} ≥_{0} x_{2} :≡ x_{1} ≥ x_{2} (for the usual primitive recursive relation ≥)
x_{1} ≥_{τρ} x_{2} :≡ ∀y^{ρ}(x_{1}y ≥_{τ} x_{2}y).

Lemma 4.2 Let ρ = τρ_{k} … ρ_{1}. Then WE-HA^{ω} ⊢ x_{1} ≥_{ρ} x_{2} ↔ ∀y_{1}^{ρ_{1}}, …, y_{k}^{ρ_{k}}(x_{1}\underline{y} ≥_{τ} x_{2}\underline{y}).

Definition 4.3 (W.A. Howard [24]) We define the relation x^{∗} maj_{ρ} x (x^{∗} majorizes x) between functionals of type ρ by induction on ρ:

\{ \begin{matrix}x^{∗} maj_{0} x :≡ x^{∗} ≥_{0} x, \\ x^{∗} maj_{τρ} x :≡ ∀y^{∗}, y(y^{∗} maj_{ρ} y → x^{∗}y^{∗} maj_{τ} xy). \end{matrix}

Chapter 4. Majorizability and the Fan Rule

Lemma 4.4 WE-HA^{ω} proves:

(i) x̃^{∗} =_{ρ} x^{∗} ∧ x̃ =_{ρ} x ∧ x^{∗} maj_{ρ} x → x̃^{∗} maj_{ρ} x̃.

(ii) x^{∗} maj_{ρ} x ∧ x ≥_{ρ} y → x^{∗} maj_{ρ} y.

(iii) For ρ = τρ_{k} … ρ_{1} :

x^{∗} maj_{ρ} x ↔ ∀y_{1}^{∗}, y_{1}, …, y_{k}^{∗}, y_{k}( ⋀_{i=1}^{k}(y_{i}^{∗} maj_{ρ_{i}} y_{i}) → x^{∗}\underline{y}^{∗} maj_{τ} x\underline{y}).

Proof: Induction on the type respectively on k. □

Definition 4.5 Define φ^{1(1)} by recursion (using only R_{0}) such that

\begin{matrix}φ(x^{1}, 0) =_{0} x0 \\ φ(x, z + 1) =_{0} max_{0}(φ(x, z), x(z + 1)), \end{matrix}

where max_{0} is the usual (primitive recursively definable) maximum between natural numbers. We write x^{M} := λz^{0}.φ(x, z) (note that x^{M}(z) = max_{i≤z}(x(i))).

This definition easily extends to finite types by λ-abstraction: For x of type ρ0 with ρ = 0ρ_{k} … ρ_{1} we define x^{M} := λz, \underline{v}.φ(λz.xz\underline{v}, z), where \underline{v} = v_{1}^{ρ_{1}}, …, v_{k}^{ρ_{k}}.

One easily proves the following

Lemma 4.6 WE-HA^{ω} ⊢ ∀x^{ρ0}(x^{M}0 =_{ρ} x0 ∧ x^{M}(z + 1) =_{ρ} max_{ρ}(x^{M}z, x(z + 1))), where max_{τρ}(x_{1}, x_{2}) :≡ λy^{ρ}. max_{τ}(x_{1}y, x_{2}y) for complex types.

Remark 4.7 Using recursion of type ρ one can define x^{M} directly by iteration of max_{ρ}. However our a bit more complicated approach shows that actually R_{0} is sufficient.

Lemma 4.8 WE-HA^{ω} ⊢ ∀x^{ρ0}, x̃^{ρ0}(∀n^{0}(x̃n maj_{ρ} xn) → x̃^{M} maj_{ρ0}x).

Proof: Let ρ = 0ρ_{k} … ρ_{1} and \underline{v} = v_{1}^{ρ_{1}}, …, v_{k}^{ρ_{k}}. One easily shows by (quantifier-free) induction on n that

∀n^{0}(∀m ≤ n(x̃^{M}n\underline{v} ≥_{0} x̃m\underline{v})).

Together with the assumption that ∀n(x̃n maj_{ρ} xn) this yields

∀n, m, \underline{v}^{∗}, \underline{v}(n ≥_{0} m ∧ \underline{v}^{∗} maj \underline{v} → x̃^{M}n\underline{v}^{∗} ≥_{0} xm\underline{v})

and hence x̃^{M} maj_{ρ} x. □

Corollary 4.9 WE-HA^{ω} ⊢ ∀x^{1}(x^{M} maj_{1} x).

Proposition 4.10 (W.A. Howard [24]) For each closed term t^{ρ} of WE-HA^{ω} one can construct a closed term t^{∗^{ρ}} of WE-HA^{ω} such that

WE-HA^{ω} ⊢ t^{∗} maj_{ρ} t.

Proof: Induction on the structure of t: Constants c: 0^{0} maj_{0} 0^{0}, S maj_{1} S. Using lemma 4.4(iii) we also have Π_{ρ,τ} maj Π_{ρ,τ} and Σ_{δ,ρ,τ} maj Σ_{δ,ρ,τ}. By induction on x^{0} one shows (using again lemma 4.4(iii))

∀x^{0}(R_{ρ}x maj R_{ρ}x).

Hence by lemma 4.8

R^{∗} := R_{ρ}^{M} maj R_{ρ}.

So for every constant c of WE-HA^{ω} we have a closed term t^{∗} such that

WE-HA^{ω} ⊢ t^{∗} maj c.

The proposition now follows from that fact that t^{∗} maj_{τρ} t∧s^{∗} maj_{ρ} s implies t^{∗}s^{∗} maj_{τ} ts. □

Theorem 4.11 ([28]) H^{ω}:=E-HA^{ω} {+ \atop −} AC {+ \atop −} IP_{ef}. Let s be a closed term, A(x, y, z) a formula containing only x, y, z as free variables and deg(τ) ≤ 2. Then the following rule holds:

\{ \begin{matrix}H^{ω} ⊢ ∀x^{1}∀y ≤_{ρ} sx∃z^{τ}A(x, y, z) ⇒ \\ H^{ω} ⊢ ∀x^{1}∀y ≤_{ρ} sx∃z ≤_{τ} tx A(x, y, z), \end{matrix}

where t is a suitable closed term which can be extracted from a given proof of the assumption.

Remark 4.12 Note that in the previous theorem the bound tx on ‘∃z’ does not depend on y.

Corollary 4.13 (Fan Rule [66]) Let A be a formula of E-HA^{ω} containing only free variables of type levels ≤ 1. Then for H^{ω} as above the following rule holds

\{ \begin{matrix}H^{ω} ⊢ ∀x ≤_{1} y∃n^{0}A(x, n) ⇒ \\ H^{ω} ⊢ ∃m^{0}∀x ≤_{1} y∃n ≤_{0} m A(x, n). \end{matrix}

Proof of the theorem 4.11: Suppose that

H^{ω} ⊢ ∀x^{1}∀y ≤_{ρ} sx∃z^{τ}A(x, y, z).

Then by corollary 3.14,2)-4) one can extract a closed term t such that

H^{ω} ⊢ ∀x^{1}∀y ≤_{ρ} sx A(x, y, txy).

By proposition 4.10 there are closed terms s^{∗}, t^{∗} such that

E-HA^{ω} ⊢ s^{∗} maj s ∧ t^{∗} maj t.

By lemma 4.4 we have in E-HA^{ω}:

∀x^{1}(s^{∗}x^{M} maj_{ρ} sx)

and therefore

∀x^{1}∀y ≤_{ρ} sx(s^{∗}x^{M} maj_{ρ} y).

Hence

∀x^{1}∀y ≤_{ρ} sx(t^{∗}(x^{M}, s^{∗}x^{M}) maj_{τ} txy).

For simplicity lets now consider only the case τ = 2:

∀x^{1}∀y ≤_{ρ} sx∀z^{1}((t^{∗}(x^{M}, s^{∗}x^{M}))z^{M} ≥_{0} txyz).

Hence

∀x^{1}∀y ≤_{ρ} sx(t̃x ≥_{2} txy),

where t̃:= λx, z.[(t^{∗}(x^{M}, s^{∗}x^{M}))(z^{M})]. Thus t̃ satisfies the claim of the theorem. □

For further applications of modified realizability combined with majorization see [38].

Exercises:

Define the type-structure S^{ω} of all set-theoretic functionals as follows:

S_{0} := IN

S_{τρ} := { all set-theoretic functionals φ : S_{ρ} → S_{τ} }

S^{ω} := ⋃_{ρ∈T} S_{ρ}.

It is clear that S^{ω} is a model of E-HA^{ω}. We can relativize ‘maj’ to S^{ω}. In the following we refer to this majorizability in S^{ω}.

1) Construct a functional φ^{2} ∈ S_{2} such that no functional φ^{∗} ∈ S_{2} exists with φ^{∗} maj φ (not even on primitive recursive arguments).

2) Show that if φ ∈ S_{2} is continuous (in the sense of the Baire space), then it can be majorized by a suitable φ^{∗} ∈ S_{2}.

Gödel’s functional (‘Dialectica-’)interpretation

Chapter 5. Functional Interpretation

The Gödel functional interpretation, introduced in [17], assigns to each formula A(\underline{a}) of WE-HA^{ω} a formula A^{D} ≡ ∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}, \underline{a}), where A_{D} is quantifier-free (and hence decidable) and \underline{x}, \underline{y} are tuples of variables of finite type. In contrast to the no-counterexample interpretation, which we briefly discussed in the first lecture, the functional interpretation does not require A to be in prenex normal form and therefore is applicable in an intuitionistic context like WE-HA^{ω} where not every formula is provably equivalent to a prenex one. In the next lecture we will introduce a translation of the classical variant WE-PA^{ω} of WE-HA^{ω} (i.e. WE-HA^{ω} plus the tertium-non-datur schema A ∨ ¬A) into WE-HA^{ω}, the so-called negative translation A ↦ A′ due to [16]. We will see that the composition of ′ and D, A ↦ (A′)^{D} provides a very subtle constructive interpretation of A which faithfully reflects the proof-theoretic and computational strength of A (in contrast to the no-counterexample interpretation of (a prenex normal form of) A which in general is a much weaker interpretation and can be established as a particular corollary of the functional interpretation). The price to be paid for this is the necessity to use functionals of arbitrary finite types already for A ∈ L(PA). Moreover the functional interpretation is much more involved than the modified realizability interpretation but has the crucial benefit that it trivially interprets the Markov principle M^{ω} which has no constructive modified realizability interpretation as we have seen. It is this fact which makes the composition of negative translation and functional interpretation a powerful tool of extractive proof theory for classical non-constructive proofs. Note that in contrast to this the combination of negative translation and modified realizability interpretation \underline{x} mr A′ would be useless since A′ is an ∃-free formula and therefore (\underline{x} mr A′) ≡ A′ where \underline{x} is the empty tuple.^{1} Functional interpretation has the same nice behaviour with respect to the logical deduction rules as the modified realizability interpretation.

Motivation of the functional interpretation:

The definition of A^{D} (like \underline{x} mr A) proceeds by induction on the logical structure of A (i.e. the length and the types of \underline{x}, \underline{y} only depend on the logical structure of A). The most interesting and difficult case again is the implication whose treatment we are going to motivate now: Suppose we have already defined the functional interpretations A^{D} ≡ ∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}) and B^{D} ≡ ∃\underline{u}∀\underline{v} B_{D}(\underline{u}, \underline{v}). We are trying to define (A → B)^{D} : First consider

(A^{D} → B^{D}) ≡ (∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}) → ∃\underline{u}∀\underline{v} B_{D}(\underline{u}, \underline{v})).

Our strategy to obtain from this a formula of the form ∃\underline{a}∀\underline{b}(A → B)_{D} (with (A → B)_{D} quantifier-free) is to transform (A^{D} → B^{D}) into prenex normal form and then to apply the axiom of choice AC. It is an easy exercise to verify that there are four different prenex normal forms of A^{D} → B^{D}. We try to choose the most constructive (or rather: the least non-constructive) one:

1One can however use modified realizability in connection with the negative translation if one applies the so-called Friedman-Dragalin A-translation as an intermediate step. See lecture 7 below.

For the first step we have two possibilities:

\begin{matrix}∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}) → ∃\underline{u}∀\underline{v} B_{D}(\underline{u}, \underline{v}) \\ ↦ \{ \begin{matrix}(1) ∀\underline{x}(∀\underline{y} A_{D}(\underline{x}, \underline{y}) → ∃\underline{u}∀\underline{v} B_{D}(\underline{u}, \underline{v})) \\ (2) ∃\underline{u}(∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}) → ∀\underline{v} B_{D}(\underline{u}, \underline{v})). \end{matrix} \end{matrix}

Here the choice is obvious: the passage to (1) is intuitionistically valid, whereas the passage to (2) not even holds in IL^{ω}+ IP_{ef}^{ω}+ M^{ω}. ¿From (1) there are two ways to proceed further:

(1) ↦ \{ \begin{matrix}(1.1) ∀\underline{x}∃\underline{u}(∀\underline{y} A_{D}(\underline{x}, \underline{y}) → ∀\underline{v} B_{D}(\underline{u}, \underline{v})) \\ (1.2) ∀\underline{x}∃\underline{y}(A_{D}(\underline{x}, \underline{y}) → ∃\underline{u}∀\underline{v} B_{D}(\underline{u}, \underline{v})). \end{matrix}

This time the choice is more difficult since both implications (1) → (1.1) and (1) → (1.2) are not provable in IL^{ω}. So we have to compromise our goal to use only strictly constructive transformation steps. However the first implication only requires a weak form of IP_{ef}^{ω} (for purely universal formulas A) in addition to IL^{ω} which has some constructive justification by the results of lecture 3. So lets choose (1.1). ¿From there we have two possibilities to finish our prenexation:

(1.1) ↦ \{ \begin{matrix}(1.1.1) ∀\underline{x}∃\underline{u}∀\underline{v}∃\underline{y}(A_{D}(\underline{x}, \underline{y}) → B_{D}(\underline{u}, \underline{v})) \\ (1.1.2) ∀\underline{x}∃\underline{u}∃\underline{y}∀\underline{v}(A_{D}(\underline{x}, \underline{y}) → B_{D}(\underline{u}, \underline{v})). \end{matrix}

Again the choice is not obvious: both implications are not provable in IL^{ω}. Lets consider (1.1) → (1.1.1) first: The first step to

∀\underline{x}∃\underline{u}∀\underline{v}(∀\underline{y} A_{D}(\underline{x}, \underline{y}) → B_{D}(\underline{u}, \underline{v}))

is perfectly valid from an intuitionistic point of view. However from there we – intuitionistically – only get

∀\underline{x}∃\underline{u}∀\underline{v}¬¬∃\underline{y}(A_{D}(\underline{x}, \underline{y}) → B_{D}(\underline{u}, \underline{v}))

and so need the Markov-principle M^{ω} to obtain (1.1.1). For (1.1) → (1.1.2) the first step to

∀\underline{x}∃\underline{u}∃\underline{y}(A_{D}(\underline{x}, \underline{y}) → ∀\underline{v} B_{D}(\underline{u}, \underline{v}))

is not intuitionistically valid but again only the passage to the weaker

∀\underline{x}∃\underline{u}¬¬∃\underline{y}(A_{D}(\underline{x}, \underline{y}) → ∀\underline{v} B_{D}(\underline{u}, \underline{v})).

However this time not even M^{ω} suffices to get rid of ¬¬ since ‘A_{D}(\underline{x}, \underline{y}) → ∀\underline{v} B_{D}(\underline{u}, \underline{v})’ is not quantifier-free. So the implication ‘(1.1) → (1.1.1)’ is less non-constructive than ‘(1.1) → (1.1.2)’. Hence we now ‘officially’ choose (1.1.1) as our prenex normal form of A^{D} → B^{D}. Applying AC to (1.1.1) we finally obtain

(A → B)^{D} :≡ ∃\underline{U}, \underline{Y} ∀\underline{x}, \underline{v}( \underbrace{A_{D}(\underline{x}, \underline{Y} \underline{x} \underline{v}) → B_{D}(\underline{U} \underline{x}, \underline{v})}_{(A→B)_{D}:≡}).

Despite of the fact that we had to make various compromises to end up with (A → B)^{D}, this interpretation works while any of the remaining three prenex normal forms of A^{D} → B^{D} would result in a definition of (A → B)^{D} which even for B :≡ A in general would fail to have a constructive (computable) realization (exercise).

Definition 5.1 (Gödel [17]) To every formula A of WE-HA^{ω} we assign a translation A^{D} ≡ ∃\underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}) in the same language. The free variables of A^{D} are that of A. The types and length of \underline{x}, \underline{y} depend only on the logical structure of A. A_{D} is a quantifier-free formula.

(i) A^{D} :≡ A_{D} :≡ A for prime formulas A.

(ii) (A ∧ B)^{D} :≡ ∃\underline{x}, \underline{u}∀\underline{y}, \underline{v}[A ∧ B]_{D} :≡ ∃\underline{x}, \underline{u}∀\underline{y}, \underline{v}[A_{D}(\underline{x}, \underline{y}) ∧ B_{D}(\underline{u}, \underline{v})],

(iii) (A ∨ B)^{D} :≡ ∃z^{0}, \underline{x}, \underline{u}∀\underline{y}, \underline{v}[A ∨ B]_{D} :≡ ∃z^{0}, \underline{x}, \underline{u}∀\underline{y}, \underline{v}[(z = 0 → A_{D}(\underline{x}, \underline{y})) ∧ (z ≠ 0 → B_{D}(\underline{u}, \underline{v}))],

Chapter 5. Functional Interpretation

(iv) (∃z^{ρ}A(z))^{D} :≡ ∃z, \underline{x}∀\underline{y}(∃z A(z))_{D} :≡ ∃z, \underline{x}∀\underline{y} A_{D}(\underline{x}, \underline{y}, z),

(v) (∀z^{ρ}A(z))^{D} :≡ ∃\underline{X}∀z, \underline{y}(∀z A(z))_{D} :≡ ∃\underline{X}∀z, \underline{y} A_{D}(\underline{X}z, \underline{y}, z), (vi) (A → B)^{D} :≡ ∃\underline{U}, \underline{Y} ∀\underline{x}, \underline{v}(A_{D}(\underline{x}, \underline{Y} \underline{x} \underline{v}) → B_{D}(\underline{U} \underline{x}, \underline{v})),

(A → B)_{D} :≡ (A_{D}(\underline{x}, \underline{Y} \underline{x} \underline{v}) → B_{D}(\underline{U} \underline{x}, \underline{v})). Remark 5.2 As a consequence of the treatment of implication we obtain

(i) (¬A)^{D} ≡ ∃\underline{Y} ∀\underline{x}¬A_{D}(\underline{x}, \underline{Y} \underline{x}), (ii) (¬¬A)^{D} ≡ ∃\underline{X}∀\underline{Y} ¬¬A_{D}(\underline{X} \underline{Y} , \underline{Y} (\underline{X} \underline{Y})) ↔ ∃\underline{X}∀\underline{Y} A_{D}(\underline{X} \underline{Y} , \underline{Y} (\underline{X} \underline{Y})),

where the equivalence is provable in WE-HA^{ω}. Definition 5.3 The independence-of-premise schema IP_{∀}^{ω} for universal premises is the union (for all types) of

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

where \underline{y} not free in ∀\underline{x} A_{0}(\underline{x}). Theorem 5.4 (soundness of functional interpretation [17],[65])

WE-HA^{ω}+ AC + IP_{∀}^{ω}+ M^{ω} ⊢ A(\underline{a}), then

WE-HA^{ω} ⊢ ∀\underline{y} A_{D}(\underline{t} \underline{a}, \underline{y}, \underline{a}),

where \underline{t} is a suitable tuple of closed terms of WE-HA^{ω} which can be extracted from a given proof of the assumption. Proof: As in the proof of the soundness theorem for modified realizability we proceed by induction on the length of the derivation.

1) Logical axioms and rules: We will discuss only two axioms and two rules to give an idea of the general proof (for full details see [65],[52]). \underline{A → A ∧ A}:

(A → A ∧ A)^{D} ≡ (∃\underline{x}∀\underline{y}A_{D}(\underline{x}, \underline{y}, \underline{a}) → ∃\underline{x}′, \underline{x}′′∀\underline{y}′, \underline{y}′′(A_{D}(\underline{x}′, \underline{y}′, \underline{a}) ∧ A_{D}(\underline{x}′′, \underline{y}′′, \underline{a})))^{D} ∃\underline{Y} , \underline{X}′, \underline{X}′′∀\underline{x}, \underline{y}′, \underline{y}′′(A_{D}(\underline{x}, \underline{Y} \underline{x} \underline{y}′\underline{y}′′, \underline{a}) → A_{D}(\underline{X}′\underline{x}, \underline{y}′, \underline{a}) ∧ A_{D}(\underline{X}′′\underline{x}, \underline{y}′′, \underline{a})). Hence

\begin{matrix}\underline{t}\underline{X}′ := \underline{t}\underline{X}′′ := λ\underline{a}, \underline{x}.\underline{x} \\ \underline{t}\underline{Y} \underline{a} \underline{x} \underline{y}′\underline{y}′′ := \{ \begin{matrix}\underline{y}′, if t_{A_{D}} \underline{x} \underline{y}′\underline{a} ≠ 0 \\ \underline{y}′′, if t_{A_{D}} \underline{x} \underline{y}′\underline{a} = 0, \end{matrix} \end{matrix}

satisfy the functional interpretation of A → A ∧ A (here t_{A_{D}} is a closed term of WE-HA^{ω} such that WE-HA^{ω} ⊢ t_{A_{D}} \underline{x} \underline{y} \underline{a} =_{0} 0 ↔ A_{D}(\underline{x}, \underline{y}, \underline{a})). \underline{A → A ∨ B} :

(A → A ∨ B)^{D} ≡ (∃\underline{x}∀\underline{y}A_{D}(\underline{x}, \underline{y}, \underline{a}) →

∃z^{0}, \underline{x}′, \underline{u}∀\underline{y}′, \underline{v}((z = 0 → A_{D}(\underline{x}′, \underline{y}′, \underline{a})) ∧ (z ≠ 0 → B_{D}(\underline{u}, \underline{v}, \underline{a}′))))^{D} ≡ ∃\underline{Y} , Z, \underline{X}′, \underline{U}∀\underline{x}, \underline{y}′, \underline{v}(A_{D}(\underline{x}, \underline{Y} \underline{x} \underline{y}′\underline{v}, \underline{a}) →

((Z\underline{x} = 0 → A_{D}(\underline{X}′\underline{x}, \underline{y}′, \underline{a})) ∧ (Z\underline{x} ≠ 0 → B_{D}(\underline{U} \underline{x}, \underline{v}, \underline{a}′)))). Hence \underline{t}\underline{Y} := λ˜\underline{a}, \underline{x}, \underline{y}′, \underline{v}.\underline{y}′, t_{Z} := λ˜\underline{a}, \underline{x}.0^{0}, \underline{t}\underline{X}′ := λ˜\underline{a}, \underline{x}.\underline{x}, \underline{t}\underline{U} := λ˜\underline{a}, \underline{x}.\underline{O}, where ˜ \underline{a} = \{\underline{a}\} ∪ \{\underline{a}′\}, satisfy the functional interpretation of A → A ∨ B. The modus ponens rule: Assume

(1) ∀\underline{y}A_{D}(\underline{t}_{1}\underline{a}, \underline{y}, \underline{a})

and

(2) ∀\underline{x}, \underline{v}(A_{D}(\underline{x}, \underline{t}_{2}˜\underline{a} \underline{x} \underline{v}, \underline{a}) → B_{D}(\underline{t}_{3}˜\underline{a} \underline{x}, \underline{v}, \underline{a}′)),

where again ˜ \underline{a} = \{\underline{a}\} ∪ \{\underline{a}′\}. We have to construct \underline{t}_{4} such that

∀\underline{v} B_{D}(\underline{t}_{4}\underline{a}′, \underline{v}, \underline{a}′).

Apply (1) to \underline{y} := \underline{t}_{2}˜\underline{a} \underline{x} \underline{v}, then (3) ∀\underline{x}, \underline{v}A_{D}(\underline{t}_{1}\underline{a}, \underline{t}_{2}˜\underline{a} \underline{x} \underline{v}, \underline{a}).

Apply (2) and (3) to \underline{x} := \underline{t}_{1}\underline{a}. Then

(4) ∀\underline{v}(A_{D}(\underline{t}_{1}\underline{a}, \underline{t}_{2}(˜\underline{a}, \underline{t}_{1}\underline{a}, \underline{v}), \underline{a}) → B_{D}(\underline{t}_{3}(˜\underline{a}, \underline{t}_{1}\underline{a}), \underline{v}, \underline{a}′))

and

(5) ∀\underline{v} A_{D}(\underline{t}_{1}\underline{a}, \underline{t}_{2}(˜\underline{a}, \underline{t}_{1}\underline{a}, \underline{v}), \underline{a}).

Hence

(6) ∀\underline{v}B_{D}(\underline{t}_{3}(˜\underline{a}, \underline{t}_{1}\underline{a}), \underline{v}, \underline{a}′).

Let \underline{t}[\underline{a}′] be the result of replacing all variables a_{i} in \underline{t}_{3}(˜\underline{a}, \underline{t}_{1}\underline{a}) which do not occur in \underline{a}′ by O of appropriate type. Then \underline{t}_{4} := λ\underline{a}′.\underline{t}[\underline{a}′] does the job.

The rule \frac{A→B , B→C}{A→C} : For notational simplicity we omit the free parameters this time. Assume

(1) ∀\underline{x}, \underline{v}(A_{D}(\underline{x}, \underline{t}_{1}\underline{x} \underline{v}) → B_{D}(\underline{t}_{2}\underline{x}, \underline{v}))

and

(2) ∀\underline{u}, \underline{w}(B_{D}(\underline{u}, \underline{t}_{3}\underline{u} \underline{w}) → C_{D}(\underline{t}_{4}\underline{u}, \underline{w})).

We have to construct \underline{t}_{5}, \underline{t}_{6} such that

∀\underline{x}, \underline{w}(A_{D}(\underline{x}, \underline{t}_{5}\underline{x} \underline{w}) → C_{D}(\underline{t}_{6}\underline{x}, \underline{w})).

Apply (1) to \underline{v} = \underline{t}_{3}(\underline{t}_{2}\underline{x}, \underline{w}) and (2) to \underline{u} = \underline{t}_{2}\underline{x}. Then

(3) ∀\underline{x}, \underline{w}(A_{D}(\underline{x}, \underline{t}_{1}(\underline{x}, \underline{t}_{3}(\underline{t}_{2}\underline{x}, \underline{w}))) → C_{D}(\underline{t}_{4}(\underline{t}_{2}\underline{x}), \underline{w})).

Hence

\underline{t}_{5} := λ\underline{x}, \underline{w}.\underline{t}_{1}(\underline{x}, \underline{t}_{3}(\underline{t}_{2}\underline{x}, \underline{w})), \underline{t}_{6} := λ\underline{x}.\underline{t}_{4}(\underline{t}_{2}\underline{x})

do the job.

2) Axioms for =_{0}, S, Π, Σ, R: These purely universal axioms are identical with their own functional interpretation.

3) The quantifier-free extensionality rule QF-ER: Both the premise and the conclusion are purely universal and so are identical to their functional interpretation.^{2} 4) The schema of induction: It is easier to use the equivalent induction rule: Let B(y^{0})^{D} ≡ ∃\underline{u}∀\underline{v}B_{D}(\underline{u}, \underline{v}, y, \underline{a}) and assume that we have already proved

2We may assume that A_{0} in QF-ER does not contain any ∨, since A_{0}(\underline{x}) can be written as t\underline{x} =_{0} 0 in WE-HA^{ω}.

\{ \begin{matrix}∀\underline{v} B_{D}(\underline{t}_{1}\underline{a}, \underline{v}, 0, \underline{a}) and \\ ∀\underline{u}, \underline{w}(B_{D}(\underline{u}, \underline{t}_{2}y \underline{a} \underline{u} \underline{w}, y, \underline{a}) → B_{D}(\underline{t}_{3}y \underline{a} \underline{u}, \underline{w}, y + 1, \underline{a})). \end{matrix}

Define \underline{t} by simultaneous primitive recursion in higher types such that

\{ \begin{matrix}\underline{t}(\underline{a}, 0) = \underline{t}_{1}\underline{a} \\ \underline{t}(\underline{a}, y + 1) = \underline{t}_{3}(y, \underline{a}, \underline{t}(\underline{a}, y)). \end{matrix}

Then

\{ \begin{matrix}∀\underline{v}B_{D}(\underline{t}(\underline{a}, 0), \underline{v}, 0, \underline{a}) and \\ ∀\underline{w}(B_{D}(\underline{t}(\underline{a}, y), \underline{t}_{2}(y, \underline{a}, \underline{t}(\underline{a}, y), \underline{w}), y, \underline{a}) → B_{D}(\underline{t}(\underline{a}, y + 1), \underline{w}, y + 1, \underline{a})) \end{matrix}

and therefore

\{ \begin{matrix}∀\underline{v}B_{D}(\underline{t}(\underline{a}, 0), \underline{v}, 0, \underline{a}) and \\ ∀\underline{v}B_{D}(\underline{t}(\underline{a}, y), \underline{v}, y, \underline{a}) → ∀\underline{v}B_{D}(\underline{t}(\underline{a}, y + 1), \underline{v}, y + 1, \underline{a}). \end{matrix}

Hence by the induction rule we obtain

∀\underline{v}B_{D}(\underline{t}(\underline{a}, y), \underline{v}, y, \underline{a}).

5) The functional interpretations of AC, M^{ω} and IP_{∀}^{ω} only need simple λterms and can be verified already in WE-HA^{ω} without the use of AC, M^{ω} and IP_{∀}^{ω}. □

Warning: The soundness theorem does not hold for E-HA^{ω}(see [24]).

Remark 5.5 Gödel actually established the conclusion of the soundness theorem in (an intensional variant of) a quantifier-free fragment qf-(WE-HA^{ω}) of WE-HA^{ω} which results if quantifiers are omitted from the language, the axiom schema of induction is replaced by a quantifier-free rule of induction

QF-IR : \frac{A_{0}(0) , A_{0}(x^{0}) → A_{0}(x + 1)}{A_{0}(x)}

and a substitution rule

Sub : \frac{A(x^{ρ})}{A(t^{ρ})}

(replacing ∀-elimination) is added. To verify A_{D}(\underline{t} \underline{a}, \underline{y}, \underline{a}) in qf-(WE-HA^{ω}) requires a somewhat more complicated treatment of induction (see e.g. [65]).

Definition 5.6 ([65]) The subset Γ_{2} of formulas ∈ L(WE-HA^{ω}) is defined inductively by

1) Prime formulas are in Γ_{2}.

2) A, B ∈ Γ_{2} ⇒ A ∧ B, A ∨ B, ∀x A(x), ∃x A(x) ∈ Γ_{2}.

3) If A is purely universal and B ∈ Γ_{2}, then (∃\underline{x}A → B) ∈ Γ_{2}.

Lemma 5.7 For A ∈ Γ_{2} one has WE-HA^{ω} ⊢ A^{D} → A.

Proof: Easy induction on the logical structure of A. □

Corollary 5.8 WE-HA^{ω}+ AC + IP_{∀}^{ω}+ M^{ω} is conservative over WE-HA^{ω} with respect to formulas A ∈ Γ_{2}.

Proof: The corollary follows from theorem 5.4 and lemma 5.7. □

Proposition 5.9 For all formulas A of WE-HA^{ω} one has

WE-HA^{ω}+ AC + IP_{∀}^{ω}+ M^{ω} ⊢ A ↔ A^{D}.

Proof: Easy induction on the logical structure of A. □

Corollary 5.10 WE-HA^{ω}+ AC + IP_{∀}^{ω}+ M^{ω} has the disjunction property DP, the existence property EP and is closed under the rules of choice ACR and of independence-of-premise for purely universal formulas IPR_{∀}^{ω}.

Proof: The corollary follows similarly to corollary 3.14 but with theorem 5.4 and proposition 5.9 instead of modified realizability with truth. □

An application of functional interpretation and majorization

Definition 5.11 (hereditarily extensional equality [65])

\{ \begin{matrix}x_{1} ≈_{0} x_{2} :≡ (x_{1} =_{0} x_{2}), \\ x_{1} ≈_{τρ} x_{2} :≡ ∀y_{1}^{ρ}, y_{2}^{ρ}(y_{1} ≈_{ρ} y_{2} → x_{1}y_{1} ≈_{τ} x_{2}y_{2}). \end{matrix}

Lemma 5.12 WE-HA^{ω} ⊢ x_{1} =_{ρ} x̃_{1} ∧ x_{2} =_{ρ} x̃_{2} ∧ x_{1} ≈_{ρ} x_{2} → x̃_{1} ≈_{ρ} x̃_{2}.

Proof: Induction on ρ. □

Proposition 5.13 Let t^{ρ} be a closed term of WE-HA^{ω}. Then

WE-HA^{ω} ⊢ t ≈_{ρ} t.

Proof: Induction on the structure of t.

(i) Constants: One easily verifies that 0^{0} ≈_{0} 0^{0}, S ≈_{1} S, Π_{ρ,τ} ≈ Π_{ρ,τ}, Σ_{δ,ρ,τ} ≈ Σ_{δ,ρ,τ}. R_{ρ}: We show by induction on x^{0} that R_{ρ}x ≈ R_{ρ}x: Suppose that y_{1} ≈ y_{2}, z_{1} ≈ z_{2}: R_{ρ}0y_{1}z_{1} = y_{1} ≈ y_{2} = R_{ρ}0y_{2}z_{2} ⇒ R_{ρ}0y_{1}z_{2} ≈ R_{ρ}0y_{2}z_{2}.

R_{ρ}(x + 1)y_{1}z_{1} = z_{1}(R_{ρ}xy_{1}z_{1})x ≈^{I.H.} z_{2}(R_{ρ}xy_{2}z_{2})x = R_{ρ}(x + 1)y_{2}z_{2}

⇒ R_{ρ}(x + 1)y_{1}z_{1} ≈ R_{ρ}(x + 1)y_{2}z_{2}. Since x_{1} =_{0} x_{2} ↔ x_{1} ≈_{0} x_{2}, we have by =_{0}-axioms

∀x_{1}, x_{2}(x_{1} ≈_{0} x_{2} → R_{ρ}x_{1} ≈ R_{ρ}x_{2}),

i.e. R_{ρ} ≈ R_{ρ}. (ii) t ≈_{τρ} t ∧ s ≈_{ρ} s → ts ≈_{τ} ts. □

Corollary 5.14 Let t^{1(1)} be a closed term of WE-HA^{ω}. Then

WE-HA^{ω} ⊢ ∀x^{1}, y^{1}(x =_{1} y → tx =_{1} ty).

Proof: This follows from proposition 5.13 since WE-HA^{ω} ⊢ x =_{1} y ↔ x ≈_{1} y. □

Proposition 5.15 Let t^{1(1)} be closed. Then t^{1(1)} is uniformly continuous on each set {x : x ≤_{1} y} with a modulus of uniform continuity which is definable in WE-HA^{ω} (uniformly in y), i.e. there is a closed term t̃^{0(1)(0)} of WE-HA^{ω}:

WE-HA^{ω} ⊢ ∀k^{0}∀x_{1}, x_{2} ≤_{1} y( ⋀_{i=0}^{t̃ky}(x_{1}i =_{0} x_{2}i) → ⋀_{j=0}^{k}(tx_{1}j =_{0} tx_{2}j)).

Proof [28]: By the corollary above we have

WE-HA^{ω} ⊢ ∀x_{1}, x_{2}(∀i(x_{1}i =_{0} x_{2}i) → ∀k∀j ≤ k(tx_{1}j =_{0} tx_{2}j)).

Hence

WE-HA^{ω} + M^{ω} ⊢ ∀k∀x_{1}, x_{2}∃i(x_{1}i =_{0} x_{2}i → ⋀_{j=0}^{k}(tx_{1}j =_{0} tx_{2}j)).

By theorem 5.4 there exists a term t̂ such that

WE-HA^{ω} ⊢ ∀k∀x_{1}, x_{2}(x_{1}(t̂kx_{1}x_{2}) =_{0} x_{2}(t̂kx_{1}x_{2}) → ⋀_{j=0}^{k}(tx_{1}j =_{0} tx_{2}j)).

By proposition 4.10 there exists a closed term t̂^{∗} such that

WE-HA^{ω} ⊢ t̂^{∗} maj t̂

and hence by lemma 4.4

WE-HA^{ω} ⊢ ∀k∀x_{1}, x_{2} ≤_{1} y(t̂^{∗}ky^{M}y^{M} ≥_{0} t̂kx_{1}x_{2}).

So t̃:= λk^{0}, y^{1}.t̂^{∗}ky^{M}y^{M} does the job. □

Exercises:

1) Solve the functional interpretation of

¬¬(∃xA_{0}(x) ∨ ¬∃xA_{0}(x))

by a closed term of WE-HA^{ω}.

2) In addition to the prenex normal form we used in the definition of (A → B)^{D}, there are three more prenex normal forms of (A^{D} → B^{D}) which give rise to corresponding functional interpretations (A → B)^{i} (i = 1, 2, 3) of A → B.

For all three of them already (A → A)^{i} fails to have a computable solution for suitable A.

Compute these interpretations (A → B)^{i} and give a counterexample to the computable solvability of (A → A)^{i} for at least one of them.

Suggested further reading: [17] (the original paper which introduced functional interpretation; an English translation with extended introductory notes by A.S. Troelstra can be found in [18]), [65] (chapter 3, section 5; this is a very concise and compact treatment of functional interpretation), [52] (covers in detail C. Spector’s extension of functional interpretation to analysis by means of bar recursion), [1] (a very readable and comprehensive treatment of the whole subject). [5] contains an interesting discussion about the functional interpretation of ‘→’ from a constructive point of view. Applications of functional interpretation to systems of bounded arithmetic are given in [9]. For further applications of functional interpretation combined with majorization see [30],[33],[34],[35],[36],[37]. For applications of functional interpretation (and majorization) in the context of approximation theory see [31],[32].

Negative translation and its use combined with functional interpretation

There are several interpretations – so-called ‘negative’ or ‘double-negation’ translations – of classical logic as well as many theories based on classical logic into their intuitionistic variant. All these translations A ↦ A′ have in common that A′ is (or is intuitionistically equivalent to) a negative formula. The first such translation is due to Gödel [16] (although G. Gentzen independently discovered a similar translation). There is some preceding work by Kolmogorov [41] and Glivenko [15]. Two further variants of Gödel’s translation are due to Kuroda [50] and it his one of these which we will adopt here:

Definition 6.1 Let A be a formula in a theory based on L(IL^{ω}). A′ is defined as A′ :≡ ¬¬A^{∗}, where A^{∗} is defined by induction on the logical structure of A:

(i) A^{∗} :≡ A, if A is a prime formula,

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

(iii) (∃x^{ρ}A(x))^{∗} :≡ ∃x^{ρ}(A(x))^{∗},

(iv) (∀x^{ρ}A(x))^{∗} :≡ ∀x^{ρ}¬¬(A(x))^{∗}.

Chapter 6. Negative and Functional Interpretation

Definition 6.2 PL^{ω} (WE-PA^{ω}, E-PA^{ω}) is the extension of IL^{ω} (WE-HA^{ω}, E-HA^{ω}) obtained by adding the tertium-non-datur schema A ∨ ¬A.

Proposition 6.3 (i) PL^{ω} ⊢ A ⇒ IL^{ω} ⊢ A′,

(ii) (W)E-PA^{ω} ⊢ A ⇒ (W)E-HA^{ω} ⊢ A′.

Proof: (i) Induction on the length of the derivation: We only treat the tertium-non-datur schema, the modus ponens and the ∀-introduction rule: (A ∨ ¬A)′ ≡ ¬¬(A^{∗} ∨ ¬A^{∗}) which is provable in IL^{ω} (it is an easy exercise that ¬¬(A ∨ ¬A) holds intuitionistically for arbitrary formulas A).

Consider \frac{A , A→B}{B} : By induction hypothesis we have ¬¬A^{∗} and ¬¬(A^{∗} → B^{∗}). By intuitionistic logic we get ¬¬A^{∗} → ¬¬B^{∗} and hence by modus ponens ¬¬B^{∗}, i.e. B′.

Consider \frac{A→B(x)}{A→∀xB(x)} : By induction hypothesis we have ¬¬(A^{∗} → (B(x))^{∗})

and therefore (by intuitionistic logic) A^{∗} → ¬¬(B(x))^{∗}. By ∀-intoduction we obtain A^{∗} → ∀x¬¬(B(x))^{∗}, i.e. (A → ∀xB(x))^{∗} and therefore (A → ∀xB(x))′. (ii) We only have to extend the proof of (i) by the treatment of the nonlogical axioms and rules: The negative translation of the purely universal =_{0}, S, Π, Σ, R-axioms trivially follows from the axioms themselves (note that WE-HA^{ω} ⊢ ¬¬A_{0} ↔ A_{0} and so the translation of purely universal axioms is in fact equivalent (relative to WE-HA^{ω}) to the axioms since intuitionistically ¬¬∀x¬¬A(x) ↔ ∀¬¬A(x)). Similarly the negative translation of (E) (resp. of the premise and the conclusion of QF-ER) can be seen to be equivalent to (E) in WE-HA^{ω}. The induction rule: By the induction hypothesis we have ¬¬(A(0))^{∗} and ¬¬((A(x))^{∗} → (A(x + 1))^{∗}). Hence also ¬¬(A(x))^{∗} → ¬¬(A(x + 1))^{∗}. Thus by the induction rule we obtain ¬¬(A(x))^{∗}, i.e. (A(x))′. □

Definition 6.4 The schema QF-AC of quantifier-free choice is the restriction of AC to quantifier-free formulas A_{0} ≡ A. For convenience we formulate

Chapter 6. Negative and Functional Interpretation

this schema for tuples^{1}:

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

where A_{0} is quantifier-free. Proposition 6.5 WE-PA^{ω}+ QF-AC ⊢ A ⇒ WE-HA^{ω}+ QF-AC +M^{ω} ⊢ A′. Proof: We only have to extend the proof of proposition 6.3 by showing that

WE-HA^{ω}+ QF-AC + M^{ω} ⊢ (QF-AC)′.

We have in WE-HA^{ω}

\begin{matrix}(∀\underline{x}∃\underline{y}A_{0}(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x}A_{0}(\underline{x}, \underline{Y} \underline{x}))′ ↔ \\ (∀\underline{x}¬¬∃\underline{y}A_{0}(\underline{x}, \underline{y}) → ¬¬∃\underline{Y} ∀\underline{x}¬¬A_{0}(\underline{x}, \underline{Y} \underline{x})), \end{matrix}

which clearly 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}),

which in turn follows from M^{ω} and QF-AC. □ Theorem 6.6

WE-PA^{ω}+ QF-AC ⊢ A(\underline{a})

⇒ one can extract closed terms \underline{t} of WE-HA^{ω} such that WE-HA^{ω} ⊢ ∀\underline{y}(A′)_{D}(\underline{t} \underline{a}, \underline{y}, \underline{a}).

Proof: Combine proposition 6.5 with theorem 5.4. □

1Actually one can show in WE-HA^{ω} that finite tuples \underline{x} of variables (of different types)

can be coded together into a single variable x whose type depends on the types of \underline{x} (see [65] for details on that).

Corollary 6.7 Let A_{0}(x, y) be a (quantifier-free) formula of WE-PA^{ω} which only contains x, y as free variables. Then the following rule holds:

WE-PA^{ω}+ QF-AC ⊢ ∀x^{ρ}∃y^{τ}A_{0}(x, y)

⇒ one can extract a closed term t of WE-HA^{ω} such that WE-HA^{ω} ⊢ ∀xA_{0}(x, tx).

Proof:

WE-PA^{ω}+QF-AC ⊢ ∀x∃yA_{0}(x, y) ⇒^{prop.6.5}

WE-HA^{ω}+QF-AC + M^{ω} ⊢ ¬¬∀x¬¬∃yA_{0}(x, y) ⇒^{M^{ω}}

WE-HA^{ω}+QF-AC + M^{ω} ⊢ ∀x∃yA_{0}(x, y) ⇒^{thm.5.4}

WE-HA^{ω} ⊢ ∀xA_{0}(x, tx) for a suitable closed term t

(note that A_{0} can be treated as a prime formula in WE-HA^{ω}). □

Combined with the majorization technique from lecture 4 we obtain Proposition 6.8 ([28]) Let A_{0}(x^{1}, y^{ρ}, z^{τ}) be a (quantifier-free) formula of WE-PA^{ω} containing only x, y, z as free variables, τ ≤ 2 and s be a closed term. Then

WE-PA^{ω}+ QF-AC ⊢ ∀x^{1}∀y ≤_{ρ} sx∃z^{τ}A_{0}(x, y, z)

⇒ one can extract a closed term t of WE-HA^{ω} such that WE-HA^{ω} ⊢ ∀x^{1}∀y ≤_{ρ} sx∃z ≤_{τ} tx A_{0}(x, y, z).

As a further application of corollary 6.7 we obtain the no-counterexample interpretation of PA by terms of WE-HA^{ω}: Proposition 6.9 Let A ∈ L(PA) be a prenex sentence. Then the following rule holds:

PA ⊢ A

⇒ one can extract closed terms \underline{Φ} of WE-HA^{ω} such that WE-HA ⊢ \underline{Φ} n.c.i. A.

Proof: Apply corollary 6.7 to A^{H}. □

Remark 6.10 Strictly speaking PA is not a subsystem of WE-PA^{ω} since we have included symbols for all primitive recursive functions as primitive notions in PA whereas they are defined notions in WE-PA^{ω}. However PA is a subsystem of a corresponding definitorial extension of WE-PA^{ω} to which corollary 6.7 applies as well.

The combination of negative translation and functional interpretation (A′)^{D} is much closer related to A than the no-counterexample interpretation is (for prenex arithmetical A), since the equivalence of A and (A′)^{D} can be proved using only quantifier-free choice (although in higher types) whereas the no-counterexample interpretation of A only implies A in the presence of (number-theoretic) choice for arithmetical formulas:

Proposition 6.11 Let A be an arbitrary formula of WE-PA^{ω}. We may assume that A does not contain ∨ (which can be defined in terms of ∧ and ¬ in WE-PA^{ω}). Then PL^{ω}+ QF-AC ⊢ A ↔ (A′)^{D}.

Proof: Exercise (Hint: Show that PL^{ω}+ QF-AC ⊢ A ↔ A^{D} for ∃-free formulas A). □

Elimination of extensionality

Definition 6.12 We define E^{ρ}(x^{ρ}) and x =_{ρ}^{e} y by induction on ρ :

E^{0}(x) :≡ (x =_{0} x), x =_{0}^{e} y :≡ (x =_{0} y),
E^{τρ}(x) :≡ ∀y, z(y =_{ρ}^{e} z → xy =_{τ}^{e} xz),
x =_{τρ}^{e} y :≡ ∀z^{ρ}(E^{ρ}(z) → xz =_{τ}^{e} yz) ∧ E^{τρ}(x) ∧ E^{τρ}(y).

Definition 6.13 For every formula A of E-PA^{ω} we define a translation A_{e} by relativizing all quantifiers to hereditarily extensional functionals in the sense of E^{ρ}:

(i) A_{e} :≡ A, if A is a prime formula, (ii) (A□B)_{e} :≡ (A_{e}□B_{e}), where □ ∈ {∧, ∨, →}, (iii) (∃x^{ρ}A(x))_{e} :≡ ∃x^{ρ}(E^{ρ}(x) ∧ A_{e}(x)), (iv) (∀x^{ρ}A(x))_{e} :≡ ∀x^{ρ}(E^{ρ}(x) → A_{e}(x)). Proposition 6.14

E-PA^{ω}+ QF-AC^{0,1}+ QF-AC^{1,0} ⊢ A(\underline{a}) ⇒

WE-PA^{ω}+ QF-AC^{0,1}+ QF-AC^{1,0} ⊢ E(\underline{a}) → A_{e}(\underline{a}),

where \underline{a} are all the free variables of A. Proof: See [52]. □ Let ˆ (W)E-PA^{ω}|^{\} ( ˆ (W)E-HA^{ω}|^{\}) be the fragment of (W)E-PA^{ω} ((W)E-HA^{ω}) where we only have the recursor R_{0} for type-0-recursion and the induction schema is restricted to the schema of quantifier-free induction

QF-IA : A_{0}(0) ∧ ∀x^{0}(A_{0}(x) → A_{0}(x + 1)) → ∀x^{0}A_{0}(x).

Lemma 6.15 ŴE-PA^{ω}|^{\}+ QF-AC^{0,0} ⊢ Σ_{1}^{0} -IA, where Σ_{1}^{0}-IA : ∃y^{0}A_{0}(0, y) ∧ ∀x^{0}(∃yA_{0}(x, y) → ∃yA_{0}(x + 1, y)) → ∀x∃yA_{0}(x, y). Proof: Assume ∃y_{0}A_{0}(0, y_{0}) and ∀x, y_{1}∃y_{2}(A_{0}(x, y_{1}) → A_{0}(x + 1, y_{2})). By QF-AC^{0,0} we get

∃f∀x, y_{1}(A_{0}(x, y_{1}) → A_{0}(x + 1, fxy_{1})).

Define

\{ \begin{matrix}Φ(0, y, f) :=_{0} y \\ Φ(x + 1, y, f) :=_{0} f(x, Φ(x, y, f)) \end{matrix}

(note that this can by done by R_{0}). Then by QF-IA one easily shows that

∀xA_{0}(x, Φ(x, y_{0}, f))

for y_{0} such that A_{0}(0, y_{0}) and therefore ∀x∃yA_{0}(x, y). □

Proposition 6.16 ([11])

ŴE-PA^{ω}|^{\} + QF-AC ⊢ A(\underline{a})
⇒ ∃ closed terms \underline{t} of ŴE-HA^{ω}|^{\} such that
ŴE-HA^{ω}|^{\} ⊢ ∀\underline{y}(A′)_{D}(\underline{t} \underline{a}, \underline{y}, \underline{a})

(Here \underline{a} are all of the free variables of A(\underline{a}).

Proof: The proof theorem 6.6 easily relativizes to ŴE-PA^{ω}|^{\}. □

One can show that the function(al)s of types ≤ 2 definable by closed terms in ŴE-HA^{ω}|^{\} are just the usual primitive recursive ones in the sense of Kleene (see [11]). From the proof of this fact combined with the previous proposition plus elimination of extensionality one gets

Proposition 6.17 Let R(x, y) be a primitive recursive relation (in the sense of PRA). Then the following rule holds:

Ê-PA^{ω}|^{\} + QF-AC^{1,0} + QF-AC^{0,1} ⊢ ∀x^{0}∃y^{0}R(x, y)

⇒ ∃ primitive recursive function p such that

P RA ⊢ R(x, px).

Let PA_{1} be the restriction of PA to induction for Σ_{1}^{0}-formulas only.

Corollary 6.18 (Parsons,Mints,Takeuti,...) PA_{1} is Π_{2}^{0}-conservative over PRA.

Extensions to fragments of analysis

An analytical principle which has received great attention during the last 20 years in proof theory is the binary (‘weak’) König’s lemma WKL formalized by the following axiom

\begin{matrix}WKL :≡ \\ ∀f^{1}(T (f) ∧ ∀x^{0}∃n^{0}(lth(n) =_{0} x ∧ f(n) =_{0} 0) → ∃b ≤_{1} 1∀x^{0}(f(\overline{b}x) =_{0} 0)), \end{matrix}

where

T (f) :≡ ∀n^{0}, m^{0}(f(n∗m) = 0 → f(n) = 0)∧∀n^{0}, x^{0}(f(n∗⟨x⟩) = 0 → x ≤ 1)

(here lth, ∗, \overline{b}x, ⟨·⟩ refer to a standard primitive recursive coding of finite sequences of numbers).

The interest in WKL rests on the following facts:

1) Already relative to a second-order fragment RCA_{0} of ŴE-PA^{ω}|^{\}+ QF-AC^{0,0}, WKL proves substantial parts of (non-constructive) classical mathematics and in particular of analysis (see e.g. [12],[62],[63],[6],[7], [25],[59]).

2) Despite of the mathematical strength of WKL, it is weak from the proof-theoretic point of view, namely a classical result due to H. Friedman states that RCA_{0}+ WKL is Π_{2}^{0}-conservative over PRA.

One can use functional interpretation combined with majorization to prove various generalizations of Friedman’s result, e.g.:

Theorem 6.19 ([30]) Let A_{0}(x, y, z) be a (quantifier-free) formula of Ê-PA^{ω}|^{\} containing only x^{1}, y^{1}, z^{0} as free variables and let s be a closed term. Then the following rule holds:

Ê-PA^{ω}|^{\} + QF-AC^{1,0} + QF-AC^{0,1} + WKL ⊢ ∀x^{1}∀y ≤_{1} sx∃z^{0}A_{0}(x, y, z)

⇒ one can extract a primitive recursive (in Kleene’s sense) Φ such that

ŴE-HA^{ω}|^{\} ⊢ ∀x^{1}∀y ≤_{1} sx∃z ≤_{0} Φx A_{0}(x, y, z).

Corollary 6.20 ([30]) Ê-PA^{ω}|^{\}+QF-AC^{1,0}+QF-AC^{0,1}+ WKL is Π_{2}^{0}-conser-vative over PRA.

The proofs for these results go beyond the scope of our lectures. One problem to be dealt with is that the functional interpretation of the negative translation of WKL is not even solvable in E-PA^{ω}.

The Friedman A-translation

In [13] H. Friedman introduced a strikingly simple device to establish closure under the Markov rule in the form

T_{i} ⊢ ¬¬∃xP (\underline{a}, x) ⇒ T_{i} ⊢ ∃xP (\underline{a}, x)

(P is a prime formula)^{1} which works for many intuitionistic theories T_{i}. As we have seen one can use functional interpretation to obtain closure under the Markov rule of those theories to which functional interpretation applies. The important feature of Friedman’s so-called A-translation however is that it is much easier to apply and also works for some systems like intuitionistic Zermelo-Fraenkel set theory ZFI for which no functional interpretation has been developed yet. Combined with the negative translation, Friedman’s A-translation therefore can be used to show Π_{2}^{0}-conservation of many classical theories T over their intuitionistic counterpart T_{i}. As a corollary of this one gets that T has the same provably recursive functions as T_{i}. By combining negative translation and A-translation with modified realizability one obtains an alternative method (to the use of negative translation and functional interpretation) for unwinding proofs of Π_{2}^{0}-sentences in e.g. PA. Note that the direct combination of negative translation and modified realizability without the intermediate step of the A-translation would be

1In theories in which every quantifier-free formula A_{0}(\underline{x}) can be written as a prime formula t_{A_{0}}(\underline{x}) = 0 this implies the usual form of the Markov rule.

Chapter 7. The Friedman A-Translation

useless since the modified realizability interpretation is trivial for negative formulas which result under negative translation.

However one should mention also some serious limitations of the approach based on the A-translation:

1) the A-translation is not sound for QF-ER and so doesn’t apply to our systems WE-HA^{ω} and ŴE-HA^{ω}|^{\} while functional interpretation does.

2) A-translation only shows closure under the Markov rule but doesn’t establish conservation results for the Markov principle with respect to general classes of formulas (which functional interpretation does). In particular it is not sound for the negative translation of QF-AC (which follows from QF-AC only in the presence of the Markov principle) and therefore cannot be used to show that e.g. the provably recursive functions of WE-PA^{ω}+ QF-AC are just the ones definable by closed terms of WE-HA^{ω} even if we omit the extensionality rule QF-ER.

3) The combination of negative translation, A-translation and modified realizability is not known to be faithful for subsystems PA_{n} of PA with restricted induction (respectively for corresponding finite type extensions of PA_{n}) whereas negative translation combined with functional interpretation is (see [56] for the latter).

Remark 7.1 The A-translation was independently also discovered by A. Dragalin in [10].

In this lecture we will establish the A-translation only for HA since this suffices to illustrate the general pattern. For extensions to other systems like ZFI the reader should consult Friedman’s original paper [13].

Definition 7.2 ([13]) Let A ∈ L(HA) be a formula of HA. For every formula F ∈ L(HA) (such that A doesn’t contain free variables which are bound in F) we define the A-translation F^{A} of F as follows: F^{A} results if all prime formulas P in F are replaced by P ∨ A.

Chapter 7. The Friedman A-Translation

Proposition 7.3 HA ⊢ F ⇒ HA ⊢ F^{A}. Proof: Easy induction on the length of the derivation. □ Corollary 7.4 HA ⊢ ∀x¬¬∃yA_{0}(x, y) ⇒ HA ⊢ ∀x∃yA_{0}(x, y). Proof: In HA, A_{0}(x, y) can be written as a prime formula t_{A_{0}}(x, y) = 0. Hence (since ¬G is an abbreviation for G → 0 = 1)

HA ⊢ ∀x¬¬∃yA_{0}(x, y)

implies

HA ⊢ (∃y(t_{A_{0}}(x, y) = 0) → 0 = 1) → 0 = 1.

By the A-translation for A :≡ ∃y(t_{A_{0}}(x, y) = 0) we get

HA ⊢ ((∃y(t_{A_{0}}(x, y) = 0) → 0 = 1) → 0 = 1)^{∃y(t_{A_{0}}(x,y)=0)}, i.e. HA proves (∃y(t_{A_{0}}(x, y) = 0∨∃y(t_{A_{0}}(x, y) = 0)) → ∃y(t_{A_{0}}(x, y) = 0)) → ∃y(t_{A_{0}}(x, y) = 0), and hence HA proves ((∃yt_{A_{0}}(x, y) = 0∨∃y(t_{A_{0}}(x, y) = 0)) → ∃y(t_{A_{0}}(x, y) = 0)) → ∃y(t_{A_{0}}(x, y) = 0). Since G ∨ G → G holds by intuitionistic logic, we get

HA ⊢ ∃y(t_{A_{0}}(x, y) = 0)

and hence

HA ⊢ ∀x∃yA_{0}(x, y).

□ For more information on the A-translation see [51]. Applications of the combination of negative translation, A-translation and realizability can be found in [4] and [55].

Final comments

In the previous lectures we have studied various proof interpretations and indicated their use as tools for unwinding the computational content of proofs (both constructive as well as non-constructive ones). A common feature of all these interpretations is that they translate a system T into another system S by assigning to every formula A of the former a formula A^{∗} of the latter such that the implication

T ⊢ A ⇒ S ⊢ A^{∗}

holds. Moreover the proof of A^{∗} in S can be obtained by a simple recursion over a given proof of A in T since the interpretations respect the logical deduction rules (locality or modularity of proof interpretations).

As a consequence of this such proof interpretations preserve to a certain extent the structure of the original proof and the resulting S-proof of A^{∗} will not be much longer than the original proof of A in T . This is in sharp contrast to structural proof transformations like cut-elimination or normalization which in general cause a non-elementary recursive blow-up of the original proof. Of course at a few places (proposition 6.17, corollary 6.20) we had to normalize the term extracted by the proof interpretation which again is of non-elementary complexity. However as we have seen one can also make substantial use of terms involving higher types by exploiting the mathematical structure of the functionals denoted by these terms without having to normalize them (see e.g. theorem 4.11, corollary 4.13, proposition 5.15 and

Chapter 8. Final Comments

– if we allow Φ to be an arbitrary closed term of ŴE-HA^{ω}|^{\}– also theorem 6.19)! So proof interpretations of the sort we investigated in the present lectures allow to separate those aspects of unwinding proofs which can be carried out locally by recursion over the proof from those which involve a global rebuilding of a proof or a term like normalization.

Another important consequence of the modularity of proof interpretations is that they can be easily extended to systems T̃ ⊃ T obtained by adding further non-logical axioms Γ to T . If the interpretation Γ^{∗} of Γ is provable in S (resp. in some extension S̃ of S), then the given interpretation immediately extends to an interpretation of T̃ in S (resp. in S̃). So it suffices to consider the new axioms.

As a simple example for such an extension consider e.g. the following: both functional interpretation and negative translation are trivial for purely universal sentences Γ := ∀xA_{0}(x). Because of this the proofs of e.g. theorem 6.6 and corollary 6.7 immediately extend to WE-PA^{ω} + Γ, WE-HA^{ω} + Γ instead of WE-PA^{ω}, WE-HA^{ω} (for Γ in the language of WE-PA^{ω}). As a corollary we obtain that the addition of (S^{ω}-true) universal axioms to WE-PA^{ω}+ QF-AC doesn’t change the provably recursive functionals of the system. This observation –which has been stressed in the context of firstorder arithmetic by G. Kreisel– can be extended also to more general classes of formulas (see e.g. [30]).

Finally, proof interpretations can easily be combined with each other: e.g in chapter 6 we used a combination of three different interpretations: elimination of extensionality, negative translation and functional interpretation.

Bibliography

[1] Avigad, J., Feferman, S., Gödel’s functional (‘Dialectica’) interpretation. To appear in: Handbook of Proof Theory (edited by S. Buss).

[2] Beeson, M., Goodman’s theorem and beyond. Pacific J. Math. 84, pp. 1-16 (1979).

[3] Berger, U., Program extraction from normalization proofs. In: M. Bezem et al.(eds.), TLCA’93, pp. 91-106. Springer LNCS 664 (1993).

[4] Berger,U., Schwichtenberg, H., Program extraction from classical proofs. In: Leivant, D. (ed.), Logic and Computational Complexity Workshop LCC’94. Springer LNCS 960, pp. 77-97 (1995).

[5] Bishop, E., Mathematics as a numerical language. In: Kino, Myhill, Vesley (eds.), Intuitionism and Proof Theory, pp. 53-71, North-Holland, Amsterdam (1970).

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

[7] Brown, D., Giusto, M., Simpson, S., Vitali’s theorem and WWKL. Preprint (1997).

[8] Buss, S.R., On Herbrand’s Theorem. In: Logic and Computational Complexity (Leivant, D., ed.), pp. 195-209. Springer LNCS 960 (1995).

[9] Cook, S., Urquart, A., Functional interpretations of feasibly constructive arithmetic. Ann. Pure Applied Logic 63, pp. 103-200 (1993).

[10] Dragalin, A.G., New kinds of realizability and the Markov rule. Dokl. Akad. Nauk. SSSR 251, pp. 534-537 (1980) (Russian). English translation: Soviet Math. Dokl. 21, pp. 461-464 (1980).

[11] Feferman, S., Theories of finite type related to mathematical practice. In: Barwise, J. (ed.), Handbook of Mathematical Logic, pp. 913-972, North-Holland, Amsterdam (1977).

[12] Friedman, H., Systems of second-order arithmetic with restricted induction (abstract). J. Symbolic Logic 41, pp. 558-559 (1976)

[13] Friedman, H., Classical and intuitionistically provably recursive functions. In: Müller,G.H., Scott, D.S. (eds.), Higher Set Theory, pp. 21-27. Springer LNM 669 (1978).

[14] Girard, J.-Y., Proof Theory and Logical Complexity Vol.I. Studies in Proof Theory. Bibliopolis (Napoli) and Elsevier Science Publishers (Amsterdam) 1987.

[15] Glivenko, V.I., Sur quelques points de la logique de M. Brouwer. Bull. Soc. Math. Belg. 15, pp. 183-188 (1929).

[16] Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, vol. 4 pp. 34–38 (1933).

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

[18] Gödel, K., Collected Work, Vol.2, S. Feferman et al. eds. Oxford University Press. New York

[19] Goodman, N., The faithfulness of the interpretation of arithmetic in the theory of constructions. J. Symbolic Logic 38, pp.453-459 (1973).

[20] Goodman, N., The theory of the Gödel functionals. J. Symbolic Logic 41, pp. 574-582 (1976).

[21] Goodman, N., Relativized realizability in intuitionistic arithmetic of all finite types. J. Symbolic Logic 43, pp. 23-44 (1978).

[22] Hacks, J., Einige Anwendungen der Funktion [x]. Acta Math. 14, 329-336 (1890).

[23] Hardy, G.H., Wright, E.M., An introduction to the theory of numbers. 5th edition, Oxford Science Publications (1979).

[24] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 454-461. Springer LNM 344 (1973).

[25] Humphreys, A.J., Simpson, S., Separation and weak König’s lemma. Preprint (1997).

[26] Kleene, S.C., On the interpretation of intuitionistic number theory. J. Symbolic Logic 10, pp. 109-124 (1945).

[27] Kleene, S.C., Introduction to Metamathematics. North-Holland (Amsterdam), Noordhoff (Groningen), Van Nostrand (New-York) 1952.

[28] Kohlenbach, U., Pointwise hereditary majorization and some applications. Arch. Math. Logic 31, pp. 227-241 (1992).

[29] Kohlenbach, U., Remarks on Herbrand normal forms and Herbrand realizations. Arch. Math. Logic 31, pp. 305-317 (1992).

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

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

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

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

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

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

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

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

[38] Kohlenbach, U., Relative constructivity. To appear in: J. Symbolic Logic.

[39] Kohlenbach, U., A note on Goodman’s theorem. To appear in: Studia Logica.

[40] Kohlenbach, U., On the no-counterexample interpretation. BRICS Report Series RS-97-42, 26pp., to appear in: J. Symbolic Logic.

[41] Kolmogorov, A.N., On the principle of the excluded middle (Russian). Mat. Sb. 32, pp.646-667 (1925).

[42] Kreisel, G., On the interpretation of non-finitist proofs, part I. J. Symbolic Logic 16, pp.241-267 (1951).

[43] Kreisel, G., On the interpretation of non-finitist proofs, part II: Interpretation of number theory, applications. J. Symbolic Logic 17, pp. 43-58 (1952).

[44] Kreisel, G., Interpretation of analysis by means of constructive functionals of finite types. In: Constructivity in Mathematics, Heyting, A. (ed.). North-Holland (Amsterdam), pp. 101-128 (1959).

[45] Kreisel, G., On weak completeness of intuitionistic predicate logic. J. Symbolic Logic 27, pp.139–158 (1962).

[46] Kreisel, G., Foundations of intuitionistic logic. In: Proc. Logic Methodology and Philosophy of Science, Nagel, E., Suppes, P., Tarski, A. (eds.). Stanford University Press (Stanford), pp. 198-210 (1962).

[47] Kreisel, G., Finiteness theorems in arithmetic: an application of Herbrand’s theorem for Σ_{2}-formulas. Proc. of the Herbrand symposium (Marseille, 1981), North-Holland (Amsterdam), pp. 39-55 (1982).

[48] Kreisel, G., Proof Theory and Synthesis of Programs: Potentials and Limitations. Eurocal ’85 (Linz 1985), Springer LNCS 203, pp. 136-150 (1986).

[49] Kreisel, G., Macintyre, A., Constructive logic versus algebraization I. Proc. L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), North-Holland (Amsterdam), pp. 217-260 (1982).

[50] Kuroda, S., Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Math. 3, pp. 35-47 (1951).

[51] Leivant, D., Syntactic translations and provably recursive functions. J. Symbolic Logic 50, pp. 252-258 (1985).

[52] Luckhardt, H., Extensional Gödel Functional Interpretation. Springer Lecture Notes in Mathematics 306, 1973.

[53] Luckhardt, H., Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, pp. 234-263 (1989).

[54] Mints, G.E., Finite investigations of transfinite derivations. J. Soviet Math. 10, pp. 548-596 (1978).

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

[56] Parsons, C., On n-quantifier induction. J. Symbolic Logic 37, pp. 466-482 (1972).

[57] Renardel de Lavalette, G.R., Extended bar induction in applicative theories. Ann. Pure Applied Logic 50, 139-189 (1990).

[58] Ruitenberg, W., Basic logic and Fregean set theory. In: Barendregt, Bezem Klop (eds.), Dirk van Dalen Festschrift. Quaestiones Infinitae Vol. V. Utrecht University 1993.

[59] Shioji, N.–Tanaka, K., Fixed point theory in weak second–order arithmetic. Ann. Pure Appl. Logic 47,pp. 167–188 (1990).

[60] Shoenfield, J.S., Mathematical Logic. Addison-Wesley Publishing Company (Reading, Massachusetts) 1967.

[61] Sieg, W., Fragments of arithmetic. Ann. Pure Appl. Logic 28,pp. 33–71 (1985).

[62] Simpson, S.G., Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations. J. Symbolic Logic 49,pp. 783–801 (1984).

[63] Simpson, S.G., Reverse Mathematics. Proc. Symposia Pure Math. 42, pp. 461–471, AMS, Providence (1985).

[64] Troelstra, A.S., Principles of Intuitionism. Springer Lecture Notes in Mathematics Vol. 95, Berlin - Heidelberg - New York, Springer 1969.

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

[66] Troelstra, A.S., Some models for intuitionistic finite type arithmetic with fan functional. J. Symbolic Logic 39, pp. 194-202 (1977).

[67] Troelstra, A.S., Realizability. To appear in: Handbook of Proof Theory (edited by S. Buss).

[68] Troelstra, A.S., van Dalen, D., Constructivism in Mathematics, vol.1. North-Holland (Amsterdam) 1988.

Recent BRICS Lecture Series Publications

LS-98-1 Ulrich Kohlenbach. Proof Interpretations. June 1998.

LS-97-1 Jan Chomicki and David Toman. Temporal Logic in Information Systems. November 1997. viii+42 pp. Full version appears in Chomicki and Saake, editors, Logics for Database and Information Systems, 3:31–70, Kluwer Academic Publishers, 1998.

LS-96-6 Torben Braüner. Introduction to Linear Logic. December 1996. iiiv+55 pp.

LS-96-5 Devdatt P. Dubhashi. What Can’t You Do With LP? December 1996. viii+23 pp.

LS-96-4 Sven Skyum. A Non-Linear Lower Bound for Monotone Circuit Size. December 1996. viii+14 pp.

LS-96-3 Kristoffer H. Rose. Explicit Substitution – Tutorial & Survey. September 1996. v+150 pp.

LS-96-2 Susanne Albers. Competitive Online Algorithms. September 1996. iix+57 pp.

LS-96-1 Lars Arge. External-Memory Algorithms with Applications in Geographic Information Systems. September 1996. iix+53 pp.

LS-95-5 Devdatt P. Dubhashi. Complexity of Logical Theories. September 1995. x+46 pp.

LS-95-4 Dany Breslauer and Devdatt P. Dubhashi. Combinatorics for Computer Scientists. August 1995. viii+184 pp.

LS-95-3 Michael I. Schwartzbach. Polymorphic Type Inference. June 1995. viii+24 pp.

LS-95-2 Sven Skyum. Introduction to Parallel Algorithms. June 1995. viii+17 pp. Second Edition.

LS-95-1 Jaap van Oosten. Basic Category Theory. January 1995. vi+75 pp.