TYPES AND THE BOOLEAN SYSTEM CB+
<_author_search_(robert k. meyer)>Robert K. Meyer
Australian National University

In [1], Barendregt, Coppo and Dezani (henceforth BCD) set out the following postulates on an ?intersection? theory of types ITD. Primitive are type variables, w (universal type), ? (type inclusion), ? (type intersection), and fi. The type symbols are the result of closing variables and w (and perhaps other constants) under fi and ?. The postulates of ITD are, for all type symbols r, s, s?, t, t?, t ? t; t ? w; w ? wfiw; t ? t ? t; s?t ? s; s?t ? t;
(sfir) ? (sfit) ? s fi (r?t); s ? t ? r fi s ? r ;
s ? s?, t ? t? fi s?t ? s??t?; s? ? s, t ? t? fi sfit ? s?fit?;
?Lord,? said I to myself on beholding these postulates,1 ?this is just the minimal relevant logic B+ that I proposed with Routley in [2] and [3].?2 More accurately, it is the fi, &, T fragment3 of B+, which may be formulated with the following axiom schemes and rules:4
AfiA; A fiT; T fi (T fifi T) ; A&B fi A; A&B fi B; (AfiB)&(AfiC)fi(AfiB&C); AfiB fi (BfiC) fi (AfiC); BfiC fi (AfiB) fi (AfiC)
AfiB and A fi B; A and B fi A&B
Why should we believe that ITD and B+ are the same system? We make the obvious identifications of T with w, of & with ?, and of provable fi in B+ with ITD ?. A quick deductive induction shows that every ITD theorem holds on B+ translation. The most elegant5 way to prove the converse is via a ?metavaluation? v, with values in {1,0}. Define v on all formulas of B+ thus:
If A is a sentential variable, v(A) = 0; v(T) = 1;
v(A&B) = 1 iff v(A) = v(B) = 1;
v(AfiB) = 1 iff (i) A ? B in ITD and (ii) v(A) = 0 or v(B) = 1.
It is readily verified that all theorems of B+ take the value 1 on v. But in view of clause (i) in the truth-condition on fi, this means that their counterparts are theorems of ITD as well. So Observation 1. A is a theorem of ITD iff it is on translation a theorem of B+.

I. Filters, theories, and relevant semantics. [1] presents its main results as providing a filter lambda model. But, as I learned from Dunn, ?filter? is just Algebra-ese for what logicians call a ?theory?. So it would seem that we have a theory lambda model as well. This explains a lot. For one thing, it explains why Routley and I were right to call Combinatory Logic the ?key to the Universe? in work cited above. For CL is, after all, just l in another guise.6 For our algebraic postulates in [2], and our relational semantical postulates in [3], separated various substructural logics on straightforward properties of combinators. Thanks to [1], we know why we were right. The semantics of relevant logics is, at root, a semantics of B+ theories. Particular additional axioms (e. g., those for the system R of [4] and [5]) put constraints on the theories admitted into the semantics, exactly corresponding to the combinators that have these axioms as their ?types?.

Let us delve deeper. The intentions of BCD in [1] and related papers were certainly very different from Routley?s and mine in [2] and [3]. Ours were to present a semantics for a class of relevant logics, of which B+ turned out to be a ?natural? minimal positive one. By contrast [1] begins from l-models, and shows

1 Thanks to J.R. Hindley, who informed me of the BCD work.
2 Thus Hindley is misleading when his title of [12] suggests that ITD is not a logic. It is just a much weaker logic than those to which the SK-chauvinists are accustomed!
3 The ?Church? constant T was not mentioned in [3], though it is familiar from other works on relevant logic. It is to be assigned the value ?true? at all ?worlds? in every B+ model.
4 For ease in reading formulas, binary connectives are ranked o,&,?,fi,? in order of increasing scope; associate equal connectives to the left; and, as above, fi is a metalogical if.
5 Belnap notes that an elegant proof is one where you feel cheated at every step!
6 [6] takes CL as the ?assembly language? for l. But the l-CL relation is delicate. See [13] and [14].