0000000000878440

AUTHOR

Peter Aczel

showing 2 related works from this author

The generalised type-theoretic interpretation of constructive set theory

2006

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.

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 theoryMathematics03F50
researchProduct

Collection Principles in Dependent Type Theory

2002

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.

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 inferenceAxiom
researchProduct