Solution to a problem of Ono and Komori (Q5966494): Difference between revisions

\textit{H. Ono} and \textit{Y. Komori} [J. Symb. Logic 50, 169-201 (1985; Zbl 0583.03018)] posed several open problems concerning some systems of contraction-free logics. This paper gives the solution to Open Problem {\#}6: Give a Gentzen-type formulation for the distributive logic \(L_{DBCC}\) [equivalently, \(H_{BCC}]\) or \(L_{DBCK}\) [equivalently, \(H_{BCK}]\), for which the cut elimination theorem holds. The Gentzen systems presented in this paper are singular on the right and utilise two kinds of sequences or methods of combining formulae on the left, as is now common in dealing with relevant logics. Once this technique is employed, the choice of appropriate structural and logical rules becomes relatively straightforward, but the proof of a cut theorem (which is given in the paper) becomes correspondingly complicated. Ono and Komori's original systems are closely related to some contractionless relevant logics, to \(TW+\) in particular. So this paper draws appropriately on \textit{J. M. Dunn} [in \textit{A. R. Anderson} and \textit{N. D. Belnap}'s book: Entailment, Vol. 1 (1975; Zbl 0323.02030), pp. 381- 391], the reviewer [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)] and \textit{R. Brady} [ibid. forthcoming]. The author points out that the techniques are easily generalised to related logics.