Abstract Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts’ seminal work establishes this property for intuitionistic propositional logic relying on a sequent calculus in which naïve backward proof-search terminates. This constructive approach has been adapted to a wide range of logics, including intuitionistic modal logics. Surprisingly, no intuitionistic modal logic with independent box and diamond has yet been shown to satisfy uniform interpolation. We fill in this gap by proving the uniform interpolation property for Constructive K (CK) and Wijesekera’s K (WK). We build on Pitts’ technique by exploiting existing terminating calculi for CK and WK, which we prove to eliminate cut, and formalise all our results in the proof assistant Rocq. Together, our results constitute the first positive uniform interpolation results for intuitionistic modal logics with diamond.

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 and apply it to reprove the uniform interpolation property for normal modal logics $\textsf{K}$, $\textsf{D}$ and $\textsf{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 $\textsf{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.

We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that ℓ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 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 IGL.

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.

Abstract We introduce a Gentzen-style framework, calledlayered sequent calculi, for modal logic $$\textsf{K5}$$ and its extensions $$\textsf{KD5}$$ , $$\textsf{K45}$$ , $$\textsf{KD45}$$ , $$\textsf{KB5}$$ , and $$\textsf{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 $$\textsf{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.

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 $$\textsf{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.

This paper characterizes the admissible rules for six interesting intuitionistic modal logics: iCK4, iCS4≡IPC, strong Löb logic iSL, modalized Heyting calculus mHC, Kuznetsov-Muravitsky logic KM, and propositional lax logic PLL. Admissible rules are rules that can be added to a logic without changing the set of theorems of the logic. We provide a Gentzen-style proof theory for admissibility that combines methods known for intuitionistic propositional logic and classical modal logic. From this proof theory, we extract bases for the admissible rules, i.e., sets of admissible rules that derive all other admissible rules. In addition, we show that admissibility is decidable for these logics.

We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction.In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table.This yields natural deduction rules for each connective separately.Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions.The aim is to remove all convertibilities and obtain a deduction in normal form.In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study.It has already been shown that this conversion is weakly normalizing.To prove strong normalization, we construct a conversionpreserving translation from deductions to terms in an extension of simply typed lambda calculus