Four relevant Gentzen systems
type: Item
instance of: scholarly article
title: Four relevant Gentzen systems
zbMATH Open document ID: 0625.03008
DOI: 10.1007/BF00396905
author: Steve Giambrone
author: Aleksandar Kron
published in: Studia Logica
publication date: 1987-01-01T00:00:00Z
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{…
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 4014678
zbMATH Keywords: relevant logics
zbMATH Keywords: proof theory
zbMATH Keywords: decision procedures
zbMATH Keywords: contractionless logic
zbMATH Keywords: contraction-free logic
zbMATH Keywords: semilattice logic
zbMATH Keywords: Gentzen systems
zbMATH Keywords: semilattice relevant logics
zbMATH Keywords: Cut Theorems
zbMATH Keywords: structural constant
zbMATH Keywords: sentential constant
MaRDI profile type: Publication
cites work: Q3674619
cites work: Proof Theories for Semilattice Logics
cites work: Semantics for relevant logics
cites work: Q4110432
cites work: An axiomatic version of positive semilattice relevance logic
cites work: Q3869324
cites work: Gentzen formulations of two positive relevance logics
cites work: Q3728879
cites work: On purported Gentzen formulations of two positive relevant logics
cites work: A consecutive calculus for positive relevant implication with necessity
cites work: \(TW_+\) and \(RW_+\) are decidable
cites work: A contractionless semilattice semantics
description: scientific article; zbMATH DE number 4014678