On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics

Tim LyonTim Lyon

ISSN: 0955-792X
Download
DOI Link

Tim Lyon
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
Journal of Logic and Computation, 31(1):213-265, 2021

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{10.1093/logcom/exaa078,
    author = {Lyon, Tim},
    title = "{On the correspondence between nested calculi and semantic systems for intuitionistic logics}",
    journal = {Journal of Logic and Computation},
    volume = {31},
    number = {1},
    pages = {213-265},
    year = {2020},
    month = {12},
    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.}",
    issn = {0955-792X},
    doi = {10.1093/logcom/exaa078},
    url = {https://doi.org/10.1093/logcom/exaa078},
    eprint = {https://academic.oup.com/logcom/article-pdf/31/1/213/36677523/exaa078.pdf},
}