# «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 ...»

Maximality is therefore immediate, while stability and local character can be established using straightforward induction arguments. Therefore Cov is indeed a topology. The other statements of the theorem are clear.

** Theorem 3.7 (Induction on covers) Let (P, Cov) be a formal space, whose topology Cov is inductively generated by a covering system C, as in the previous theorem.**

Suppose P (x) is a property of basis elements x ∈ P, such that

and suppose S is a cover of an element a ∈ P such that P (y) holds for all y ∈ S.

Then P (a) holds.

**Proof. Suppose P has the property in the hypothesis of the theorem. Deﬁne:**

S ∈ Cov∗ (p) ⇔ (∀q ≤ p) ((∀r ∈ q ∗ S) P (r)) → P (q).

Then one checks that Cov∗ is a topology extending C. So by Theorem 3.6 we have S ∈ Cov(a) ⊆ Cov∗ (a), from which the desired result follows.

3.3 Formal Baire and Cantor space We will write X N for the set of ﬁnite sequences of elements from X. Elements of X N will usually be denoted by the letters u, v, w,.... Also, we will write u ≤ v if v is an initial segment of u, |v| for the length of v and u ∗ v for the concatenation of sequences u and v. If u ∈ X N and q ≥ |u| is a natural number,

**then we deﬁne u[q] by:**

u[q] = {v ∈ X N : |v| = q and v ≤ u}.

The basis elements of formal Cantor space C are ﬁnite sequences u ∈ 2N (with 2 = {0, 1}), ordered by saying that u ≤ v, whenever v is an initial segment of u. Furthermore, we put S ∈ Cov(u) ⇔ (∃q ≥ |u|) u[q] ⊆ S and BCov(u) = {u[q] : q ≥ |u|}. Note that this will make formal Cantor space compact by deﬁnition (where a formal space is compact, if for every cover S of u there is a K-ﬁnite subset α of S such that ↓ α ∈ Cov(u)).

**Proposition 3.8 Formal Cantor space is a presentable formal space.**

Proof. We leave maximality and stability to the reader and only check local character. Suppose S is a sieve on u for which a sieve R ∈ Cov(u) can be found such that for all v ∈ R the sieve v ∗ S = (↓ v) ∩ S belongs to Cov(v). Since R ∈ Cov(u) there is q ≥ |u| such that u[q] ⊆ R. Therefore we have for any v ∈ u[q] that (↓ v) ∩ S covers v and hence that there is a r ≥ q such that v[r] ⊆ S. Since the set u[q] is ﬁnite, the elements r can be chosen as a function v. For p = max{rv : v ∈ u[q]}, it holds that

as desired.

Formal Baire space B is an example of an inductively deﬁned space. The underlying poset has as elements ﬁnite sequences u ∈ NN, ordered as for Cantor

**space above. The Grothendieck topology is inductively generated by:**

C(u) = {u ∗ n : n ∈ N},

**and therefore we have the following induction principle:**

Corollary 3.9 (Bar Induction for formal Baire space) Suppose P (x) is a property of ﬁnite sequences u ∈ NN, such that

and suppose that S is a cover of v in formal Baire space such that P (x) holds for all x ∈ S. Then P (v) holds.

Note that this means that Bar Induction for formal Baire space is provable.

**As a special case of Theorem 3.6 we have:**

Corollary 3.10 In CZF+ one can show that formal Baire space is presentable.

In contrast, we observe that formal Baire space cannot be shown to be presentable in CZF proper (a proof can be found in Appendix A).

3.4 Points of a formal space The characteristic feature of formal topology is that one takes the notion of basic open as primitive and the notion of a point as derived. In fact, the notion

**of a point is deﬁned as follows:**

Deﬁnition 3.11 A point of a formal space (P, Cov) is an inhabited subset α ⊆ P such that (1) α is upwards closed, (2) α is downwards directed, (3) if S ∈ Cov(a) and a ∈ α, then S ∩ α is inhabited.

We say that a point α belongs to (or is contained in) a basic open p ∈ P if p ∈ α, and we will write ext(p) for the class of points of the basic open p.

If (P, Cov) is a formal space whose points form a set, one can deﬁne a new formal space pt(P, Cov) = (Ppt, Covpt ), whose set of basic opens Ppt is again P,

**but now ordered by:**

p ≤pt q ⇔ ext(p) ⊆ ext(q),

**while the topology is deﬁned by:**

The space pt(P, Cov) will be called the space of points of the formal space (P, Cov). It follows immediately from the deﬁnition of a point that

The other directions of these implications do not hold, in general. Indeed, if they do, one says that the formal space has enough points. It turns out that one can quite easily construct formal spaces that do not have enough points (even in a classical metatheory).

Note that points in formal Cantor space are really functions α: N → {0, 1} and points in formal Baire space are functions α: N → N. In fact, their spaces of points are (isomorphic to) “true” Cantor space and “true” Baire space, respectively. When talking about such points α we will use α both to denote a subset as in Deﬁnition 3.11 and a function on N. In particular, the equivalent notations u∈α⇔α≤u both indicate that u is an initial segment of α.

The following two results were already mentioned in the introduction and are well-known in the impredicative settings of topos theory or intuitionistic set theory IZF. Here we wish to emphasise that they hold in CZF as well.

**Proposition 3.12 The following statements are equivalent:**

(1) Formal Cantor space has enough points.

(2) Cantor space is compact.

(3) The Fan Theorem: If S is a downwards closed subset of 2N and

Proof. The equivalence of (2) and (3) holds by deﬁnition of compactness and the equivalence of (1) and (3) by the deﬁnition of having enough points.

**Proposition 3.13 The following statements are equivalent:**

(1) Formal Baire space has enough points.

(2) Monotone Bar Induction: If S is a downwards closed subset of NN and

(see the construction just before Lemma 3.5). However, since S is downwards closed (by Lemma 3.5), a bar (because S is a bar and S ⊆ S) and inductive (by construction), we may apply Monotone Bar Induction to S to deduce that ∈ S, as desired.

3.5 Morphisms of formal spaces Points are really a special case of morphisms of formal spaces. Here we will assume that the formal spaces we consider are presentable or at least satisfy the additional condition that the collection of basis elements covered by a ﬁxed sieve form a set.

** Deﬁnition 3.14 A continuous map or a morphism of formal spaces F : (P, Cov) → (Q, Cov ) is a subset F ⊆ P × Q such that:**

(1) If F (p, q), p ≤ p and q ≤ q, then F (p, q ).

(2) For every p ∈ P there is a cover S ∈ Cov(p) such that each p ∈ S is related via F to some element q ∈ Q.

(3) For every q, q ∈ Q and element p ∈ P such that F (p, q) and F (p, q ), there is a cover S ∈ Cov(p) such that every p ∈ S is related via F to an element which is smaller than or equal to both q and q.

(4) Whenever F (p, q) and T covers q, there is a sieve S covering p, such that every p ∈ S is related via F to some q ∈ T.

(5) For every q ∈ Q, the set {p : F (p, q)} is closed under the covering relation.

In condition (5) we say that a sieve S is closed under covering relation (or simply closed ), if R ∈ Cov(a), R ⊆ S =⇒ a ∈ S.

To help the reader to make sense of this deﬁnition, it might be good to recall some facts from locale theory (see [25]). A locale is a partially ordered class A which has ﬁnite meets and small joins, with the small joins distributing over the ﬁnite meets. In addition, a morphism of locales A → B is a map B → A preserving ﬁnite meets and small joins.

Every formal space (P, Cov) determines a locale Idl(P, Cov), whose elements are the closed sieves on P, ordered by inclusion. Moreover, every morphism of locales ϕ: Idl(P, Cov) → Idl(Q, Cov ) determines a relation F ⊆ P × Q by p ∈ ϕ(q), with q being the least closed sieve containing q. The reader should verify that this relation F has the properties of a map of formal spaces and that every such F determines a unique morphism of locales ϕ: Idl(P, Cov) → Idl(Q, Cov ).

Together with the continuous maps the class of formal spaces organises itself into a superlarge category, with composition given by composition of relations and identity I: (P, Cov) → (P, Cov) by I(p, q) ⇐⇒ (∃S ∈ Cov(p)) (∀r ∈ S) r ≤ q.

(if the formal space is subcanonical (p =↓ p for all p ∈ P ), this simpliﬁes to I(p, q) iﬀ p ≤ q). Note that in a predicative metatheory, this category cannot be expected to be locally small.

A point of a formal space (P, Cov) is really the same thing as a map 1 → (P, Cov), where 1 is the one-point space ({∗}, Cov ) with Cov (∗) = {∗}.

Indeed, if F : 1 → (P, Cov) is a map, then α = {p ∈ P : F (∗, p)} is a point, and, conversely, if α is a point, then F (∗, p) ⇔ p ∈ α deﬁnes a map. Moreover, these operations are clearly mutually inverse. This implies that any continuous map F : (P, Cov) → (Q, Cov ) induces a function pt(F ): pt(P, Cov) → pt(Q, Cov ) (by postcomposition). Since this map is continuous, pt deﬁnes an endofunctor on the category of those formal spaces on which pt is well-deﬁned.

In addition, we have for any formal space (P, Cov) on which pt is well-deﬁned a continuous map F : pt(P, Cov) → (P, Cov) given by F (p, q) iﬀ ext(p) ⊆ ext(q).

This map F is an isomorphism precisely when (P, Cov) has enough points. (In fact, F is the component at (P, Cov) of a natural transformation pt ⇒ id.)

3.6 The double of a formal space Although the Fan Theorem and Monotone Bar Induction are not provable in CZF, we will show below that they do hold as derived rules. For that purpose, we use a construction on formal spaces, which is due to Joyal and which we have dubbed the “double construction”.2 This construction will enable us to relate the sheaf semantics over a formal space to external truth (see part 3 of Lemma 4.2). The best way to explain it is to consider the analogous construction for ordinary topological spaces ﬁrst.

Starting from a topological space X, the double construction takes two disjoint copies of X, so that every subset of it can be considered as a pair (U, V ) of subsets of X. Such a pair will be open, if U is open in X and U ⊆ V. Note that we do not require V to be open in X: V can be an arbitrary subset of X.

Therefore the double construction can be seen as a kind of mapping cylinder with Sierpi´ski space replacing the unit interval: the ordinary mapping cylinder n of a map f : Y → X is obtained by taking the space [0, 1] × Y + X and then identifying points (0, y) with f (y) (for all y ∈ Y ). The double of a space X is obtained from this construction by replacing the unit interval [0, 1] by Sierpi´ski n space and considering the canonical map Xdiscr → X.

The construction for formal spaces is now as follows: suppose (U, Cov) is a formal space whose points form a set Q. The set of basic opens of D(U, Cov) = (UD, CovD ) is D(u) : u ∈ U + {q} : q ∈ Q.

Here both D(u) and {q} are formal symbols for a basic open, representing the pairs (u, u) and (∅, {q}) in the topological case. The preorder on UD is generated

**by:**

D(v) ≤ D(u) if v ≤ u in U, {q} ≤ D(v) if v ∈ q, {p} ≤ {q} if p = q.

In addition, the covering relation is given by

Proposition 3.15 D(U, Cov) as deﬁned above is a formal space, which is presentable, whenever (U, Cov) is.

Proof. This routine veriﬁcation we leave to the reader. Note that if BCov is a presentation for the covering relation Cov, then

is a presentation for CovD.

2 See [33, Section 15.4]. This construction is known in the impredicative case for locales, but here we wish to emphasise that it works in a predicative setting for formal spaces as well.

The formal space D(U, Cov) comes equipped with three continuous maps.

First of all, there is a closed map µ: (U, Cov) → D(U, Cov) given by µ(u, p) iﬀ p = D(v) for some v ∈ U with I(u, v). In addition, there is a map π: D(U, Cov) → (U, Cov) given by π(p, u) iﬀ there is a v ∈ U with u = D(v) and I(v, u). Note that π ◦µ = id. And, ﬁnally, there is an open map of the form ν: (U, Cov)discr → D(U, Cov). The domain of this map (U, Cov)discr is the formal space whose basic opens are singletons {q} (with the discrete ordering) and whose only covering sieves are the maximal ones. The map ν is then given by ν({q}, u) iﬀ u = {q}.

**We depict these maps in the following diagram:**

4 Sheaf models In [19] and [12] it is shown how sheaves over a presentable formal space give rise to a model of CZF. Moreover, since this fact is provable within CZF itself, sheaf models can be used to establish proof-theoretic facts about CZF, such as derived rules. We will exploit this fact to prove Derived Fan and Bar Induction rules for (extensions of) CZF.

**4.1 Basic properties of sheaf semantics**

We recapitulate the most important facts about sheaf models below. We hope this allows the reader who is not familiar with sheaf models to gain the necessary informal understanding to make sense of the proofs in this section. The reader who wants to know more or wishes to see some proofs, should consult [19] and [12].

A presheaf X over a preorder P is a functor X: Pop → Sets. This means that X is given by a family of sets X(p), indexed by elements p ∈ P, and a

**family of restriction operations − q: X(p) → X(q) for q ≤ p, satisfying:**

Given a topology Cov on P, a presheaf X will be called a sheaf, if it satisﬁes the

**following condition:**