On deriving nested calculi for intuitionistic logics from semantic systems

DOI10.1007/978-3-030-36755-8_12zbMATH Open1485.03021arXiv1910.06576OpenAlexW2994955096MaRDI QIDQ2177587FDOQ2177587

Authors: Tim S. Lyon 

Publication date: 6 May 2020

Abstract: This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.

Full work available at URL: https://arxiv.org/abs/1910.06576

Recommendations

• On the correspondence between nested calculi and semantic systems for intuitionistic logics
• A semantical view of proof systems
• Sequentialising nested systems
• Nested sequents for intuitionistic logics
• A proof-theoretic study of bi-intuitionistic propositional sequent calculus

zbMATH Keywords

proof theoryintuitionistic logicKripke semanticslabelled calculinested calculistructural rule elimination

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cited In (4)

• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
• A semantical view of proof systems
• On the correspondence between nested calculi and semantic systems for intuitionistic logics

This page was built for publication: On deriving nested calculi for intuitionistic logics from semantic systems

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