CZF and Second Order Arithmetic

Robert S. Lubarsky^{∗} Dept. of Mathematical Sciences Florida Atlantic University Boca Raton, FL 33431, USA Robert.Lubarsky@alum.mit.edu

July 10, 2006

Abstract

Constructive ZF + full Separation is shown to be equiconsistent with Second Order Arithmetic.

1 Introduction

CZF, Constructive Zermelo-Fraenkel Set Theory, is an axiomatization of set theory in intuitionistic logic strong enough to do much standard mathematics yet modest enough in proof-theoretical strength to qualify as constructive. Based originally on Myhill’s CST [10], CZF was first identified and named by Aczel [1, 2, 3]. Its axioms are:

• Pairing: ∀x, y ∃z ∀w w ∈ z ↔ (w = x ∨ w = y)

• Union: ∀x ∃y ∀z(z ∈ y ↔ ∃w(w ∈ x ∧ z ∈ w)

• Extensionality: ∀x, y x = y ↔ ∀z(z ∈ x ↔ z ∈ y)

• Set Induction (Schema): (∀x((∀y ∈ x ϕ(y)) → ϕ(x))) → ∀x ϕ(x)

• Δ_{0} Separation (Schema): ∀x ∃y ∀z z ∈ y ↔ (z ∈ x ∧ ϕ(z)), for ϕ a Δ_{0} formula

• Strong Infinity: ∃x [(∅ ∈ x) ∧ (∀y ∈ x (y ∪ {y}) ∈ x) ∧ ∀z((∅ ∈ z ∧ ∀y ∈ z y ∪ {y} ∈ z) → z ⊆ x)]

• Fullness (AKA Subset Collection): ∀x, y ∃z ∀ R (if R is a total relation from x to y then there is a total relation R’ ∈ z from x to y such that R’ ⊆ R)

• Strong Collection (Schema): ∀x(∀y ∈ x ∃z ϕ(y, z) → ∃w (∀y ∈ x ∃z ∈ w ϕ(y, z) ∧ ∀z ∈ w ∃y ∈ x ϕ(y, z)).

∗Thanks are due to the referee for the careful reading and helpful suggestions received.

Among Aczel’s accomplishments was an interpretation of CZF, and various extensions thereof, in Martin-Löf type theory, which established CZF as a predicative theory. As it turns out, CZF is proof-theoretically equivalent with Martin-Löf type theory ML_{1}V, as well as KP (Kripke-Platek admissible set theory), ID (inductive definability), and a host of other identified theories. Such theories can arguably be considered to be the limit of predicative mathematics, allow for a philosophical justification as being constructive, and are in any case very much weaker prooftheoretically than ZF. For an overview, references, and some proofs, see [11].

It is a natural enough question to ask about the strength of variants of CZF. Michael Rathjen conjectured that adding full Separation to CZF elevates the theory’s strength from ID, which is a small fragment of Second Order Arithmetic, to full Second Order Arithmetic. In this note, this conjecture will be shown to be correct.

What is the value of such a result? It is certainly nicer if a theory is shown to be weak, in that one can then use that theory with fewer philosophical scruples. This is the case for instance in [2], see also [11], where it is shown that adding certain choice principles to CZF does not change the proof-theoretic strength. Still, knowing that CZF + full Separation has the strength of Second Order Arithmetic tells us at least that the former theory is not predicative, providing a warning to the constructivelyminded mathematician not to work within it. In addition, the exact determination of this strength provides independence results. For instance, Rathjen ([12], prop. 7.12 (ii)) shows that CZF + Power Set is prooftheoretically stronger than n^{th} Order Arithmetic for all n, from which it follows that CZF, being much weaker, does not prove Power Set. Similarly, it follows from the result in this paper that even with the addition of full Separation Power Set does not follow. (The latter result is re-proven model-theoretically in [8].) None of this should be surprising. Both the main result of this paper and the consequences just cited were anticipated by Rathjen (and perhaps others), and the ideas contained in the proof to follow are themselves mostly a reworking of those found in [1] and [11]. Still, at least now the results are formally established.

By way of additional background, recent work on CZF and other intuitionistic set theories, often involving categorical models, has been done by S. Awodey, C. Butz, N. Gambino, E. Griffor, A. Joyal, I. Moerdijk, E. Palmgren, A.K. Simpson, Th. Streicher, and M. Warren. For an excellent overview and references, see [4] or [13].

2 Interpreting CZF + full Separation in Second Order Arithmetic

First we will work within Second Order Arithmetic with the Axiom of Choice (AC_{ω}) to prove the consistency of CZF + full Separation. The Axiom of Choice in this context is the assertion that ∀n ∃X ϕ(n, X) → ∃X ∀n ϕ(n, X_{n}), where X_{n} is the n^{th} slice of X according to some recursive coding scheme. It is an old observation that the consistency strength of Second Order Arithmetic is unchanged by the addition of AC_{ω}; see for instance [6].

NOTATION: Natural numbers will be used to stand for recursive functions, via some standard encoding. The variables used for numbers in this context will be e, f, g, h, and variants thereof. It is assumed that the language in question has a two-place function symbol App, which on inputs e and x returns the result of applying the e^{th} recursive function to x. For readability, this will be written as {e}(x). We will avail ourselves of λ-notation to describe recursive functions. This means that if some recursive procedure P is given for producing an integer P(x), depending uniformly on an input integer x, then λx.P(x) will stand for an integer e such that {e}(x) = P(x). We also assume the choice of a distinguished recursive tupling function, ⟨ ⟩, with recursive arity function and recursive projection functions (-)_{i}, i ∈ ω. Vector notation a⃗ will be used to denote tuples, i.e. a⃗ is an abbreviation for ⟨a_{0}, ..., a_{n}⟩. Concatenation of tuples is given by ⌢: a⃗ ⌢ b⃗ = ⟨a_{0}, ..., a_{n}, b_{0}, ..., b_{m}⟩. If â is an integer then a⃗ ⌢ â is taken as shorthand for a⃗ ⌢ ⟨â⟩, and similarly for â ⌢ a⃗. If X is a collection of tuples, then a⃗ ⌢ X = {a⃗ ⌢ b⃗ | b⃗ ∈ X}. Also, let a^{X} be { b⃗ | a⃗ ⌢ b⃗ ∈ X }. If a⃗ = ⟨a⟩, then ⟨a⟩ ⌢ X and ⟨a⟩^{X} will often be abbreviated as a ⌢ X and a^{X} respectively. (Note that a^{X} might well be non-trivial even if a⃗ ∉ X, as X might contain only proper extensions of a⃗.)

The proof will be via a realizability interpretation. By way of terminology, we will refer to certain reals in the model of arithmetic as representing or being sets in the model of CZF. A real is itself a set of integers. In order to avoid confusion as to whether any given object is claimed to be a set of integers in the given model of arithmetic or to be a CZF-set, the word “set” will be reserved exclusively for the latter, the former being referred to as collections of integers or, more simply, reals.

Under this interpretation, a set is given by a non-empty real S, consisting only of tuples, which forms a tree, and which moreover is well-founded:

∀X[(X ⊆ S ∧ ∀a⃗ ∈ S(∀a⃗ ⌢ â ∈ S a⃗ ⌢ â ∈ X → a⃗ ∈ X)) → X = S].

(Any X satisfying the condition in the antecedent will be called inductive. Since inductivity is, strictly speaking, dependent on the choice of ambient real S, sometimes for clarity such an X will be described as inductive relative to S.) The idea is that the members of S are given by integers a such that ⟨a⟩ ∈ S, a’s members are given by integers b such that ⟨a, b⟩ ∈ S, and so on. The property of being a set, notated as Set(S), is Π_{1}^{1}-definable.

Lemma 2.0.1 If Set(S) and a⃗ ∈ S then Set(a^{S}).

proof: Suppose X ⊆ a^{S} is inductive: ∀b⃗ ∈ a^{S}(∀b⃗ ⌢ b̂ ∈ a^{S} b⃗ ⌢ b̂ ∈ X → b⃗ ∈ X). We must show that X = a^{S}.

Let X^{+} = (a⃗ ⌢ X) ∪ (S \ (a⃗ ⌢ a^{S})). We claim that also X^{+} is inductive (relative to S). To see this, suppose that, for a given b⃗, for all b̂ such that b⃗ ⌢ b̂ ∈ S, b⃗ ⌢ b̂ ∈ X^{+}. If b⃗ does not extend a⃗ then b⃗ ∈ S\(a⃗ ⌢ a^{S}) ⊆ X^{+}. If b⃗ does extend a^{S}, say b⃗ = a⃗ ⌢ c⃗, then, if c⃗ ⌢ b̂ ∈ a^{S}, b⃗ ⌢ b̂ ∈ S. By the hypothesis on b⃗, b⃗ ⌢ b̂ ∈ X^{+}, hence c⃗ ⌢ b̂ ∈ X. Since X is inductive, c⃗ ∈ X, which yields b⃗ ∈ X^{+}. Hence X^{+} is inductive. Since Set(S), X^{+} = S.

To finish up, if b⃗ ∈ a^{S}, then a⃗ ⌢ b⃗ is in S, and hence also in X^{+}. Since a⃗ ⌢ b⃗ could not enter X^{+} via the second clause (in X^{+}’s definition), it must have entered via the first: a⃗ ⌢ b⃗ ∈ (a⃗ ⌢ X). That means b⃗ ∈ X, i.e. a^{S} ⊆ X.

The realizability relation is defined recursively as follows:

• e ⊢ X ∈ S ↔ e_{1} ⊢ X = e_{0}^{S} ∧ ⟨e_{0}⟩ ∈ S

• e ⊢ S = T ↔ (∀⟨a⟩ ∈ S {e_{0}}(a) ⊢ a^{S} ∈ T) ∧ (∀⟨b⟩ ∈ T {e_{1}}(b) ⊢ b^{T} ∈ S)

• e ⊢ ϕ ∨ ψ ↔ (e_{0} = 0 ∧ e_{1} ⊢ ϕ) ∨ (e_{0} = 1 ∧ e_{1} ⊢ ψ)

• e ⊢ ϕ ∧ ψ ↔ (e_{0} ⊢ ϕ) ∧ (e_{1} ⊢ ψ)

• e ⊢ ϕ → ψ ↔ ∀f (f ⊢ ϕ → {e}(f) ⊢ ψ)

• e ⊢ ∀Xϕ(X) ↔ ∀X(Set(X) → e ⊢ ϕ(X))

• e ⊢ ∃Xϕ(X) ↔ ∃X(Set(X) ∧ e ⊢ ϕ(X))

(As is standard, ϕ ↔ ψ is an abbreviation for ϕ → ψ ∧ ψ → ϕ, and ¬ϕ for ϕ → ⊥, where it follows by omission from the above that nothing realizes ⊥.)

Although intuitionistically the Levy hierarchy of Σ_{n} and Π_{n} formulas does not work as in the classical case, we will still have use of the classical Levy rank of a formula. In the following, the assertion “ϕ is Σ_{n} (resp. Π_{n})” is to be understood as giving ϕ’s classical rank, even when ϕ is intended and used as an intuitionistic formula. The reason for this is that the relation “e ⊢ ϕ” is Σ_{n+1}^{1} (resp. Π_{n+1}^{1}) for ϕ a Σ_{n} (resp. Π_{n}) formula (classically), uniformly in e and ϕ. This fact follows easily from the inductive definition of ⊢.

We now show that under this interpretation all of the axioms of CZF are valid.

1. intuitionistic logic That all of the (standard) realizability interpretations satisfy the axioms and inference rules of intuitionistic logic is by now well understood. For examples and details, see for instance [5] or [9]. (Thanks to the referee for relaying the information that in the latter the proof of the closure lemma seems to be mistaken. A correction is reported to appear in [7].)

2. equality axioms Realizers need to be given for:

(a) ∀x x = x

(b) ∀x, y x = y → y = x

(c) ∀x, y, z x = y ∧ y = z → x = z

(d) ∀x, y, z x = y ∧ z ∈ x → z ∈ y

(e) ∀x, y, z x = y ∧ x ∈ z → y ∈ z.

(a) Unraveling the definitions, we need to find a realizer e so that, for i = 0,1

∀⟨a⟩ ∈ x {e_{i}}(a)_{1} ⊢ ⟨a⟩^{x} = {e_{i}}(a)_{0}^{x}.

With this in mind, let g be such that

{g}(f) = ⟨λx.⟨x, f⟩, λx.⟨x, f⟩⟩.

Let e be a fixed point for g: e = {g}(e). e is as desired. (In clauses 9) and 10) below, e will be referred to as Id.)

(b) λe.⟨e_{1}, e_{0}⟩ is as desired.

(c)-(e) are of a similar flavor, and are left to the reader, who can also find proofs in [9]. Note that it follows by induction on formulas that for all formulas ϕ there is a realizer for (x = y ∧ ϕ(x)) → ϕ(y), with (c)-(e) being the base cases.

3. extensionality A realizer for this follows readily from the equality axioms above and the definitions of “e ⊢ S = T ” and “e ⊢ X ∈ S”.

4. set induction Given a formula ϕ, we need a realizer for

∀S(∀T ∈ S ϕ(T) → ϕ(S)) → ∀Sϕ(S).

Let e realize the antecedent. We need a realizer h(e) for the conclusion, recursively and uniformly in e; then λe.h(e) would be the desired realizer. Let h(e) be {e}(λ x. h(e)). By the Recursion Theorem, h(e) is a recursive function, and by its definition is uniform in e. To see that h(e) ⊢ ∀Sϕ(S), let S be a set; we need to show that h(e) ⊢ ϕ(S). Let X be {a⃗ ∈ S | h(e) ⊢ ϕ(a^{S})}. By the assumption on e and definition of h(e), if ∀a⃗ ⌢ â ∈ S a⃗ ⌢ â ∈ X, then a⃗ ∈ X. By the well-foundedness of S, X=S. Hence ⟨ ⟩ ∈ X, and h(e) ⊢ ϕ(⟨ ⟩^{S}).

5. pairing Given S and T, let U be (0 ⌢ S) ∪ (1 ⌢ T). U is as desired.

6. union Given S, let T be {a⃗ | ∃a a ⌢ a⃗ ∈ S} ∪ {⟨ ⟩}. T is as desired. (The reader might wonder why we have to throw the empty sequence into T. Recall that, in order to represent a set, T must be non-empty, by definition. If S represents the empty set, i.e. if S = {⟨ ⟩}, then {a⃗ | ∃a a ⌢ a⃗ ∈ S} would be the empty set itself. In this case T as actually defined would consist solely of ⟨ ⟩, making ⋃ ∅ = ∅, as desired.)

7. strong infinity We will define S_{n} inductively on n. Let S_{0} be {⟨ ⟩}. Given S_{m}(m < n) let S_{n} be {m ⌢ a⃗ | m < n ∧ a⃗ ∈ S_{m}}. Let S_{ω} be {n ⌢ a⃗ | n ∈ ω, a⃗ ∈ S_{n}}. S_{ω} is as desired.

8. full separation Given a set S and a formula ϕ, we need to show the existence of {a ∈ S | ϕ(a)}. Let S_{ϕ} be {⟨⟨f, a_{0}⟩, a_{1}, ..., a_{n}⟩ | ⟨a_{0}, a_{1}, ..., a_{n}⟩ ∈ S ∧ f ⊢ ϕ(a_{0}^{S})}. S_{ϕ} exists, by the definability of ⊢. It is also a tree, almost, lacking merely the empty sequence. So let Set_{S,ϕ} be S_{ϕ} ∪ {⟨ ⟩}. We claim that Set_{S,ϕ} is as desired.

To see that Set_{S,ϕ} is a set, it remains only to check that it is wellfounded. To this end, suppose X ⊆ Set_{S,ϕ} is inductive. It is easy to verify that for any a⃗ a^{X} is an inductive subset of a^{Set_{S,ϕ}}. Moreover, if a⃗ ≠ ⟨ ⟩ then there is a b⃗ such that a^{Set_{S,ϕ}} = b⃗^{S} (For a⃗ = ⟨⟨f, a_{0}⟩, a_{1}, ..., a_{n}⟩, let b⃗ = ⟨a_{0}, a_{1}, ..., a_{n}⟩.). By the lemma earlier in this section, b⃗^{S} is a set (i.e. is well-founded), so a^{X} = b⃗^{S} and a^{X} = a^{Set_{S,ϕ}}. This shows that S_{ϕ} ⊆ X. As a final step, since X is inductive, Set_{S,ϕ} ⊆ X. It remains only to find a realizer for

∀x (x ∈ Set_{S,ϕ} ↔ (x ∈ S ∧ ϕ(x)))

which is independent of S and Set_{S,ϕ}. (The independence is necessary by the ∀ and ∃ clauses in the definition of ⊢, which do not allow the realizer to access the sets chosen.) Choose any set x. Going from left to right, suppose e ⊢ “x ∈ Set_{S,ϕ}”. That means that e_{1} ⊢ “x = e_{0}^{Set_{S,ϕ}}” and ⟨e_{0}⟩ ∈ Set_{S,ϕ}. By the definition of Set_{S,ϕ}, ⟨e_{01}⟩ ∈ S, e_{01}^{S} = e_{0}^{Set_{S,ϕ}}, and e_{00} ⊢ ϕ(e_{01}^{S}). This yields that ⟨e_{01}, e_{1}⟩ ⊢ “x ∈ S”. Furthermore, from e_{00} ⊢ ϕ(e_{0}^{Set_{S,ϕ}}) and e_{1} ⊢ “x = e_{0}^{Set_{S,ϕ}}”, a realizer g for ϕ(x) can be computed (uniformly in e_{00} and e_{1}). The desired realizer for the right hand side is then ⟨⟨e_{01}, e_{1}⟩, g⟩. The other direction is similar.

9. subset collection We will prove Fullness, which means finding an integer e such that

∀S, T ∃C e ⊢ “C ⊆ T otRel(S, T)∧∀U ∈ T otRel(S, T) ∃V ∈ C V ⊆ U”

where TotRel(S,T) is the collection of total relations from S to T. The choice of e will be facilitated by considering the kind of C’s we will ultimately be working worth (although e must not depend on the choice of C!). To motivate the choice of C’s, suppose we have a realizer for U being such a total relation: f ⊢ ∀x ∈ S ∃y ∈ T ⟨x, y⟩ ∈ U (neglecting here that every element in U must also come from S × T). Unraveling the definitions yields

∀x, g(g ⊢ “x ∈ S” → ∃y{f}(g)_{01} ⊢ “y = {f}(g)_{00}^{T}”∧{f}(g)_{11} ⊢ “⟨x, y⟩ = {f}(g)_{10}^{U}”).

Letting Id be such that Id ⊢ ∀x x = x, and a so that ⟨a⟩ ∈ S, unraveling the definitions shows that ⟨a, Id⟩ ⊢ a^{S} ∈ S. Instantiating x with a^{S} and g with ⟨a, Id⟩ produces

{f}(⟨a, Id⟩)_{11} ⊢ “⟨a^{S}, y⟩ = {f}(⟨a, Id⟩)_{10}^{U}”.

Let

f ↾ S × T = {a⃗ ∈ U | ∃⟨a⟩ ∈ S a_{0} = {f}(⟨a, Id⟩)_{10}} ∪ {⟨ ⟩}.

From the definition, it would seem that f ↾ S × T depends on U as well as f and S, and not on T, but actually that’s not the case, which is important in what follows (hence mention of U is suppressed in the notation). That f ↾ S × T does not depend on U can be seen from the role of f. Since f ⊢ ∀x ∈ S ∃y ∈ T ⟨x, y⟩ ∈ U, given f, S, and T, we can determine U, or at least that part of U relevant to the definition of f ↾ S × T. (In a little detail, feed ⟨a, Id⟩ to {f}, as a ranges through the members of S. {f} will produce the code for the corresponding y in T, as well as that for ⟨a, y⟩ in U. To get more information about U, meaning to get codes for members of members, unravel the given a and the produced y.) So if the same f realizes that some V ≠ U is also a total relation (from S to T), which is possible, the same f ↾ S × T would be produced using V instead of U. Let

ST = {f ⌢ a⃗ | ∃U f ⊢ “U ∈ T otRel(S, T)” ∧ a⃗ ∈ f ↾ S × T } ∪ {⟨ ⟩}.

ST will be the desired C. Toward this end, first we must verify that ST is a set. The most difficult part of this is that it be well-founded. A member of ^{S}T is given by an f realizing that some U is a total relation. However, there could be many different U’s realized as a total relation by the same f. If we were to stick all those different U’s together, the result might not be well-founded. However, since f ↾ S × T doesn’t depend on U, this is not a problem. The rest of showing that ^{S}T is a set is left to the reader. Next we need a realizer for ^{S}T being a set of total relations. A member of ^{S}T is given by a realizer f that some U is a total relation; that same f will work as such a realizer for the member of ^{S}T named by f (essentially f ↾ S × T). Also, given a U realized by f to be a total relation, we must produce a member V of ^{S}T and a realizer that V ⊆ U. This V will be f ↾ S × T; its name in ^{S}T will be exactly U’s realizer f; and it is easy to realize the necessary set inclusion, as f ↾ S × T is literally a subset of U. We leave to the reader the piecing together of the strands above for the determination of the realizer e showing that ^{S}T is full. The fact that the procedure just sketched will work for any S and T shows that e can be chosen independently of S and T. Observe that not only is ^{S}T full, it is also the set of functions from S to T.

10. strong collection

Suppose

e ⊢ ∀X ∈ S ∃Y ϕ(X, Y).

This implies that

∀⟨a⟩ ∈ S ∃Y {e}(⟨a, Id⟩) ⊢ ϕ(a^{S}, Y),

where Id ⊢ ∀x x = x. By the Axiom of Choice, for each such a let Y_{a} be such a Y. Let Z be

{⟨a, a_{0}, ..., a_{n}⟩ | ⟨a_{0}, ..., a_{n}⟩ ∈ Y_{a}} ∪ {⟨ ⟩}.

Z is as desired.

3 Interpreting Second Order Arithmetic in CZF + full Separation

Within CZF + full Separation, let the natural numbers be given by the set posited by the Strong Infinity Axiom, and let the sets of natural numbers be all subsets of said set. This is a model of Intuitionistic Second Order Arithmetic. It is an already established result that the consistency strength of Second Order Arithmetic is unchanged by going from intuitionistic to classical logic (see for instance [14], where this is shown via a double-negation translation).

References

[1] Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory, in Logic Colloquium ’77 (A. MacIntyre, L. Pacholski, J. Paris, eds.) (North-Holland, Amsterdam, 1978), p. 55-66

[2] Peter Aczel, The type theoretic interpretation of constructive set theory: choice principles, in A.S. Troelstra and D. van Dalen (eds.), The L.E.J. Brouwer Centenary Symposium (North-Holland, Amsterdam, 1982), p. 1-40

[3] Peter Aczel, The type theoretic interpretation of constructive set theory: inductive definitions, in R.B. Marcus et al. (eds.), Logic, Methodology and Philosophy of Science VII (North-Holland, Amsterdam, 1986), p. 17-49

[4] Peter Aczel and Michael Rathjen, Notes on constructive set theory, Technical Report 40, 2000/2001, Mittag-Leffler Institute, Sweden, 2001.

[5] Michael Beeson, Foundations of Constructive Mathematics, Springer-Verlag, Berlin, 1985

[6] W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg, Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Mathematics No. 897, Springer-Verlag, Berlin, 1981

[7] Claire Kouwenhoven-Gentil and Jaap van Oosten, Algebraic Set Theory and the Effective Topos, Journal of Symbolic Logic, to appear; also at http://www.math.uu.nl/people/jvoosten/realizability.html

[8] Robert Lubarsky, Independence results around constructive ZF, Annals of Pure and Applied Logic, 2005, p. 209-225

[9] David McCarty, Realizability and recursive mathematics, Ph.D. thesis, Oxford University (1984) and Carnegie-Mellon University Technical Report CMU-CS-84-131

[10] John Myhill, Constructive set theory, Journal of Symbolic Logic, 1975, p. 347-382

[11] Michael Rathjen, The Strength of Some Martin-Löf Type Theories, Archive for Mathematical Logic, 1994, p. 347-385 [12] Michael Rathjen, The higher infinite in proof theory, in J.A.

Makowsky and E.V. Ravve (eds.), Logic Colloquium ’95, Springer Lecture Notes in Logic, Vol. 11 (Springer, New York, Berlin, 1998), p. 275-304

[13] Alex Simpson, Constructive set theories and their category-theoretic models, in L.Crosilla and P.Schuster, eds., From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, Selected Articles from a Workshop, San Servolo, Venice, Italy, 12–16 May 2003 (Oxford Logic Guides, Oxford University Press, forthcoming)

[14] A.S. Troelstra, Intuitionistic formal systems, in A.S. Troelstra (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics No. 344 (series editors Dold and Eckmann), Springer-Verlag, Berlin-Heidelberg-New York, 1973, ch. 10