Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lyndon interpolation property for extensions of $\mathbf{S4}$ and intermediate propositional logics

Taishi Kurahashi

TL;DR

The paper provides a comprehensive study of Lyndon-type interpolation properties for extensions of $oldsymbol{S4}$ and for intermediate logics. It develops a general ULIP-based method, showing that if a modal logic is sound and complete w.r.t. a class of Kripke frames with $n$-IP, then ULIP holds, enabling systematic verification across many logics; it classifies the LIP status among 18 finite-height $oldsymbol{S4}$-extensions with CIP. For intermediate logics, it proves that CIP, LIP, and ULIP are equivalent by employing Gödel translation and modal companions, delivering new results such as LIP for $oldsymbol{GV}$ (and hence $oldsymbol{LV}$) and ULIP for several intermediate logics, including $oldsymbol{Int}$ and $oldsymbol{KC}$ via Grz-derived methods. It also demonstrates failures of LIP in certain logics and delineates a clear boundary between CIP and LIP in the intermediate realm. Overall, the work deepens the connection between interpolation properties, model-theoretic frame conditions, and translations between modal and intermediate logics, with implications for both theory and potential automated reasoning tools.

Abstract

We study the Lyndon interpolation property (LIP) and the uniform Lyndon interpolation property (ULIP) for extensions of $\mathbf{S4}$ and intermediate propositional logics. We prove that among the 18 consistent normal modal logics of finite height extending $\mathbf{S4}$ known to have CIP, 11 logics have LIP and 7 logics do not. We also prove that for intermediate propositional logics, the Craig interpolation property, LIP, and ULIP are equivalent.

Lyndon interpolation property for extensions of $\mathbf{S4}$ and intermediate propositional logics

TL;DR

The paper provides a comprehensive study of Lyndon-type interpolation properties for extensions of and for intermediate logics. It develops a general ULIP-based method, showing that if a modal logic is sound and complete w.r.t. a class of Kripke frames with -IP, then ULIP holds, enabling systematic verification across many logics; it classifies the LIP status among 18 finite-height -extensions with CIP. For intermediate logics, it proves that CIP, LIP, and ULIP are equivalent by employing Gödel translation and modal companions, delivering new results such as LIP for (and hence ) and ULIP for several intermediate logics, including and via Grz-derived methods. It also demonstrates failures of LIP in certain logics and delineates a clear boundary between CIP and LIP in the intermediate realm. Overall, the work deepens the connection between interpolation properties, model-theoretic frame conditions, and translations between modal and intermediate logics, with implications for both theory and potential automated reasoning tools.

Abstract

We study the Lyndon interpolation property (LIP) and the uniform Lyndon interpolation property (ULIP) for extensions of and intermediate propositional logics. We prove that among the 18 consistent normal modal logics of finite height extending known to have CIP, 11 logics have LIP and 7 logics do not. We also prove that for intermediate propositional logics, the Craig interpolation property, LIP, and ULIP are equivalent.
Paper Structure (21 sections, 31 theorems, 40 equations, 29 figures, 3 tables)

This paper contains 21 sections, 31 theorems, 40 equations, 29 figures, 3 tables.

Table of Contents

  1. Introduction
  2. ULIP for classical propositional logic
  3. A sufficient condition for ULIP in modal logic
  4. Some lemmas on matching between clusters
  5. Modal companions of $\mathbf{Cl}$
  6. $\mathbf{Triv}$
  7. $\mathbf{S5}$
  8. Modal companions of $\mathbf{LS}$
  9. $\mathbf{GW.2}$
  10. $\Gamma(\mathbf{LS}, 2, 1)$
  11. $\mathbf{S4.4}$
  12. Modal companions of $\mathbf{LV}$
  13. $\mathbf{GV}$
  14. $\Gamma(\mathbf{LV}, 2, 1)$
  15. $\Gamma(\mathbf{LV}, \omega, 1)$
  16. ...and 6 more sections

Key Result

Lemma 2.2

Let $P^+$ and $P^-$ be any finite sets of propositional variables and $\mathsf{V}_0$ and $\mathsf{V}_1$ be any truth assignments. Then, the following are equivalent:

Figures (29)

  • Figure 1: The model $M_i = (W_i, R_i, \Vdash_i)$
  • Figure 2: A frame of $\mathbf{S5}$
  • Figure 3: The frame of $\mathbf{GW.2}$
  • Figure 4: The frame $(W^*, R^*)$
  • Figure 5: The frame of $\Gamma(\mathbf{LS}, 2, 1)$
  • ...and 24 more figures

Theorems & Definitions (64)

  • Definition 2.1
  • Lemma 2.2: Cf. Kurahashi20
  • Theorem 2.3
  • proof
  • Theorem 2.4
  • proof
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Lemma 3.4: Cf. Kurahashi20
  • ...and 54 more