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)

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

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, Craig Interpolation in Displayable Logics, A Unified Display Proof Theory for Bunched Logic, CONSERVATIVITY OF HEYTING IMPLICATION OVER RELEVANT QUANTIFICATION

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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