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  
  • What is a Higher Level Set?Dimitris Tsementzis - 2016 - Philosophia Mathematica:nkw032.
    Structuralist foundations of mathematics aim for an ‘invariant’ conception of mathematics. But what should be their basic objects? Two leading answers emerge: higher groupoids or higher categories. I argue in favor of the former over the latter. First, I explain why to choose between them we need to ask the question of what is the correct ‘categorified’ version of a set. Second, I argue in favor of groupoids over categories as ‘categorified’ sets by introducing a pre-formal understanding of groupoids as (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Univalent foundations as structuralist foundations.Dimitris Tsementzis - 2017 - Synthese 194 (9):3583-3617.
    The Univalent Foundations of Mathematics provide not only an entirely non-Cantorian conception of the basic objects of mathematics but also a novel account of how foundations ought to relate to mathematical practice. In this paper, I intend to answer the question: In what way is UF a new foundation of mathematics? I will begin by connecting UF to a pragmatist reading of the structuralist thesis in the philosophy of mathematics, which I will use to define a criterion that a formal (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Comparing material and structural set theories.Michael Shulman - 2019 - Annals of Pure and Applied Logic 170 (4):465-504.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Categories with families and first-order logic with dependent sorts.Erik Palmgren - 2019 - Annals of Pure and Applied Logic 170 (12):102715.
    First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics.Martín H. Escardó - 2013 - Journal of Symbolic Logic 78 (3):764-784.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 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  
    		•