{
  "id": "2011.10383",
  "version": "v1",
  "published": "2020-11-20T12:46:24.000Z",
  "updated": "2020-11-20T12:46:24.000Z",
  "title": "Proof Theory for Intuitionistic Strong Löb Logic",
  "authors": [
    "Iris van der Giessen",
    "Rosalie Iemhoff"
  ],
  "comment": "29 pages, 4 figures, submitted to the Special Volume of the Workshop Proofs! held in Paris in 2017",
  "categories": [
    "math.LO"
  ],
  "abstract": "This paper introduces two sequent calculi for intuitionistic strong L\\\"ob logic ${\\sf iSL}_\\Box$: a terminating sequent calculus ${\\sf G4iSL}_\\Box$ based on the terminating sequent calculus ${\\sf G4ip}$ for intuitionistic propositional logic ${\\sf IPC}$ and an extension ${\\sf G3iSL}_\\Box$ of the standard cut-free sequent calculus ${\\sf G3ip}$ without structural rules for ${\\sf IPC}$. One of the main results is a syntactic proof of the cut-elimination theorem for ${\\sf G3iSL}_\\Box$. In addition, equivalences between the sequent calculi and Hilbert systems for ${\\sf iSL}_\\Box$ are established. It is known from the literature that ${\\sf iSL}_\\Box$ is complete with respect to the class of intuitionistic modal Kripke models in which the modal relation is transitive, conversely well-founded and a subset of the intuitionistic relation. Here a constructive proof of this fact is obtained by using a countermodel construction based on a variant of ${\\sf G4iSL}_\\Box$. The paper thus contains two proofs of cut-elimination, a semantic and a syntactic proof.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2020-11-20T12:46:24.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B45",
      "03F03",
      "03F05"
    ],
    "keywords": [
      "intuitionistic strong löb logic",
      "proof theory",
      "terminating sequent calculus",
      "intuitionistic modal kripke models",
      "syntactic proof"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 29,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}