Sequent calculi for intuitionistic Gödel-Löb logic (Q1982008)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Sequent calculi for intuitionistic Gödel-Löb logic |
scientific article |
Statements
Sequent calculi for intuitionistic Gödel-Löb logic (English)
0 references
7 September 2021
0 references
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.
0 references
intuitionistic modal logic
0 references
Gödel-Löb logic
0 references
sequent calculus
0 references
cut admissibility
0 references
0 references
0 references