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

deﬁnes a presentation of S.

By the lemma it follows that if B has a presentation, the sheaves on the site

**S provide a model for CZF. We observe the following property of the model:**

Proposition A.2 (See [18] and [33, Section 15.6].) Assume B has a presentation. Then Monotone Bar Induction holds in the CZF-model given by sheaves on S.

Corollary A.3 The theory CZF + DC does not prove that B has a presentation.

Proof. If CZF + DC would prove that B has a presentation, then, by the proposition, this would imply that the consistency of CZF + DC implies the consistency of CZF + Monotone Bar Induction. But the latter is known to have greater proof-theoretic strength (see [31]).

Proof. (Of Proposition A.2.) Suppose X ∈ S and S ∈ Pow(NN )(X) is a (small) subsheaf of NN which forms an “internal bar”; i.e., (1) X −(∀α ∈ NN ) (∃n ∈ N) (α(0),..., α(n)) ∈ S, (2) X −(∀u, v ∈ NN ) (u ≤ v ∧ v ∈ S → u ∈ S), (3) X −(∀u ∈ NN ) ((∀n ∈ N )u ∗ n ∈ S → u ∈ S).

The projection π2 : X × B → B at the stage π1 : X × B → X over X represents a (generic) element of the sheaf NN, and (1) implies X × B −(∃n ∈ N) (π2 (0),..., π2 (n)) ∈ S.

By deﬁnition, this means that there is a cover of X ×B by basic opens Ui ×B(vi ) such that for each i we have that (4) (∃n ∈ N) Ui × B(vi ) −(π2 (0),..., π2 (n)) ∈ S (where we simply write S for the restriction of S along Ui × B(vi ) → Ui ⊆ X).

We claim that we can choose the cover Ui × B(vi ) in such a way that for each i it holds that (5) Ui −vi ∈ S.

Indeed, if we can choose the n in (4) such that n ≤ |vi |, then (4) implies (5) by assumption (2) on S. On the other hand, if (4) holds for n |vi |, we can replace the single element Ui × B(vi ) in the cover by all elements of the form Ui × B(w) where w is an extension of vi of length n. Then Ui × B(w) −w ∈ S by (4) and monotonicity of forcing, hence Ui −w ∈ S because projections cover.

Let U × B(v) ∈ S : U ⊆ X open, v ∈ NN and U −v ∈ S.

W= Then W covers X ×B as we have just seen. Moreover, if any U ×B(v) is covered by elements of W then it belongs to W. Indeed, to show this it suﬃces to prove

**the following two properties:**

(6) If {Ui } covers U and Ui × B(v) ∈ W, then U × B(v) ∈ W.

(7) If U × B(v ∗ n ) ∈ W for each n, then U × B(v) ∈ W.

But (6) holds by the local character of forcing, while (7) holds by assumption (3) on S. By induction on covers (Theorem 3.7) we conclude that X − ∈ S, which completes the proof.

B Brouwer ordinals Recall that we deﬁned CZF+ to be any extension of CZF in which the set compactness theorem is provable and which is stable under sheaves. We do not expect that CZF + ACω + “The Brouwer ordinals form a set” is such a theory CZF+. Nevertheless, our main results apply to this theory as well. To show this, we have to prove (1) that this theory proves that formal Baire space is presentable and (2) that this theory is stable under taking sheaves over the double of formal Baire space. In this appendix we work out the details.

First, we recall the deﬁnition of the Brouwer ordinals.

1. Every T ∈ BCov(u) is countable.

Lemma B.3

2. Suppose Rv ∈ BCov(v) is a collection of basic covering sieves indexed by elements v from a sieve T. If T belongs to BCov(u) then so does v∈T Rv.

3. If T ∈ BCov(u) and v ≤ u, then there is an S ∈ BCov(v) such that S ⊆ v∗ ↓ T.

Proof. It suﬃces to prove these statements in the special case where u = ;

in that case, they follow easily by induction on T.

Proposition B.4 (ACω ) (NN, Cov) as deﬁned above is an alternative description of formal Baire space and therefore formal Baire space is presentable whenever the Brouwer ordinals form a set.

Proof. We begin by showing that (NN, Cov) is a formal space. Since maximality is clear and stability follows from item 3 of the previous lemma, it remains to check local character.

Suppose S is a sieve on u and there is a sieve R ∈ Cov(u) such that for all v ∈ R the sieve v ∗ S belongs to Cov(v). Since R ∈ Cov(u) there is a T ∈ BCov(u) such that T ⊆ R. Therefore we have for any v ∈ T that v ∗ S covers v and hence that there is a Z ∈ BCov(v) such that Z ⊆ S. Since T is countable, we can use ACω or the ﬁnite axiom of choice (which is provable in CZF) to choose the elements Z as a function Zv of v ∈ T. Then let K = v∈T Zv. K is covering by the previous lemma and because Zv ⊆ S, K= v∈T the same must be true for S.

It now follows from the discussion preceeding the deﬁnition of BCov(u) above that each BCov(u) will be a set, if the Brouwer ordinals form a set. Hence the formal space (NN, Cov) will be presentable if BO is a set.

To easiest way to prove that we have given a diﬀerent presentation of formal Baire space is to show that Cov is the smallest topology such that ↓ {u ∗ n : n ∈ N} ∈ Cov(u).

Clearly, Cov has this property, so suppose Cov∗ is another. One now shows by induction on T ∈ BCov(u) that ↓ T ∈ Cov∗ (u). This completes the proof.

Corollary B.5 The theory CZF+DC does not prove that the Brouwer ordinals form a set.

Proof. Because this theory does not prove that formal Baire space has a presentation (see Corollary A.3).

It will follow from the next theorem, whose proof will take the remainder of this appendix, that CZF + ACω + “The Brouwer ordinals form a set” is a theory which is stable under taking sheaves over the double of formal Baire space.

Theorem B.6 Let (P, Cov) be a presentable formal space which is CC. Then the combination of ACω and smallness of the Brouwer ordinals implies their joint validity in Sh(P, Cov).

In view of Proposition 4.10 it suﬃces to show that the Brouwer ordinals are small in Sh(P, Cov). To that purpose, we will give an explicit construction of the Brouwer ordinals in this category, from which it can immediately be seen that they are small (the description is a variation on those presented in [10] and [12]).

Let V be the class of all well-founded trees, in which

• nodes are labelled with triples (p, α, ϕ) with p an element of P, α a countable and disjoint subset of ↓ p such that ↓ α ∈ Cov(p) and ϕ a function α → {0, 1},

• edges into nodes labelled with (p, α, ϕ) are labelled with pairs (q, n) with q ∈ α and n ∈ N, in such a way that

• if a node is labelled with (p, α, ϕ) and q ∈ α is such that ϕ(q) = 0, then there is no edge labelled with (q, n) into this node, but

• if a node is labelled with (p, α, ϕ) and q ∈ α is such that ϕ(q) = 1, then there is for every n ∈ N a unique edge into this node labelled with (q, n).

Using that the Brouwer ordinals form a set, one can show also that V is a set. If v denotes a well-founded tree in V, we will also use the letter v for the function that assigns to labels of edges into the root of v the tree attached to this edge.

So if (q, n) is a label of one of the edges into the root of v, we will write v(q, n) for the tree that is attached to this edge; this is again an element of V. Note that an element of V is uniquely determined by the label of its root and the function we just described.

We introduce some terminology and notation: we say that a tree v ∈ V is rooted at an element p in P, if its root has a label whose ﬁrst component is p.

A tree v ∈ V whose root is labelled with (p, α, ϕ) is composable, if for any (q, n) with q ∈ α and ϕ(q) = 1, the tree v(q, n) is rooted at q. We will write W for the set of trees that are hereditarily composable (i.e. not only are they themselves composable, but the same is true for all their subtrees).

**Next, we deﬁne by transﬁnite recursion a relation ∼ on V:**

By transﬁnite induction one veriﬁes that ∼ is an equivalence relation on both V and W. Write BO for the quotient of W by ∼. The following sequence of lemmas establishes that BO can be given the structure of a sheaf and is in fact the object of Brouwer ordinals in the category of sheaves.

**Lemma B.7 BO can be given the structure of a presheaf.**

Proof. Since by deﬁnition of ∼, all trees w ∈ W in an equivalence class are rooted at the same element, we can say without any danger of ambiguity that an element w ∈ BO is rooted at p ∈ P. We will denote the collection of trees in BO rooted at p by BO(p).

Suppose [w] ∈ W(p) and q ≤ p. If the root of w is labelled by (p, α, ϕ), then there is a countable and disjoint reﬁnement β of q ∗ ↓ α (by stability and the fact that (P, Cov) is a CC-space). For each r ∈ β there is a unique q ∈ α such that r ≤ q (by disjointness), so one can deﬁne ψ: β → {0, 1} by ψ(r) = ϕ(q) and, whenever ψ(r) = ϕ(q) = 1, v(r, n) = w(q, n). The data (q, β, ψ) and v determine an element w ∈ W(q) and we put

One easily veriﬁes that this is well-deﬁned and gives BO the structure of a presheaf.

Lemma B.8 BO is separated.

Proof. Suppose T is a sieve covering p and w, w ∈ W(p) are such that [w] t = [w ] t for all t ∈ T. We have to show w ∼ w, so suppose (p, α, ϕ) is the label of the root of w and (p, α, ϕ ) is the label of the root of w. Since w is rooted at p, we have p = p.

Let R consist of those r ∈ (↓ α) ∩ (↓ α ), for which there are q ∈ α and q ∈ α such that (1) r ≤ q, q, (2) ϕ(q) = ϕ (q ) and (3) ϕ(q) = ϕ (q ) = 1 implies w(q, n) ∼ w (q, n) for all n ∈ N. R is a sieve, and the statement of the lemma will follow once we show that it is covering.

Fix an element t ∈ T. Unwinding the deﬁnitions in [w] t = [w ] t gives us the existence of a covering sieve S ⊆ t∗ (↓ α) ∩ t∗ (↓ α ) such that S ⊆ t∗ R. So R is a covering sieve by local character.

**Lemma B.9 BO is a sheaf.**

Proof. Let S be a covering sieve on p and suppose we have a compatible family of elements (wq ∈ BO)q∈S. Let α be a countable and disjoint reﬁnement of S and use ACω to choose for every element q ∈ α a representative (wq ∈ W)q∈α such that [wq ] = wq. For every q ∈ α the representative wq has a root labelled by something of form (q, βq, ϕq ). If we put β = q∈α βq, then β is countable and disjoint and ↓ β covers p (by local character). If r ∈ β, then there is a unique q ∈ α such that r ∈ βq (by disjointness), so therefore it makes sense to deﬁne ϕ(r) = ϕq (r) and w(r, n) = wq (r, n).

We claim the element [w] ∈ BO determine by the data (p, β, ϕ) and the function w just deﬁned is the amalgamation of the elements (wq ∈ BO)q∈S. To that purpose, it suﬃces to prove that [w] q = wq = [wq ] for all q ∈ α. This is not hard, because if q ∈ α and r ∈ βq, then w(r, n) = wq (r, n), by construction.

This completes the proof.

**Lemma B.10 BO is an algebra for the functor F (X) = 1 + X N.**

Proof. We have to describe a natural transformation sup: F (BO) → BO, i.e., a natural transformation 1 → BO and a natural transformation BON → BO.

For the natural transformation 1 → BO, we deﬁne supp (∗) on ∗ ∈ 1(p) to be the equivalence class of the unique element in W determined by the data (p, {p}, ϕ) with ϕ(p) = 0. To deﬁne the natural transformation BON → BO on t: N → BO(p), we use ACω to choose a function t: N → W(p) such that [t(n)] = t(n) for all n ∈ N. Then we deﬁne supp (t) to be the equivalence class of the element w determined by the data (p, {p}, ϕ) with ϕ(p) = 1 and w(p, n) = t(n). We leave the veriﬁcation that this makes sup well-deﬁned and natural to the reader.

** Lemma B.11 BO is the initial algebra for the functor F (X) = 1 + X N.**

Proof. We follow the usual strategy: we show that sup: F (BO) → BO is monic and that BO has no proper F -subalgebras (i.e., we apply Theorem 26 of [8]). It is straightforward to check that sup is monic, so we only show that BO has no proper F -subalgebras, for which we use the inductive properties of V.

Let I be a sheaf and F -subalgebra of BO. We claim that J = {v ∈ V : if v is hereditarily composable, then [v] ∈ I} is such that if all immediate subtrees of an element v ∈ V belong to it, then so does v itself.

Proof: Suppose v ∈ V is a hereditarily composable tree such that all its immediate subtrees belong to J. Assume moreover that (p, α, ϕ) is the label of its root. We know that for all n ∈ N and q ∈ α with ϕ(q) = 1, [v(f, y)] ∈ I and our aim is to show that [v] ∈ I.

For the moment ﬁx an element q ∈ α. Either ϕ(q) = 0 or ϕ(q) = 1. If ϕ(q) = 0, then [v] q equals supq (∗) and therefore [v] q ∈ I, because I is a F -algebra.

If ϕ(q) = 1, then we may put t(n) = [v(q, n)] and [v] q will equal supq (t).

Therefore [v] q ∈ I, again because J is a F -algebra. So for all q ∈ α we have [v] q ∈ I. But then it follows that [v] ∈ I, since I is a sheaf.

We conclude that J = V and I = BO.

This completes the proof of the correctness of our description of the Brouwer ordinals in a category of sheaves and thereby of Theorem B.6.

References [1] P. Aczel. The type theoretic interpretation of constructive set theory. In Logic Colloquium ’77 (Proc. Conf., Wroclaw, 1977), volume 96 of Stud.

Logic Foundations Math., pages 55–66. North-Holland, Amsterdam, 1978.

[2] P. Aczel. The type theoretic interpretation of constructive set theory:

choice principles. In The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Found. Math., pages 1–40.

North-Holland Publishing Co., Amsterdam, 1982.

[3] P. Aczel. The type theoretic interpretation of constructive set theory: inductive deﬁnitions. In Logic, methodology and philosophy of science, VII (Salzburg, 1983), volume 114 of Stud. Logic Found. Math., pages 17–49.

North-Holland Publishing Co., Amsterdam, 1986.

[4] P. Aczel. Aspects of general topology in constructive set theory. Ann. Pure Appl. Logic, 137(1-3):3–29, 2006.

[5] P. Aczel and M. Rathjen. Notes on constructive set theory. Technical Report No. 40, Institut Mittag-Leﬄer, 2000/2001.