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

For any given sieve S ∈ Cov(p) and family {xq ∈ X(q) : q ∈ S}, which is compatible, meaning that (xq ) r = xr for every r ≤ q ∈ S, there is a unique x ∈ X(p) (the “amalgamation” of the compatible family) such that x q = xq for all q ∈ S.

** Lemma 4.1 If a formal space (P, Cov) is generated by a covering system C, then it suﬃces to check the sheaf axiom for those families which belong to the covering system.**

Proof. Suppose X is a presheaf satisfying the sheaf axiom with respect to the

**covering system C, in the following sense:**

Therefore Cov ⊆ Cov∗, which implies that X is a sheaf with respect to the Grothendieck topology Cov.

A morphism of presheaves F : X → Y is a natural transformation, meaning that it consists of functions {Fp : X(p) → Y (p) : p ∈ P} such that for all q ≤ p

**we have a commuting square:**

The category of sheaves is a full subcategory of the category of presheaves, so every natural transformation F : X → Y between sheaves X and Y is regarded as a morphism of sheaves.

The category of sheaves is a Heyting category and therefore has an “internal logic”. This internal logic can be seen as a a generalisation of forcing, in that truth in the model can be explained using a binary relation between elements

**Lemma 4.2 Sheaf semantics has the following properties:**

1. (Monotonicity) If p −ϕ and q ≤ p, then q −ϕ.

2. (Local character) If S covers p and q −ϕ for all q ∈ S, then p −ϕ.

3. If p is minimal (so q ≤ p implies q = p) and Cov(p) = {p}, then forcing at p coincides with truth, i.e., we have ϕ iﬀ p −ϕ.

Proof. By induction on the structure of ϕ.

Note, in connection with Section 3.6, that every element of the form {q} in the double forms a minimal element to which the hypothesis of part 3 of Lemma

4.2 applies.

Using this forcing relation, one deﬁnes truth in the model as being forced by every condition p ∈ P. If P has a top element 1, this coincides with being forced at this element (by monotonicity).

One way to see sheaf semantics is as a generalisation of forcing for classical

**set theory, which one retrieves by putting:**

S ∈ Cov(p) ⇔ S is dense below p.

Forcing for this speciﬁc forcing relation validates classical logic, but in general sheaf semantics will only validate intuitionistic logic.

Sheaf semantics as described above is a way of interpreting ﬁrst-order theories in a category of sheaves over (P, Cov). To obtain a semantics for the language of set theory, one uses the machinery of algebraic set theory and proceeds as follows (see [29, 9, 11]). Let π: E → U be the universal small map in the category of sheaves and let V = W (π)/ ∼ be the extensional (Mostowski) collapse of the W-type W = W (π). Like any W-type, W comes equipped with a relation M generated by t(e) M supu (t) for any e ∈ Eu and t: Eu → W. This relation M descends to a well-deﬁned relation on V, which interprets the membership symbol in the language of set

**theory and will be denoted by. For the resulting model (V, ) we have:**

** Theorem 4.3 If (P, Cov) is a presentable formal space, then sheaf semantics over (P, Cov) is sound for CZF, as it is for CZF extended with small W-types WS and the axiom of multiple choice AMC.**

Moreover, the former is provable within CZF, while the latter is provable in CZF + WS + AMC.

Proof. This is proved in [12, 29] for the general case of sheaves over a site. For the speciﬁc case of sheaves on a formal space and CZF alone, this was proved earlier by Gambino in terms of Heyting-valued models [19, 20].

** Remark 4.4 The requirement that (P, Cov) has a presentation is essential: the theorem is false without it (see [20]).**

Therefore we will assume from now on that (P, Cov) is presentable.

For the proofs below we need to compute various objects related to Cantor space and Baire space in diﬀerent categories of sheaves. We will discuss the construction of N in sheaves in some detail: this will hopefully give the reader suﬃciently many hints to see why the formulas we give for the others are correct.

To compute N in sheaves, one ﬁrst computes N in presheaves, where it is pointwise constant N. The corresponding object in sheaves is obtained by sheaﬁfying this object, which means by twice applying the plus-construction (the standard treatment as in [26] can also be followed in CZF). In case every covering sieve is inhabited, the presheaf N is already separated, so then it suﬃces

**to apply the plus-construction only once. In that case, we obtain:**

= {(S, ϕ) : S ∈ Cov(p), ϕ: S → N compatible}/ ∼, N(p) with (S, ϕ) ∼ (T, ψ), if there is an R ∈ Cov(p) with R ⊆ S ∩ T and ϕ(r) = ψ(r) for all r ∈ R, and (S, ϕ) q = (q ∗ S, ϕ q ∗ S).

** Remark 4.5 If P has a top element 1 (as often is the case), then elements of N(1) correspond to continuous functions (P, Cov) → Ndiscr.**

** Remark 4.6 Borrowing terminology from Boolean-valued models [7], we could call elements of N(p) of the form (Mp, ϕ) pure and others mixed (recall that Mp =↓ p is the maximal sieve on p).**

As one sees from the description of N in sheaves, the pure elements lie dense in this object, meaning that for every x ∈ N(p), {q ≤ p : x q is pure} ∈ Cov(p).

This, together with the local character of sheaf semantics, has the useful consequence that in the clauses for the quantiﬁers p −(∃x ∈ N) ϕ(x) ⇔ {q ≤ p : (∃x ∈ N(q)) q −ϕ(x)} ∈ Cov(p) p −(∀x ∈ N) ϕ(x) ⇔ (∀q ≤ p) (∀x ∈ N(q)) q −ϕ(x) one may restrict one’s attention to those x ∈ N(q) that are pure.

**We also have the following useful formulas:**

All these objects come equipped with the obvious equivalence relations and restriction operations. We will not show the correctness of these formulas, which

**relies heavily on the following fact:**

Proposition 4.7 [26, Proposition III.1, p. 136] The sheaves form an exponential ideal in the category of presheaves, so if X is a sheaf and Y is a presheaf, then X Y (as computed in presheaves) is a sheaf.

From these formulas one sees that, if P has a top element 1, then 2N (1) can be identiﬁed with the set of continuous functions (P, Cov) → C to formal Cantor space and NN (1) with the set of continuous functions (P, Cov) → B to formal Baire space. Also, in 2N and NN the “pure” elements are again dense. (But this is not true for 2N and NN, in general.)

4.2 Choice principles For our purposes it will be convenient to introduce the following ad hoc terminology.

Deﬁnition 4.8 A formal space (P, Cov) will be called a CC-space, if every cover has a countable, disjoint reﬁnement. This means that for every S ∈ Cov(p), there is a countable α ⊆ S such that ↓ α ∈ Cov(p) and for all p, q ∈ α, either p = q or ↓ p ∩ ↓ q = ∅.

** Example 4.9 Formal Cantor space is a CC-space and if ACω holds, then so is formal Baire space (see Proposition B.**

4). Also, doubles of CC-spaces are again CC.

Our main reason for introducing the notion of a CC-space is the following

**proposition, which is folklore (see, for instance, [21]):**

Proposition 4.10 Suppose (P, Cov) is a presentable formal space which is CC.

If DC or ACω holds in the metatheory, then the same choice principle holds in Sh(P, Cov). Moreover, this fact is provable in CZF.

Proof. We check this for ACω, the argument for DC being very similar. So suppose X is some sheaf and

Using that the pure elements in N are dense (Remark 4.6), this means that for every n ∈ N there is a cover S ∈ Cov(p) such that for all q ∈ S there is an x ∈ X(q) such that q −ϕ(n, x).

Because the space is assumed to be CC we have S =↓ α for a set α which is countable and disjoint. Furthermore, since ACω holds, the x ∈ X(q) can be chosen as a function of n ∈ N and q ∈ α. As α is disjoint, we can therefore amalgamate the xq,n ∈ X(q) to an element xn ∈ X(p) such that

So if we set f (n) = xn we obtain the desired result.

5 Main results In this ﬁnal section we present the main results of this paper: the validity of various derived rules for CZF and its extension of the form CZF+. A system of a slightly diﬀerent kind to which these results apply as well will be discussed in Appendix B. The proofs are based on the fact that an appropriate predicative formulation of sheaf semantics can be proved inside CZF to be sound for CZF, together with the special features of the double construction mentioned after Lemma 4.2.

** Theorem 5.1 (Derived Fan Rule) Suppose ϕ(x) is a deﬁnable property of elements u ∈ 2N.**

If

Proof. We work in CZF. We pass to sheaves over the double of formal Cantor space D(C), where there is a global section π of the exponential sheaf 2N deﬁned by letting π(n) be the equivalence class of

Under the correspondence between such global sections with continuous functions D(C) → C, this is precisely the map π from Section 3.7 (second map in the list).

** Remark 5.2 By using the fact that CZF has the numerical existence property [30] we see that the conclusion of the previous theorem could be strengthened (∀v ∈ [n]) ϕ(v).**

to: then there is a natural number n such that CZF Indeed, there is a primitive recursive algorithm for extracting this n from a formal derivation in CZF.

** Remark 5.3 It is not hard to show that CZF proves the existence of a deﬁnable surjection 2N → [0, 1]Cauchy from Cantor space to the set of Cauchy reals lying in the unit interval.**

This, in combination with Theorem 5.1, implies that one also has a derived local compactness rule for the Cauchy reals in CZF. It also implies that we have a local compactness rule for the Dedekind reals in CZF + ACω and in CZF + DC, because both ACω and DC are stable under sheaves over the double of formal Cantor space (see Proposition 4.10) and using either of these two axioms, one can show that the Cauchy and Dedekind reals coincide.

Recall that we use CZF+ to denote any theory extending CZF which allows one to prove set compactness and which is stable under sheaves.

Proof. We reason in CZF+. We pass to sheaves over the double of formal Baire space D(B), where there is a global section π of the sheaf NN deﬁned by letting π(n) be the equivalence class of

Now D(v) −π ∈ u implies v ≤ u and because sheaf semantics is monotone this in turn implies D(v) −ϕ(v). By choosing a point α ∈ v and using monotonicity again, one obtains that {α} −ϕ(v), and hence ϕ(v) by part 3 of Lemma 4.2.

Summarising: we have a cover S such that for all v ∈ S the statement ϕ(v) holds. Hence ϕ( ) holds by Corollary 3.9.

** Theorem 5.5 (Derived Continuity Rule for Baire Space) Suppose ϕ(x, y) is a formula deﬁning a subset of NN ×NN.**

If CZF+ (∀α ∈ NN ) (∃!β ∈ NN ) ϕ(α, β), then

Proof. Again, we work in CZF+ and pass to sheaves over the double of formal Baire space D(B), where there is a global section of the sheaf NN, namely the projection π: D(B) → B. Since

Consider the maps µ: B → D(B) and ν: Bdiscr → D(B) from Section 3.7.

The continuity of ρ implies that pt(ρµ) = pt(ρν): NN → NN ; writing f = pt(ρµ), one sees that f : NN → NN is continuous. Moreover, if α ∈ NN, then {α} −ϕ(pt(π)(α), pt(ρ)(α)), i.e. {α} −ϕ(α, f (α)), and hence ϕ(α, f (α)).

** These proofs can be adapted in various ways to prove similar results for (extensions of) CZF, for instance:**

- Theorem 5.1 holds for any extension of CZF which is stable under sheaves over the double of formal Cantor space, such as the extension of CZF with choice principles like DC or ACω (because of Proposition 4.10).

- For the same reason Theorem 5.4 and Theorem 5.5 remain valid if we extend CZF+ with choice principles. These results also hold for the theory CZF + ACω + “The Brouwer ordinals form a set” (see Appendix B).

- The same method of proof as in Theorem 5.5 should establish a derived continuity rule for the Dedekind reals and many other deﬁnable formal spaces.

A Independence of presentability of formal Baire space in CZF The aim of this appendix is to show that CZF does not prove the existence of a presentation of formal Baire space. For this purpose, we use forcing over a site as in [12] rather than forcing over a formal space. Recall that in [12] we showed that what happens when one does forcing over a site is completely analogous to what happens when one does forcing over a formal space: it leads, provably in CZF, to a sound semantics of CZF, as long as the site is assumed to have a presentation (see [12] for the deﬁnition of a presentation for a site).

Let S be a small category of formal spaces and continuous maps, whose objects are basic open subsets of Bn of the form B(u1 ) ×... × B(un ) (where u1,..., un ∈ NN and we write B(u) for the basic open determined by the ﬁnite sequence u) and whose maps contain the inclusions between open subsets and the projections. (For example, S could be given by these objects and all continuous maps between them.) Equip S with the Grothendieck topology induced by the open covers of the formal space S and the projections (the latter are automatically included if, for example, constant maps are included so that projections have sections in S).

Lemma A.1 If B has a presentation, then so does S.

Proof. This is clear from the fact that if B has a presentation, so does each B(u1 ) ×... × B(un ). In fact, to be explicit, for X = B(u1 ) ×... × B(un ) the formula