The Better Bubbling Lemma

BCD Barendregt, Henk, Mario Coppo and Mariangiola Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, JSL 48 (1983), 931–940] relies for its modeling of λ calculus in intersection type filters on a key theorem which I call BL (for the Bubbling Lemma, following someone). This lemma has been extended in Castagna, Giuseppe, and Alain Frisch. A gentle introduction to semantic subtyping. In PPDP05, ACM Press (full version) and ICALP05, LNCS volume 3580, Springer-Verlag (summary), 2005. Joint ICALP-PPDP keynote talk; Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp] to encompass Boolean structure, including specifically union types; this extended lemma I call BBL (the Better Bubbling Lemma). There are resonances, explored in Dezani-Ciancaglini, M., R.K. Meyer and Y. Motohama, The semantics of entailment omega, NDJFL 43 (2002), 129–145] and Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp], between intersection and union type theories and the already existing minimal positive relevant logic B+ of Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192–208]. (Indeed Pal, Koushik, and Robert K. Meyer. 2005. Basic relevant theories for combinators at levels I and II, AJL 3, http://www.philosophy.unimelb.edu.au/2005/2003_2.pdf, 19 pages] applies BL and BBL to get further results linking combinators to relevant theories and propositions.) On these resonances the filters of algebra become the theories of logic. The semantics of Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., “Truth and Probability: Essays in Honour of Hugues Leblanc,” pages 59–84, College Publications, King's College, London, 2005] yields here a new and short proof of BBL, which takes account of full Boolean structure by encompassing not only B+ but also its conservative Boolean extension CB Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192–208; Meyer, Robert K., 1995. Types and the Boolean system CB+, cslab.anu.edu.au/ftp/techreports/SRS/1995/TR-SRS-5-95/meyer.ps.gz; Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., “Truth and Probability: Essays in Honour of Hugues Leblanc,” pages 59–84, College Publications, King's College, London, 2005.].