The Semantics of Entailment Omega

This paper discusses the relation between the minimal positive relevant logic B+ and intersection and union type theories. There is a marvellous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking B T of B+, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her co-authors then become theory models of these calculi. (The logician's Theory is the algebraist's Filter.) The coincidence extends to a dual interpretation of key particles

• Type: Journal
• Year: 2002
• Where: NDJFL
• Authors: Mariangiola Dezani-Ciancaglini, Robert K. Meyer, Yoko Motohama
• Keywords: NDJFL 2002, Relevant Logic B+, Type Discipline ITD, Union Type Theories