6533b86dfe1ef96bd12c9fe3
RESEARCH PRODUCT
Collection Principles in Dependent Type Theory
Peter AczelNicola Gambinosubject
Discrete mathematicsInterpretation (logic)Dependent type theory constructive set theory propositions-as-typesComputer scienceConstructive set theoryIntuitionistic logicIntuitionistic type theoryDependent typeAlgebraMathematics::LogicTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESDependent type theoryType theoryTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSComputer Science::Logic in Computer ScienceDouble negationSet theoryRule of inferenceAxiomdescription
We introduce logic-enriched intuitionistic type theories, that extend intuitionistic dependent type theories with primitive judgements to express logic. By adding type theoretic rules that correspond to the collection axiom schemes of the constructive set theory CZF we obtain a generalisation of the type theoretic interpretation of CZF. Suitable logic-enriched type theories allow also the study of reinterpretations of logic. We end the paper with an application to the double-negation interpretation.
year | journal | country | edition | language |
---|---|---|---|---|
2002-01-01 |