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

DOI10.1215/00294527-2021-0011zbMath1490.03013OpenAlexW3171305237MaRDI QIDQ1982008

Rosalie Iemhoff, Iris van der Giessen

Publication date: 7 September 2021

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1215/00294527-2021-0011

zbMATH Keywords

sequent calculusintuitionistic modal logicGödel-Löb logiccut admissibility

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (4)

Terminating calculi and countermodels for constructive modal logics ⋮ Admissible rules for six intuitionistic modal logics ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ The G4i analogue of a G3i sequent calculus

Uses Software

• Pesca

Cites Work

• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
• The modal logic of provability: cut-elimination
• Uniform interpolation and propositional quantifiers in modal logics
• Proof theory. 2nd ed
• A modal calculus analogous to K4W, based on intuitionistic propositional logic, \(I^0\)
• Provability interpretations of modal logic
• Uniform interpolation and sequent calculi in modal logic
• Provability logic and the completeness principle
• VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED
• On modal systems having arithmetical interpretations
• Proving termination with multiset orderings
• Contraction-free sequent calculi for intuitionistic logic
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Terminating sequent calculi for two intuitionistic modal logics
• Constructive Modalities with Provability Smack
• Interpolation theorems for intuitionistic predicate logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Sequent calculi for intuitionistic Gödel-Löb logic