A note on sequent calculi intermediate between LJ and LK

DOI10.1007/BF00370289MaRDI QIDQ1115420zbMATH OpenOpenAlexFDO

Authors Branislav Boričić

Publication date 1988

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00370289

zbMATH Keywords

cut-free class of sequent derivationscut-free Gentzen-type formulationdecidable intermediate logicnormalizable natural deduction formulationsseparabilitysubsystems of Gentzen's sequent calculus LK

Mathematics Subject Classification ID

Intermediate logics (03B55) Cut-elimination and normal-form theorems (03F05)

Review text

We consider some subsystems of Gentzen's sequent calculus LK for classical first-order logic and find that for every first-order logic intermediate between the intuitionistic and the classical one, there exists a corresponding cut-free class of sequent derivations. An immediate consequence of such a consideration is that each decidable intermediate logic has a corresponding cut-free Gentzen-type formulation. This investigation together with the sequence-conclusion approach to natural deduction systems [see the author, J. Philos. Logic 14, 359-377 (1985; Zbl 0572.03033)] make it possible to get the normalizable natural deduction formulations of intermediate logics and provide also an opportunity to treat the problem of separability of intermediate logics [see \textit{T. Hosoi}, J. Tsuda College 6, 23-38 (1974)].

Recommendations

• On certain normalizable natural deduction formulations of some propositional intermediate logics
• Proof analysis in intermediate logics
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
• scientific article; zbMATH DE number 3853043
• MULTIPLE FORMS OF GENTZEN'S RULES AND SOME INTERMEDIATE LOGICS

Cites work

• A cut-free Gentzen-type system for the logic of the weak law of excluded middle
• A second paper “On the interpolation theorem for the logic of constant domains”
• Algebra of proofs
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• scientific article; zbMATH DE number 4106814 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• On intermediate propositional logics
• On logics intermediate between intuitionistic and classical predicate logic
• On sequence-conclusion natural deduction systems
• On the interpolation theorem for the logic of constant domains
• Über die Zwischensysteme der Aussagenlogik

Cited in

(11)

• On sequence-conclusion natural deduction systems
• A cut-free Gentzen-type system for the logic of the weak law of excluded middle
• On certain normalizable natural deduction formulations of some propositional intermediate logics
• Subformula and separation properties in natural deduction via small Kripke models
• MULTIPLE FORMS OF GENTZEN'S RULES AND SOME INTERMEDIATE LOGICS
• Sequent calculus for the intersection of LK and the reversed
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• Some conservative extension results on classical and intuitionistic sequent calculi
• scientific article; zbMATH DE number 3236052 (Why is no real title available?)
• Vetoing: social, logical and mathematical aspects

This page was built for publication: A note on sequent calculi intermediate between LJ and LK

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