Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM

Hugo Férée, Ian Shillito

TL;DR

Pitts'proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, is adapted to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM, and deduce the coherence of the class of KM-algebras.

Abstract

Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM

TL;DR

Pitts'proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, is adapted to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM, and deduce the coherence of the class of KM-algebras.

Abstract

Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.
Paper Structure (10 sections, 11 theorems, 13 equations, 3 figures)

This paper contains 10 sections, 11 theorems, 13 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Syntax
  4. Axiomatic system
  5. Kripke semantics
  6. A $\mathsf{G4}$ calculus for $\mathsf{KM}$
  7. Uniform interpolation for $\mathsf{KM}$ à la Pitts
  8. Algebraic consequence of uniform interpolation
  9. Conclusion
  10. Acknowledgments.

Key Result

lemma thmcounterlemma

For any model $\mathcal{M}=(W,\leq,R,I)$, formula $\varphi$ and points $w,v\in W$, if $w\leq v$ and $\mathcal{M},w\Vdash\varphi$ then $\mathcal{M},v\Vdash\varphi$.

Figures (3)

  • Figure 1: Generalised Hilbert calculus $\mathsf{KMH}$ for $\mathsf{KM}$ (\BaseUrl/KM.GHC.KMH.html).
  • Figure 2: The sequent calculus \ref{['seq:GfourKM']} (\BaseUrl/KM.Sequent.Sequents.html#Provable).
  • Figure 3: Clauses to define $\mathsf{E}_{p}(\Gamma)$ and $\mathsf{A}_{p}(\Gamma \Rightarrow \Delta)$. In all clauses, $q \neq p$.

Theorems & Definitions (30)

  • definition thmcounterdefinition: \BaseUrl/KM.Kripke.kripke_sem.html#model
  • definition thmcounterdefinition: \BaseUrl/KM.Kripke.kripke_sem.html#forces
  • lemma thmcounterlemma: Persistence \BaseUrl/KM.Kripke.kripke_sem.html#Persistence
  • definition thmcounterdefinition: \BaseUrl/KM.Sequent.syntax_facts.html#weight
  • definition thmcounterdefinition: Ordering on sequents \BaseUrl/KM.Sequent.Order.html#env_pair_order
  • proposition thmcounterproposition
  • proof
  • remark thmcounterremark
  • proposition thmcounterproposition: Decidability \BaseUrl/KM.Sequent.DecisionProcedure.html#Provable_dec
  • proposition thmcounterproposition
  • ...and 20 more