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

<< HOME
CONTACTS

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

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

–  –  –

Pages:     | 1 | 2 || 4 | 5 |

Similar works:

«samudra Women in Fisheries Series No. 3 DOSSIER Women for Sustainable Fisheries Report of the First Phase of the Women in Fisheries Programme of ICSF International Collective in Support of Fishworkers 27 College Road, Chennai 600 006, India Contents Acknowledgements Introduction............................................ 3 Programme Objectives.................................. 4 Plan of Action...............»

«Norwegian University of Life Sciences Faculty of Environmental Science and Technology Department of Environmental Sciences Master Thesis 2015 60 credits Efficiency of Chitosan and Alginate compared with a Chemical precipitating Agent in treating drilling Fluids produced from Road Construction – A laboratory Experiment. Tone-Lise Rustøen Preface This master thesis is written as a part of the Nordic Road Water (NORWAT) research and development program directed by the Norwegian Public Roads...»

«TURBULENCE AND SYSTEMIC RISK IN THE EUROPEAN UNION FINANCIAL SYSTEM Sorin DUMITRESCU, PhD∗ Abstract The purpose of this paper is to analyze the performance of the Absorption Ratio (AR), defined as the fraction of the total variance of a set of asset returns explained or “absorbed” by a fixed number of eigenvectors, as a leading indicator of turbulence in the European Union financial markets over the period January 2000 – July 2015. Using an event study methodology centered around...»

«Article On Their Own: Contemporay Legends of Women Alone in the Urban Landscape Diane Tye Ethnologies, vol. 27, n° 2, 2005, p. 219-236.Pour citer cet article, utiliser l'information suivante : URI: http://id.erudit.org/iderudit/014047ar DOI: 10.7202/014047ar Note : les règles d'écriture des références bibliographiques peuvent varier selon les différents domaines du savoir. Ce document est protégé par la loi sur le droit d'auteur. L'utilisation des services d'Érudit (y compris la...»

«Gyroglider Unregistered (not required) AAIB Bulletin No: 1/98 Ref: EW/C97/5/5Category: 2.3 Gyroglider Unregistered (not required) Aircraft Type and Registration: None No & Type of Engines: 1995 approx Year of Manufacture: 17 May 1997 at 0930 hrs Date & Time (UTC): Kemble Airfield Location: Private Type of Flight: Crew 1 Passengers 1 Persons on Board: Crew Fatal Passengers Fatal Injuries: Aircraft destroyed Nature of Damage: PPL(G) Commander's Licence: 60 years Commander's Age: Believed to be...»

«Philosophy and Phenomenological Research Vol. LXXVI No. 3, May 2008 Ó 2008 International Phenomenological Society ´ Precis of Action In Perception: Philosophy and Phenomenological Research ¨ alva noe University of California Berkeley We perceive as much as we do because, in a way, we perceive so little. Traditional approaches to perception have found it difﬁcult to accommodate the distinctive amodality of perceptual consciousness. Take vision, for example. If we think of what is visible in...»

«Frequent Flier Credit Cards Generate More Than \$4 Billion for Major U.S. Airlines A Report from IdeaWorks Card issuers, such as American Express, Bank of America, Chase, Citi, and US Bank, are attracted by annual charge volumes estimated to be in excess of \$337 billion. Frequent flier programs were launched more than 25 years ago as a tool to identify the highest revenue-producing travelers, establish regular customer communication, and enhance brand loyalty. In today’s revenue hungry...»

«Bored piles with expansive concrete by Harydharaan Gopalan (CHR) Fourth-year undergraduate project in Group D, 2012/13 I hereby declare that, except where specifically indicated, the work submitted herein is my own original work. Bored piles with expansive concrete. Harydharaan Gopalan (CHR) Technical Abstract Piled foundations are an increasingly common method of conveying loads from a structure built on soft ground to a strong bearing stratum. Bored piles, especially friction piles, rely on...»

«Sample In-Pew Commitment Weekend Pulpit Presentation This instruction is most successful when delivered by the Pastor either before Mass or after the Homily. It is time for us to enthusiastically welcome the 2016 Annual Pastoral Appeal Open the Door to Mercy. This is our parish appeal that invites every parishioner to participate in our financial responsibility to our diocesan ministries, programs and services that serve us and the many in need outside of our parish boundaries. As your Pastor,...»

«The Neurobiology of Giftedness John G. Geake Westminster Institute of Education Oxford Brookes University United Kingdom ABSTRACT Gifted children learn more rapidly and efficiently than others, presumably due to neurophysiological differences that affect neuronal efficiency. Data from many neuroimaging studies support this conjecture. Gifted subjects have greater interconnectivity between different areas of their brains, the coordination and integration of which is supported by precociously...»

«Ephesians 2:1-10 JD “God’s Riches Turn Filth Into Masterpieces” Constable notes that this passage concludes Paul’s revelation of the Christian’s individual calling in Christ. Chapter two begins by showing how separated the audience had been from God. Wuest points out that this death or separation was due to our trespasses and sins, in that it was moral and ethical, not physical. Verses two and three are somewhat parenthetical. Hoehner calls this a delineation and Wuest an...»

«JANUARY/FEBRUARY 2016 THE BUZZ ISSUE 39 CONTENTS Dear Buzz Readers, 3. Date for your Diary.4. International Dance/ Table Top. Happy New Year to everyone.5. Facebook!.Carol Singing.6. Sheila’s Mentions. 2016 will be a special year for 7. Coffee Club/ our ‘Open Gardens’ committee Neighbourhood Watch Notes. celebrating ten years of 8/9. Our Nativity. opening gardens in and around 10. Community Champion our village for the benefit of Runner-up. The Devon and Cornwall Air 12. 50 Years...»

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