5 found
  1.  80
    On an interpretation of second order quantification in first order intuitionistic propositional logic.Andrew M. Pitts - 1992 - 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 (8 more)  
    Export citation  
    Bookmark   46 citations  
  2.  14
    Conceptual completeness for first-order Intuitionistic logic: an application of categorical logic.Andrew M. Pitts - 1989 - Annals of Pure and Applied Logic 41 (1):33-81.
  3.  52
    A note on Russell's paradox in locally cartesian closed categories.Andrew M. Pitts & Paul Taylor - 1989 - 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 (4 more)  
    Export citation  
    Bookmark   2 citations  
  4.  26
    Saunders Mac Lane and Ieke Moerdijk. Sheaves in geometry and logic. A first introduction to topos theory. Universitext. Springer-Verlag, New York, Berlin, etc., 1992, xii – 627 pp. [REVIEW]Andrew M. Pitts - 1995 - Journal of Symbolic Logic 60 (1):340-342.
  5.  20
    Review: Saunders Mac Lane, Ieke Moerdjik, Sheaves in Geometry and Logic. A First Introduction to Topos Theory. [REVIEW]Andrew M. Pitts - 1995 - Journal of Symbolic Logic 60 (1):340-342.