Relational proof system for relevant logics (Q4032669)

This paper is an expanded version of the author's paper in Bull. Sect. Logic, Pol. Acad. Sci. 19, No. 2, 39-48 (1990; Zbl 0716.03010). It presents relational proof systems for a number of relevant logics similar to those given earlier for various modal logics (and for intuitionistic logic) [the author, ibid. 17, No. 1, 2-14 (1988; Zbl 0651.03011), Algebraic logic, Colloq. Math. Soc. J. Bolyai 54, 443-471 (1991; Zbl 0751.03009)]. The paper begins by presenting the relational proof system of a slight strengthening of the basic affixing system \({\mathbf B}\) (trade in the rule of contraposition for the corresponding axiom) as presented, for instance, by \textit{R. Routley}, \textit{V. Plumwood}, \textit{R. K. Meyer} and \textit{R. T. Brady} [Relevant logics and their rivals, Vol. 1 (1982; Zbl 0579.03011)]. (This system was presented by the author in her first paper mentioned above.) Formulas of relevant logic are mapped onto ternary relations. Then an appropriate logic of ternary relations is developed by adding a distinguished ternary relation \(R\) and then basically specifying rules of inference that build in the right semantic postulates from the Routley-Meyer relational semantics, as in, for instance, \textit{R. Routley} and \textit{R. K. Meyer} [Truth, syntax and modality, Stud. Logic Found. Math. 68, 199-243 (1973; Zbl 0317.02017)]. Formulae of the relational logic are then of the form \(Rabc\), \((A\to B)dtu\), etc. Those that do not use \(R\) are called non-degenerate. One then goes on to use the rules of inference to define decomposition trees, fundamental decomposition trees and complete decomposition trees for non-degenerate formulae. It is then claimed that a formula \(A\) of relevant logic is valid iff the corresponding formula \(A0ab\) of the relational logic has a fundamental decomposition tree. The author then extends her previous results by presenting proof systems for stronger relevant logics such as \({\mathbf T}{\mathbf W}\), \({\mathbf T}\), \({\mathbf R}\) and \({\mathbf R}\)-\textbf{Mingle}. Completeness proofs are presented in some detail. Readers who are familiar with the Routley-Meyer relational semantics for relevant logics will better understand this relational proof system if they note that 1) the proof system is thoroughly semantically based, and 2) the ``ternariness'' of the relations for non-degenerate formulae is really ``unariness'' -- the second and third place of the relation have no functional role. A formula of the form \(Aabc\) can be more or less read as ``\(A\) is true on every valuation at every point \(a\) in every model structure''. So a decomposition tree of a formula of the form \(A0ab\) is simply an attempt to show that \(A\) is valid in the relational semantics. A fundamental decomposition tree is a successful attempt, and a complete but non-fundamental decomposition tree will yield a method of specifying a counter-model to the validity of the formula in question. Cf. Urquhart's subscripted Gentzen systems for semilattice relevant logics as in the reviewer and \textit{A. Urquhart} [Z. Math. Logik Grundlagen Math. 33, 433-439 (1987; Zbl 0627.03005)].