Bunder, Martin Intersection type systems and logics related to the Meyer-Routley system \(B^+\). (English) Zbl 1048.03012 Australas. J. Log. 1, 43-55 (2003). 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. Reviewer: Osamu Sonobe (Follonica) Cited in 1 Document 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) Keywords:lambda calculus; intersection type theory; Meyer-Routley minimal relevance logic; intuitionistic implicational logic; type assignment system PDFBibTeX XMLCite \textit{M. Bunder}, Australas. J. Log. 1, 43--55 (2003; Zbl 1048.03012)