BRICS RS-99-11 U. Kohlenbach: On the Uniform Weak König’s Lemma BRICS

Basic Research in Computer Science

On the Uniform Weak König’s Lemma

Ulrich Kohlenbach BRICS Report Series RS-99-11 ISSN 0909-0878 March 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Ulrich Kohlenbach.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/99/11/

On the uniform weak König’s lemma

Ulrich Kohlenbach

BRICS^{∗}

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

March 1999

Abstract

The so-called weak König’s lemma WKL asserts the existence of an infinite path b in any infinite binary tree (given by a representing function f). Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π_{2}^{0}- conservative over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In [10] we established such conservation results relative to finite type extensions PRA^{ω} of PRA (together with a quantifier-free axiom of choice schema). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in [10] actually can be used to eliminate even this uniform weak König’s lemma provided that PRA^{ω} only has a quantifier-free rule of extensionality QF-ER instead of the full axioms (E) of extensionality for all finite types. In this paper we show that in the presence of (E), UWKL is much stronger than WKL: whereas WKL remains to be Π_{2}^{0}-conservative over PRA, PRA^{ω} + (E)+UWKL contains (and is conservative over) full Peano arithmetic PA.

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

1 Introduction

The binary (so-called ‘weak’) König’s lemma WKL plays an important role in the formulation of mathematically strong but proof-theoretically weak subsystems of analysis. In particular the fragment (WKL_{0}) of second-order arithmetic which is based on recursive comprehension (with set parameters), Σ_{1}^{0}-induction (with set parameters) and WKL occurs prominently in the context of reverse mathematics (see [16]). Although (WKL_{0}) allows to carry out a great deal of classical mathematics, it is Π_{2}^{0}-conservative over primitive recursive arithmetic PRA as was shown first by H. Friedman using a model-theoretic argument. In [15] a proof-theoretic argument is given for a variant of (WKL_{0}) which uses function variables instead of set variables. In [10] we established various conservation results for WKL relative to subsystems of arithmetic in all finite types. As a special case these results yield that

(1) E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+WKL is Π_{2}^{0}-conservative over PRA,

where E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+WKL is a finite type extension of (WKL_{0}) (see below for a precise definition). The proof of this fact relies on a combination of Gödel’s functional interpretation with elimination of extensionality (see [12]), negative translation and Howard’s [8] majorization technique. The first step of the proof reduces the case with the full axiom of extensionality to a subsystem WE-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+WKL which is based on a weaker quantifier-free rule of extensionality only (see below) which was introduced in Spector [17]. From this system, WKL is then eliminated. This elimination actually eliminates WKL via a strong uniform version of WKL, called UWKL below, which states the existence of a functional which selects uniformly in a given infinite binary tree an infinite path from that tree. This yields the following conservation result (which isn’t stated explicitly in [10] but which can be obtained from the proofs in section 4 of that paper, see below)

(2) WE-PRA^{ω}+QF-AC+UWKL is Π_{2}^{0}-conservative over PRA.^{1} For WE-PA^{ω} we get the following result (with the same convention on + as above)

(3) WE-PA^{ω}+QF-AC+UWKL is conservative over PA.

(2) is of interest in the context of so-called explicit mathematics as developed by S. Feferman (starting with [3]) and further investigated also by A. Cantini, G. Jäger and T. Strahm among others, since the uniform weak König’s lemma UWKL seems to be a very natural ‘explicit’ formulation of WKL. We have been asked about the status of UWKL in the presence of full extensionality. In this note we give a surprisingly simple answer to this question showing, in particular, that

(4)E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+UWKL contains (and is conservative over) PA

and

(5)E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+UWKL has the same strength as (Π_{1}^{0}-CA)_{<ε_{0}},

where PA denotes full first-order Peano arithmetic.

Acknowledgement: This paper was prompted by discussions the author has had with Gerhard Jäger and Thomas Strahm who asked him about the status of the uniform weak König’s lemma in a fully extensional context.

2 Preliminaries

The set T of all finite types is defined inductively by

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

Terms which denote a natural number have type 0. Elements of type τ(ρ) are functions which map objects of type ρ to objects of type τ. The set P ⊂ T of pure types is defined by

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

1In this weakly extensional context based on a quantifier-free rule of extensionality ‘+’ must be understood in the sense that the axioms QF-AC and WKL must not be used in the proof of a premise of an application of the extensionality rule. See [10] (where we use a special symbol ‘⊕’ to emphasize this point) for details on this. Actually it is sufficient to impose this restriction on the use of the additional axioms for UWKL only.

The conservation results in [10] are much more general than the one we mentioned. This makes the proofs more involved than is needed for the special (Π_{2}^{0}-)case relevant here. A corresponding simplification of our argument has been worked out in [1].

Brackets whose occurrences are uniquely determined are often omitted, e.g. we write 0(00) instead of 0(0(0)). Furthermore we write for short τρ_{k} … ρ_{1} instead of τ(ρ_{k}) … (ρ_{1}). Pure types can be represented by natural numbers: 0(n) := n+1. The types 0, 00, 0(00), 0(0(00)) … are so represented by 0, 1, 2, 3 … For arbitrary types ρ ∈ T the degree of ρ (for short deg(ρ)) is defined by deg(0) := 0 and deg(τ(ρ)) := max(deg(τ),deg(ρ)+1). For pure types the degree is just the number which represents this type.

The system E-PRA^{ω} is formulated in the language of functionals of all finite types and contains Π_{ρ,τ}, Σ_{δ,ρ,τ}-combinators for all types (which allow to define λ-abstraction) and all primitive recursive functionals in the sense of Kleene (i.e. primitive recursion is available only on the type 0). More formally, E-PRA^{ω} results from Feferman’s system P̂A^{ω}|^{\} in [4] if we add the axioms of extensionality

(E) : ∀x^{ρ}, y^{ρ}, z^{τρ}(x =_{ρ} y → zx =_{τ} zy)

for all finite types (where for ρ = 0ρ_{k} … ρ_{1}, x =_{ρ} y is defined as ∀z_{1}^{ρ_{1}}, …, z_{k}^{ρ_{k}}(xz_{1} … z_{k} =_{0} yz_{1} … z_{k}) ).^{2} We only include equality =_{0} between numbers as a primitive predicate.

E-PA^{ω} is the extension of E-PRA^{ω} obtained by the addition of the schema of full induction and all (impredicative) primitive recursive functionals in the sense of Gödel [6] and coincides with Troelstra’s [18] system (E-HA^{ω})^{c}. The ‘weakly extensional’^{3} versions WE-PRA^{ω} and WE-PA^{ω} of these systems result if we replace the extensionality axioms (E) by a quantifier-free rule of extensionality (due to Spector [17])

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

where A_{0} is quantifier-free, s^{ρ}, t^{ρ}, r[x^{ρ}]^{τ} are arbitrary terms of the system and ρ, τ ∈ are arbitrary types. Note that QF-ER allows to derive the extensionality axiom for type 0 but already the extensionality axiom for type-1-arguments, i.e.

∀z^{2}∀x^{1}, y^{1}(x =_{1} y → zx =_{0} zy)

2We deviate slightly from our notation in [11]. The system denoted by E-PRA^{ω} in the present paper results from the corresponding system in [11] if we replace the universal axioms 9) in the definition of the latter by the schema of quantifier-free induction.

3This terminology is due to [18].

is underivable in WE-PA^{ω} (see [8]). The schema of quantifier-free choice is given by

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

where A_{0} is a quantifier-free formula.

In the following we use the formal definition of the binary (‘weak’) König’s lemma as given in [19] (here ∗, \overline{b}x, lth(n) refer to the primitive recursive coding of finite sequences from [18]):

Definition 2.1 (Troelstra(74)) WKL:≡ ∀f^{1}(T (f) ∧ ∀x^{0}∃n^{0}(lth(n) = x ∧ fn = 0) → ∃b^{1}∀x^{0}(f(\overline{b}x) = 0)), where T f :≡ ∀n^{0}, m^{0}(f(n ∗ m) =_{0} 0 → fn =_{0} 0) ∧ ∀n^{0}, x^{0}(f(n ∗ ⟨x⟩) =_{0} 0 → x ≤_{0} 1) (i.e. T (f) asserts that f represents a 0,1–tree).

Notation 2.2 T^{∞}(f) :≡ T (f) ∧ ∀x^{0}∃n^{0}(lth(n) = x ∧ fn = 0), i.e. T^{∞}(f) expresses that f represents an infinite binary tree. So WKL ≡ ∀f^{1}(T^{∞}(f) → ∃b^{1}∀x^{0}(f(\overline{b}x) = 0)).

Definition 2.3 The uniform weak König’s lemma UWKL is defined as

UWKL :≡ ∃Φ^{1(1)}∀f^{1}(T^{∞}(f) → ∀x^{0}(f((\overline{Φf})x) = 0)).

3 Results

For the weakly extensional systems WE-PRA^{ω} and WE-PA^{ω} we have the following conservation results for UWKL:

Theorem 3.1 1) WE-PRA^{ω}+QF-AC+UWKL is Π_{2}^{0}-conservative over PRA.

2) WE-PA^{ω}+QF-AC+UWKL is conservative over PA. (Here, again, + must be understood in the sense of footnote 1).

Proof: 1) In [10] (4.2-4.7), we constructed a primitive recursive functional

f^{1}, g^{1} ↦ ζfg := \binom{}{ f̂_{g}} such that

(1) WE-PRA^{ω} ⊢ ∀f, g T^{∞}(ζfg)

and

(2) WE-PRA^{ω} ⊢ ∀f(T^{∞}(f) → ∃g(f =_{1} ζfg)).

By the proof of theorem 4.8 in [10] (and the fact that WE-PRA^{ω} is Π_{2}^{0}-conservative over PRA), it follows that

WE-PRA^{ω}+QF-AC+UWKL^{∗} is Π_{2}^{0}-conservative over PRA,

where

UWKL^{∗} := ∃B∀f, g, x((ζfg)((\overline{Bfg})x) =_{0} 0).

It remains to show that

WE-PRA^{ω} ⊢ UWKL^{∗} → UWKL.

The proof of (2) in [10](4.7) shows that g can be primitive recursively defined in f as

f̃(x) := \{ \begin{matrix}min n ≤ \overline{1^{1}}x[lth(n) = x ∧ f(n) = 0], if such an n exists \\ 0^{0}, otherwise. \end{matrix}

Thus for ξf := ζ(f, f̃)

(2)′ WE-PRA^{ω} ⊢ ∀f(T^{∞}(f) → f =_{1} ξf).

Define Φf := B(f, f̃) for B satisfying UWKL^{∗}. Then

∀x((ξf)((\overline{Φf})x) =_{0} 0)

and so for f such that T^{∞}(f) (which implies f =_{1} ξf)

∀x(f((\overline{Φf})x) =_{0} 0),

i.e. Φ satisfies UWKL.

2) As in 1) we obtain from the proof of 4.8 in [10] that

WE-PA^{ω}+QF-AC+UWKL is ∀\underline{x}\underline{ρ}∃\underline{y}^{0}A_{0}(\underline{x}, \underline{y})-conservative over WE-PA^{ω},

where \underline{x}\underline{ρ} is a tuple of variables of type levels ≤ 1, A_{0} is quantifier-free and contains only \underline{x}, \underline{y} as free variables. Now let A be a sentence in the language of PA which can be assumed to be in prenex normal form and assume that

WE-PA^{ω}+QF-AC+UWKL ⊢ A.

Then a fortiori

WE-PA^{ω}+QF-AC+UWKL ⊢ A^{H},

where A^{H} is the Herbrand normal form of A. By the conservation result just mentioned we get

WE-PA^{ω} ⊢ A^{H}

and therefore by [9](theorem 4.1)

PA ⊢ A.

Remark 3.2 The passage from the provability of A^{H} to that of A used in the proof of 2) above does not apply to WE-PRA^{ω} and PRA (see [9] for a counterexample). Indeed, already WE-PRA^{ω}+QF-AC^{0,0} is not Π_{3}^{0}-conservative over PRA: the former theory proves the schema of Σ_{1}^{0}-collection Σ_{1}^{0}-CP, but it is known that there are instances of Σ_{1}^{0}-CP (which always can be prenexed as Π_{3}^{0}-sentences)^{4} which are unprovable in PRA (see [14]).

We now show that the picture changes completely if we consider the systems E-PRA^{ω} amd E-PA^{ω} with full extensionality instead of WE-PRA^{ω}, WE-PA^{ω}. This phenomenon is due to the following

Proposition 3.3 E-PRA^{ω} ⊢ UWKL ↔ ∃φ^{2}∀f^{1}(φf =_{0} 0 ↔ ∃x^{0}(fx =_{0} 0)).

Proof: 1) ‘→’: We first show that any Φ satisfying UWKL is – provably in E-PRA^{ω} – (effectively) discontinuous^{5}, i.e.

E-PRA^{ω} ⊢ \begin{cases}∀Φ^{1(1)}(∀f^{1}(T^{∞}(f) → ∀x^{0}(f((\overline{Φf})x) =_{0} 0)) → \\ ∃g_{(·)}^{1(0)}, g^{1}(T^{∞}(g) ∧ ∀iT^{∞}(g_{i}) ∧ ∀i∀j ≥ i(g_{j}(i) =_{0} g(i)) \\ ∧∀i, j(Φ(g_{i}, 0) = Φ(g_{j}, 0) ≠ Φ(g, 0)))) \end{cases}

and, moreover, g_{(·)}, g can be computed uniformly in Φ by closed terms of E-PRA^{ω}. Define g primitive recursively such that

g(k) = \{ \begin{matrix}0, if ∀m < lth(k)((k)_{m} = 0) ∨ ∀m < lth(k)((k)_{m} = 1) \\ 1, otherwise. \end{matrix}

4Here PRA is understood not as a quantifier-free theory but with full first-order predicate logic.

5The term ‘effectively discontinuous’ is due to [7] on which we rely in the second part of our proof.

It is clear that (provably in E-PRA^{ω}) T^{∞}(g). Now let Φ^{1(1)} be such that

∀f^{1}(T^{∞}(f) → ∀x(f((\overline{Φf})x) =_{0} 0)).

\underline{Case 1}: Φ(g, 0) = 0. Define a primitive recursive function λi, k.g_{i}(k) such that

g_{i}(k) = \{ \begin{matrix}0, if [lth(k) ≤ i ∧ ∀m < lth(k)((k)_{m} = 0)] ∨ [∀m < lth(k)((k)_{m} = 1)] \\ 1, otherwise. \end{matrix}

Again we easily verify within E-PRA^{ω} that ∀iT^{∞}(g_{i}). From the construction of g_{i} and g it is clear that

∀k∀l ≥ lth(k)(g_{l}(k) = g(k)).

Since our coding has the property that lth(k) ≤ k, we get

∀k∀l ≥ k(g_{l}(k) = g(k)).

Since λx.1 is the only infinite path of the binary tree represented by g_{i}, it follows that

∀i(Φ(g_{i}, 0) = 1).

\underline{Case 2}: Φ(g, 0) = 1. The proof is analogous to case 1 with

g_{i}(k) := \{ \begin{matrix}0, if [lth(k) ≤ i ∧ ∀m < lth(k)((k)_{m} = 1)] ∨ [∀m < lth(k)((k)_{m} = 0)] \\ 1, otherwise. \end{matrix}

This finishes the proof of the discontinuity of Φ. We now show – using an argument from [7] known as ‘Grilliot’s trick’ ^{6} – that the functional φ^{2} defined by (+)∀f^{1}(φf =_{0} 0 ↔ ∃x(fx =_{0} 0)) can be defined primitive recursively in Φ such that (+) holds provably in E-PRA^{ω}: We can construct a closed term t^{1(1)} of E-PRA^{ω} such that (provably in E-PRA^{ω}) we have

thi = \{ \begin{matrix}g_{j}(i), for the least j < i such that h(j) > 0, if existent \\ g_{i}(i), otherwise. \end{matrix}

6This argument plays an important role in the context of the Kleene/Kreisel countable functionals, see [13] whose formulation of it we adopt here.

Together with ∀i∀j ≥ i(g_{j}(i) = g_{i}(i)) this yields

∃j(h(j) > 0) → th =_{1} g_{j} for the least such j

and together with ∀i(g_{i}(i) = g(i))

∀j(h(j) = 0) → th =_{1} g.

Hence using the extensionality axiom for type-2-functionals we get

∀j(h(j) = 0) ↔ Φ(th, 0) =_{0} Φ(g, 0).

So φ := λh^{1}.\overline{sg} ∘ |Φ(t(\overline{sg} ∘ h), 0) − Φ(g, 0)| where \overline{sg}(x) := 0 for x ≠ 0 and = 1 otherwise, does the job. We now combine the two constructions of φ corresponding to the two cases above into a single functional which defines φ primitive recursively in Φ: Let χ be a closed term such that

E-PRA^{ω} ⊢ ∀x^{0}((x =_{0} 0 → χx =_{1(1)} t) ∧ (x ≠ 0 → χx =_{1(1)} t̃)),

where t is defined as above with g_{i} from case 1 whereas t̃ is defined analogously but with g_{i} as in case 2. Then define φ := λh^{1}.\overline{sg} ∘ |Φ((χ(Φ(g, 0))(\overline{sg} ∘ h), 0) − Φ(g, 0)|.

2) ‘←’: Primitive recursively in φ one can easily compute a functional Φ which even selects the leftmost infinite branch of an infinite binary tree.

Corollary to the proof of proposition 3.3: One can construct closed terms t_{1}, t_{2} of E-PRA^{ω} such that

E-PRA^{ω} ⊢ \begin{cases}∀Φ^{1(1)}(∀f^{1}(T^{∞}(f) → ∀x^{0}(f((\overline{Φf})x) = 0)) → \\ ∀f^{1}((t_{1}Φ)f =_{0} 0 ↔ ∃x(fx = 0))) \end{cases}

and

WE-PRA^{ω} ⊢ \begin{cases}∀φ^{2}(∀f^{1}(φf = 0 ↔ ∃x(fx = 0)) → \\ ∀f^{1}(T^{∞}(f) → ∀x^{0}(f((\overline{t_{2}φf})x) = 0))). \end{cases}

Corollary 3.4 E-PRA^{ω} + QF-AC^{1,0} ⊢ UWKL ↔ ∃μ^{2}∀f^{1}(∃x^{0}(fx = 0) → f(μf) = 0).

Proof: The existence of μ obviously implies the existence of φ in proposition 3.3 and hence of Φ. For the other direction we only have to observe that the existence of φ implies the existence of μ be applying QF-AC^{1,0} to

∀f∃x(φ(f) = 0 → fx = 0).

Remark 3.5 In contrast to the corollary to the proof of proposition 3.3 above there exists no closed term t in E-PRA^{ω} which computes μ in Φ, i.e.

S^{ω} ⊧ / ∀Φ^{1(1)}(∀f^{1}(T^{∞}(f) → ∀n^{0}(f(\overline{Φf})n = 0)) → ∀f^{1}(∃x(fx = 0) → f(tΦf) = 0)

for every closed term t (of appropriate type) of E-PRA^{ω}, since – by [8] – every such term has a majorant t^{∗}, Φ is majorized by λf^{1}, x^{0}.1 and so μ would have a majorant λf^{M}.t^{∗}(1^{1(1)}, f^{M}) (where f^{M}(x) := max(f0, …, fx)), which contradicts the easy observation that μ has not even a majorant in S^{ω} (here S^{ω} denotes the full set-theoretic type structure).

Theorem 3.6 1) E-PRA^{ω}+UWKL contains Peano arithmetic PA.

2) E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+UWKL is conservative over PA.

3) E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+UWKL proves the consistency of PA and has the same proof-theoretic strength as (and is Π_{2}^{1}-conservative over) the second order system (Π_{1}^{0}-CA)_{<ε_{0}}.

Proof: 1) Using φ from proposition 3.3 one easily gets characteristic functions for all arithmetical formulas A(\underline{x}). By applying the quantifier-free induction axiom of E-PRA^{ω} to them, one obtains every arithmetical instance of induction.

2) This follows from corollary 3.4 and the conservation of E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + μ over PA which is due [4] (note that the usual elimination of extensionality procedure – which applies to the existence of μ but not to UWKL – yields a reduction of E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + μ to its variant where the extensionality axioms for types > 0 are dropped, see [12] for details on this).

3) follows from [4],[5] using again corollary 3.4 above and elimination of extensionality.

Remark 3.7 1) The functionals φ and μ from proposition 3.3 and corollary 3.4 provide uniform versions (in the same sense in which UWKL is a uniform version of WKL) of

(1) Π_{1}^{0}-CA : ∀f∃g∀x^{0}(g(x) =_{0} 0 ↔ ∃y^{0}(f(x, y) =_{0} 0))

respectively of

(2) Π_{1}^{0}-ĈA : ∀f∃g∀x^{0}, z^{0}(f(x, gx) =_{0} 0 ∨ f(x, z) ≠ 0),

but yet φ, μ are not stronger than (1), (2) relative to E-PRA^{ω} (but only relative to E-PA^{ω}) as Feferman’s results cited in the proof above show. The reason for this is, that E-PRA^{ω} is too weak to iterate φ or μ uniformly since this would require a primitive recursion of type level 1. In contrast to this fact, UWKL is stronger than WKL already relative to E-PRA^{ω}.

2) One might ask whether UWKL gets weaker if we allow Φ^{1(1)} to be a partial functional which is required to be defined only on those functions f which represent an infinite binary tree. However the construction ξ (used in the proof of theorem 3.1) such that

(1) ∀f^{1}T^{∞}(ξf)

and

(2) ∀f^{1}(T^{∞}(f) → ξf =_{1} f)

shows that any such partial Φ could be easily extended to a total one.

References

[1] Avigad, J., Feferman, S., Gödel’s functional (‘Dialectica’) interpretation. In: [2], pp. 337-405 (1998).

[2] Buss, S.R. (editor), Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics Vol 137, Elsevier, vii+811 pp. (1998).

[3] Feferman, S., A language and axioms for explicit mathematics. In: Crossley, J.N. (ed.), Algebra and Logic, Springer Lecture Notes in Mathematics 450, pp. 87–139 (1975).

[4] 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).

[5] Feferman, S., Hilbert’s program relativized: proof-theoretical and foundational reductions. J. Symbolic Logic 53, pp. 364–384 (1988).

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

[7] Grilliot, T.J., On effectively discontinuous type-2 objects. J. Symbolic Logic 36, pp. 245–248 (1971).

[8] 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).

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

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

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

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

[13] Normann, D., Recursion on the Countable Functionals. Springer Lecture Notes in Mathematics 811, v+190 p., 1980.

[14] Parsons, C., On a number theoretic choice schema and its relation to induction. In: Intuitionism and proof theory, pp. 459-473. North-Holland, Amsterdam (1970).

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

[16] Simpson, S.G., Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag. xiv+445 pp. 1999.

[17] Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (J.C.E. Dekker (ed.)), AMS, Providence, R.I., pp. 1–27 (1962).

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

[19] Troelstra, A.S., Note on the fan theorem. J. Symbolic Logic 39, pp. 584–596 (1974).

Recent BRICS Report Series Publications

RS-99-11 Ulrich Kohlenbach. On the Uniform Weak König’s Lemma. March 1999. 13 pp.

RS-99-10 Jon G. Riecke and Anders B. Sandholm. A Relational Account of Call-by-Value Sequentiality. March 1999. 51 pp. To appear in Information and Computation, LICS ’97 Special Issue. Extended version of an article appearing in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 258–267. This report supersedes the earlier report BRICS RS-97-41.

RS-99-9 Claus Brabrand, Anders Møller, Anders B. Sandholm, and Michael I. Schwartzbach. A Runtime System for Interactive Web Services. March 1999. 21 pp. Appears in Mendelzon, editor, Eighth International World Wide Web Conference, WWW8 Proceedings, 1999, pages 313–323 and Computer Networks, 31:1391–1401, 1999.

RS-99-8 Klaus Havelund, Kim G. Larsen, and Arne Skou. Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. March 1999. 23 pp. To appear in Katoen, editor, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, ARTS ’99 Proceedings, LNCS, 1999.

RS-99-7 Glynn Winskel. Event Structures as Presheaves—Two Representation Theorems. March 1999. 16 pp.

RS-99-6 Rune B. Lyngsø, Christian N. S. Pedersen, and Henrik Nielsen. Measures on Hidden Markov Models. February 1999. 27 pp. To appear in Seventh International Conference on Intelligent Systems for Molecular Biology, ISMB ’99 Proceedings, 1999.

RS-99-5 Julian C. Bradfield and Perdita Stevens. Observational Mu-Calculus. February 1999. 18 pp.

RS-99-4 Sibylle B. Fröschle and Thomas Troels Hildebrandt. On Plain and Hereditary History-Preserving Bisimulation. February 1999. 21 pp.

RS-99-3 Peter Bro Miltersen. Two Notes on the Computational Complexity of One-Dimensional Sandpiles. February 1999. 8 pp.

RS-99-2 Ivan B. Damgård. An Error in the Mixed Adversary Protocol by Fitzi, Hirt and Maurer. February 1999. 4 pp.