Switch to: References

Add citations

You must login to add citations.
  1. Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf.Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm (eds.) - 2012 - Dordrecht, Netherland: Springer.
    This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • The axiom of multiple choice and models for constructive set theory.Benno van den Berg & Ieke Moerdijk - 2014 - Journal of Mathematical Logic 14 (1):1450005.
    We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it is interpretable in Martin-Löf's type theory. In addition, it is strong enough to prove the Set Compactness theorem and the results in formal topology which make use of this theorem. Moreover, it is stable under the standard constructions from algebraic set theory, namely exact completion, realizability models, forcing as well as (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • 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.
  • Aspects of predicative algebraic set theory I: Exact Completion.Benno van den Berg & Ieke Moerdijk - 2008 - Annals of Pure and Applied Logic 156 (1):123-159.
    This is the first in a series of papers on Predicative Algebraic Set Theory, where we lay the necessary groundwork for the subsequent parts, one on realizability [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory II: Realizability, Theoret. Comput. Sci. . Available from: arXiv:0801.2305, 2008], and the other on sheaves [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory III: Sheaf models, 2008 ]. We introduce the notion of a predicative category with small (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  • Constructive toposes with countable sums as models of constructive set theory.Alex Simpson & Thomas Streicher - 2012 - Annals of Pure and Applied Logic 163 (10):1419-1436.
  • Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets.Erik Palmgren - 2012 - Annals of Pure and Applied Logic 163 (10):1384-1399.
  • Models of intuitionistic set theory in subtoposes of nested realizability toposes.Samuele Maschio & Thomas Streicher - 2015 - Annals of Pure and Applied Logic 166 (6):729-739.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Relational dual tableau decision procedures and their applications to modal and intuitionistic logics.Joanna Golińska-Pilarek & Taneli Huuskonen - 2014 - Annals of Pure and Applied Logic 165 (2):428-502.
    This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementary topos, since any such is equivalent to (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Exact completion and constructive theories of sets.Jacopo Emmenegger & Erik Palmgren - 2020 - Journal of Symbolic Logic 85 (2):563-584.
    In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects. Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Lawvere-Tierney Sheaves in Algebraic Set Theory.S. Awodey, N. Gambino & M. A. Warren - 2009 - Journal of Symbolic Logic 74 (3):861 - 890.
    We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Relating first-order set theories, toposes and categories of classes.Steve Awodey, Carsten Butz, Alex Simpson & Thomas Streicher - 2014 - Annals of Pure and Applied Logic 165 (2):428-502.