Ternary relations and relevant semantics (Q598309)

This is a largely expository paper on the family of relevant logics. Meyer gives some history and also shows that all these relevant logics can be motivated by the properties of a ternary relation \(R\), where \(RXYZ\) is \(X\circ Y \subseteq Z\) and \[ X\circ Y=\{ B: \exists A(A\to B\in X \text{ and }A\in Y)\}. \] The ``worlds'' \(X, Y\ldots \) over which such binary and ternary relations usually range in semantics, are here ``demythologized'' as theories. Theories are sets of formulas subject to certain truth conditions and may represent (relevant) logics. These theories can be seen as the unions of the types of combinators. In the case of some theories the simple types of some combinators are sufficient. In these cases the theory is in fact a model of the corresponding combinatory logic, where application is interpreted as fusion \((o)\). Meyer's ``Key to the Universe'' is the fact that \(B\wedge T\), a theory based on intersection types, models SK (i.e. full) combinatory logic. The following illustrates the key to the universe syntactically: We list two combinators, their ``fusion fact'' (i.e. their reduction rule) and their ``implication fact'' (i.e. their type): \[ \begin{alignedat}{3} &S &\qquad ABC&\leq AC(BC) &\qquad A\to (B\to C)&\leq (A\to B)\to (A\to C)\\ W&B &\qquad AB&\leq A(AB) &\qquad (B\to C)&\wedge (A\to B) \leq A\to C. \end{alignedat} \] If \(L\) is any logic extending \(B[\to, \wedge , 0]\), then a fusion fact is a theorem scheme of \(L\) iff the corresponding implication fact is a theorem scheme.