Dualized Simple Type Theory

TL;DR

This paper introduces Dualized Type Theory (DTT), a simple, strongly normalizing bi-intuitionistic type theory with a corresponding polarized sequent calculus, based on a new logic called Dualized Intuitionistic Logic (DIL).

Contribution

It presents DTT and DIL, simplifying previous bi-intuitionistic logic by removing inference rules and establishing normalization, consistency, and completeness proofs.

Findings

DTT is strongly normalizing and type-preserving.

DIL simplifies bi-intuitionistic logic with polarities.

The logic maintains consistency and completeness.

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.