Sequent calculi for intuitionistic Gödel-Löb logic
type: Item
instance of: scholarly article
title: Sequent calculi for intuitionistic Gödel-Löb logic
zbMATH Open document ID: 1490.03013
DOI: 10.1215/00294527-2021-0011
author: Iris van der Giessen
author: Rosalie Iemhoff
published in: Notre Dame Journal of Formal Logic
publication date: 2021-09-07T00:00:00Z
review text: The paper investigates two sequent calculi for the modal logic iGL, which is the intuitionistic version of the Gödel-Löb logic (the classical provability logic). The first one, GL3i, is a common cut-free one-sided sequent calculus for intuitionistic logic augmented with the GL modal rule \[ \frac{\Box\Gamma,\Gamma,\Box A\Rightarrow A}{\Pi,\Box\Gamma\Rightarrow\Box A}; \] the second-one, GL4i, is based on the Dyckhoff-Hudelmaier terminating intuitionistic calculus. The paper proves in detail that cut is admissible in GL3i, using ideas by \textit{S. Valentini} [J. Philos. Logic 12, 471--476 (1983; Zbl 0535.03031)] and \textit{R. Goré} and \textit{R. Ramanayake} [Rev. Symb. Log. 5, No. 2, 212--238 (2012; Zbl 1254.03113)], and that GL4i is terminating. The authors go on to show the equivalence of GL3i and GL4i (which implies cut admissibility in GL4i, and that both calculi are sound and complete for the logic iGL), and the Craig interpolation property for iGL.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F45
zbMATH DE Number: 7391973
zbMATH Keywords: intuitionistic modal logic
zbMATH Keywords: Gödel-Löb logic
zbMATH Keywords: sequent calculus
zbMATH Keywords: cut admissibility
describes a project that uses: Pesca
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1215/00294527-2021-0011
OpenAlex ID: W3171305237
cites work: The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
cites work: On modal systems having arithmetical interpretations
cites work: Uniform interpolation and propositional quantifiers in modal logics
cites work: Q3607747
cites work: Proving termination with multiset orderings
cites work: Contraction-free sequent calculi for intuitionistic logic
cites work: Valentini's cut-elimination for provability logic resolved
cites work: An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
cites work: Terminating sequent calculi for two intuitionistic modal logics
cites work: Uniform interpolation and sequent calculi in modal logic
cites work: Q3909044
cites work: Constructive Modalities with Provability Smack
cites work: Interpolation theorems for intuitionistic predicate logic
cites work: Structural proof theory. With an appendix by Aarne Ranta
cites work: Provability interpretations of modal logic
cites work: Proof theory. 2nd ed
cites work: Q4499084
cites work: A modal calculus analogous to K4W, based on intuitionistic propositional logic, \(I^0\)
cites work: The modal logic of provability: cut-elimination
cites work: Provability logic and the completeness principle
description: scientific article; zbMATH DE number 7391973