×

Intersection type systems and logics related to the Meyer-Routley system \(B^+\). (English) Zbl 1048.03012

The (arrow) types assigned to closed terms in the lambda calculus are known to coincide on the theorems of intuitionistic implicational logic. However, there are also some closed terms that do not have types. This gap is filled by extending these simple types to intersection (or implication-conjunction) types. That is, all the closed lambda terms have types according to the extension. On the other hand, the logic corresponding to the extended type assignment constitutes the Meyer-Routley minimal relevance logic (without disjunction) which is weaker than the implication-conjunction fragment of intuitionistic logic.
In this paper, the author first provides an introduction to these issues on type assignment in lambda calculus and the corresponding logical system. Then, for certain interesting subsystems of the full intersection type theory, their corresponding logical systems are determined.

MSC:

03B40 Combinatory logic and lambda calculus
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B20 Subsystems of classical logic (including intuitionistic logic)
PDFBibTeX XMLCite