On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
From MaRDI portal
Publication:6365611
DOI10.1093/LOGCOM/EXAA078zbMATH Open1509.03033arXiv2104.09215MaRDI QIDQ6365611
Publication date: 19 April 2021
Abstract: This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting's nested calculi naturally arise from their corresponding labelled calculi--for each of the aforementioned logics--via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic's semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic's semantics.
Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
This page was built for publication: On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
