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

<< HOME
CONTACTS

Pages:     | 1 || 3 | 4 |   ...   | 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 2 ] --

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:

Pages:     | 1 || 3 | 4 |   ...   | 5 |

Similar works:

«                                        Free Download from the book Mipeninei Noam Elimelech  translated and compiled by Tal Moshe Zwecker  by permission from Targum Press, Inc.    NOT FOR RETAIL SALE    All rights reserved © 2008    To buy the book click here  Or visit  http://www.targum.com              THE PRAYER BEFORE PRAYING The Sabba Kaddisha of Radoshitz, in his sefer, Niﬂaos (vol. 1, pp. 21– 22), recorded an...»

«Helpsheet 295 Tax year 6 April 2013 to 5 April 2014 Relief for gifts and similar transactions A Contacts This helpsheet explains how gifts are dealt with for Capital Gains Tax purposes, and is mainly concerned with hold-over relief, which in effect Please phone: • the number printed allows liability to be deferred and passed to the person to whom the gift is on page TR 1 of made. It also covers gifts to charities, but it is only an introduction. If you your tax return are in any doubt about...»

«Excerpts from Penetrating Wisdom: The Aspiration of Samantabhadra released by Snow Lion Publications Five Wisdoms The next section of the Prayer talks about the self-appearing spontaneous wisdom within which, in the case of Samantabhadra, full awakening is manifested. The absolute reality of rigpa, which is the true essence of wisdom, the true fundamental nature of phenomena, arises from this one nature. The spontaneous wisdom of kadak manifests within this one absolute reality. The unceasing...»

«Revised 10/03/2016 THE CITADEL SCHOOL OF ENGINEERING CURRICULUM VITAE Name: Charles Olan Skipper, PhD, PE, PMP; Colonel, US Marine Corps (Ret) Citizenship: USA Office Address: Grimsley Hall, Room 335, 171 Moultrie Street, Charleston, SC 29425 Phone: 843-953-9811 Education (Beginning with Baccalaureate Degree): Institution/Location Years Degree/Date (Mo/Yr) Field of Study Citadel/South Carolina 1967-1971 BS 5/1971 Civil Engineering USC/South Carolina 1971-1972 Masters 8/1972 Engineering...»

«PHILANTHROPY MIAMI 2016 Philanthropy Reinvented Innovative Ways to Frame and Fund your Mission THURSDAY, MARCH 3, 2016 | JUNGLE ISLAND PHILANTHROPY MIAMI 2016 Philanthropy Reinvented Innovative Ways to Frame and Fund Your Mission Jungle Island | 1111 Parrot Jungle Trail | 8:30 a.m. 5:00 p.m. 8:30 a.m. Welcome Henry “Hank” Raattama, Shareholder, Akerman LLP; Co-Chair, LEAVE A LEGACY Teresa V-F Weintraub, Managing Director, The Weintraub-Alessi Group, Merrill Lynch; Co-Chair, LEAVE A LEGACY...»

«CONVENTION ON THE RIGHTS OF PERSONS WITH DISABILITIES Preamble The States Parties to the present Convention, (a) Recalling the principles proclaimed in the Charter of the United Nations which recognize the inherent dignity and worth and the equal and inalienable rights of all members of the human family as the foundation of freedom, justice and peace in the world, (b) Recognizing that the United Nations, in the Universal Declaration of Human Rights and in the International Covenants on Human...»

«Denotational and Operational Preciseness of Subtyping: A Roadmap Dedicated to Frank de Boer on the Occasion of His 60th Birthday Mariangiola Dezani-Ciancaglini1, Silvia Ghilezan2, Svetlana Jakˇi´ 2 sc, Jovanka Pantovi´ 2, and Nobuko Yoshida3† c 1 Universit` di Torino, Italy a 2 Univerzitet u Novom Sadu, Serbia 3 Imperial College London, England Abstract. The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as...»

«Credit Opinion: Alfa-Bank Global Credit Research 14 Mar 2016 Moscow, Russia Ratings Category Moody's Rating Rating(s) Under Outlook Review Bank Deposits *Ba2/NP Baseline Credit Assessment **ba3 Adjusted Baseline Credit **ba3 Assessment Counterparty Risk Assessment *Ba1(cr)/NP(cr) Senior Unsecured **Ba2 Subordinate *B2 * Rating(s) within this class was/were placed on review on March 9, 2016 ** Placed under review for possible downgrade on March 9, 2016 Contacts Analyst Phone Irakli Pipia/London...»

«English Teaching: Practice and Critique September, 2013, Volume 12, Number 2 http://education.waikato.ac.nz/research/files/etpc/files/2013v12n2art7.pdf pp. 121-139 Athenian and Shakespearean tragedies in Oceania: Teaching dramatic literatures in Fiji NICOLE ANAE School of Education, University of South Australia, Australia ABSTRACT: This paper presents a theorised classroom-based narrative discussing the author’s interdisciplinary approach to the teaching of English dramatic literatures –...»

«Why God Became a Man A Conversation with Anselm’s Cur Deus Homo By Tami Jelinek Part One Is Anselm faithful to Paul’s argument in Romans 3? In Romans 3, Paul precedes his argument for Christ’s sacrifice as sufficient for, and accomplishing “satisfaction” (Gr: Hilasterion; translated “sacrifice of atonement,” or “propitiation,” vs. 25) by affirming first that even though our unrighteousness demonstrates the righteousness of God, and that the truthfulness of God is increasingly...»

«MID-SESSION REVIEW GOVERNMENT BUDGET OF THE U.S. FISCAL YEAR 2017 OFFICE OF MANAGEMENT AND BUDGET MID-SESSION REVIEW GOVERNMENT BUDGET OF THE U.S. FISCAL YEAR 2017 OFFICE OF MANAGEMENT AND BUDGET Scan here to go to our website. TABLE OF CONTENTS Page List of Tables...»

<<  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.