LE^t_ , LR^ _, LK and cutfree proofs

DOI10.1007/S10992-007-9048-0MaRDI QIDQ2454875zbMATH OpenOpenAlexFDO

Authors Katalin Bimbó

Publication date 22 October 2007

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

Full work available at URL https://doi.org/10.1007/s10992-007-9048-0

zbMATH Keywords

cut eliminationrelevance logicsstructurally free logics

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Review text

This paper contains two cut-elimination proofs: for the implicational fragment of the logic of entailment with truth and for the disjunction-free logic of nondistributive relevant implication. Also, a new, purely inductive, cut-elimination proof for Gentzen's sequent calculus LK is sketched.

Recommendations

• Gentzen's cut-free calculus versus the logic of paradox
• A cut-elimination proof in intuitionistic predicate logic
• Natural deduction and sequent calculus for intuitionistic relevant logic
• Structural cut elimination. I: Intuitionistic and classical logic
• A cut-free Gentzen calculus with subformula property for first-degree entailments in \(\mathbf{LC}\)

Cites work

• A Decision Procedure For the System E_Ī of Entailment with Negation
• Admissibility of cut in LC with fixed point combinator
• Combinators and structurally free logic
• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• scientific article; zbMATH DE number 596497 (Why is no real title available?)
• scientific article; zbMATH DE number 1028818 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 4117898 (Why is no real title available?)
• Structural proof theory. With an appendix by Aarne Ranta
• Two extensions of the structurally free logic LC

Cited in

(18)

• Cut elimination for entailment relations
• Valentini's cut-elimination for provability logic resolved
• scientific article; zbMATH DE number 1823879 (Why is no real title available?)
• THE CLASSICAL PROPOSITIONAL CALCULUS OF ARGUMENTS
• A note on the cut-elimination proof in ``Truth without contra(di)ction
• A cut-free Gentzen calculus with subformula property for first-degree entailments in \(\mathbf{LC}\)
• About some symmetries of negation
• Sequent calculus for the intersection of LK and the reversed
• scientific article; zbMATH DE number 1361537 (Why is no real title available?)
• scientific article; zbMATH DE number 2118592 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• On the decidability of implicational ticket entailment
• From Hilbert proofs to consecutions and back
• Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
• RELEVANCE LOGICS AND RELATION ALGEBRAS
• Gentzen's cut-free calculus versus the logic of paradox
• New consecution calculi for \(R^{t}_{\to}\)
• Entailment, mingle and binary accessibility

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs

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