6533b839fe1ef96bd12a5cdd
RESEARCH PRODUCT
The generalised type-theoretic interpretation of constructive set theory
Peter AczelNicola Gambinosubject
Discrete mathematicsLogicConstructive set theoryType (model theory)Translation (geometry)Constructive Set TheoryInterpretation (model theory)AlgebraPhilosophyType theoryDependent type theoryDependent Type TheoryComputer Science::Logic in Computer Science03F25Constructive set theory Dependent type theoryMathematics03F50description
We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive instead of being formulated via the propositions-as-types representation. 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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2006-03-01 |