### Abstract

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.

Original language | English (US) |
---|---|

Journal | Logical Methods in Computer Science |

Volume | 12 |

Issue number | 3 |

DOIs | |

Publication status | Published - Jan 1 2016 |

### Fingerprint

### Keywords

- Bi-intuitionistic logic
- Coinduction
- Completeness
- Consistency
- Dual
- Exclusion
- Kripke model
- Sequent calculus
- Simple type theory
- Subtraction

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Logical Methods in Computer Science*,

*12*(3). https://doi.org/10.2168/LMCS-12(3:2)2016