Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Six Proofs of Interpolation for the Modal Logic K

Nick Bezhanishvili, Balder ten Cate, Rosalie Iemhoff

TL;DR

Craig interpolation for the modal logic $\mathsf{K}$ is studied. The paper presents six distinct proofs of the interpolation theorem, drawing from model theory, proof theory, syntactic methods, automata theory, quasi-models, and algebra. It analyzes interpolant size under both $|\varphi|$ and $|\varphi|_{\text{DAG}}$, discusses the feasibility of uniform interpolation, and compares the computational trade-offs of the different approaches. The work offers a multi-faceted view of interpolation in non-classical logics and informs algorithmic interpolant construction across related modal frameworks.

Abstract

In this chapter, we present six different proofs of Craig interpolation for the modal logic K, each using a different set of techniques (model-theoretic, proof-theoretic, syntactic, automata-theoretic, using quasi-models, and algebraic). We compare the pros and cons of each proof technique.

Six Proofs of Interpolation for the Modal Logic K

TL;DR

Craig interpolation for the modal logic is studied. The paper presents six distinct proofs of the interpolation theorem, drawing from model theory, proof theory, syntactic methods, automata theory, quasi-models, and algebra. It analyzes interpolant size under both and , discusses the feasibility of uniform interpolation, and compares the computational trade-offs of the different approaches. The work offers a multi-faceted view of interpolation in non-classical logics and informs algorithmic interpolant construction across related modal frameworks.

Abstract

In this chapter, we present six different proofs of Craig interpolation for the modal logic K, each using a different set of techniques (model-theoretic, proof-theoretic, syntactic, automata-theoretic, using quasi-models, and algebraic). We compare the pros and cons of each proof technique.
Paper Structure (2 sections, 2 theorems, 5 equations, 1 figure, 2 tables)

This paper contains 2 sections, 2 theorems, 5 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Basic Definitions

Key Result

Theorem 1

Every valid modal implication $\models\varphi\to\psi$ has a Craig interpolant, that is, a modal formula $\vartheta$ such that the following hold:

Figures (1)

  • Figure 1: Pointed Kripke models (over the empty propositional signature) that are modally indistinguishable but not bisimilar. The first has branches of all finite lengths. The second has, in addition, an infinite branch.

Theorems & Definitions (3)

  • Theorem 1: Craig Interpolation for the Modal Logic $\mathsf{K}$
  • Example 2
  • Theorem 3