# «Derived rules for predicative set theory: an application of sheaves Benno van den Berg & Ieke Moerdijk November 16, 2011 Abstract We show how one may ...»

**Derived rules for predicative set theory:**

an application of sheaves

Benno van den Berg & Ieke Moerdijk

November 16, 2011

Abstract

We show how one may establish proof-theoretic results for constructive

Zermelo-Fraenkel set theory, such as the compactness rule for Cantor

space and the Bar Induction rule for Baire space, by constructing sheaf

models and using their preservation properties.

1 Introduction

This paper is concerned with Aczel’s predicative constructive set theory CZF and with related systems for predicative algebraic set theory; it also studies extensions of CZF, for example by the axiom of countable choice.

We are particularly interested in certain statements about Cantor space 2N, Baire space NN and the unit interval [0, 1] of Dedekind real numbers in such theories, namely the compactness of 2N and of [0, 1], and the related “Bar Induction” property for Baire space. The latter property states that if S is a set of ﬁnite sequences of natural numbers for which

- for each α there is an n such that α(0), α(1),...., α(n) belongs to S (“S is a bar”),

- if u belongs to S then so does every extension of u (“S is monotone”),

- if u is a ﬁnite sequence for which the concatenation u ∗ n belongs to S for all n, then u belongs to S (“S is inductive”), then the empty sequence belongs to S. It is well-known that these statements, compactness of 2N and of [0, 1] and Bar Induction for NN, cannot be derived in intuitionistic set or type theories. In fact, they fail in sheaf models over locales, as explained in [17]. Sheaf models can also be used to show that all implications in the chain (BI) =⇒ (F T ) =⇒ (HB) are strict (where BI stands for Bar Induction for NN, while FT stands for the Fan Theorem (compactness of 2N ) and HB stands for the Heine-Borel Theorem (compactness of the unit interval), see [27]).

On the other hand, one may also deﬁne Cantor space C, Baire space B, and the unit interval I as locales or formal spaces. Compactness is provable for formal Cantor space, as is Bar Induction for formal Baire space. Although Bar Induction may seem to be a statement of a slightly diﬀerent nature, it is completely analogous to compactness, as explained in [17] as well. Indeed, the locales C and I have enough points (i.e., are true topological spaces) iﬀ the spaces 2N and [0, 1] are compact, while the locale B has enough points iﬀ Bar Induction holds for the space NN. The goal of this paper is to prove that the compactness properties of these (topological) spaces do hold for CZF (with countable choice), however, when they are reformulated as derived rules. Thus, for example, Cantor space is compact in the sense that if S is a property of ﬁnite sequencesof 0’s and 1’s which is deﬁnable in the language of set theory and for which CZF proves for all α in 2N there is an n such that α(0), α(1),...., α(n) belongs to S (“S is a cover”), then there are such ﬁnite sequences u1,..., uk for which CZF proves that each ui belongs to S as well as that for each α as above there are an n and an i such that α(0), α(1),...., α(n) = ui. We will also show that compactness of the unit interval and Bar Induction hold when formulated as derived rules for CZF and suitable extensions of CZF, respectively.

This is a proof-theoretic result, which we will derive by purely model-theoretic means, using sheaf models for CZF and a doubling construction for locales originating with Joyal. Although our results for the particular theory CZF seem to be new, similar results occur in the literature for other constructive systems, and are proved by various methods, such as purely proof-theoretic methods, realizability methods or our sheaf-theoretic methods.1 In this context it is important to observe that derived rules of the kind “if T proves ϕ, then T proves ψ” are diﬀerent results for diﬀerent T, and can be related only in the presence of conservativity results. For example, a result for CZF like the ones above does not imply a similar result for the extension of CZF with countable choice, or vice versa.

Our motivation to give detailed proofs of several derived rules comes from various sources. First of all, the related results just mentioned predate the theFor example, Beeson in [6] used a mixture of forcing and realizability for Feferman-style systems for explicit mathematics. Hayashi used proof-theoretic methods for HAH, the system for higher-order Heyting arithmetic corresponding to the theory of elementary toposes in [23], and sheaf-theoretic methods in [24] for the impredicative set theory IZF, an intuitionistic version of Zermelo-Fraenkel set theory. Grayson [22] gives a sheaf-theoretic proof of a local continuity rule for the system HAH, and mentions in [21] that the method should also apply to systems without powerset.

ory CZF, which is now considered as one of the most robust axiomatisations of predicative constructive set theory and is closely related to Martin-L¨f type o theory [1, 2, 3]. Secondly, the theory of sheaf models for CZF has only recently been ﬁrmly established (see [19, 20, 12]), partly in order to make applications to proof theory such as the ones exposed in this paper possible. Thirdly, the particular sheaf models over locales necessary for our application hinge on some subtle properties and constructions of locales (or formal spaces) in the predicative context, such as the inductive deﬁnition of covers in formal Baire space in the absence of power sets. These aspects of predicative locale theory have only recently emerged in the literature [14, 4]. In these references, the regular extension axiom REA plays an important role. In fact, one needs an extension of CZF, which on the one hand is suﬃciently strong to handle suitable inductive deﬁnitions, while on the other hand it is stable under sheaf extensions. One possible choice is the extension of CZF by the smallness axiom for W-types and the axiom of multiple choice AMC (see [13]).

**The results of this paper were presented by the authors on various occasions:**

by the second author in July 2009 at the TACL’2009 conference in Amsterdam and in March 2010 in the logic seminar in Manchester and by the ﬁrst author in May 2010 at the meeting “Set theory: classical and constructive”, again in Amsterdam. We would like to thank the organizers of all these events for giving us these opportunities. We are also grateful to the referee for a very careful reading of the original manuscript and to the editors for their patience.

2 Constructive set theory Throughout the paper we work in Aczel’s constructive set theory CZF, or extensions thereof. (An excellent reference for CZF is [5].)

CZF is a set theory whose underlying logic is intuitionistic and whose axioms

**are:**

Extensionality: ∀x ( x ∈ a ↔ x ∈ b ) → a = b.

Empty set: ∃x ∀y ¬y ∈ x.

Pairing: ∃x ∀y ( y ∈ x ↔ y = a ∨ y = b ).

Union: ∃x ∀y ( y ∈ x ↔ ∃z ∈ a y ∈ z ).

Set induction: ∀x ∀y ∈ x ϕ(y) → ϕ(x) → ∀x ϕ(x).

Inﬁnity: ∃a ( ∃x x ∈ a ) ∧ ( ∀x ∈ a ∃y ∈ a x ∈ y ).

Bounded separation: ∃x ∀y y ∈ x ↔ y ∈ a∧ϕ(y), for any bounded formula ϕ in which a does not occur.

Strong collection: ∀x ∈ a ∃y ϕ(x, y) → ∃b B(x ∈ a, y ∈ b) ϕ.

Subset collection: ∃c ∀z ∀x ∈ a ∃y ∈ b ϕ(x, y, z) → ∃d ∈ c B(x ∈ a, y ∈

d) ϕ(x, y, z).

In the last two axioms, the expression

has been used as an abbreviation for ∀x ∈ a ∃y ∈ b ϕ ∧ ∀y ∈ b ∃x ∈ a ϕ.

Throughout this paper, we will use denumerable to mean “in bijective correspondence with the set of natural numbers” and ﬁnite to mean “in bijective correspondence with an initial segment of natural numbers”. A set which is either ﬁnite or denumerable, will be called countable. In addition, we will call a set K-ﬁnite, if it is the surjective image of an initial segment of the natural numbers. Observe that if a set has decidable equality, then it is ﬁnite if and only if it is K-ﬁnite.

In this paper we will also consider the following choice principles (countable

**choice and dependent choice):**

It is well-known that DC implies ACω, but not conversely (not even in ZF).

Any use of these additional axioms will be indicated explicitly.

2.2 Inductive deﬁnitions in CZF Deﬁnition 2.1 Let S be a class. We will write Pow(S) for the class of subsets of S. An inductive deﬁnition is a subclass Φ of Pow(S) × S. One should think of the pairs (X, a) ∈ Φ as rules of the kind: if all elements in X have a certain property, then so does a. Accordingly, a subclass A of S will be called Φ-closed, if X⊆A⇒a∈A whenever (X, a) is in Φ.

In CZF one can prove that for any inductive deﬁnition Φ on a class S and for any subclass U of S there is a least Φ-closed subclass of S containing U (see [5]). We will denote this class by I(Φ, U ). However, for the purposes of

**predicative locale theory one would like to have more:**

** Theorem 2.2 (Set Compactness) If S and Φ are sets, then there is a subset B of Pow(S) such that for each set U ⊆ S and each a ∈ I(Φ, U ) there is a set V ∈ B such that V ⊆ U and a ∈ I(Φ, V ).**

This result cannot be proved in CZF proper, but it can be proved in extensions of CZF. For example, this result becomes provable in CZF extended with Aczel’s regular extension axiom REA [5] or in CZF extended with the axioms WS and AMC [13]. The latter extension is known to be stable under sheaves [29, 13], while the former presumably is as well. Below, we will denote by CZF+ any extension of CZF which allows one to prove set compactness and which is stable under sheaves.

3 Predicative locale theory In this section we have collected the deﬁnitions and results from predicative locale theory that we need in order to establish derived rules for CZF. We have tried to keep our presentation self-contained, so that this section can actually be considered as a crash course on predicative locale theory or “formal topology”.

(In a predicative context, locales are usually called “formal spaces”, hence the name. Some important references for formal topology are [16, 14, 32, 4] and, unless we indicate explicitly otherwise, the reader may ﬁnd the results explained in this section in these sources.)

**3.1 Formal spaces**

Deﬁnition 3.1 A formal space is a small site whose underlying category is a preorder. By a preorder, we mean a set P together with a small relation ≤ ⊆ P × P which is both reﬂexive and transitive. If a is an element of P then we will write ↓ a or Ma for {p ∈ P : p ≤ a}, and if α is a subset of P then we will write ↓ α = {p ∈ P : (∃a ∈ α) p ≤ a}. For the beneﬁt of the reader, we repeat the axioms for a site from [12] for the special case of preorders.

Fix an element a ∈ P. By a sieve on a we will mean a downwards closed subset of ↓ a. The set Ma = ↓ a will be called the maximal sieve on a. In a predicative setting, the sieves on a form in general only a class.

If S is a sieve on a and b ≤ a, then we write b∗ S for the sieve b∗ S = S ∩ ↓ b on b. We will call this sieve the restriction of S to b.

A (Grothendieck) topology Cov on P is given by assigning to every object

**a ∈ P a collection of sieves Cov(a) such that the following axioms are satisﬁed:**

(Maximality) The maximal sieve Ma belongs to Cov(a).

(Stability) If S belongs to Cov(a) and b ≤ a, then b∗ S belongs to Cov(b).

(Local character) Suppose S is a sieve on a. If R ∈ Cov(a) and all restrictions b∗ S to elements b ∈ R belong to Cov(b), then S ∈ Cov(a).

A pair (P, Cov) consisting of a preorder P and a Grothendieck topology Cov on it is called a formal topology or a formal space. If a formal topology (P, Cov) has been ﬁxed, the elements of P will be referred to as basic opens or basis elements and the sieves belonging to some Cov(a) will be referred to as the covering sieves. If S belongs to Cov(a) one says that S is a sieve covering a, or that a is covered by S.

To develop a predicative theory of locales one needs to assume that the formal spaces one works with have a presentation, in the following sense. (Note that it was a standing assumption in [12] that sites had a presentation.) Deﬁnition 3.2 A presentation for a formal topology (P, Cov) is a function BCov assigning to every a ∈ P a small collection of basic covering sieves

**BCov(a) such that:**

A formal topology which has a basis will be called presentable.

One of the ways in which presentable formal spaces behave better than general ones, is that, in CZF, only presentable formal spaces give rise to categories of sheaves again modelling CZF (see Theorem 4.3 and Remark 4.4 below). For this reason, it will be an important theme in this section to sort out whether the concrete formal spaces we work with can be proved to be presentable in CZF or in extensions thereof.

Remark 3.3 Another property of presentable formal spaces, which is sometimes useful, is that for a given sieve S the collection of a ∈ P which are covered by S form a set, as it can be written as

This property is often included in the deﬁnition of a formal space, but for our purposes this was not necessary. (We thank Giovanni Curi for bringing this issue to our attention; see also [15].)

3.2 Inductively generated formal topologies Deﬁnition 3.4 If P is a preorder, then a covering system is a map C assigning to every a ∈ P a small collection C(a) of subsets of ↓ a such that the following

**covering axiom holds:**

Both statements are now proved by an induction argument, using the covering axiom.

** Theorem 3.6 Every covering system generates a formal topology.**

More precisely, for every covering system C there is a smallest Grothendieck topology Cov such that α ∈ C(a) =⇒↓ α ∈ Cov(a).

In CZF+ one can show that this formal topology has a presentation.