Intersection Type Systems and Logics Related to the Meyer–Routley System B+

  • Martin Bunder Department of Mathematics, University of Wollongong

Abstract

Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (→) types to intersection (or →∧) types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer–Routley minimal logic B+ (without ∨), is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain interesting subsystems of the full →∧ type theory.

Author Biography

Martin Bunder, Department of Mathematics, University of Wollongong
Published
2012-09-16
How to Cite
BUNDER, Martin. Intersection Type Systems and Logics Related to the Meyer–Routley System B+. The Australasian Journal of Logic, [S.l.], v. 1, sep. 2012. ISSN 1448-5052. Available at: <https://ojs.victoria.ac.nz/ajl/article/view/1762>. Date accessed: 14 nov. 2019. doi: https://doi.org/10.26686/ajl.v1i0.1762.