David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Philosophical Logic 18 (4):399 - 422 (1989)
Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all well-founded sets). The occurrence of the contradiction is explained in set theoretical terms. Crucial here is the way a proof-object of an existential proposition is understood. It is shown that also Russell's paradox can be translated into type theory. The type theory extended with the axiom mentioned above contains constructive higher order logic, but even if one only adds constructive second order logic to type theory the contradictions arise.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Giuseppe Primiero (2009). Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information. History and Philosophy of Logic 30 (3):257-282.
Maria Emilia Maietti & Silvio Valentini (1999). Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory? Mathematical Logic Quarterly 45 (4):521-532.
Similar books and articles
Paul C. Gilmore (2001). An Intensional Type Theory: Motivation and Cut-Elimination. Journal of Symbolic Logic 66 (1):383-400.
John Bell (2008). The Axiom of Choice and the Law of Excluded Middle in Weak Set Theories. Mathematical Logic Quarterly 54 (2):194-201.
Ingrid Lindström (1989). A Construction of Non-Well-Founded Sets Within Martin-Löf's Type Theory. Journal of Symbolic Logic 54 (1):57-64.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. Journal of Symbolic Logic 49 (3):730-753.
Adam Obtułowicz (1989). Categorical and Algebraic Aspects of Martin-Löf Type Theory. Studia Logica 48 (3):299 - 317.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Added to index2009-01-28
Total downloads18 ( #153,723 of 1,726,249 )
Recent downloads (6 months)4 ( #183,615 of 1,726,249 )
How can I increase my downloads?