Journal of Symbolic Logic 71 (1):67 - 103 (2006)

Abstract
We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1140641163
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,379
Through your library

References found in this work BETA

The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Wellfounded Trees in Categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.
Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1-3):164-188.

View all 10 references / Add more references

Citations of this work BETA

The Axiom of Choice.John L. Bell - 2008 - Stanford Encyclopedia of Philosophy.
A Minimalist Two-Level Foundation for Constructive Mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
Rudimentary and Arithmetical Constructive Set Theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.
The Associated Sheaf Functor Theorem in Algebraic Set Theory.Nicola Gambino - 2008 - Annals of Pure and Applied Logic 156 (1):68-77.

View all 8 citations / Add more citations

Similar books and articles

The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Godel's Interpretation of Intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.
Syntactic Calculus with Dependent Types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
Implicit Epistemic Aspects of Constructive Logic.Göran Sundholm - 1997 - Journal of Logic, Language and Information 6 (2):191-212.

Analytics

Added to PP index
2010-08-24

Total views
36 ( #318,163 of 2,519,663 )

Recent downloads (6 months)
1 ( #406,756 of 2,519,663 )

How can I increase my downloads?

Downloads

My notes