Mechanised uniform interpolation for modal logics K, GL, and iSL

TL;DR

This work presents a fully mechanised, constructive treatment of uniform interpolation for three logics—$\mathsf{K}$, $\mathsf{GL}$, and $\mathsf{iSL}$—within the Coq proof assistant, producing verified procedures that compute $p$-free interpolants. It builds on terminating sequent calculi $\mathsf{KS}$, $\mathsf{GLS}$, and $\mathsf{G4iSLt}$ to define and prove correctness of the interpolant operators $\mathsf{A}_{p}$ and $\mathsf{E}_{p}$, ensuring $p$-freeness, implication, and the uniformity property. For $\mathsf{K}$ the interpolation construction follows established methods; for $\mathsf{GL}$ the authors fix an incompleteness in prior work by introducing a mutually recursive GL construction with a contraction-based canopy refinement; and for $\mathsf{iSL}$ they present the first proof-theoretic UIP for this intuitionistic modal logic. The verified pipeline yields executable interpolants (via Coq extraction to OCaml) and a demo web interface, enabling practical computation of interpolants from input formulas. These results advance the reliability and applicability of uniform interpolation in modal and intuitionistic logics, with potential impact on definability, proof theory, and logic-based tooling.

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 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.

Figures (5)

• Figure 1: Classical sequent rules. Here, $\Phi$ and $\Psi$ do not contain boxed formulae.
• Figure 2: The sequent calculus $\mathsf{G4iSLt}$. The sequent calculus $\mathsf{G4iP}$ is the restriction of $\mathsf{G4iSLt}$ obtained by omitting the two rules involving $\space\text{ }$.
• Figure 3: Definition of function $\mathsf{N}_{p}(\cdot,\cdot)$ from Bil06, where $t = (\Sigma \Rightarrow \Pi)$.
• Figure 4: Two sequents that are equivalent up to contraction, but the canopies are not.
• Figure 5: The top part of each table, i.e., $(\mathsf{E_p^\mathsf{IL}}0)$-$(\mathsf{E_p^\mathsf{IL}}8)$ and $(\mathsf{A_p^\mathsf{IL}}1)$-$(\mathsf{A_p^\mathsf{IL}}13)$ define $\mathsf{E}_{p}(\Gamma)$ and $\mathsf{A}_{p}(\Gamma \Rightarrow \varphi)$ for $\mathsf{IL}$ as defined in Pit92. The complete table provides definitions for $\mathsf{E}_{p}(\Gamma)$ and $\mathsf{A}_{p}(\Gamma \Rightarrow \varphi)$ for $\mathsf{iSL}$. In all clauses, $q \neq p$.

Theorems & Definitions (24)

• definition thmcounterdefinition
• lemma thmcounterlemma
• proof
• definition thmcounterdefinition
• remark thmcounterremark
• remark thmcounterremark
• remark thmcounterremark
• definition thmcounterdefinition: \BaseUrl/K.Interpolation.UIK_braga.html#GUI
• theorem thmcountertheorem
• proof