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.
  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 (2 more)  
     
    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