The ``relevance'' of intersection and union types (Q1381437): Difference between revisions

It is well known that the (simple \(\to\)) types of combinators are exactly the theorems of intuitionistic implicational logic. In the extended \(\to\wedge\) type theory all combinators with normal forms have types, but these types form a Hilbert-style logic, discovered by Venneri, related to the Meyer-Routley minimal logic \(B^+\), that is a proper sublogic of the \(\to\wedge\) fragment of intuitionistic logic. This paper examines the logic that corresponds to a further extension of type theory for combinators, that also includes union types. The Hilbert style logic obtained is again related to Meyer and Routley's \(B^+\), but while its \(\to\wedge\) fragment remains a sublogic of the \(\to\wedge\) fragment of intuitionistic logic, surprisingly the full \(\to\wedge\vee\) logic obtained from the type theory is not a sublogic of intuitionistic logic.