Displaying and deciding substructural logics. I: Logics with contraposition

DOI10.1023/A:1017998605966zbMath0913.03029MaRDI QIDQ1267081

Greg Restall

Publication date: 24 May 1999

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

Full work available at URL: https://doi.org/10.1023/a:1017998605966

zbMATH Keywords

decidability; cut-elimination; correspondence theory; display logic; relevant logics; intuitionistic implication; display proof theory

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03F05: Cut-elimination and normal-form theorems

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

03F03: Proof theory in general (including proof-theoretic semantics)

Related Items

On Displaying Negative Modalities, Displaying the modal logic of consistency, Power and Limits of Structural Display Rules, Understanding negation implicationally in the relevant logic R, Synchronized linear-time temporal logic, Combining linear-time temporal logic with constructiveness and paraconsistency, Display calculi and other modal calculi: a comparison, Bunched logics displayed, Hypersequent and display calculi -- a unified perspective, Disentangling structural connectives or life without display property, Craig Interpolation in Displayable Logics, A Unified Display Proof Theory for Bunched Logic, CONSERVATIVITY OF HEYTING IMPLICATION OVER RELEVANT QUANTIFICATION

Cites Work

• Linear logic
• Simplified semantics for relevant logics (and some of their rivals)
• Linear logic displayed
• The word problem for Smullyan's lark combinator is decidable
• How to decide the lark
• Display logic
• Gentzenization and decidability of some contraction-less relevant logics
• The undecidability of entailment and relevant implication
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item