Sequent Calculi for Intuitionistic Gödel–Löb Logic

2021/05/01 by Iris van der Giessen, Rosalie Iemhoff
Computer Science · #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic #Logic, programming, and type systems

paper · pdf · doi:10.1215/00294527-2021-0011

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.

Citations

• Provability interpretations of modal logic

Related

• Proof Theory for Intuitionistic Strong Löb Logic
• Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
• Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
• A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
• Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics