Four relevant Gentzen systems

contraction-free logic contractionless logic Cut Theorems decision procedures Gentzen systems proof theory relevant logics semilattice logic semilattice relevant logics sentential constant structural constant

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Review text

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.

Recommendations

Cites work

Cited in

(10)

This page was built for publication: Four relevant Gentzen systems

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