Sequent calculi for intuitionistic Gödel-Löb logic
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.
- A modal calculus analogous to K4W, based on intuitionistic propositional logic, I^0
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Constructive modalities with provability smack
- Contraction-free sequent calculi for intuitionistic logic
- scientific article; zbMATH DE number 5520283 (Why is no real title available?)
- scientific article; zbMATH DE number 3719132 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- Interpolation theorems for intuitionistic predicate logic
- On modal systems having arithmetical interpretations
- Proof theory. 2nd ed
- Provability interpretations of modal logic
- Provability logic and the completeness principle
- Proving termination with multiset orderings
- Structural proof theory. With an appendix by Aarne Ranta
- Terminating sequent calculi for two intuitionistic modal logics
- The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
- The modal logic of provability: cut-elimination
- Uniform interpolation and propositional quantifiers in modal logics
- Uniform interpolation and sequent calculi in modal logic
- Valentini's cut-elimination for provability logic resolved
- A cut-free calculus for second-order Gödel logic
- The G4i analogue of a G3i sequent calculus
- Terminating calculi and countermodels for constructive modal logics
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- Circular proofs for the Gödel-Löb provability logic
- Admissible rules for six intuitionistic modal logics
- scientific article; zbMATH DE number 4150121 (Why is no real title available?)
- scientific article; zbMATH DE number 1950262 (Why is no real title available?)
- Terminating sequent calculi for two intuitionistic modal logics
- Sequent Calculi for Intuitionistic Linear Logic with Strong Negation
- Hypersequent Calculi for Godel Logics -- a Survey
- Gentzen sequent calculi for some intuitionistic modal logics
- Cut-free and analytic sequent calculus of intuitionistic epistemic logic
- Sequent and hypersequent calculi for abelian and łukasiewicz logics
- Sequent Calculus for Intuitionistic Epistemic Logic IEL
- Computer Science Logic
- scientific article; zbMATH DE number 7668109 (Why is no real title available?)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 12--17, 2023
- Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
- Proof analysis in modal logic
This page was built for publication: Sequent calculi for intuitionistic Gödel-Löb logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1982008)
