WWW.THESIS.DISLIB.INFO FREE ELECTRONIC LIBRARY - Online materials, documents

<< HOME
CONTACTS

Pages:     | 1 |   ...   | 2 | 3 || 5 |

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

-- [ Page 4 ] --

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.

Pages:     | 1 |   ...   | 2 | 3 || 5 |

Similar works:

«Length-weight relationships adapted to freshwater prawn Macrobrachium rosenbergii morphological types.GILLES MER, JEAN-CLAUDE FALGUIERE, DENIS LACROIX, PHILIPPE GONDOUIN and GILBERT DUTTO, IFREMER GIE RA. BP 477. 97331 CAYENNE Cedex FRENCH GUIANA. ABSTRACT The social organization in a Macrobrachium rosenbergii population involves the emergence of different subpopulations (blue and orange claws males, small males, berried and nonberried females). In a population, prawns of a same size can get...»

«Cleveland Clinic Vendor Representative Handbook Cleveland Clinic Supply Chain Management 1950 Richmond Rd. TR301 Lyndhurst, OH 44124 Telephone: 216-448-8000 Fax: 216-448-8080 April 2015 Page 1 of 13 Table of Contents Vision and Mission Statements Supplier Information Supplier Code of Conduct Visits within Cleveland Clinic Vendor Credentialing Process Compliance Requirements Access to the OR Non-Compliance Supplier Diversity Contacting the Supply Chain Management Department Service Calls Product...»

«A coloring book and guide to prayer Pray by the best-selling author of Praying in Color color and Sybil MacBeth paraclete press BREWSTER, MASSACHUSETTS In Gratitude for the Life of Phyllis Tickle The most colorful and prayerful woman I have known 2016 First printing Pray and Color: A coloring book and guide to prayer by the best-selling author of Praying in Color Copyright © 2016 by Sybil MacBeth ISBN 978-1-61261-827-2 Unless otherwise marked, Scripture references are taken from the New...»

«President’s Convocation and Welcome Back Address Dianne F. Harrison, Ph.D. President California State University, Northridge Thursday, August 21, 2014 Valley Performing Arts Center at California State University, Northridge Program 9 a.m. Introduction by Faculty President Shane Frehlich Welcome by A.S. President Tiffany Zaich Welcome Back Address by President Dianne F. Harrison Reception / Welcome Back Gathering UNIVERSITY PRIORITIES 1. Student success 2. Focus on employees for success 3....»

«AMPLEFORTH COLLEGE SIXTH FORM OPTIONS BOOKLET 2015-16 -iCONTENTS CONTENTS The benefits of life in the Sixth Form Becoming an independent learner Sixth Form Prep Study periods The importance of Year 12 Introduction Reformed A levels in 2015 What is the effect of these reforms? Timescale for subject reforms Unreformed A levels – change here also AS levels in reformed A levels subjects Ampleforth College Sixth Form curriculum Extended Project Qualification (EPQ) Choice of subjects Seeking help...»

«REPORT ON THE FIRST MONITORING AND ADVISORY MEETING FOR THE EUROPEAN CAPITALS OF CULTURE 2016 Issued by The Monitoring and Advisory Panel for the European Capital of Culture October 2013 This is the report of the Monitoring and Advisory Panel following the first monitoring and advisory meeting concerning the 2016 European Capitals of Culture, namely Wrocław (Poland) and Donostia San Sebastián (Spain), which took place on 15 October 2013 in Brussels. 1. BACKGROUND Designation of Wrocław and...»

«Universalism Unravels Lynn M. LoPucki1 I. Trying to Fix Universalism.................................................... 6 A. Claiming Cases....................................................... 6 1. Judge Bufford’s Due Process Proposal............................... 7 2. Due Process Will Not Solve the Problem..........................»

«ISSN: 2443-6348 Analytical Web Note 6/2015 High and rising inequalities; what can be done about it (at EU level)? Employment, Social Affairs & Inclusion High and rising inequalities; what can be done about it (at EU level)? This note reviews the main drivers of inequality in the EU and reflects on what can be done about it at EU level. It was prepared by I. Maquet, in collaboration with E. Meyermans and M. Duiella from DG EMPL with the reviewing support of R. Maly and R. Strauss. Any views...»

«1    A SHORT METHOD OF PRAYER By J. M. B. DE LA MOT GUYON. Translated from the Paris Edition of 1790 By A. W. MARSTON. LONDON: SAMPSON LOW, MARSTON, LOW, & SEARLE, CROWN BUILDINGS, 188 FLEET STREET. 1875. PRINTED BY BALLANTYNE AND COMPANY EDINBURGH AND LONDON 2    PREFACE TO THE ENGLISH PROTESTANT EDITION. Some apology is perhaps needed when a Protestant thus brings before Protestant readers the works of a consistent Roman Catholic author. The plea must be, that the doctrine and experience...»

«PREGUNTAS FRECUENTES SOBRE LA LIBERTAD RELIGIOSA Hoja de datos de USCCB 2015 ¿Qué es la libertad religiosa? En la doctrina católica, el Concilio Vaticano II “declaró que la persona humana tiene derecho a la libertad religiosa. Esta libertad consiste en que todos los hombres han de estar inmunes de coacción, tanto por parte de individuos como de grupos sociales y de cualquier potestad humana, y esto de tal manera que, en materia religiosa, ni se obligue a nadie a obrar contra su...»

«The Master’s Seminary Journal 12/2 (Fall 2001) 149-166. Copyright © 2001 by Masters Theological Seminary. Cited with permission. THE OPENNESS OF GOD: DOES PRAYER CHANGE GOD? William D. Barrick Professor of Old Testament A proper understanding of two OT prayers, one by Hezekiah and one by Moses, helps in determining whether prayer is the means by which God gets His will done on earth or the means by which the believer's will is accomplished in heaven. A chronological arrangement of the three...»

«The Project Gutenberg EBook of The Cid, by Pierre Corneille This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at www.gutenberg.net Title: The Cid Author: Pierre Corneille Release Date: February 7, 2005 [EBook #14954] Language: English Character set encoding: ISO-8859-1 *** START OF THIS PROJECT GUTENBERG EBOOK THE CID...»

<<  HOME   |    CONTACTS
2017 www.thesis.dislib.info - Online materials, documents

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.