-
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.
-
Uniform interpolation via nested sequents and hypersequents
Authors:
Iris van der Giessen,
Raheleh Jalali,
Roman Kuznets
Abstract:
A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents a…
▽ More
A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics $\mathsf{K}$, $\mathsf{D}$, and $\mathsf{T}$. We then use the know-how developed for nested sequents to apply the same method to hypersequents and obtain the first direct proof of uniform interpolation for $\mathsf{S5}$ via a cut-free sequent-like calculus. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents and hypersequents also uses semantic notions, including bisimulation modulo an atomic proposition.
△ Less
Submitted 23 May, 2021;
originally announced May 2021.
