Dualized Simple Type Theory
2017
We propose a new bi-intuitionistic type theory called Dualized Type Theory
(DTT). It is a simple type theory with perfect intuitionistic duality, and
corresponds to a single-sided polarized sequent calculus. We prove DTT strongly
normalizing, and prove type preservation. DTT is based on a new propositional
bi-intuitionistic logic called Dualized Intuitionistic Logic (DIL) that builds
on Pinto and Uustalu's logic L. DIL is a simplification of L by removing
several admissible inference rules while maintaining consistency and
completeness. Furthermore, DIL is defined using a dualized syntax by labeling
formulas and logical connectives with polarities thus reducing the number of
inference rules needed to define the logic. We give a direct proof of
consistency, but prove completeness by reduction to L.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
13
References
2
Citations
NaN
KQI