Solution to a problem of Ono and Komori (Q5903941)

\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_{DBCC}]\) or \(L_{DBCK}\) [equivalently, \(H_{DBCK}]\), for which a cut elimination theorem holds. The axiomatisation of the former is very much like that for the contractionless relevant logic \(RW+\) with fusion (intensional conjunction) and a false constant, F. Simply drop Permutation and an explicit Identity axiom in favor of \(A\to.B\to A\) and the rule: From \(A\to.B\to C\) and B to conclude \(A\to C\). For the latter, keep the Permutation axiom, add the axiom just given, and Replace the normal \(\vee\)-Composition axiom with the stronger \(A\to C\to.B\to C\to.A\vee B\to C.\) The Gentzen systems of this paper \((LL_{DBCC}\), \(LL_{DBCK}\), respectively) 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. See \textit{J. M. Dunn} [in: \textit{A. R. Anderson} and \textit{N. D. Belnap jun.}, Entailment, Vol. 1 (1975; Zbl 0323.02030), pp. 381-391], for example. Once this technique is employed, the choice of appropriate structural and logical rules becomes relatively straightforward: Add a rule of intensional weakening and the axiom F:A to \(LRW+\) (without the rule of intensional permutation or exchange for the former). See the reviewer [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)], for instance. However, the proof of an appropriate cut theorem becomes correspondingly complicated. The author chooses the form: \[ \frac{X1:A1,...,Xn:An\quad y(A1...An):B}{Y(X1...Xn):B} \] which is proven by triple induction on rank, degree and the number of contractions (applications of extensional contraction) above the major premise.