Displaying and deciding substructural logics. I: Logics with contraposition (Q1267081)

Belnap's display logic provides a cut-free consecution (sequent-style) calculus for relevant logics, in particular for the relevant systems \textbf{R} and \textbf{E}. This is done by enriching the calculus so that simple cuts are enough. If one needs to perform a cut on a formula which is inside a structure, the consecution can be transformed so that the formula to be cut stands alone as either the antecedent or the consequent of the consecution. Belnap proved that for relevant logics, a proof with simple Cut can be made Cut-free. Belnap's original paper utilized boolean negation, which is objectionable from the relevant point of view. The author shows that it is possible to formulate a display system for relevant logics without using boolean negation, by enriching the vocabulary with intuitionistic implication. This yields a conservative extension. The author used this display logic to give decidability results about a whole class of extensions to \textbf{DW}. Any logic extending \textbf{DW}, using axioms of the form \(A\rightarrow B\), where \(A\) and \(B\) are so-called confusions (formulas with connectives restricted to \(\circ\) or \(\wedge\)), has a corresponding display calculus rule, and a condition on \textbf{DW} frames, together with a soundness, completeness results and a correspondence condition with associated relations. If the axioms are further restricted to proper axioms (every proposition \(p_i\) in \(B\) appears in \(A\), and no \(p_i\) appears more than once in \(B\)), the extension has a Cut-free display calculus with the subformula property. Extensions of \textbf{DW} by so-called flat rules (proper rules such that the complexity of the premise is not greater than the complexity of the conclusion) yield decidable logics. The author points out that this display proof theory is not a solution of finding a proof theory for \textbf{R} or \textbf{E} which restricts itself to the original vocabulary of relevant logic (\(\wedge , \vee , \sim , \rightarrow \)).