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  
  • Constructive characterizations of bar subsets.Silvio Valentini - 2007 - Annals of Pure and Applied Logic 145 (3):368-378.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
    We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  • Regular universes and formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):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   4 citations  
  • 1996 European Summer Meeting of the Association for Symbolic Logic.G. Mints, M. Otero, S. Ronchi Della Rocca & K. Segerberg - 1997 - Bulletin of Symbolic Logic 3 (2):242-277.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • 1996 European Summer Meeting of the Association for Symbolic Logic.Daniel Lascar - 1997 - Bulletin of Symbolic Logic 3 (2):242-277.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Induction–recursion and initial algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.
    Induction–recursion is a powerful definition method in intuitionistic type theory. It extends inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive–recursive definitions by modeling them as initial algebras in slice categories. (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Predicative functionals and an interpretation of ⌢ID.Jeremy Avigad - 1998 - Annals of Pure and Applied Logic 92 (1):1-34.
    In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
    A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
    Direct download (13 more)  
     
    Export citation  
     
    Bookmark   20 citations