Sequent calculi for intuitionistic Gödel-Löb logic

Iris van der Giessen; Rosalie Iemhoff

doi:10.1215/00294527-2021-0011

Sequent calculi for intuitionistic Gödel-Löb logic

Iris van der Giessen, Rosalie Iemhoff

Research output: Contribution to journal › Article › peer-review

5 Downloads (Pure)

Abstract

This paper provides a study of sequent calculi for intuitionistic Gödel–Löb logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as Gödel–Löb logic. We present two different sequent calculi, one of which we prove to be the terminating version of the other. We study those systems from a proof-theoretic point of view. One of our main results is a syntactic proof for the cut-admissibility result for those systems. Finally, we apply this to prove Craig interpolation for intuitionistic Gödel–Löb logic.

Original language	English
Pages (from-to)	221-246
Number of pages	26
Journal	Notre Dame Journal of Formal Logic
Volume	62
Issue number	2
DOIs	https://doi.org/10.1215/00294527-2021-0011
Publication status	Published - 9 Jun 2021
Externally published	Yes

Keywords

cut-admissibility
Gödel–Löb logic
Intuitionistic logic
sequent calculi

Access to Document

10.1215/00294527-2021-0011

vdGiessen2021Sequent
This is an accepted manuscript version of an article first published in Notre Dame Journal of Formal Logic. The final version of record is available at https://doi.org/10.1215/00294527-2021-0011
Accepted author manuscript, 282 KBLicence: None: All rights reserved

Cite this

@article{c7479fc582f14e56bd47ccde2948e00a,

title = "Sequent calculi for intuitionistic G{\"o}del-L{\"o}b logic",

abstract = "This paper provides a study of sequent calculi for intuitionistic G{\"o}del–L{\"o}b logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as G{\"o}del–L{\"o}b logic. We present two different sequent calculi, one of which we prove to be the terminating version of the other. We study those systems from a proof-theoretic point of view. One of our main results is a syntactic proof for the cut-admissibility result for those systems. Finally, we apply this to prove Craig interpolation for intuitionistic G{\"o}del–L{\"o}b logic.",

keywords = "cut-admissibility, G{\"o}del–L{\"o}b logic, Intuitionistic logic, sequent calculi",

author = "{van der Giessen}, Iris and Rosalie Iemhoff",

year = "2021",

month = jun,

day = "9",

doi = "10.1215/00294527-2021-0011",

language = "English",

volume = "62",

pages = "221--246",

journal = "Notre Dame Journal of Formal Logic",

issn = "0029-4527",

publisher = "University of Notre Dame",

number = "2",

}

TY - JOUR

T1 - Sequent calculi for intuitionistic Gödel-Löb logic

AU - van der Giessen, Iris

AU - Iemhoff, Rosalie

PY - 2021/6/9

Y1 - 2021/6/9

N2 - This paper provides a study of sequent calculi for intuitionistic Gödel–Löb logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as Gödel–Löb logic. We present two different sequent calculi, one of which we prove to be the terminating version of the other. We study those systems from a proof-theoretic point of view. One of our main results is a syntactic proof for the cut-admissibility result for those systems. Finally, we apply this to prove Craig interpolation for intuitionistic Gödel–Löb logic.

AB - This paper provides a study of sequent calculi for intuitionistic Gödel–Löb logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as Gödel–Löb logic. We present two different sequent calculi, one of which we prove to be the terminating version of the other. We study those systems from a proof-theoretic point of view. One of our main results is a syntactic proof for the cut-admissibility result for those systems. Finally, we apply this to prove Craig interpolation for intuitionistic Gödel–Löb logic.

KW - cut-admissibility

KW - Gödel–Löb logic

KW - Intuitionistic logic

KW - sequent calculi

U2 - 10.1215/00294527-2021-0011

DO - 10.1215/00294527-2021-0011

M3 - Article

SN - 0029-4527

VL - 62

SP - 221

EP - 246

JO - Notre Dame Journal of Formal Logic

JF - Notre Dame Journal of Formal Logic

IS - 2

ER -

Sequent calculi for intuitionistic Gödel-Löb logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this