{
  "id": "2104.09215",
  "version": "v1",
  "published": "2021-04-19T11:20:58.000Z",
  "updated": "2021-04-19T11:20:58.000Z",
  "title": "On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics",
  "authors": [
    "Tim Lyon"
  ],
  "comment": "arXiv admin note: text overlap with arXiv:1910.06576",
  "doi": "10.1093/logcom/exaa078",
  "categories": [
    "math.LO",
    "cs.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2021-04-19T11:20:58.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "semantic systems",
      "first-order intuitionistic logic",
      "correspondence",
      "labelled calculi",
      "nested calculi inherit proof-theoretic properties"
    ],
    "tags": [
      "journal article"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}