Ternary relations and relevant semantics

DOI10.1016/J.APAL.2003.11.015MaRDI QIDQ598309zbMATH OpenOpenAlexFDO

Publication date 6 August 2004

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2003.11.015

bunch combinators combinatory logic fusion key2u theorem relevant entailment relevant logic ternary relation

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Relational systems, laws of composition (08A02)

Review text

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.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Ternary relations and relevant semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q598309)