Summary: BCD [H. Barendregt et al., J. Symb. Log. 48, 931–940 (1983; Zbl 0545.03004)] relies for its modeling of \(\lambda\) calculus in intersection type filters on a key theorem – BL (for the bubbling lemma, following someone). This lemma has been extended to BBL (the Better Bubbling Lemma) in [G. Castagna and A. Frisch, Lect. Notes Comput. Sci. 3580, 30–34 (2005; Zbl 1082.68581); M. Dezani-Ciancaglini et al., Electron. Notes Theor. Comput. Sci. 70, No. 1, 88–105 (2003; Zbl 1270.03043)] to encompass Boolean structure, including specifically union types. There are resonances, explored in [Dezani-Ciancaglini et al., loc. cit.; M. Dezani-Ciancaglini et al., Notre Dame J. Formal Logic 43, No. 3, 129–145 (2002; Zbl 1042.03019)], between intersection and union type theories and the already existing minimal positive relevant logic B+ of [R. Routley and the author, J. Philos. Log. 1, 192–208 (1972; Zbl 0317.02019)]. (Indeed [K. Pal and the author, Australas. J. Log. 3, 14–32 (2005; Zbl 1073.03011)] 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 [the author et al., Tributes 3, 59–84 (2005; Zbl 1245.03028)] 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 and the author, loc. cit.; the author et al., loc. cit.]
For the entire collection see [Zbl 1273.68035].