On deriving nested calculi for intuitionistic logics from semantic systems

DOI10.1007/978-3-030-36755-8_12MaRDI QIDQ2177587zbMATH OpenOpenAlexFDO

Authors Tim S. Lyon

Publication date 6 May 2020

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

zbMATH Keywords

intuitionistic logicKripke semanticslabelled calculinested calculiproof theorystructural rule elimination

Mathematics Subject Classification ID

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

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.

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

Cited in

(5)

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

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)