FREE ELECTRONIC LIBRARY - Online materials, documents

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

Derived rules for predicative set theory:

an application of sheaves

Benno van den Berg & Ieke Moerdijk

November 16, 2011


We show how one may establish proof-theoretic results for constructive

Zermelo-Fraenkel set theory, such as the compactness rule for Cantor

space and the Bar Induction rule for Baire space, by constructing sheaf

models and using their preservation properties.

1 Introduction

This paper is concerned with Aczel’s predicative constructive set theory CZF and with related systems for predicative algebraic set theory; it also studies extensions of CZF, for example by the axiom of countable choice.

We are particularly interested in certain statements about Cantor space 2N, Baire space NN and the unit interval [0, 1] of Dedekind real numbers in such theories, namely the compactness of 2N and of [0, 1], and the related “Bar Induction” property for Baire space. The latter property states that if S is a set of finite sequences of natural numbers for which

- for each α there is an n such that α(0), α(1),...., α(n) belongs to S (“S is a bar”),

- if u belongs to S then so does every extension of u (“S is monotone”),

- if u is a finite sequence for which the concatenation u ∗ n belongs to S for all n, then u belongs to S (“S is inductive”), then the empty sequence belongs to S. It is well-known that these statements, compactness of 2N and of [0, 1] and Bar Induction for NN, cannot be derived in intuitionistic set or type theories. In fact, they fail in sheaf models over locales, as explained in [17]. Sheaf models can also be used to show that all implications in the chain (BI) =⇒ (F T ) =⇒ (HB) are strict (where BI stands for Bar Induction for NN, while FT stands for the Fan Theorem (compactness of 2N ) and HB stands for the Heine-Borel Theorem (compactness of the unit interval), see [27]).

On the other hand, one may also define Cantor space C, Baire space B, and the unit interval I as locales or formal spaces. Compactness is provable for formal Cantor space, as is Bar Induction for formal Baire space. Although Bar Induction may seem to be a statement of a slightly different nature, it is completely analogous to compactness, as explained in [17] as well. Indeed, the locales C and I have enough points (i.e., are true topological spaces) iff the spaces 2N and [0, 1] are compact, while the locale B has enough points iff Bar Induction holds for the space NN. The goal of this paper is to prove that the compactness properties of these (topological) spaces do hold for CZF (with countable choice), however, when they are reformulated as derived rules. Thus, for example, Cantor space is compact in the sense that if S is a property of finite sequencesof 0’s and 1’s which is definable in the language of set theory and for which CZF proves for all α in 2N there is an n such that α(0), α(1),...., α(n) belongs to S (“S is a cover”), then there are such finite sequences u1,..., uk for which CZF proves that each ui belongs to S as well as that for each α as above there are an n and an i such that α(0), α(1),...., α(n) = ui. We will also show that compactness of the unit interval and Bar Induction hold when formulated as derived rules for CZF and suitable extensions of CZF, respectively.

This is a proof-theoretic result, which we will derive by purely model-theoretic means, using sheaf models for CZF and a doubling construction for locales originating with Joyal. Although our results for the particular theory CZF seem to be new, similar results occur in the literature for other constructive systems, and are proved by various methods, such as purely proof-theoretic methods, realizability methods or our sheaf-theoretic methods.1 In this context it is important to observe that derived rules of the kind “if T proves ϕ, then T proves ψ” are different results for different T, and can be related only in the presence of conservativity results. For example, a result for CZF like the ones above does not imply a similar result for the extension of CZF with countable choice, or vice versa.

Our motivation to give detailed proofs of several derived rules comes from various sources. First of all, the related results just mentioned predate the theFor example, Beeson in [6] used a mixture of forcing and realizability for Feferman-style systems for explicit mathematics. Hayashi used proof-theoretic methods for HAH, the system for higher-order Heyting arithmetic corresponding to the theory of elementary toposes in [23], and sheaf-theoretic methods in [24] for the impredicative set theory IZF, an intuitionistic version of Zermelo-Fraenkel set theory. Grayson [22] gives a sheaf-theoretic proof of a local continuity rule for the system HAH, and mentions in [21] that the method should also apply to systems without powerset.

ory CZF, which is now considered as one of the most robust axiomatisations of predicative constructive set theory and is closely related to Martin-L¨f type o theory [1, 2, 3]. Secondly, the theory of sheaf models for CZF has only recently been firmly established (see [19, 20, 12]), partly in order to make applications to proof theory such as the ones exposed in this paper possible. Thirdly, the particular sheaf models over locales necessary for our application hinge on some subtle properties and constructions of locales (or formal spaces) in the predicative context, such as the inductive definition of covers in formal Baire space in the absence of power sets. These aspects of predicative locale theory have only recently emerged in the literature [14, 4]. In these references, the regular extension axiom REA plays an important role. In fact, one needs an extension of CZF, which on the one hand is sufficiently strong to handle suitable inductive definitions, while on the other hand it is stable under sheaf extensions. One possible choice is the extension of CZF by the smallness axiom for W-types and the axiom of multiple choice AMC (see [13]).

The results of this paper were presented by the authors on various occasions:

by the second author in July 2009 at the TACL’2009 conference in Amsterdam and in March 2010 in the logic seminar in Manchester and by the first author in May 2010 at the meeting “Set theory: classical and constructive”, again in Amsterdam. We would like to thank the organizers of all these events for giving us these opportunities. We are also grateful to the referee for a very careful reading of the original manuscript and to the editors for their patience.

2 Constructive set theory Throughout the paper we work in Aczel’s constructive set theory CZF, or extensions thereof. (An excellent reference for CZF is [5].)

–  –  –

CZF is a set theory whose underlying logic is intuitionistic and whose axioms


Extensionality: ∀x ( x ∈ a ↔ x ∈ b ) → a = b.

Empty set: ∃x ∀y ¬y ∈ x.

Pairing: ∃x ∀y ( y ∈ x ↔ y = a ∨ y = b ).

Union: ∃x ∀y ( y ∈ x ↔ ∃z ∈ a y ∈ z ).

Set induction: ∀x ∀y ∈ x ϕ(y) → ϕ(x) → ∀x ϕ(x).

Infinity: ∃a ( ∃x x ∈ a ) ∧ ( ∀x ∈ a ∃y ∈ a x ∈ y ).

Bounded separation: ∃x ∀y y ∈ x ↔ y ∈ a∧ϕ(y), for any bounded formula ϕ in which a does not occur.

Strong collection: ∀x ∈ a ∃y ϕ(x, y) → ∃b B(x ∈ a, y ∈ b) ϕ.

Subset collection: ∃c ∀z ∀x ∈ a ∃y ∈ b ϕ(x, y, z) → ∃d ∈ c B(x ∈ a, y ∈

d) ϕ(x, y, z).

In the last two axioms, the expression

–  –  –

has been used as an abbreviation for ∀x ∈ a ∃y ∈ b ϕ ∧ ∀y ∈ b ∃x ∈ a ϕ.

Throughout this paper, we will use denumerable to mean “in bijective correspondence with the set of natural numbers” and finite to mean “in bijective correspondence with an initial segment of natural numbers”. A set which is either finite or denumerable, will be called countable. In addition, we will call a set K-finite, if it is the surjective image of an initial segment of the natural numbers. Observe that if a set has decidable equality, then it is finite if and only if it is K-finite.

In this paper we will also consider the following choice principles (countable

choice and dependent choice):

–  –  –

It is well-known that DC implies ACω, but not conversely (not even in ZF).

Any use of these additional axioms will be indicated explicitly.

2.2 Inductive definitions in CZF Definition 2.1 Let S be a class. We will write Pow(S) for the class of subsets of S. An inductive definition is a subclass Φ of Pow(S) × S. One should think of the pairs (X, a) ∈ Φ as rules of the kind: if all elements in X have a certain property, then so does a. Accordingly, a subclass A of S will be called Φ-closed, if X⊆A⇒a∈A whenever (X, a) is in Φ.

In CZF one can prove that for any inductive definition Φ on a class S and for any subclass U of S there is a least Φ-closed subclass of S containing U (see [5]). We will denote this class by I(Φ, U ). However, for the purposes of

predicative locale theory one would like to have more:

Theorem 2.2 (Set Compactness) If S and Φ are sets, then there is a subset B of Pow(S) such that for each set U ⊆ S and each a ∈ I(Φ, U ) there is a set V ∈ B such that V ⊆ U and a ∈ I(Φ, V ).

This result cannot be proved in CZF proper, but it can be proved in extensions of CZF. For example, this result becomes provable in CZF extended with Aczel’s regular extension axiom REA [5] or in CZF extended with the axioms WS and AMC [13]. The latter extension is known to be stable under sheaves [29, 13], while the former presumably is as well. Below, we will denote by CZF+ any extension of CZF which allows one to prove set compactness and which is stable under sheaves.

3 Predicative locale theory In this section we have collected the definitions and results from predicative locale theory that we need in order to establish derived rules for CZF. We have tried to keep our presentation self-contained, so that this section can actually be considered as a crash course on predicative locale theory or “formal topology”.

(In a predicative context, locales are usually called “formal spaces”, hence the name. Some important references for formal topology are [16, 14, 32, 4] and, unless we indicate explicitly otherwise, the reader may find the results explained in this section in these sources.)

3.1 Formal spaces

Definition 3.1 A formal space is a small site whose underlying category is a preorder. By a preorder, we mean a set P together with a small relation ≤ ⊆ P × P which is both reflexive and transitive. If a is an element of P then we will write ↓ a or Ma for {p ∈ P : p ≤ a}, and if α is a subset of P then we will write ↓ α = {p ∈ P : (∃a ∈ α) p ≤ a}. For the benefit of the reader, we repeat the axioms for a site from [12] for the special case of preorders.

Fix an element a ∈ P. By a sieve on a we will mean a downwards closed subset of ↓ a. The set Ma = ↓ a will be called the maximal sieve on a. In a predicative setting, the sieves on a form in general only a class.

If S is a sieve on a and b ≤ a, then we write b∗ S for the sieve b∗ S = S ∩ ↓ b on b. We will call this sieve the restriction of S to b.

A (Grothendieck) topology Cov on P is given by assigning to every object

a ∈ P a collection of sieves Cov(a) such that the following axioms are satisfied:

(Maximality) The maximal sieve Ma belongs to Cov(a).

(Stability) If S belongs to Cov(a) and b ≤ a, then b∗ S belongs to Cov(b).

(Local character) Suppose S is a sieve on a. If R ∈ Cov(a) and all restrictions b∗ S to elements b ∈ R belong to Cov(b), then S ∈ Cov(a).

A pair (P, Cov) consisting of a preorder P and a Grothendieck topology Cov on it is called a formal topology or a formal space. If a formal topology (P, Cov) has been fixed, the elements of P will be referred to as basic opens or basis elements and the sieves belonging to some Cov(a) will be referred to as the covering sieves. If S belongs to Cov(a) one says that S is a sieve covering a, or that a is covered by S.

To develop a predicative theory of locales one needs to assume that the formal spaces one works with have a presentation, in the following sense. (Note that it was a standing assumption in [12] that sites had a presentation.) Definition 3.2 A presentation for a formal topology (P, Cov) is a function BCov assigning to every a ∈ P a small collection of basic covering sieves

BCov(a) such that:

–  –  –

A formal topology which has a basis will be called presentable.

One of the ways in which presentable formal spaces behave better than general ones, is that, in CZF, only presentable formal spaces give rise to categories of sheaves again modelling CZF (see Theorem 4.3 and Remark 4.4 below). For this reason, it will be an important theme in this section to sort out whether the concrete formal spaces we work with can be proved to be presentable in CZF or in extensions thereof.

Remark 3.3 Another property of presentable formal spaces, which is sometimes useful, is that for a given sieve S the collection of a ∈ P which are covered by S form a set, as it can be written as

–  –  –

This property is often included in the definition of a formal space, but for our purposes this was not necessary. (We thank Giovanni Curi for bringing this issue to our attention; see also [15].)

3.2 Inductively generated formal topologies Definition 3.4 If P is a preorder, then a covering system is a map C assigning to every a ∈ P a small collection C(a) of subsets of ↓ a such that the following

covering axiom holds:

–  –  –

Both statements are now proved by an induction argument, using the covering axiom.

Theorem 3.6 Every covering system generates a formal topology.

More precisely, for every covering system C there is a smallest Grothendieck topology Cov such that α ∈ C(a) =⇒↓ α ∈ Cov(a).

In CZF+ one can show that this formal topology has a presentation.

–  –  –

Pages:   || 2 | 3 | 4 | 5 |

Similar works:

«QUESTIONS ON FAQ: 1. What is considered harassment on Twitter?2. What is not considered harassment on Twitter?3. What should I do if I am harassed on Twitter?4. How long should I wait before I report abuse on Twitter?5. How do I know if I have blocked a Twitter account?6. How do I unblock a Twitter account?7. How do I know if I have muted a Twitter account? 8. How do I unmute a Twitter account? 9. How do I share block lists on Twitter? 10. How can I report harassment on Twitter? 11. What are...»

«VELOUR Plant Growth Regulator N FOR USE ON COTTON AND TOBACCO NOT FOR USE IN RESIDENTIAL AREAS E ACTIVE INGREDIENT: Ethephon: (2-Chloroethyl) phosphonic acid* OTHER INGREDIENTS: IM TOTAL: * 1 gallon contains 6 lbs. ethephon. C KEEP OUT OF REACH OF CHILDREN DANGER / PELIGRO E P Si usted no entiende la etiqueta, busque a alguien para que se la explique a usted en detalle. (If you do not understand the label, find someone to explain it to you in detail.) S See inside booklet for FIRST AID and...»

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

«Toxins 2015, 7, 2159-2187; doi:10.3390/toxins7062159 OPEN ACCESS toxins ISSN 2072-6651 www.mdpi.com/journal/toxins Review Bioinformatics-Aided Venomics Quentin Kaas * and David J. Craik Institute for Molecular Bioscience, the University of Queensland, Brisbane, QLD 4072, Australia; E-Mail: d.craik@imb.uq.edu.au * Author to whom correspondence should be addressed; E-Mail: q.kaas@imb.uq.edu.au; Tel.: +61-7-3346-2021; Fax: +61-7-3346-2101. Academic Editor: Bryan Grieg Fry Received: 1 May 2015 /...»

«Model: AHP300 Electrically Controlled Ventilator 1720 Sublette Ave St. Louis, MO 63110 Phone 314-771-2400 S168-AHP300-001 Rev. D Patent Pending Table of Contents 1. Intended Use: 2. Product Description: 3. Explanation of Warnings: 4. Explanation of Abbreviations: 5. Symbols: 6. Controls and Connections: 7. Operating the AHP300 Ventilator : 8. Ventilation Modes: 9. Breath Types: 10. Programmable Presets: Quick Start Modes: Custom Modes: 11. O2 Conserve Mode: 12. Manual Breaths: 13. Measured...»


«Religion, State & Society, Vo!. 23, No. 3, 1995 Impressions of the Contemporary Russian Orthodox Church: Its Problems and Its Theological Education DIMITRY POSPIELOVSKY The Russian Orthodox Church has failed to find in itself the living force to lead Russian society morally or spiritually, as was hoped by both believers and nonbelievers when the collapse of the Soviet state had become obvious. The 1988 Millennial Council (Sobor) of the Church adopted a statute which is close in essence and...»

«Explorations of Gender Identity A Study of Masculinity and Gender Predicaments in Cormac McCarthy’s Suttree By Erik Myren Vågnes Masters Thesis University of Bergen Department of Foreign Languages May 2012 Table of Contents Page Acknowledgements Introduction 3 Chapter 1: The Predicaments of Masculinity 9 Chapter 2: Fathers— and the Flight from Hegemonic Masculinity Chapter 3: Negotiations of Identity Chapter 4: The Mother—and the Fear of Gender Transgression Conclusion Works Cited...»

«Lectures on Interpreted Languages and Compositionality Marcus Kracht Department of Linguistics, UCLA 3125 Campbell Hall PO Box 951543 Los Angeles, CA 90095-1543 kracht@humnet.ucla.edu August 21, 2008 FAQ Question: Why did you write this book? Answer: It seems to me that the purely syntactic approach to language structure has been exhausted. More and more people are becoming convinced that what was previously diagnosed as a syntactic phenomenon really has to do with semantics. However, this...»

«GUIDANCE SOFTWARE | Tableau TD2 User’s Guide Tableau TD2 Version 4.01 User’s Guide Copyright © 2009‐2012 Guidance Software, Inc. All rights reserved.  EnCase®, EnScript®, FastBloc®, Guidance Software® and EnCE® are registered trademarks or trademarks owned by Guidance Software  in the United States and other jurisdictions and may not be used without prior written permission. All other marks and brands may be ...»

«MTS Discussion Paper 3.08 God’s Prayer Book By Tony Payne © Matthias Media (The Briefing #174; www.matthiasmedia.com.au/briefing). Used with permission. That ancient treasury of prayers, the Psalms, has much to teach us about talking to God. In this final article in our series on prayer, we explore the rich and varied nature of God’s own prayer book, and find out how we can make best use of it in our own prayers. The always quotable Martin Luther described the Psalms as “a little Bible....»

«Bruce Fithian, Music Director Com6atancrcaroCs Friday, May 29, 2015, 7:30.PM · Cathedral Church,of Saint Luke 143' State Street, Portland, Maine ' Sunday, May 31,2015, 4:00 PM Episcopal Church of Saint Mary 43 Foreside Road, Falmouth Foreside, Maine With special reception to follow performance Tuesday, June 2, 2015, 7:30 PM First Parish Church 9 Cleaveland Street, Brunswick, Maine ~-~~~. Cotnbat and Carols I Songs of Love and War Claudio Monteverdi (1567.1643) Come dolce hoggi l'auretta...»

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