-
Mechanised uniform interpolation for modal logics K, GL, and iSL
Authors:
Hugo Férée,
Iris van der Giessen,
Sam van Gool,
Ian Shillito
Abstract:
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an…
▽ More
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.
△ Less
Submitted 29 April, 2024; v1 submitted 16 February, 2024;
originally announced February 2024.
-
Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
Authors:
Anupam Das,
Iris van der Giessen,
Sonia Marin
Abstract:
We derive an intuitionistic version of Gödel-Löb modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestep** the barrier that $\sf{GL}$'s usual frame c…
▽ More
We derive an intuitionistic version of Gödel-Löb modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestep** the barrier that $\sf{GL}$'s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of $\sf{GL}$ are typically defined over only the box (and not the diamond), our presentation includes both modalities.
Our main result is that $\sf{\ell IGL}$ coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic $\sf{IGL}$. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of $\sf{IGL}$.
△ Less
Submitted 1 September, 2023;
originally announced September 2023.
-
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Authors:
Ian Shillito,
Iris van der Giessen,
Rajeev Goré,
Rosalie Iemhoff
Abstract:
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direc…
▽ More
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.
△ Less
Submitted 1 September, 2023;
originally announced September 2023.
-
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
Authors:
Iris van der Giessen,
Raheleh Jalali,
Roman Kuznets
Abstract:
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive…
▽ More
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.
△ Less
Submitted 21 July, 2023;
originally announced July 2023.
-
Proof Theory for Intuitionistic Strong Löb Logic
Authors:
Iris van der Giessen,
Rosalie Iemhoff
Abstract:
This paper introduces two sequent calculi for intuitionistic strong Löb logic ${\sf iSL}_\Box$: a terminating sequent calculus ${\sf G4iSL}_\Box$ based on the terminating sequent calculus ${\sf G4ip}$ for intuitionistic propositional logic ${\sf IPC}$ and an extension ${\sf G3iSL}_\Box$ of the standard cut-free sequent calculus ${\sf G3ip}$ without structural rules for ${\sf IPC}$. One of the main…
▽ More
This paper introduces two sequent calculi for intuitionistic strong Löb logic ${\sf iSL}_\Box$: a terminating sequent calculus ${\sf G4iSL}_\Box$ based on the terminating sequent calculus ${\sf G4ip}$ for intuitionistic propositional logic ${\sf IPC}$ and an extension ${\sf G3iSL}_\Box$ of the standard cut-free sequent calculus ${\sf G3ip}$ without structural rules for ${\sf IPC}$. One of the main results is a syntactic proof of the cut-elimination theorem for ${\sf G3iSL}_\Box$. In addition, equivalences between the sequent calculi and Hilbert systems for ${\sf iSL}_\Box$ are established. It is known from the literature that ${\sf iSL}_\Box$ is complete with respect to the class of intuitionistic modal Kripke models in which the modal relation is transitive, conversely well-founded and a subset of the intuitionistic relation. Here a constructive proof of this fact is obtained by using a countermodel construction based on a variant of ${\sf G4iSL}_\Box$. The paper thus contains two proofs of cut-elimination, a semantic and a syntactic proof.
△ Less
Submitted 20 November, 2020;
originally announced November 2020.
