Switch to: References

Add citations

You must login to add citations.
  1. Regular Universes and Formal Spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1):299-316.
    We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Generalising the Fan Theorem.Silvio Valentini - 2017 - Mathematical Logic Quarterly 63 (1-2):85-93.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Vagueness, Kant and Topology: A Study of Formal Epistemology.Giovanni Boniolo & Silvio Valentini - 2008 - Journal of Philosophical Logic 37 (2):141-168.
    In this paper we propose an approach to vagueness characterised by two features. The first one is philosophical: we move along a Kantian path emphasizing the knowing subject’s conceptual apparatus. The second one is formal: to face vagueness, and our philosophical view on it, we propose to use topology and formal topology. We show that the Kantian and the topological features joined together allow us an atypical, but promising, way of considering vagueness.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Compactness in Locales and in Formal Topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1):413-438.
    If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • Embedding Locales and Formal Topologies Into Positive Topologies.Francesco Ciraulo & Giovanni Sambin - 2018 - Archive for Mathematical Logic 57 (7-8):755-768.
    A positive topology is a set equipped with two particular relations between elements and subsets of that set: a convergent cover relation and a positivity relation. A set equipped with a convergent cover relation is a predicative counterpart of a locale, where the given set plays the role of a set of generators, typically a base, and the cover encodes the relations between generators. A positivity relation enriches the structure of a locale; among other things, it is a tool to (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Positivity Relations on a Locale.Francesco Ciraulo & Steven Vickers - 2016 - Annals of Pure and Applied Logic 167 (9):806-819.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1):164-188.
    We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory . These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  • Pretopologies and a Uniform Presentation of Sup-Lattices, Quantales and Frames.Giulia Battilotti & Giovanni Sambin - 2006 - Annals of Pure and Applied Logic 137 (1):30-61.
    We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology.Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales.The (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • On the Collection of Points of a Formal Space.Giovanni Curi - 2006 - Annals of Pure and Applied Logic 137 (1):126-146.
    On the collection of points of a formal space.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  • Programming Interfaces and Basic Topology.Peter Hancock & Pierre Hyvernat - 2006 - Annals of Pure and Applied Logic 137 (1--3):189-239.
    A pattern of interaction that arises again and again in programming is a 'handshake', in which two agents exchange data. The exchange is thought of as provision of a service. Each interaction is initiated by a specific agent--the client or Angel--and concluded by the other--the server or Demon. We present a category in which the objects--called interaction structures in the paper--serve as descriptions of services provided across such handshaken interfaces. The morphisms--called (general) simulations--model components that provide one such service, relying (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  • Formal Zariski Topology: Positivity and Points.Peter Schuster - 2006 - Annals of Pure and Applied Logic 137 (1):317-359.
    The topic of this article is the formal topology abstracted from the Zariski spectrum of a commutative ring. After recollecting the fundamental concepts of a basic open and a covering relation, we study some candidates for positivity. In particular, we present a coinductively generated positivity relation. We further show that, constructively, the formal Zariski topology cannot have enough points.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Independence Results in Formal Topology.Silvio Valentini - 2012 - Annals of Pure and Applied Logic 163 (2):151-156.
  • A Coverage Construction of the Reals and the Irrationals.Harold Simmons - 2007 - Annals of Pure and Applied Logic 145 (2):176-203.
    I modify the standard coverage construction of the reals to obtain the irrationals. However, this causes a jump in ordinal complexity from ω+1 to Ω.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  • The Problem of the Formalization of Constructive Topology.Silvio Valentini - 2004 - Archive for Mathematical Logic 44 (1):115-129.
  • Locatedness and Overt Sublocales.Bas Spitters - 2010 - Annals of Pure and Applied Logic 162 (1):36-54.
    Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Exact Approximations to Stone–Čech Compactification.Giovanni Curi - 2007 - Annals of Pure and Applied Logic 146 (2):103-123.
    Given a locale L and any set-indexed family of continuous mappings , fi:L→Li with compact and completely regular co-domain, a compactification η:L→Lγ of L is constructed enjoying the following extension property: for every a unique continuous mapping exists such that . Considered in ordinary set theory, this compactification also enjoys certain convenient weight limitations.Stone–Čech compactification is obtained as a particular case of this construction in those settings in which the class of [0,1]-valued continuous mappings is a set for all L. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Cantor Theorem and Friends, in Logical Form.Silvio Valentini - 2013 - Annals of Pure and Applied Logic 164 (4):502-508.
    We prove a generalization of the hyper-game theorem by using an abstract version of inductively generated formal topology. As applications we show proofs for Cantor theorem, uncountability of the set of functions from N to N and Gödel theorem which use no diagonal argument.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Spatiality and Classical Logic.Milena Stefanova & Silvio Valentini - 2011 - Mathematical Logic Quarterly 57 (4):432-440.
    In this short note we show that any proof of a general spatiality theorem for inductively generated formal topologies requires full classical logic. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Topological Inductive Definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
    In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Constructive Characterizations of Bar Subsets.Silvio Valentini - 2007 - Annals of Pure and Applied Logic 145 (3):368-378.
  • A Constructive Galois Connection Between Closure and Interior.Francesco Ciraulo & Giovanni Sambin - 2012 - Journal of Symbolic Logic 77 (4):1308-1324.
    We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior operators via complement.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Space of Valuations.Thierry Coquand - 2009 - Annals of Pure and Applied Logic 157 (2-3):97-109.
    The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev , Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Every Countably Presented Formal Topology is Spatial, Classically.Silvio Valentini - 2006 - Journal of Symbolic Logic 71 (2):491-500.
    By using some classical reasoning we show that any countably presented formal topology, namely, a formal topology with a countable axiom set, is spatial.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Constructive Version of Boolean Algebra.F. Ciraulo, M. E. Maietti & P. Toto - 2013 - Logic Journal of the IGPL 21 (1):44-62.
  • Cut Elimination for Entailment Relations.Davide Rinaldi & Daniel Wessel - forthcoming - Archive for Mathematical Logic:1-21.
    Entailment relations, introduced by Scott in the early 1970s, provide an abstract generalisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Cosheaves and Connectedness in Formal Topology.Steven Vickers - 2012 - Annals of Pure and Applied Logic 163 (2):157-174.
  • Derived Rules for Predicative Set Theory: An Application of Sheaves.Benno van den Berg & Ieke Moerdijk - 2012 - Annals of Pure and Applied Logic 163 (10):1367-1383.
  • Sublocales in Formal Topology.Steven Vickers - 2007 - Journal of Symbolic Logic 72 (2):463 - 482.
    The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • A Localic Theory of Lower and Upper Integrals.Steven Vickers - 2008 - Mathematical Logic Quarterly 54 (1):109-123.
    An account of lower and upper integration is given. It is constructive in the sense of geometric logic. If the integrand takes its values in the non-negative lower reals, then its lower integral with respect to a valuation is a lower real. If the integrand takes its values in the non-negative upper reals, then its upper integral with respect to a covaluation and with domain of integration bounded by a compact subspace is an upper real. Spaces of valuations and of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • On the Existence of Stone-Čech Compactification.Giovanni Curi - 2010 - Journal of Symbolic Logic 75 (4):1137-1146.
  • The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
    We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • A Constructive Semantics for Non-Deducibility.Francesco Ciraulo - 2008 - Mathematical Logic Quarterly 54 (1):35-48.
    This paper provides a constructive topological semantics for non-deducibility of a first order intuitionistic formula. Formal topology theory, in particular the recently introduced notion of a binary positivity predicate, and co-induction are two needful tools.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • On Some Peculiar Aspects of the Constructive Theory of Point-Free Spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
    This paper presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations