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

TL;DR

This paper mechanises the computation of uniform interpolants in modal logics K, GL, and iSL, providing verified algorithms and formal proofs in Coq for these properties.

Contribution

It introduces the first proof-theoretic construction of uniform interpolants for iSL and formalises the process for K and GL in Coq, ensuring correctness.

Findings

Verified algorithms for propositional quantifiers in K, GL, and iSL

Formal proofs of uniform interpolation in Coq for these logics

Clarification of an incomplete proof for GL in sequent calculus

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\"odel-L\"ob logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong L\"ob 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.