Inhabitation in intersection and union type assignment systems

Abstract

Union does not correspond to intuitionistic disjunction and intersection does not correspond to intuitionistic conjunction. The Curry-Howard isomorphism between types inhabited in the intersection and union type assignment system and formulae provable in intuitionistic propositional logic with implication, conjunction, disjunction and truth does not hold. This is shown semantically. The extension of the simply typed lambda calculus with conjunction and disjunction types and the corresponding elimination and introduction rules is considered. By the Curry-Howard isomorphism types inhabited in this extension of the simply typed lambda calculus correspond to the intuitionistically provable formulae. We shall link the inhabitation in the intersection and union type assignment system with the inhabitation in this extension of the simply typed lambda calculus.