PhilPapers is currently in read-only mode while we are performing some maintenance. You can use the site normally except that you cannot sign in. This shouldn't last long.
5 found
Sort by:
  1. Andrew M. Pitts (1995). Mac Lane Saunders and Moerdijk Ieke. Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Universitext. Springer-Verlag, New York, Berlin, Etc., 1992, Xii–627 Pp. [REVIEW] Journal of Symbolic Logic 60 (1):340-342.
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Andrew M. Pitts (1995). Review: Saunders Mac Lane, Ieke Moerdjik, Sheaves in Geometry and Logic. A First Introduction to Topos Theory. [REVIEW] Journal of Symbolic Logic 60 (1):340-342.
    Direct download  
     
    My bibliography  
     
    Export citation  
  3. Andrew M. Pitts (1992). On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. Journal of Symbolic Logic 57 (1):33-52.
    We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. Andrew M. Pitts (1989). Conceptual Completeness for First-Order Intuitionistic Logic: An Application of Categorical Logic. Annals of Pure and Applied Logic 41 (1):33-81.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  5. Andrew M. Pitts & Paul Taylor (1989). A Note on Russell's Paradox in Locally Cartesian Closed Categories. Studia Logica 48 (3):377 - 387.
    Working in the fragment of Martin-Löfs extensional type theory [12] which has products (but not sums) of dependent types, we consider two additional assumptions: firstly, that there are (strong) equality types; and secondly, that there is a type which is universal in the sense that terms of that type name all types, up to isomorphism. For such a type theory, we give a version of Russell's paradox showing that each type possesses a closed term and (hence) that all terms of (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation