Four relevant Gentzen systems (Q579235)

This paper is a study of four subscripted Gentzen systems \(G^ uR_+\), \(G^ uT_+\), \(G^ uRW_+\), and \(G^ uTW_+\). \textit{S. Giambrone} and \textit{A. Urquhart} [Z. Math. Logik Grundlagen Math. (to appear; Zbl 0611.03005)] show that the first three are equivalent to the semilattice relevant logics of \textit{A. Urquhart} [The Semantics of Eintailment (University of Pittsburgh Doctoral Dissertation, University Microfilms, Ann Arbor, Michigan) (1973) and J. Symb. Logic 37, 159-169 (1972; Zbl 0245.02028)], and \textit{R. K. Meyer} et al. [Z. Math. Logik Grundlagen Math. (to appear)] show that the implication conjunction fragement of \(G^ uTW_+\) is equivalent to the corresponding fragment of \({}^ uTW_+\). In this paper Cut Theorems and the admissibility of modus ponens are proved for each system, and decision procedures are provided for the contractionless or contraction-free systems, \(G^ uTW_+\) and \(G^ uRW_+.\) A placeholder is used for the proof of Cut as is usual with relevant Gentzen systems. In this case a structural constant I is used rather than the sentential constant t. The unusual problems raised by t in contractionless relevant logics was noted in \textit{S. Giambrone} [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)] and in \textit{S. Giambrone} and \textit{R. K. Meyer} [``Completeness and conservative extension results for some Boolean relevant logics'', forthcoming]. In these subscripted Gentzen systems special theorems are required for I even in the proof of Cut. In particular, it is shown that all occurrences of I in a derivation can be introduced before any other rules are used. I is also shown to be eliminable as required for the proof of admissibility of modus ponens in the contractionless systems, which proofs are normally trivial (given Cut Theorems) for systems with Contraction. The decidability argument utilizes König's Lemma. The conceptual motivation for the proof of the Finite Branch Property is relevantly similar to that of \textit{S. Giambrone} [loc. cit.]: the existence of finite upper bounds is shown for both the extensional and intensional complexity of consecutions, as ``represented'' by the subscripts in these systems.