A note on Russell's paradox in locally cartesian closed categories
Studia Logica 48 (3):377 - 387 (1989)
| Abstract | 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 each type are provably equal. We consider the kind of category theoretic structure which corresponds to this kind of type theory and obtain a categorical version of the paradox. A special case of this result is the degeneracy of a locally cartesian closed category with a morphism which is generic in the sense that every other morphism in the category can be obtained from it via pullback. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesAndré Fuhrmann (2002). Russell's Way Out of the Paradox of Propositions. History and Philosophy of Logic 23 (3):197-213.
André Fuhrmann (2002). Russell's Way Out of the Paradox of Propositions. History and Philosophy of Logic 23 (3):197-213.
Fairouz Kamareddine & Ewan Klein (1993). Nominalization, Predication and Type Containment. Journal of Logic, Language and Information 2 (3):171-215.
M. E. Szabo (1989). Coherence in Cartesian Closed Categories and the Generality of Proofs. Studia Logica 48 (3):285 - 297.
Paliath Narendran, Frank Pfenning & Richard Statman (1997). On the Unification Problem for Cartesian Closed Categories. Journal of Symbolic Logic 62 (2):636-647.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Stephen H. Voss & Charles Sayward (1980). The Structure of Type Theory. Journal of Philosophy 77 (5):241-259.
Adam Obtułowicz (1989). Categorical and Algebraic Aspects of Martin-Löf Type Theory. Studia Logica 48 (3):299 - 317.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads15 ( #78,648 of 549,087 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
