Solution to a problem of Ono and Komori

DOI10.1007/BF00296176MaRDI QIDQ5966494zbMATH OpenFDO

Authors John K. Slaney

Publication date 1989

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00296176

zbMATH Keywords

BCC logicBCK logiccontraction-free logicscontractionless logiccut eliminationGentzen systemsTW

Mathematics Subject Classification ID

General logic (03B99) Cut-elimination and normal-form theorems (03F05)

Review text

\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.

Recommendations

• Solution to a problem of Ono and Komori
• The proof-theoretical analysis of contraction-less relevant logics
• scientific article; zbMATH DE number 823590
• Simple Gentzenizations for the normal formulae of contraction-less logics
• Four relevant Gentzen systems

Cites work

• \(TW_+\) and \(RW_+\) are decidable
• Display logic
• Logics without the contraction rule

Cited in

(9)

• On purported Gentzen formulations of two positive relevant logics
• On the solution of a problem of Okuyama
• Correction to: ``Solution to a problem of Ono and Komori
• Cut-elimination for a logic with definitions and induction
• Gentzenization and decidability of some contraction-less relevant logics
• Solutions to some open problems from Slaney
• A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
• scientific article; zbMATH DE number 3926850 (Why is no real title available?)
• Solution to a problem of Ono and Komori

This page was built for publication: Solution to a problem of Ono and Komori

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