\(TW_+\) and \(RW_+\) are decidable (Q1072541)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | \(TW_+\) and \(RW_+\) are decidable |
scientific article |
Statements
\(TW_+\) and \(RW_+\) are decidable (English)
0 references
1985
0 references
This paper provides consecution calculi (Gentzen systems) and decision procedures for the contractionless relevant logics \(TW_+\) and \(RW_+\), which are, respectively, the positive fragments of the systems T of ticket entailment and R of relevant implication without the contraction axiom \((A\to.A\to B)\to.A\to B\). The decision procedures are proof- theoretic in character and based upon the Gentzen systems provided. Aside from the inherent interest of contractionless relevant logics, these results are significant for at least two other reasons. In the first place, consecution calculi for full positive relevant logics are of a higher order of complexity than the usual ones, e.g., those for classical and intuitionistic logic. This is the first time such complex systems have been successfully used to obtain major results. Further, \(TW_+\) and \(RW_+\) will be nearly the strongest decidable relevant logics, as is indicated by \textit{A. Urquhart}'s ''The undecidability of entailment and relevant implication'' [J. Symb. Logic 49, 1059-1073 (1984; Zbl 0581.03011)] in which it is shown that even the deducibility problem for \(TW_+\) is undecidable.
0 references
proof theory
0 references
consecution calculi
0 references
Gentzen systems
0 references
decision procedures
0 references
contractionless relevant logics
0 references
positive fragments
0 references
ticket entailment
0 references
relevant implication
0 references