23 found
Order:
  1.  4
    Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
    Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   25 citations  
  2.  30
    The Modal Logic of Provability. The Sequential Approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
  3.  10
    Topology and Duality in Modal Logic.Giovanni Sambin & Virginia Vaccaro - 1988 - Annals of Pure and Applied Logic 37 (3):249-296.
  4.  15
    An Effective Fixed-Point Theorem in Intuitionistic Diagonalizable Algebras.Giovanni Sambin - 1976 - Studia Logica 35 (4):345 - 361.
    Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following: Let T be any first-order theory with a predicate Pr satisfying the canonical derivability conditions, including Löb's property. Then any formula in T built up from the propositional variables $q,p_{1},...,p_{n}$ , using logical connectives and the predicate Pr, has the same "fixed-points" relative to q (that is, formulas $\psi (p_{1},...,p_{n})$ for which for all $p_{1},...,p_{n}\vdash _{T}\phi (\psi (p_{1},...,p_{n}),p_{1},...,p_{n})\leftrightarrow \psi (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   16 citations  
  5.  49
    Provability: The Emergence of a Mathematical Modality.George Boolos & Giovanni Sambin - 1991 - Studia Logica 50 (1):1 - 23.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  6.  8
    Pretopologies and Completeness Proofs.Giovanni Sambin - 1995 - Journal of Symbolic Logic 60 (3):861-878.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  7.  11
    Formal Topologies on the Set of First-Order Formulae.Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan M. Smith - 2000 - Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  8.  62
    An Incomplete System of Modal Logic.George Boolos & Giovanni Sambin - 1985 - Journal of Philosophical Logic 14 (4):351 - 358.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  9.  8
    Basic Logic: Reflection, Symmetry, Visibility.Giovanni Sambin, Giulia Battilotti & Claudia Faggian - 2000 - Journal of Symbolic Logic 65 (3):979-1013.
    We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  10.  1
    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 (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  11.  8
    Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995.Giovanni Sambin & Jan M. Smith (eds.) - 1998 - Oxford University Press.
    This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  12.  16
    A Simpler Proof of Sahlqvist's Theorem on Completeness of Modal Logics.Giovanni Sambin - 1980 - Bulletin of the Section of Logic 9 (2):50-54.
  13. Twenty-Five Years of Constructive Type Theory.Giovanni Sambin & Jan Smith (eds.) - 1998 - Clarendon Press.
     
    Export citation  
     
    My bibliography   1 citation  
  14.  15
    Topological Characterization of Scott Domains.Giovanni Sambin & Silvio Valentini - forthcoming - Archive for Mathematical Logic.
    Direct download  
     
    Export citation  
     
    My bibliography  
  15.  5
    Preface of Special Issue on Formal Topology.Thierry Coquand & Giovanni Sambin - forthcoming - Annals of Pure and Applied Logic.
  16.  5
    Why Topology in the Minimalist Foundation Must Be Pointfree.Maria Emilia Maietti & Giovanni Sambin - 2013 - Logic and Logical Philosophy 22 (2):167-199.
    We give arguments explaining why, when adopting a minimalist approach to constructive mathematics as that formalized in our two-level minimalist foundation, the choice for a pointfree approach to topology is not just a matter of convenience or mathematical elegance, but becomes compulsory. The main reason is that in our foundation real numbers, either as Dedekind cuts or as Cauchy sequences, do not form a set.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  17.  9
    Fixed Points Through the Finite Model Property.Giovanni Sambin - 1978 - Studia Logica 37 (3):287 - 289.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  18.  2
    Preface.Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster - 2012 - Annals of Pure and Applied Logic 163 (2):85-86.
  19.  3
    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  
     
    My bibliography  
  20.  1
    Preface.Bernhard Banaschewski, Thierry Coquand & Giovanni Sambin - 2006 - Annals of Pure and Applied Logic 137 (1-3):1-2.
  21. Formal Topologies on the Set of First-Order Formulae.Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan Smith - 2000 - Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download  
     
    Export citation  
     
    My bibliography  
  22. Preface.Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin & Peter Schuster - 2016 - Annals of Pure and Applied Logic 167 (9):725.
  23. Basic Logic: Reflection, Symmetry, Visibility.Giovanni Sambin, Giulia Battilotti & Claudia Faggian - 2000 - Journal of Symbolic Logic 65 (3):979-1013.
    We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...)
    Direct download  
     
    Export citation  
     
    My bibliography