1 Introduction
The Craig Interpolation Theorem was first proved by Craig [Reference Craig2] for classical first-order predicate logic, and has been studied for many logics. Let
$v(\varphi )$
denote the set of all propositional variables contained in a propositional formula
$\varphi $
. We say that a propositional logic L has the Craig interpolation property (CIP) iff for any formulas
$\varphi $
and
$\psi $
, if
$L \vdash \varphi \to \psi $
, then there exists a formula
$\rho $
such that
$v(\rho ) \subseteq v(\varphi ) \cap v(\psi )$
,
$L \vdash \varphi \to \rho $
, and
$L \vdash \rho \to \psi $
. CIP has been extensively investigated in modal and intermediate propositional logics. In particular, Maksimova [Reference Maksimova12] proved that there are exactly seven intermediate propositional logics having CIP. They are classical propositional logic
$\mathbf {Cl}$
,
$\mathbf {LS}$
,
$\mathbf {LV}$
,
$\mathbf {LP}_2$
, the Gödel–Dummett logic
$\mathbf {LC}$
, the Jankov logic
$\mathbf {KC}$
, and intuitionistic propositional logic
$\mathbf {Int}$
Footnote
1
. Moreover, Maksimova proved that there are at most 36 consistent normal extensions of
$\mathbf {S4}$
having CIP, and that at least 30 consistent logics among them have CIP (see [Reference Gabbay and Maksimova5, Reference Maksimova16]). In particular, there are exactly 18 consistent normal modal logics of finite height extending
$\mathbf {S4}$
and having CIP (see Table 1
Footnote
2
).
CIP and LIP for consistent normal modal logics of finite height extending
$\mathbf {S4}$
.
Lyndon [Reference Lyndon11] proved that classical first-order predicate logic enjoys a stronger interpolation property. Let
$v^{+}(\varphi )$
(resp.
$v^{-}(\varphi )$
) be the set of all propositional variables occurring in a propositional formula
$\varphi $
positively (resp. negatively). We say that a propositional logic L has the Lyndon interpolation property (LIP) iff for any formulas
$\varphi $
and
$\psi $
, if
$L \vdash \varphi \to \psi $
, then there exists a formula
$\rho $
such that
$v^{\circ }(\rho ) \subseteq v^{\circ }(\varphi ) \cap v^{\circ }(\psi )$
for
$\circ \in \{+, -\}$
,
$L \vdash \varphi \to \rho $
, and
$L \vdash \rho \to \psi $
. LIP for extensions of
$\mathbf {S4}$
has been studied by Maksimova [Reference Maksimova15, Reference Maksimova17], Fitting [Reference Fitting3], and Kuznets [Reference Kuznets7, Reference Kuznets8]. It is also verifiable that Shimura’s proofs of CIP for some extensions of
$\mathbf {S4}$
also work with respect to LIP [Reference Shimura22]Footnote
3
. Among the 30 logics known to have CIP, it has been proved that 12 logics actually have LIPFootnote
4
and 4 logics do not. LIP for intermediate propositional logics has been studied by Maksimova [Reference Maksimova15, Reference Maksimova17] and Kuznets and Lellmann [Reference Kuznets and Lellmann9, Reference Kuznets and Lellmann10]. Among these seven logics known to have CIP, LIP for the six logics other than
$\mathbf {LV}$
has already been provedFootnote
5
and the problem of LIP for
$\mathbf {LV}$
was open (see Maksimova [Reference Maksimova17] and Table 2).
Interpolation properties for intermediate propositional logics.
In the present article, we focus on the 18 extensions of
$\mathbf {S4}$
of finite height listed in Table 1. The first goal of this article is to provide a complete description concerning LIP for these logics. We prove that five of them have LIP and three do not. Then, we conclude that among these 18 logics, 11 logics have LIP and 7 logics do not (see Table 1). Our strategy for proving LIP for these logics is to prove a stronger property, the uniform LIP (ULIP). We say that a propositional logic L has the ULIP iff for any formula
$\varphi $
and any finite sets
$P^{+}, P^{-}$
of propositional variables, there exists a formula
$\theta $
satisfying the following three conditions:
-
1.
$L \vdash \varphi \to \theta $
, -
2.
$v^{\circ }(\theta ) \subseteq v^{\circ }(\varphi ) \setminus P^{\circ }$
for
$\circ \in \{+, -\}$
, -
3. for any formula
$\psi $
with
$L \vdash \varphi \to \psi $
and
$v^{\circ }(\psi ) \cap P^{\circ } = \emptyset $
for
$\circ \in \{+, -\}$
, we have
$L \vdash \theta \to \psi $
.
Here,
$\theta $
is called a uniform Lyndon interpolant of
$(\varphi , P^{+}, P^{-})$
in L. ULIP is a simultaneous strengthening of LIP and the uniform interpolation property (UIP), and the notion ULIP was introduced in [Reference Kurahashi6]. In that paper, by extending the semantic technique for proving UIP developed by Visser [Reference Visser23], it was proved that the modal logics, such as
$\mathbf {K}$
,
$\mathbf {KT}$
,
$\mathbf {KB}$
,
$\mathbf {GL}$
, and
$\mathbf {Grz,}$
have ULIP. We say that a logic L is locally tabular iff for any finite set P of propositional variables, there are finitely many formulas built from variables in P up to L-provable equivalence. It is known that LIP and ULIP are equivalent for every locally tabular logic (cf. [Reference Kurahashi6]). Since the logics in Table 1 are all locally tabular, to prove LIP for these logics, we will adopt the method of proving stronger ULIP.
We also discuss LIP and ULIP for intermediate propositional logics. The problem of LIP for the modal logic
$\mathbf {GV}$
was stated to be open in Maksimova [Reference Maksimova17], but in this article, by proving LIP for
$\mathbf {GV}$
, we immediately obtain LIP for the intermediate logic
$\mathbf {LV}$
. From this, we conclude that CIP and LIP are equivalent for intermediate propositional logics. Since the logics
$\mathbf {Cl}$
,
$\mathbf {LS}$
,
$\mathbf {LV}$
,
$\mathbf {LP}_2$
, and
$\mathbf {LC}$
are known to be locally tabular (cf. [Reference Chagrov and Zakharyaschev1, p. 428]), they are shown to enjoy ULIP. ULIP for
$\mathbf {Int}$
follows immediately from ULIP for
$\mathbf {Grz}$
. In the present article, we prove ULIP for
$\mathbf {Grz.2}$
, which implies that
$\mathbf {KC}$
also has ULIP. From these investigations, we also conclude that CIP and ULIP are equivalent for intermediate propositional logics (see Table 2).
This article is organized as follows. In Section 2, we develop the basis of our method of proving ULIP for several logics. We present a simple proof of ULIP for classical propositional logic
$\mathbf {Cl}$
using the basis of our method. Section 3 is devoted to developing a sufficient condition for modal logics to have ULIP. More precisely, we introduce the notion that a class of Kripke models enjoys n-IP and prove that a logic L has ULIP if L is sound and complete with respect to a class of models enjoying n-IP for some natural number n. In Section 4, we prepare some lemmas on matching between clusters of Kripke models, which are used in our proofs of ULIP for several logics. In Sections 5–8, we use our method to prove ULIP for 11 logics in Table 1, including six logics for which LIP has already been proved. In Section 9, we discuss the failure of LIP for some logics. At last, in Section 10, we discuss LIP and ULIP for intermediate propositional logics.
2 ULIP for classical propositional logic
In this section, we develop the basis of our method for proving ULIP of several modal logics and we apply this basis to prove ULIP of classical propositional logic. For this section only, we assume that formulas mean formulas of classical propositional logic. The language of classical propositional logic consists of propositional variables, logical constant
$\bot $
, and logical connectives
$\land , \lor , \neg $
, and
$\to $
.
For each formula
$\varphi $
, we define the sets
$v^{+}(\varphi )$
and
$v^{-}(\varphi )$
recursively as follows:
-
•
$v^{+}(p) = \{p\}$
and
$v^{-}(p) = \emptyset $
for every propositional variable p, -
•
$v^{\circ }(\bot ) = \emptyset $
for
$\circ \in \{+, -\}$
, -
•
$v^{\circ }(\varphi \ast \psi ) = v^{\circ }(\varphi ) \cup v^{\circ }(\psi )$
for
$\circ \in \{+, -\}$
and
$\ast \in \{\land , \lor \}$
, -
•
$v^{+}(\neg \varphi ) = v^{-}(\varphi )$
and
$v^{-}(\neg \varphi ) = v^{+}(\varphi )$
, -
•
$v^{+} (\varphi \to \psi ) = v^{-}(\varphi ) \cup v^{+}(\psi )$
and
$v^{-}(\varphi \to \psi ) = v^{+}(\varphi ) \cup v^{-}(\psi )$
.
Also, let
$v(\varphi ) : = v^{+}(\varphi ) \cup v^{-}(\varphi )$
.
Definition 2.1. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables.
-
1. A formula
$\varphi $
is said to be a
$(P^{+}, P^{-})$
-formula iff
$v^{\circ }(\varphi ) \subseteq P^{\circ }$
for
$\circ \in \{+, -\}$
. -
2. Let
$\Phi ^{(P^{+}, P^{-})}_{0}$
denote a fixed finite set of
$(P^{+}, P^{-})$
-formulas such that for any
$(P^{+}, P^{-})$
-formula
$\varphi $
, there exists a
$\psi \in \Phi ^{(P^{+}, P^{-})}_{0}$
such that
$\mathbf {Cl} \vdash \varphi \leftrightarrow \psi $
. The existence of such a finite set
$\Phi ^{(P^{+}, P^{-})}_{0}$
is easily proved. Here, the subscript
$0$
indicates box-free. -
3. For every truth assignments
$\mathsf {V}_0$
and
$\mathsf {V}_1$
of formulas, we write iff for any
$$\begin{align*}\mathsf{V}_0 \xrightarrow[0]{(P^{+}, P^{-})} \mathsf{V}_1 \end{align*}$$
$(P^{+}, P^{-})$
-formula
$\varphi $
, if
$\mathsf {V}_0(\varphi ) = 1$
, then
$\mathsf {V}_1(\varphi ) = 1$
.
-
4. For every truth assignment
$\mathsf {V}$
, let
$\chi ^{(P^{+}, P^{-})}_{0}[\mathsf {V}]$
denote the
$(P^{+}, P^{-})$
-formula
$$\begin{align*}\bigwedge \{\varphi \in \Phi^{(P^{+}, P^{-})}_{0} \mid \mathsf{V}(\varphi) = 1\}. \end{align*}$$
The following lemma is easily verified, and therefore we use the lemma freely without referring to it.
Lemma 2.2 (Cf. [Reference Kurahashi6, Proposition 6]).
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:
-
1.
$\mathsf {V}_0 \xrightarrow [0]{(P^{+}, P^{-})} \mathsf {V}_1$
. -
2.
$\mathsf {V}_1 \xrightarrow [0]{(P^{-}, P^{+})} \mathsf {V}_0$
. -
3.
$\mathsf {V}_1 \big (\chi ^{(P^{+}, P^{-})}_{0}[\mathsf {V}_0] \big ) = 1$
. -
4.
$\mathsf {V}_0 \big (\chi ^{(P^{-}, P^{+})}_{0}[\mathsf {V}_1] \big ) = 1$
.
We prove the following theorem, which is an adaptation of a result proved in [Reference Kurahashi6, Proof of Lemma 1] to the framework of this section.
Theorem 2.3. Let
$P_0^{+}, P_1^{+}, P_2^{+}, P_0^{-}, P_1^{-}$
, and
$P_2^{-}$
be finite sets of propositional variables such that
$P_0^{\circ }$
,
$P_1^{\circ }$
, and
$P_2^{\circ }$
are pairwise disjoint for
$\circ \in \{+, -\}$
. Let
$\mathsf {V}_0$
and
$\mathsf {V}_1$
be truth assignments. If
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
, then there exists a truth assignment
$\mathsf {V}^{*}$
such that
$\mathsf {V}_0 \xrightarrow [0]{(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})} \mathsf {V}^{*}$
and
$\mathsf {V}^{*} \xrightarrow [0]{(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})} \mathsf {V}_1$
.
Proof. Let
$\mathsf {V}_0$
and
$\mathsf {V}_1$
be any truth assignments such that
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
. We define a truth assignment
$\mathsf {V}^{*}$
by referring to Table 3. For each propositional variable p, let
$\mathsf {V}^{*}(p) = 1$
iff p meets one of the conditions stated in the 16 rows of the table. For example, the fifth row in the table states the condition that
$p \in P_1^{+} \cap P_0^{-}$
,
$p \notin P_0^{+} \cup P_2^{+} \cup P_1^{-} \cup P_2^{-}$
, and
$\mathsf {V}_0(p) = 1$
.
The definition of
$\mathsf {V}^{*}$
.
For the proof of
$\mathsf {V}_0 \xrightarrow [0]{(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})} \mathsf {V}^{*}$
, we simultaneously prove the following two conditions by induction on the construction of
$\varphi $
:
-
1. If
$\varphi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$\mathsf {V}_0(\varphi ) = 1$
, then
$\mathsf {V}^{*}(\varphi ) = 1$
. -
2. If
$\varphi $
is a
$(P_0^{-} \cup P_1^{-}, P_0^{+} \cup P_1^{+})$
-formula and
$\mathsf {V}_0(\varphi ) = 0$
, then
$\mathsf {V}^{*}(\varphi ) = 0$
.
The case of
$\bot $
trivially holds. We prove the case of a propositional variable p.
1. Suppose
$p \in P_0^{+} \cup P_1^{+}$
and
$\mathsf {V}_0(p) = 1$
. If
$p \in P_0^{+}$
, then p meets one of 1, 2, 3, and 4, and hence
$\mathsf {V}^{*}(p) = 1$
. If
$p \in P_1^{+}$
, then we have
$\mathsf {V}_1(p) = 1$
because
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
. Then, p meets one of 5, 6, 7, and 8, and thus we obtain
$\mathsf {V}^{*}(p) = 1$
.
2. Suppose
$p \in P_0^{-} \cup P_1^{-}$
and
$\mathsf {V}^{*}(p) = 1$
. In this case, p meets one of 1, 2, 5, 6, 9, 10, 13, and 14. If p meets one of 1, 2, 5, 9, and 13, then we have
$\mathsf {V}_0(p) = 1$
. If p meets one of 6, 10, and 14, then
$p \in P_1^{-}$
and
$\mathsf {V}_1(p) = 1$
. Since
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
, we obtain
$\mathsf {V}_0(p) = 1$
.
The cases of the Boolean combinations are easily proved by using the induction hypothesis.
For the proof of
$\mathsf {V}^{*} \xrightarrow [0]{(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})} \mathsf {V}_1$
, we simultaneously prove the following two conditions by induction on the construction of
$\varphi $
:
-
1. If
$\varphi $
is a
$(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})$
-formula and
$\mathsf {V}^{*}(\varphi ) = 1$
, then
$\mathsf {V}_1(\varphi ) = 1$
. -
2. If
$\varphi $
is a
$(P_1^{-} \cup P_2^{-}, P_1^{+} \cup P_2^{+})$
-formula and
$\mathsf {V}^{*}(\varphi ) = 0$
, then
$\mathsf {V}_1(\varphi ) = 0$
.
We give only the proof of the case that
$\varphi $
is a propositional variable p.
1. Suppose
$p \in P_1^{+} \cup P_2^{+}$
and
$\mathsf {V}^{*}(p) = 1$
. Then, p meets one of 5, 6, 7, 8, 9, 10, 11, and 12. If p meets one of 6, 7, 9, 10, 11, and 12, then
$\mathsf {V}_1(p)=1$
. If p meets one of 5 and 8, then
$p \in P_1^{+}$
and
$\mathsf {V}_0(p) = 1$
. Since
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
, we obtain
$\mathsf {V}_1(p) = 1$
.
2. Suppose
$p \in P_1^{-} \cup P_2^{-}$
and
$\mathsf {V}_1(p) = 1$
. If
$p \notin P_0^{+} \cap P_1^{-}$
, then p meets one of 3, 6, 7, 10, 11, 14, and 15, and hence
$\mathsf {V}^{*}(p) = 1$
. If
$p \in P_0^{+} \cap P_1^{-}$
, then we have
$\mathsf {V}_0(p) = 1$
because
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
. Then p meets 2, and thus we get
$\mathsf {V}^{*}(p) = 1$
.
By using Theorem 2.3, we can easily prove ULIP for classical propositional logic
$\mathbf {Cl}$
.
Theorem 2.4. The logic
$\mathbf {Cl}$
has ULIP.
Proof. Let
$\varphi $
be any formula and
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables. Let
$P_0^{\circ } : = P^{\circ }$
and
$P_1^{\circ } : = v^{\circ }(\varphi ) \setminus P^{\circ }$
for
$\circ \in \{+, -\}$
. Let
$\theta $
be the
$(P_1^{+}, P_1^{-})$
-formula
$$\begin{align*}\bigwedge \{\psi \in \Phi_0^{(P_1^{+}, P_1^{-})} \mid \mathbf{Cl} \vdash \varphi \to \psi\}. \end{align*}$$
We prove that
$\theta $
is a uniform Lyndon interpolant of
$(\varphi , P^{+}, P^{-})$
in
$\mathbf {Cl}$
. The conditions
$\mathbf {Cl} \vdash \varphi \to \theta $
and
$v^{\circ }(\theta ) \subseteq v^{\circ }(\varphi ) \setminus P^{\circ }$
for
$\circ \in \{+, -\}$
are easily verified. Let
$\rho $
be any formula such that
$\mathbf {Cl} \nvdash \theta \to \rho $
and
$v^{\circ }(\rho ) \cap P^{\circ } = \emptyset $
for
$\circ \in \{+, -\}$
. It suffices to prove
$\mathbf {Cl} \nvdash \varphi \to \rho $
. Let
$P_2^{\circ } : = v^{\circ }(\rho ) \setminus v^{\circ }(\varphi )$
for
$\circ \in \{+, -\}$
. Since
$v^{\circ }(\rho ) \cap P^{\circ } = \emptyset $
, we have that
$P_0^{\circ }$
,
$P_1^{\circ }$
, and
$P_2^{\circ }$
are pairwise disjoint for
$\circ \in \{+, -\}$
.
Since
$\mathbf {Cl} \nvdash \theta \to \rho $
, there exists a truth assignment
$\mathsf {V}_1$
such that
$\mathsf {V}_1(\theta ) = 1$
and
$\mathsf {V}_1(\rho ) = 0$
. Since
$\mathsf {V}_1\big (\chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1] \big ) = 1$
, we have
$\mathsf {V}_1\big (\theta \to \neg \chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1] \big ) = 0$
. Thus,
$\mathbf {Cl} \nvdash \theta \to \neg \chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1]$
. Since
$\neg \chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1]$
is a
$(P_1^{+}, P_1^{-})$
-formula, by the definition of
$\theta $
, we obtain
$\mathbf {Cl} \nvdash \varphi \to \neg \chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1]$
. Hence, there exists a truth assignment
$\mathsf {V}_0$
such that
$\mathsf {V}_0(\varphi ) = 1$
and
$\mathsf {V}_0 \big (\chi _0^{(P_1^{-}, P_1^{+})}[\mathsf {V}_1] \big ) = 1$
. By Lemma 2.2, we get
$\mathsf {V}_0 \xrightarrow [0]{(P_1^{+}, P_1^{-})} \mathsf {V}_1$
.
It follows from Theorem 2.3 that there exists a truth assignment
$\mathsf {V}^{*}$
such that
$\mathsf {V}_0 \xrightarrow [0]{(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})} \mathsf {V}^{*}$
and
$\mathsf {V}^{*} \xrightarrow [0]{(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})} \mathsf {V}_1$
. Since
$\varphi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$\rho $
is a
$(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})$
-formula, we obtain
$\mathsf {V}^{*}(\varphi ) = 1$
and
$\mathsf {V}^{*}(\rho ) = 0$
. Therefore,
$\mathsf {V}^{*}(\varphi \to \rho ) = 0$
. We conclude
$\mathbf {Cl} \nvdash \varphi \to \rho $
.
3 A sufficient condition for ULIP in modal logic
In this section, we present a sufficient condition for modal logics to have ULIP. For this purpose, we extend Definition 2.1 to the framework of modal propositional logic. From now on, we assume that formulas mean formulas of modal propositional logic. The language of modal propositional logic is obtained from that of classical propositional logic by adding the unary modal operator
$\Box $
. Let
$\Diamond \varphi $
be the abbreviation for
$\neg \Box \neg \varphi $
. The notions of positive variables and negative variables of formulas are extended to the language of modal propositional logic with the following clause:
-
•
$v^{\circ }(\Box \varphi ) = v^{\circ }(\varphi )$
for
$\circ \in \{+, -\}$
.
Definition 3.1. For each formula
$\varphi $
, let
$d(\varphi )$
denote the maximum number of nested occurrences of
$\Box $
in
$\varphi $
. More precisely,
$d(\varphi )$
is defined recursively as follows:
-
•
$d(p) = d(\bot ) = 0$
, where p is a propositional variable p, -
•
$d(\neg \varphi ) = d(\varphi )$
, -
•
$d(\varphi \circ \psi ) = \max \{d(\varphi ), d(\psi )\}$
for
$\circ \in \{\land , \lor , \to \}$
, -
•
$d(\Box \varphi ) = d(\varphi ) + 1$
.
Definition 3.2.
-
• A pair
$(W, R)$
is called an (
$\mathbf {S4}$
-)Kripke frame iff W is a non-empty set and R is a reflexive and transitive binary relation on W. -
• A triple
$(W, R, \Vdash )$
is called a Kripke model iff
$(W, R)$
is a Kripke frame and
$\Vdash $
is a satisfaction relation between elements of W and formulas fulfilling the usual conditions for each propositional connective and the following condition:
$$\begin{align*}(M, x) \Vdash \Box \varphi \iff \forall y (x R y \Rightarrow (M, y) \Vdash \varphi). \end{align*}$$
Definition 3.3. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and n be any natural number.
-
1. A formula
$\varphi $
is said to be a
$(P^{+}, P^{-})$
-formula iff
$v^{\circ }(\varphi ) \subseteq P^{\circ }$
for
$\circ \in \{+, -\}$
. -
2. Let
$\Phi ^{(P^{+}, P^{-})}_{n}$
denote a fixed finite set of
$(P^{+}, P^{-})$
-formulas
$\varphi $
with
$d(\varphi ) \leq n$
satisfying that for any
$(P^{+}, P^{-})$
-formula
$\psi $
with
$d(\psi ) \leq n$
, there exists a
$\rho \in \Phi ^{(P^{+}, P^{-})}_{n}$
such that
$\mathbf {K} \vdash \psi \leftrightarrow \rho $
. The existence of such a finite set
$\Phi ^{(P^{+}, P^{-})}_{n}$
is proved by induction on n. -
3. For Kripke models
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
and elements
$w_0 \in W_0$
and
$w_1 \in W_1$
, we write iff for any
$$\begin{align*}(M_0, w_0) \xrightarrow[n]{(P^{+}, P^{-})} (M_1, w_1) \end{align*}$$
$(P^{+}, P^{-})$
-formula
$\varphi $
with
$d(\varphi ) \leq n$
, if
$(M_0, w_0) \Vdash _0 \varphi $
, then
$(M_1, w_1) \Vdash _1 \varphi $
.
-
4. For every Kripke model
$M = (W, R, \Vdash )$
and element
$w \in W$
, let
$\chi ^{(P^{+}, P^{-})}_{n}[M, w]$
denote the
$(P^{+}, P^{-})$
-formula
$$\begin{align*}\bigwedge \{\varphi \in \Phi^{(P^{+}, P^{-})}_{n} \mid (M, w) \Vdash \varphi\}. \end{align*}$$
Lemma 3.4 (Cf. [Reference Kurahashi6, Proposition 6]).
Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables,
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models,
$w_0 \in W_0$
and
$w_1 \in W_1$
, and n be any natural number. Then, the following are equivalent:
-
1.
$(M_0, w_0) \xrightarrow [n]{(P^{+}, P^{-})} (M_1, w_1)$
. -
2.
$(M_1, w_1) \xrightarrow [n]{(P^{-}, P^{+})} (M_0, w_0)$
. -
3.
$(M_1, w_1) \Vdash _1 \chi ^{(P^{+}, P^{-})}_{n}[M_0, w_0]$
. -
4.
$(M_0, w_0) \Vdash _0 \chi ^{(P^{-}, P^{+})}_{n}[M_1, w_1]$
.
Definition 3.5 (p-morphisms).
Let
$F = (W, R)$
and
$F' = (W', R')$
be Kripke frames. A mapping
$f: W \to W'$
is called a p-morphism iff the following conditions hold:
-
• For any
$x, y \in W$
, if
$x R y$
, then
$f(x) R' f(y)$
. -
• For any
$x \in W$
and
$w \in W'$
, if
$f(x) R' w$
, then there exists
$z \in W$
such that
$x R z$
and
$f(z) = w$
.
We introduce a key notion in this article.
Definition 3.6 (n-IP).
Let
$\mathcal {C}$
be a class of Kripke models and n be a natural number. We say that
$\mathcal {C}$
enjoys n-IP iff for any finite sets
$P^{+}$
and
$P^{-}$
of propositional variables, any Kripke models
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
in
$\mathcal {C}$
, and any elements
$w_0 \in W_0$
and
$w_1 \in W_1$
, if
$(M_0, w_0) \xrightarrow [n]{(P^{+}, P^{-})} (M_1, w_1)$
, then there exist a Kripke frame
$\mathcal {F}^{*} = (W^{*}, R^{*})$
, an element
$w^{*} \in W^{*}$
, and two p-morphisms
$f_0: W^{*} \to W_0$
and
$f_1: W^{*} \to W_1$
satisfying the following three conditions:
-
1. all Kripke models based on
$\mathcal {F}^{*}$
are in
$\mathcal {C}$
, -
2.
$f_0(w^{*}) = w_0$
and
$f_1(w^{*}) = w_1$
, -
3. for any
$x^{*} \in W^{*}$
, we have
$(M_0, f_0(x^{*})) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, f_1(x^{*}))$
.
We are ready to prove our main instrument in the present article. The following theorem is an adaptation of [Reference Kurahashi6, Theorem 2] for the purpose of this article, and it also extends the proof of Theorem 2.4 to modal logic. We note that our sufficient condition for ULIP resembles to Marx’s condition on bisimulation products for CIP [Reference Marx18].
Theorem 3.7. If a modal logic L is sound and complete with respect to some class
$\mathcal {C}$
of Kripke models enjoying n-IP for some natural number n, then L has ULIP.
Proof. Suppose that a class
$\mathcal {C}$
of Kripke models enjoys n-IP and that L is sound and complete with respect to
$\mathcal {C}$
. Let
$\varphi $
be any formula and
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables. Let
$P_0^{\circ } : = P^{\circ }$
and
$P_1^{\circ } : = v^{\circ }(\varphi ) \setminus P^{\circ }$
for
$\circ \in \{+, -\}$
. Let
$\theta $
be the
$(P_1^{+}, P_1^{-})$
-formula
$$\begin{align*}\bigwedge \{\psi \in \Phi_n^{(P_1^{+}, P_1^{-})} \mid L \vdash \varphi \to \psi\}. \end{align*}$$
We prove that
$\theta $
is a uniform Lyndon interpolant of
$(\varphi , P^{+}, P^{-})$
in L. The conditions
$L \vdash \varphi \to \theta $
and
$v^{\circ }(\theta ) \subseteq v^{\circ }(\varphi ) \setminus P^{\circ }$
for
$\circ \in \{+, -\}$
are easily verified. Let
$\rho $
be any formula such that
$L \nvdash \theta \to \rho $
and
$v^{\circ }(\rho ) \cap P^{\circ } = \emptyset $
for
$\circ \in \{+, -\}$
. We prove
$L \nvdash \varphi \to \rho $
. Let
$P_2^{\circ } : = v^{\circ }(\rho ) \setminus v^{\circ }(\varphi )$
for
$\circ \in \{+, -\}$
. Since
$v^{\circ }(\rho ) \cap P^{\circ } = \emptyset $
, we have that
$P_0^{\circ }$
,
$P_1^{\circ }$
, and
$P_2^{\circ }$
are pairwise disjoint for
$\circ \in \{+, -\}$
.
Since
$L \nvdash \theta \to \rho $
, by the completeness, there exists a Kripke model
$M_1 = (W_1, R_1, \Vdash _1)$
in
$\mathcal {C}$
and
$w_1 \in W_1$
such that
$(M_1, w_1) \Vdash _1 \theta $
and
$(M_1, w_1) \nVdash _1 \rho $
. Since
$(M_1, w_1) \Vdash _1 \chi _n^{(P_1^{-}, P_1^{+})}[M_1, w_1]$
, we have
$$\begin{align*}(M_1, w_1) \nVdash_1 \theta \to \neg \chi_n^{(P_1^{-}, P_1^{+})}[M_1, w_1]. \end{align*}$$
By the soundness,
$L \nvdash \theta \to \neg \chi _n^{(P_1^{-}, P_1^{+})}[M_1, w_1]$
. Since
$\neg \chi _n^{(P_1^{-}, P_1^{+})}[M_1, w_1]$
is a
$(P_1^{+}, P_1^{-})$
-formula, by the definition of
$\theta $
, we obtain
$L \nvdash \varphi \to \neg \chi _n^{(P_1^{-}, P_1^{+})}[M_1, w_1]$
. By the completeness, there exists a Kripke model
$M_0 = (W_0, R_0, \Vdash _0)$
in
$\mathcal {C}$
and
$w_0 \in W_0$
such that
$(M_0, w_0) \Vdash _0 \varphi $
and
$(M_0, w_0) \Vdash _0 \chi _n^{(P_1^{-}, P_1^{+})}[M_1, w_1]$
. By Lemma 3.4, we get
$(M_0, w_0) \xrightarrow [n]{(P_1^{+}, P_1^{-})} (M_1, w_1)$
.
Since
$\mathcal {C}$
enjoys n-IP, there exists a Kripke frame
$\mathcal {F}^{*} = (W^{*}, R^{*})$
, an element
$w^{*} \in W^{*}$
, and two p-morphisms
$f_0: W^{*} \to W_0$
and
$f_1: W^{*} \to W_1$
satisfying the following three conditions:
-
1. all Kripke models based on
$\mathcal {F}^{*}$
are in
$\mathcal {C}$
, -
2.
$f_0(w^{*}) = w_0$
and
$f_1(w^{*}) = w_1$
, -
3. for any
$x^{*} \in W^{*}$
, we have
$(M_0, f_0(x^{*})) \xrightarrow [0]{(P_1^{+}, P_1^{-})} (M_1, f_1(x^{*}))$
.
We define a Kripke model
$M^{*} = (W^{*}, R^{*}, \Vdash ^{*})$
as follows: Let
$x^{*} \in W^{*}$
. Since
$(M_0, f_0(x^{*})) \xrightarrow [0]{(P_1^{+}, P_1^{-})} (M_1, f_1(x^{*}))$
, it follows from Theorem 2.3 that there exists a truth assignment
$\mathsf {V}^{*}$
such that for any formula
$\psi $
with
$d(\psi ) = 0$
, the following two conditions hold:
-
1. If
$\psi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$(M_0, f_0(x^{*})) \Vdash _0 \psi $
, then
$\mathsf {V}^{*}(\psi ) = 1$
. -
2. If
$\psi $
is a
$(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})$
-formula and
$\mathsf {V}^{*}(\psi ) = 1$
, then
$(M_1, f_1(x^{*})) \Vdash _1 \psi $
.
Let
$(M^{*}, x^{*}) \Vdash ^{*} p: \iff \mathsf {V}^{*}(p) = 1$
.
By the first condition of n-IP, we have
$M^{*} \in \mathcal {C}$
.
We prove that for any formula
$\psi $
and any
$x^{*} \in W^{*}$
,
-
1. If
$\psi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$(M_0, f_0(x^{*})) \Vdash _0 \psi $
, then
$(M^{*}, x^{*}) \Vdash ^{*} \psi $
. -
2. If
$\psi $
is a
$(P_0^{-} \cup P_1^{-}, P_0^{+} \cup P_1^{+})$
-formula and
$(M_0, f_0(x^{*})) \nVdash _0 \psi $
, then
$(M^{*}, x^{*}) \nVdash ^{*} \psi $
.
We simultaneously prove these two statements by induction on the construction of
$\psi $
. The case that
$d(\psi ) = 0$
directly follows from Theorem 2.3. The cases of propositional connectives easily follow from the induction hypothesis. So we give only the proof of the case that
$\psi $
is of the form
$\Box \xi $
.
1. Suppose that
$\Box \xi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$(M^{*}, x^{*}) \nVdash ^{*} \Box \xi $
. Then, there exists
$y^{*} \in W^{*}$
such that
$x^{*} R^{*} y^{*}$
and
$(M^{*}, y^{*}) \nVdash ^{*} \xi $
. Since
$\xi $
is also a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula, by the induction hypothesis, we have
$(M_0, f_0(y^{*})) \nVdash _0 \xi $
. We have
$f_0(x^{*}) R_0 f_0(y^{*})$
because
$f_0$
is a p-morphism, and so we obtain
$(M_0, f_0(x^{*})) \nVdash _0 \Box \xi $
.
2. Suppose that
$\Box \xi $
is a
$(P_0^{-} \cup P_1^{-}, P_0^{+} \cup P_1^{+})$
-formula and
$(M_0, f_0(x^{*})) \nVdash _0 \Box \xi $
. There exists
$y_0 \in W_0$
such that
$f_0(x^{*}) R_0 y_0$
and
$(M_0, y_0) \nVdash _0 \xi $
. Since
$f_0$
is a p-morphism, there exists
$y^{*} \in W^{*}$
such that
$x^{*} R^{*} y^{*}$
and
$f_0(y^{*}) = y_0$
. Since
$\xi $
is also a
$(P_0^{-} \cup P_1^{-}, P_0^{+} \cup P_1^{+})$
-formula, by the induction hypothesis, we have
$(M^{*}, y^{*}) \nVdash ^{*} \xi $
. Hence,
$(M^{*}, x^{*}) \nVdash ^{*} \Box \xi $
.
In the same way, we can prove that for any formula
$\psi $
and any
$x^{*} \in W^{*}$
,
-
• If
$\psi $
is a
$(P_1^{+}\hspace{-0.5pt} \cup\hspace{-0.5pt} P_2^{+}, P_1^{-}\hspace{-0.5pt} \cup\hspace{-0.5pt} P_2^{-})$
-formula and
$(M^{*}, x^{*})\hspace{-0.5pt} \Vdash\hspace{-0.5pt} ^{*} \psi $
, then
$(M_1, f_1(x^{*}))\hspace{-0.5pt} \Vdash _1 \psi $
.
Since
$\varphi $
is a
$(P_0^{+} \cup P_1^{+}, P_0^{-} \cup P_1^{-})$
-formula and
$(M_0, w_0) = (M_0, f_0(w^{*})) \Vdash _0 \varphi $
, we have
$(M^{*}, w^{*}) \Vdash ^{*} \varphi $
. Also, since
$\rho $
is a
$(P_1^{+} \cup P_2^{+}, P_1^{-} \cup P_2^{-})$
-formula and
$(M_1, w_1) = (M_1, f_1(w^{*})) \nVdash _1 \rho $
, we obtain
$(M^{*}, w^{*}) \nVdash ^{*} \rho $
. Therefore,
$(M^{*}, w^{*}) \nVdash ^{*} \varphi \to \rho $
. By the soundness, we conclude
$L \nvdash \varphi \to \rho $
.
Remark 3.8. In Definition 3.6, if we label each
$x^{*} \in W^{*}$
with the pair
$(f_0(x^{*}), f_1(x^{*}))$
and we roughly write
$x^{*}$
as its label
$(f_0(x^{*}), f_1(x^{*}))$
, then the conditions required for
$\mathcal {F}^{*}$
in the definition can be rewritten as follows without mentioning p-morphisms:
-
1. all Kripke models based on
$\mathcal {F}^{*}$
are in
$\mathcal {C}$
, -
2.
$(w_0, w_1) \in W^{*}$
, -
3. if
$(x_0, x_1) R^{*} (y_0, y_1)$
, then
$x_0 R_0 y_0$
and
$x_1 R_1 y_1$
, -
4. if
$(x_0, x_1) \in W^{*}$
and
$x_0 R_0 y_0$
, then
$(x_0, x_1) R^{*} (y_0, y_1)$
for some
$y_1 \in W_1$
, -
5. if
$(x_0, x_1) \in W^{*}$
and
$x_1 R_1 y_1$
, then
$(x_0, x_1) R^{*} (y_0, y_1)$
for some
$y_0 \in W_0$
, -
6. if
$(x_0, x_1) \in W^{*}$
, then
$(M_0, x_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, x_1)$
.
Since there may be distinct elements of
$W^{*}$
with the same label, the above description is somewhat imprecise. For example, Clause 4 should be precisely as follows:
-
• if
$x^{*} \in W^{*}$
has a label
$(x_0, x_1)$
and
$x_0 R_0 y_0$
, then there exist
$y^{*} \in W^{*}$
and
$y_1 \in W_1$
such that
$y^{*}$
has the label
$(y_0, y_1)$
and
$x^{*} R^{*} y^{*}$
.
Since this rough labeling notation makes it easy to check that a given model meets the required conditions, in the subsequent sections, we will adopt this notation to describe the elements of
$W^{*}$
.
4 Some lemmas on matching between clusters
Before actually proving ULIP for several logics using the method developed in the last section, in this section, we present some lemmas on matching between clusters, which will be used in our proofs of ULIP.
For each Kripke frame
$(W, R)$
, we say that a subset
$I \subseteq W$
is a cluster iff I is an equivalence class of the equivalence relation
$R^s$
defined by
$x R^s y : \iff x R y\ \&\ y R x$
. All the modal logics for which we prove their ULIP in this article are extensions of
$\Gamma (\mathbf {LP}_2, \omega , 1)$
, and so we will basically deal only with finite Kripke models
$(W, R, \Vdash )$
such that W may have or may not have the unique root element x and
$W \setminus \{x\}$
is a disjoint union of finitely many clusters of final elements. For two such models
$M_0 = (W_0, R_0, \Vdash _0)$
,
$M_1 = (W_1, R_1, \Vdash _1)$
and elements
$w_0 \in W_0$
,
$w_1 \in W_1$
, we discuss some conclusions that can be obtained from the assumption that
$(M_0, w_0) \xrightarrow [n]{(P^{+}, P^{-})} (M_1, w_1)$
holds. In this section, for
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$C_i^0, C_i^1, \ldots , C_i^{j_i}$
be all the clusters of final elements of
$M_i$
. The model
$M_i$
is visualized in Figure 1.
The model
$M_i = (W_i, R_i, \Vdash _i)$
.
Definition 4.1. We say that a cluster
$C_0^k$
of
$M_0$
matches a cluster
$C_1^l$
of
$M_1$
iff the following two conditions hold:
-
1. For any
$u_0 \in C_0^k$
, there exists
$u_1 \in C_1^l$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
. -
2. For any
$u_1 \in C_1^l$
, there exists
$u_0 \in C_0^k$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
Lemma 4.2. For
$w_0 \in C_0^k$
and
$w_1 \in C_1^l$
, if
$(M_0, w_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, w_1)$
, then
$C_0^k$
matches
$C_1^l$
.
Proof. Suppose
$(M_0, w_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, w_1)$
. We prove the two clauses of Definition 4.1.
1. For each
$u_0 \in C_0^k$
, since
$(M_0, u_0) \Vdash _0 \chi ^{(P^{+}, P^{-})}_{0}[M_0, u_0]$
, we have
$(M_0, w_0) \Vdash _0 \Diamond \chi ^{(P^{+}, P^{-})}_{0}[M_0, u_0]$
because
$w_0 R_0 u_0$
. Since
$(M_0, w_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, w_1)$
, this formula is also true in
$(M_1, w_1)$
. Thus, we find some
$u_1 \in C_1^l$
such that
$(M_1, u_1) \Vdash _1 \chi ^{(P^{+}, P^{-})}_{0}[M_0, u_0]$
. By Lemma 3.4, we obtain
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
2. For each
$u_1 \in C_1^l$
, we have
$(M_1, w_1) \Vdash _1 \Diamond \chi ^{(P^{-}, P^{+})}_{0}[M_1, u_1]$
. Since
$(M_0, w_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, w_1)$
, this formula is also true in
$(M_0, w_0)$
. Then as above, we find some
$u_0 \in C_0^k$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
Lemma 4.3. For
$w_0 \in C_0^k$
, if
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, x_1)$
, then
$C_0^k$
matches all the clusters
$C_1^l$
of
$M_1$
.
Proof. Suppose
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, x_1)$
. Let
$C_1^l$
be any cluster of
$M_1$
and
$u_1$
be any element of
$C_1^l$
. Since
$(M_1, u_1) \Vdash _1 \chi ^{(P^{-}, P^{+})}_{1}[M_1, u_1]$
, we have
$(M_1, x_1) \Vdash _1 \Diamond \chi ^{(P^{-}, P^{+})}_{1}[M_1, u_1]$
. By the supposition, we have that this formula is also true in
$(M_0, w_0)$
. So, there exists some
$u_0 \in C_0^k$
such that
$(M_0, u_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, u_1)$
. By Lemma 4.2, we have that
$C_0^k$
matches
$C_1^l$
.
Lemma 4.4. If
$(M_0, x_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, x_1)$
, then the following two properties hold:
-
1. For any cluster
$C_0^k$
of
$M_0$
, there exists a cluster
$C_1^l$
of
$M_1$
such that
$C_0^k$
matches
$C_1^l$
. -
2. For any cluster
$C_1^l$
of
$M_1$
, there exists a cluster
$C_0^k$
of
$M_0$
such that
$C_0^k$
matches
$C_1^l$
.
Proof. Suppose
$(M_0, x_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, x_1)$
. We give only a proof of the first clause and the second clause can be proved in the same way.
1. Let
$C_0^k$
be any cluster of
$M_0$
. For any
$v_0 \in C_0^k$
, we have
$$\begin{align*}(M_0, v_0) \Vdash_0 \bigvee_{u_0 \in C_0^k} \chi^{(P^{+}, P^{-})}_{1}[M_0, u_0] \end{align*}$$
and hence
$$\begin{align*}(M_0, v_0) \Vdash_0 \Box \bigvee_{u_0 \in C_0^k} \chi^{(P^{+}, P^{-})}_{1}[M_0, u_0]. \end{align*}$$
Then,
$$\begin{align*}(M_0, x_0) \Vdash_0 \Diamond \Box \bigvee_{u_0 \in C_0^k} \chi^{(P^{+}, P^{-})}_{1}[M_0, u_0]. \end{align*}$$
Since
$(M_0, x_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, x_1)$
, this formula is also true in
$(M_1, x_1)$
. Then, for some
$y_1 \in W_1$
,
$$\begin{align*}(M_1, y_1) \Vdash_1 \Box \bigvee_{u_0 \in C_0^k} \chi^{(P^{+}, P^{-})}_{1}[M_0, u_0]. \end{align*}$$
Hence, we find some cluster
$C_1^l$
of
$M_1$
and an element
$u_1 \in C_1^l$
such that
$$\begin{align*}(M_1, u_1) \Vdash_1 \bigvee_{u_0 \in C_0^k} \chi^{(P^{+}, P^{-})}_{1}[M_0, u_0]. \end{align*}$$
Thus, there exists
$u_0 \in C_0^k$
such that
$(M_0, u_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, u_1)$
. By Lemma 4.2, we conclude that
$C_0^k$
matches
$C_1^l$
.
Lemma 4.5. Let
$A = \{a_0, a_1\}$
and
$B = \{b_0, b_1\}$
be any sets consisting of two elements and let
$R \subseteq A \times B$
be any binary relation. Suppose that R satisfies the following two conditions:
-
1. For any
$a \in A$
, there exists
$b \in B$
such that
$(a, b) \in R$
. -
2. For any
$b \in B$
, there exists
$a \in A$
such that
$(a, b) \in R$
.
Then, there exist
$c, d \in B$
such that
$c \neq d$
,
$(a_0, c) \in R$
, and
$(a_1, d) \in R$
.
Proof. If both
$(a_0, b_0)$
and
$(a_1, b_1)$
are in R, then the statement holds for
$c = b_0$
and
$d = b_1$
. If
$(a_0, b_0) \notin R$
or
$(a_1, b_1) \notin R$
, then by considering the two conditions, we find that both
$(a_0, b_1)$
and
$(a_1, b_0)$
are in R, and so the statement holds for
$c = b_1$
and
$d = b_0$
.
Lemma 4.6. If the clusters
$C_0^k = \{y_0, z_0\}$
and
$C_1^l = \{y_1, z_1\}$
consist of two elements and
$C_0^k$
matches
$C_1^l$
, then there exist
$u_1, v_1 \in C_1^l$
such that
$u_1 \neq v_1$
and
$$\begin{align*}(M_0, y_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1)\ \text{and}\ (M_0, z_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, v_1). \end{align*}$$
Lemma 4.7. Suppose both
$M_0$
and
$M_1$
include exactly two clusters
$C_0^0, C_0^1$
and
$C_1^0, C_1^1$
of final elements, respectively. If
$(M_0, x_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, x_1)$
, then there exist distinct clusters
$D_1^0$
and
$D_1^1$
of
$M_1$
such that
$C_0^k$
matches
$D_1^k$
for
$k \in \{0, 1\}$
.
5 Modal companions of
$\mathbf {Cl}$
In this section, we prove ULIP for the logics
$\mathbf {Triv}$
and
$\mathbf {S5}$
as test cases for our application of Theorem 3.7.
5.1
$\mathbf {Triv}$
Let
$\mathcal {C}_{\mathbf {Triv}}$
be the class of all Kripke models whose frame consists of a single reflexive world. The logic
$\mathbf {Triv}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {Triv}}$
.
Theorem 5.1 (Maksimova [Reference Maksimova15]).
$\mathbf {Triv}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {Triv}}$
enjoys
$0$
-IP. Then, ULIP for
$\mathbf {Triv}$
follows from Theorem 3.7. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (\{w_0\}, R_0, \Vdash _0)$
and
$M_1 = (\{w_1\}, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {Triv}}$
, and suppose
$(M_0, w_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, w_1)$
. Let
$W^{*} : = \{(w_0, w_1)\}$
and
$R^{*} : = (W^{*})^2$
. Then, it is easy to check that
$\mathcal {F}^{*} = (W^{*}, R^{*})$
satisfies the conditions stated in Remark 3.8.
5.2
$\mathbf {S5}$
Let
$\mathcal {C}_{\mathbf {S5}}$
be the class of all Kripke models whose frame forms a finite cluster. Figure 2 visualizes such a frame. In the following, we assume that each diagram represents the Kripke frame of the transitive and reflexive closure of the arrows shown in the diagram. The logic
$\mathbf {S5}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {S5}}$
.
A frame of
$\mathbf {S5}$
.
Theorem 5.2 (Fitting [Reference Fitting3]).
$\mathbf {S5}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {S5}}$
enjoys
$1$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {S5}}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [1]{(P^{+}, P^{-})} (M_1, w_1)$
. Then, both
$W_0$
and
$W_1$
are clusters of
$M_0$
and
$M_1$
, respectively. By Lemma 4.2, we have that
$W_0$
matches
$W_1$
.
Let
$W^{*} := \{(x_0, x_1) \mid (M_0, x_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, x_1)\}$
and
$R^{*} : = (W^{*})^2$
. We check that
$\mathcal {F}^{*} = (W^{*}, R^{*})$
fulfills the conditions stated in Remark 3.8.
-
1. Since
$\mathcal {F}^{*}$
forms a finite cluster, all Kripke models based on
$\mathcal {F}^{*}$
are in
$\mathcal {C}_{\mathbf {S5}}$
. -
2.
$(w_0, w_1) \in W^{*}$
because
$(M_0, w_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, w_1)$
. -
3. If
$(x_0, x_1) R^{*} (y_0, y_1)$
, then
$x_0, y_0 \in W_0$
and
$x_1, y_1 \in W_1$
. Since both
$W_0$
and
$W_1$
form clusters, we obtain
$x_0 R_0 y_0$
and
$x_1 R_1 y_1$
. -
4. Suppose
$(x_0, x_1) \in W^{*}$
and
$x_0 R_0 y_0$
. Since
$W_0$
matches
$W_1$
, we find some
$y_1 \in W_1$
such that
$(M_0, y_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, y_1)$
. Hence
$(y_0, y_1) \in W^{*}$
. Since
$R^{*} = (W^{*})^2$
, we obtain
$(x_0, x_1) R^{*} (y_0, y_1)$
. -
5. Suppose
$(x_0, x_1) \in W^{*}$
and
$x_1 R_1 y_1$
. In the same way as above, we can find some
$y_0 \in W_0$
such that
$(y_0, y_1) \in W^{*}$
. Then,
$(x_0, x_1) R^{*} (y_0, y_1)$
. -
6. If
$(x_0, x_1) \in W^{*}$
, then
$(M_0, x_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, x_1)$
by the definition of
$W^{*}$
.
It follows from Theorem 3.7 that
$\mathbf {S5}$
has ULIP.
6 Modal companions of
$\mathbf {LS}$
In this section, we prove that the three logics
$\mathbf {GW.2} = \Gamma (\mathbf {LS}, 1, 1)$
,
$\Gamma (\mathbf {LS}, 2, 1)$
, and
$\mathbf {S4.4} = \Gamma (\mathbf {LS}, \omega , 1)$
have ULIP. In particular, LIP for
$\Gamma (\mathbf {LS}, 2, 1)$
is new.
6.1
$\mathbf {GW.2}$
Let
$\mathcal {C}_{\mathbf {GW.2}}$
be the class of all Kripke models whose frames are of the form shown in Figure 3. The logic
$\mathbf {GW.2}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {GW.2}}$
.
The frame of
$\mathbf {GW.2}$
.
Theorem 6.1 (Maksimova [Reference Maksimova15]).
$\mathbf {GW.2}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {GW.2}}$
enjoys
$2$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {GW.2}}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0,1\}$
, let
$y_i$
be the final element of
$M_i$
.
We show that
$(M_0, y_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, y_1)$
. Since
$v_1 R_1 y_1$
for all
$v_1 \in W_1$
, we have
$(M_1, w_1) \Vdash _1 \Box \Diamond \chi ^{(P^{-}, P^{+})}_{0}[M_1, y_1]$
. Since
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, w_1)$
, we get
$(M_0, w_0) \Vdash _0 \Box \Diamond \chi ^{(P^{-}, P^{+})}_{0}[M_1, y_1]$
. Since
$w_0 R_0 y_0$
, we have
$(M_0, y_0) \Vdash _0 \Diamond \chi ^{(P^{-}, P^{+})}_{0}[M_1, y_1]$
, and hence
$(M_0, y_0) \Vdash _0 \chi ^{(P^{-}, P^{+})}_{0}[M_1, y_1]$
. By Lemma 3.4,
$(M_0, y_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, y_1)$
.
It is easy to check that the frame
$\mathcal {F}^{*} = (W^{*}, R^{*})$
drawn in Figure 4 satisfies all the required conditions stated in Remark 3.8. Note that in our rough labeling notation, the situation
$(w_0, w_1) = (y_0, y_1)$
is allowed.
The frame
$(W^{*}, R^{*})$
.
6.2
$\Gamma (\mathbf {LS}, 2, 1)$
Let
$\mathcal {C}_{\Gamma (\mathbf {LS}, 2, 1)}$
be the class of all Kripke models whose frames are of the form shown in Figure 5. The logic
$\Gamma (\mathbf {LS}, 2, 1)$
is sound and complete with respect to
$\mathcal {C}_{\Gamma (\mathbf {LS}, 2, 1)}$
.
The frame of
$\Gamma (\mathbf {LS}, 2, 1)$
.
Theorem 6.2.
$\Gamma (\mathbf {LS}, 2, 1)$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\Gamma (\mathbf {LS}, 2, 1)}$
enjoys
$2$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\Gamma (\mathbf {LS}, 2, 1)}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, w_1)$
. Let
$C_i = \{y_i, z_i\}$
be the cluster of final elements of
$M_i$
for
$i \in \{0, 1\}$
.
We show that
$C_0$
matches
$C_1$
. Let
$u_1 \in C_1$
. Since
$v_1 R_1 u_1$
for all
$v_1 \in W_1$
and
$w_0 R_0 y_0$
, in the same way as in the proof of Theorem 6.1, we have
$(M_0, y_0) \Vdash _0 \Diamond \chi ^{(P^{-}, P^{+})}_{0}[M_1, u_1]$
. Then,
$\chi ^{(P^{-}, P^{+})}_{0}[M_1, u_1]$
is true in at least one of
$y_0$
and
$z_0$
. Hence,
$$ \begin{align} (M_0, y_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1)\ \text{or}\ (M_0, z_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1). \end{align} $$
In a similar way, we can prove that for
$u_0 \in \{y_0, z_0\}$
,
$$ \begin{align} (M_0, u_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, y_1)\ \text{or}\ (M_0, u_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, z_1). \end{align} $$
Since both
$C_0$
and
$C_1$
consist of two elements, by Lemma 4.6, there exist
$u_1, v_1 \in C_1$
such that
$(M_0, y_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
and
$(M_0, z_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1)$
It is easy to check that the frame
$(W^{*}, R^{*})$
in Figure 6 satisfies all the required conditions.
The frame
$(W^{*}, R^{*})$
.
6.3
$\mathbf {S4.4}$
Let
$\mathcal {C}_{\mathbf {S4.4}}$
be the class of all finite Kripke models whose frames are of the form shown in Figure 7. The logic
$\mathbf {S4.4}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {S4.4}}$
.
A frame of
$\mathbf {S4.4}$
.
Theorem 6.3 (Shimura [Reference Shimura22]).
$\mathbf {S4.4}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {S4.4}}$
enjoys
$2$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {S4.4}}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, w_1)$
. Let
$C_i$
be the finite cluster of final elements of
$M_i$
for
$i \in \{0, 1\}$
.
We show that
$C_0$
matches
$C_1$
. For each
$v_0 \in C_0$
, we have
$$\begin{align*}(M_0, v_0) \Vdash_0 \bigvee_{u_0 \in C_0} \chi^{(P^{+}, P^{-})}_{0}[M_0, u_0], \end{align*}$$
and hence
$$\begin{align*}(M_0, v_0) \Vdash_0 \Box \bigvee_{u_0 \in C_0} \chi^{(P^{+}, P^{-})}_{0}[M_0, u_0]. \end{align*}$$
So,
$$\begin{align*}(M_0, w_0) \Vdash_0 \Diamond \Box \bigvee_{u_0 \in C_0} \chi^{(P^{+}, P^{-})}_{0}[M_0, u_0]. \end{align*}$$
Since
$(M_0, w_0) \xrightarrow [2]{(P^{+}, P^{-})} (M_1, w_1)$
, we obtain that this formula is also true in
$(M_1, w_1)$
. It follows that for every
$u_1 \in C_1$
, we get
$$\begin{align*}(M_1, u_1) \Vdash_1 \bigvee_{u_0 \in C_0} \chi^{(P^{+}, P^{-})}_{0}[M_0, u_0], \end{align*}$$
and thus, there exists
$u_0 \in C_0$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
In the same way, we can show that for any
$u_0 \in C_0$
, there exists
$u_1 \in C_1$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
Let
$$\begin{align*}C^{*} : = \{(u_0, u_1) \mid u_0 \in C_0, u_1 \in C_1,\ \text{and}\ (M_0, u_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1)\}. \end{align*}$$
Then, the frame
$(W^{*}, R^{*})$
shown in Figure 8 satisfies all the required conditions.
The frame
$(W^{*}, R^{*})$
.
7 Modal companions of
$\mathbf {LV}$
In this section, we newly prove that the three logics
$\mathbf {GV} = \Gamma (\mathbf {LV}, 1, 1)$
,
$\Gamma (\mathbf {LV}, 2, 1)$
, and
$\Gamma (\mathbf {LV}, \omega , 1)$
have ULIP. In particular, LIP for
$\mathbf {GV}$
is mentioned in [Reference Maksimova17] as an open problem.
7.1
$\mathbf {GV}$
Let
$\mathcal {C}_{\mathbf {GV}}$
be the class of all Kripke models whose frames are of the form shown in Figure 9. The logic
$\mathbf {GV}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {GV}}$
.
The frame of
$\mathbf {GV}$
.
Theorem 7.1.
$\mathbf {GV}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {GV}}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {GV}}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and
$y_i, z_i$
be two distinct final elements of
$M_i$
. We distinguish the following three cases.
Case 1.
$w_0 \in \{y_0, z_0\}$
and
$w_1 \in \{y_1, z_1\}$
.
Case 2.
$w_0 \in \{y_0, z_0\}$
and
$w_1 = x_1$
.
For the case where
$w_0 = x_0$
and
$w_1 \in \{y_1, z_1\}$
, we can draw the required frame
$(W^{*}, R^{*})$
similar to that corresponding to Case 2 in Figure 10. In subsequent proofs, we will basically omit the mention of such similar cases. In Case 2, by Lemma 4.3, we have that
$(M_0, w_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
for
$u_1 \in \{y_1, z_1\}$
.
The frames
$(W^{*}, R^{*})$
.
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
Since both
$M_0$
and
$M_1$
consist of two clusters, by Lemma 4.7, there exist two distinct final elements
$u_1$
and
$v_1$
of
$M_1$
such that
$(M_0, y_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
and
$(M_0, z_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1)$
.
Our frames
$(W^{*}, R^{*})$
corresponding to each of the three cases are shown together in Figure 10. It is easy to check that these frames satisfy all the required conditions.
7.2
$\Gamma (\mathbf {LV}, 2, 1)$
Let
$\mathcal {C}_{\Gamma (\mathbf {LV}, 2, 1)}$
be the class of all Kripke models whose frames are of the form shown in Figure 11. The logic
$\Gamma (\mathbf {LV}, 2, 1)$
is sound and complete with respect to
$\mathcal {C}_{\Gamma (\mathbf {LV}, 2, 1)}$
.
The frame of
$\Gamma (\mathbf {LV}, 2, 1)$
.
Theorem 7.2.
$\Gamma (\mathbf {LV}, 2, 1)$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\Gamma (\mathbf {LV}, 2, 1)}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\Gamma (\mathbf {LV}, 2, 1)}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$C_i^0 = \{y_i^0, z_i^0\}$
and
$C_i^1 = \{y_i^1, z_i^1\}$
be two distinct clusters of final elements of
$M_i$
. We distinguish the following three cases.
Case 1.
$w_0 \in C_0^0$
and
$w_1 \in C_1^0$
.
By Lemma 4.2, we have that
$C_0^0$
matches
$C_1^0$
. Since each cluster consists of two elements, by Lemma 4.6, there exist
$u_1^0, v_1^0 \in C_1^0$
such that
$(M_0, y_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1^0)$
and
$(M_0, z_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1^0)$
.
Case 2.
$w_0 \in C_0^0$
and
$w_1 = x_1$
.
By Lemma 4.3,
$C_0^0$
matches both
$C_1^0$
and
$C_1^1$
. Then, by Lemma 4.6, for
$k \in \{0, 1\}$
, there exist
$u_1^k, v_1^k \in C_1^k$
such that
$(M_0, y_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1^k)$
and
$(M_0, z_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1^k)$
.
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
Since both
$M_0$
and
$M_1$
consist of two clusters, by Lemma 4.7, there exist two distinct clusters
$D_1^0$
and
$D_1^1$
of final elements of
$M_1$
such that for
$k \in \{0, 1\}$
,
$C_0^k$
matches
$D_1^k$
. Also, since each cluster consists of two elements, by Lemma 4.6, for
$k \in \{0, 1\}$
, there exist
$u_1^k, v_1^k \in D_1^k$
such that
$(M_0, y_0^k) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1^k)$
and
$(M_0, z_0^k) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1^k)$
.
Our frames
$(W^{*}, R^{*})$
corresponding to Cases 1 and 2 are shown together in Figure 12. Figure 13 shows our frame
$(W^{*}, R^{*})$
corresponding to Case 3. These frames satisfy all the required conditions.
The frame
$(W^{*}, R^{*})$
in Case 3.
7.3
$\Gamma (\mathbf {LV}, \omega , 1)$
Let
$\mathcal {C}_{\Gamma (\mathbf {LV}, \omega , 1)}$
be the class of all finite Kripke models whose frames are of the form shown in Figure 14. The logic
$\Gamma (\mathbf {LV}, \omega , 1)$
is sound and complete with respect to
$\mathcal {C}_{\Gamma (\mathbf {LV}, \omega , 1)}$
.
A frame of
$\Gamma (\mathbf {LV}, \omega , 1)$
.
Theorem 7.3.
$\Gamma (\mathbf {LV}, \omega , 1)$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\Gamma (\mathbf {LV}, \omega , 1)}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\Gamma (\mathbf {LV}, \omega , 1)}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$C_i^0$
and
$C_i^1$
be two distinct clusters of final elements of
$M_i$
. We distinguish the following three cases.
Case 1.
$w_0 \in C_0^0$
and
$w_1 \in C_1^0$
.
By Lemma 4.2,
$C_0^0$
matches
$C_1^0$
. Let
$$\begin{align*}C^{*} : = \{(u_0^0, u_1^0) \mid u_0^0 \in C_0^0, u_1^0 \in C_1^0,\ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^0)\}. \end{align*}$$
Case 2.
$w_0 \in C_0^0$
and
$w_1 = x_1$
.
By Lemma 4.3,
$C_0^0$
matches both
$C_1^0$
and
$C_1^1$
. Let
$$ \begin{align*} C^{*, 0} : & = \{(u_0^0, u_1^0) \mid u_0^0 \in C_0^0, u_1^0 \in C_1^0,\ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^0)\}, \\ C^{*, 1} : & = \{(u_0^0, u_1^1) \mid u_0^0 \in C_0^0, u_1^1 \in C_1^1,\ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^1)\}. \end{align*} $$
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
Since both
$M_0$
and
$M_1$
consist of two clusters, by Lemma 4.7, there exist two distinct clusters
$D_1^0$
and
$D_1^1$
of final elements of
$M_1$
such that for
$k \in \{0, 1\}$
,
$C_0^k$
matches
$D_1^k$
. Thus, let
$$ \begin{align*} C^{*,0} : & = \{(u_0^0, u_1^0) \mid u_0^0 \in C_0^0, u_1^0 \in D_1^0,\ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^0)\}, \\ C^{*,1} : & = \{(v_0^0, v^1_1) \mid v_0^0 \in C_0^1, v_1^1 \in D_1^1,\ \text{and}\ (M_0, v_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, v_1^1)\}. \end{align*} $$
Our frames
$(W^{*}, R^{*})$
corresponding to these three cases are shown together in Figure 15. We can easily check that these frames satisfy all the required conditions.
The frame
$(W^{*}, R^{*})$
.
8 Modal companions of
$\mathbf {LP}_2$
In this section, we prove that the three logics
$\mathbf {GW} = \Gamma (\mathbf {LP}_2, 1, 1)$
,
$\Gamma (\mathbf {LP}_2, 2, 1)$
, and
$\Gamma (\mathbf {LP}_2, \omega , 1)$
have ULIP. In particular, LIP for
$\Gamma (\mathbf {LP}_2, 2, 1)$
is new.
8.1
$\mathbf {GW}$
Let
$\mathcal {C}_{\mathbf {GW}}$
be the class of all finite Kripke models whose frames are of the form shown in Figure 16. The logic
$\mathbf {GW}$
is sound and complete with respect to
$\mathcal {C}_{\mathbf {GW}}$
.
A frame of
$\mathbf {GW}$
.
Theorem 8.1 (Shimura [Reference Shimura22]; Maksimova [Reference Maksimova17]).
$\mathbf {GW}$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\mathbf {GW}}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\mathbf {GW}}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$F_i$
be the set of all final elements of
$M_i$
. We distinguish the following three cases.
Case 1.
$w_0 \in F_0$
and
$w_1 \in F_1$
.
Case 2.
$w_0 \in F_0$
and
$w_1 = x_1$
.
By Lemma 4.3, for all
$u_1 \in F_1$
, we have that
$(M_0, w_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
. Let
$F^{*} : = \{(w_0, u_1) \mid u_1 \in F_1\}$
.
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
By Lemma 4.4, we obtain the following properties:
-
1. For any
$u_0 \in F_0$
, there exists
$u_1 \in F_1$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
. -
2. For any
$u_1 \in F_1$
, there exists
$u_0 \in F_0$
such that
$(M_0, u_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1)$
.
Let
$$\begin{align*}F^{*} : = \{(u_0, u_1) \mid u_0 \in F_0, u_1 \in F_1,\ \text{and}\ (M_0, u_0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1)\}. \end{align*}$$
Our frames
$(W^{*}, R^{*})$
corresponding to these three cases are shown together in Figure 17. It is easy to check that these frames satisfy all the required conditions.
The frames
$(W^{*}, R^{*})$
.
8.2
$\Gamma (\mathbf {LP}_2, 2, 1)$
Let
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, 2, 1)}$
be the class of all finite Kripke models whose frames are of the form shown in Figure 18. The logic
$\Gamma (\mathbf {LP}_2, 2, 1)$
is sound and complete with respect to
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, 2, 1)}$
.
A frame of
$\Gamma (\mathbf {LP}_2, 2, 1)$
.
Theorem 8.2.
$\Gamma (\mathbf {LP}_2, 2, 1)$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, 2, 1)}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, 2, 1)}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$C_i^0, C_i^1, \ldots , C_i^{j_i}$
be all the clusters of final elements of
$M_i$
. Also let
$C_i^k = \{y_i^k, z_i^k\}$
. We distinguish the following three cases.
Case 1.
$w_0 \in C_0^0$
and
$w_1 \in C_1^0$
.
By Lemma 4.2,
$C_0^0$
matches
$C_1^0$
. Since these clusters consist of two elements, by Lemma 4.6, there exist
$u_1^0, v_1^0 \in C_1^0$
such that
$(M_0, y_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1^0)$
and
$(M_0, z_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1^0)$
.
Case 2.
$w_0 \in C_0^0$
and
$w_1 = x_1$
.
By Lemma 4.3,
$C_0^0$
matches all the clusters
$C_1^k$
of final elements of
$M_1$
. Since every cluster consists of two elements, by Lemma 4.6, for each cluster
$C_1^k$
of
$M_1$
, there exist
$u_1^k, v_1^k \in C_1^k$
such that
$(M_0, y_0^0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, u_1^k)$
and
$(M_0, z^0_0) \xrightarrow [0]{(P^{+}, P^{-})} (M_1, v_1^k)$
.
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
By Lemmas 4.4 and 4.6, we obtain the following two properties:
-
1. For any cluster
$C_0^k$
of
$M_0$
, there exist a cluster
$C_1^{k'}$
of
$M_1$
and
$u_1^{k'}, v_1^{k'} \in C_1^{k'}$
such that
$u_1^{k'} \neq v_1^{k'}$
and
$$\begin{align*}(M_0, y_0^k) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^{k'})\ \text{and}\ (M_0, z_0^k) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, v_1^{k'}). \end{align*}$$
-
2. For any cluster
$C_1^k$
of
$M_1$
, there exist a cluster
$C_0^{k'}$
of
$M_0$
and
$u_0^{k'}, v_0^{k'} \in C_0^{k'}$
such that
$u_0^{k'} \neq v_0^{k'}$
and
$$\begin{align*}(M_0, u_0^{k'}) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, y_1^{k})\ \text{and}\ (M_0, v_0^{k'}) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, z_1^{k}). \end{align*}$$
Our frames
$(W^{*}, R^{*})$
corresponding to Cases 1 and 2 are drawn in Figure 19. Our frame
$(W^{*}, R^{*})$
corresponding to Case 3 is shown in Figure 20. These frames satisfy all the required conditions.
The frame
$(W^{*}, R^{*})$
in Case 3.
8.3
$\Gamma (\mathbf {LP}_2, \omega , 1)$
Let
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, \omega , 1)}$
be the class of all finite Kripke models whose frames are of the form shown in Figure 21. The logic
$\Gamma (\mathbf {LP}_2, \omega , 1)$
is sound and complete with respect to
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, \omega , 1)}$
.
A frame of
$\Gamma (\mathbf {LP}_2, \omega , 1)$
.
Theorem 8.3 (Shimura [Reference Shimura22]).
$\Gamma (\mathbf {LP}_2, \omega , 1)$
has ULIP.
Proof. We prove that
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, \omega , 1)}$
enjoys
$3$
-IP. Let
$P^{+}$
and
$P^{-}$
be any finite sets of propositional variables and let
$M_0 = (W_0, R_0, \Vdash _0)$
and
$M_1 = (W_1, R_1, \Vdash _1)$
be Kripke models in
$\mathcal {C}_{\Gamma (\mathbf {LP}_2, \omega , 1)}$
, let
$w_0 \in W_0$
and
$w_1 \in W_1$
, and suppose
$(M_0, w_0) \xrightarrow [3]{(P^{+}, P^{-})} (M_1, w_1)$
. For
$i \in \{0, 1\}$
, let
$x_i$
be the root element of
$M_i$
and let
$C_i^0, C_i^1, \ldots , C_i^{j_i}$
be all the clusters of final elements of
$M_i$
. We distinguish the following three cases.
Case 1.
$w_0 \in C_0^0$
and
$w_1 \in C_1^0$
.
By Lemma 4.2,
$C_0^0$
matches
$C_1^0$
. Let
$$\begin{align*}C^{*} : = \{(u_0^0, u_1^0) \mid u_0^0 \in C_0^0, u_1^0 \in C_1^0,\ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^0)\}. \end{align*}$$
Case 2.
$w_0 \in C_0^0$
and
$w_1 = x_1$
.
By Lemma 4.3,
$C_0^0$
matches all the clusters
$C_1^k$
of final elements of
$M_1$
. Then, for each cluster
$C_1^k$
of
$M_1$
, let
$$\begin{align*}C^{*,k} = \{(u_0^0, u_1^k) \mid u_0^0 \in C_0^0, u_1^k \in C_1^k, \ \text{and}\ (M_0, u_0^0) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^k)\}. \end{align*}$$
Case 3.
$w_0 = x_0$
and
$w_1 = x_1$
.
By Lemma 4.4, we obtain the following two properties:
-
1. For any cluster
$C_0^k$
of
$M_0$
, there exists a cluster
$C_1^{k'}$
of
$M_1$
such that
$C_0^k$
matches
$C_1^{k'}$
. -
2. For any cluster
$C_1^k$
of
$M_1$
, there exists a cluster
$C_0^{k'}$
of
$M_0$
such that
$C_0^{k'}$
matches
$C_1^{k}$
.
For each cluster
$C_0^k$
of
$M_0$
, let
$$\begin{align*}C_0^{*, k} : = \{(u_0^k, u_1^{k'}) \mid u_0^k \in C_0^k, u_1^{k'} \in C_1^{k'}, \ \text{and}\ (M_0, u_0^k) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^{k'})\}. \end{align*}$$
Also, for each cluster
$C_1^k$
of
$M_1$
, let
$$\begin{align*}C_1^{*, k} : = \{(u_0^{k'}, u_1^{k}) \mid u_0^{k'} \in C_0^{k'}, u_1^{k} \in C_1^{k}, \ \text{and}\ (M_0, u_0^{k'}) \xrightarrow[0]{(P^{+}, P^{-})} (M_1, u_1^{k})\}. \end{align*}$$
Our frames
$(W^{*}, R^{*})$
corresponding to Cases 1 and 2 are drawn in Figure 22. Our frame
$(W^{*}, R^{*})$
corresponding to Case 3 is shown in Figure 23. We can check that these frames satisfy all the required conditions.
The frame
$(W^{*}, R^{*})$
in Case 3.
9 Failure of LIP
In this section, we investigate the failure of LIP. Maksimova [Reference Maksimova15] proved that each of the logics
$\Gamma (\mathbf {LP}_2, 1, 2)$
,
$\Gamma (\mathbf {LV}, 1, 2)$
,
$\Gamma (\mathbf {LS}, 1, 2)$
, and
$\Gamma (\mathbf {Cl}, 2, 0)$
has CIP but does not have LIP (see also [Reference Gabbay and Maksimova5, Reference Maksimova16]). We prove that the three further logics
$\Gamma (\mathbf {LP}_2, 1, \omega )$
,
$\Gamma (\mathbf {LV}, 1, \omega )$
, and
$\Gamma (\mathbf {LS}, 1, \omega )$
also do not have LIP. Moreover, we will prove this in a form that includes a part of Maksimova’s results, namely, we prove that every logic L satisfying
$\Gamma (\mathbf {LP}_2, 1, \omega ) \subseteq L \subseteq \Gamma (\mathbf {LS}, 1, 2)$
does not have LIP.
Before proving our theorem, we prepare the following lemma.
Lemma 9.1. Over the logic
$\Gamma (\mathbf {LS}, 1, 2)$
, every formula
$\varphi $
satisfying
$v^{+}(\varphi ) \subseteq \{p\}$
and
$v^{-}(\varphi ) = \emptyset $
is provably equivalent to one of the following eight formulas:
$$\begin{align*}\bot, \quad \Box p, \quad p \land \Box \Diamond p, \quad \Box \Diamond p, \quad p, \quad p \lor \Box \Diamond p, \quad \Diamond p, \quad \top. \end{align*}$$
Proof. The logic
$\Gamma (\mathbf {LS}, 1, 2)$
is characterized by the Kripke frame shown in Figure 24. It is easy to see that
$\Gamma (\mathbf {LS}, 1, 2)$
contains
$\Box \Diamond p \leftrightarrow \Diamond \Box p$
.
The diagram in Figure 25 shows the implications between these eight formulas over
$\mathbf {S4}$
.
We prove the lemma by induction on the construction of
$\varphi $
. If
$\varphi $
is one of p,
$\bot $
, and
$\top $
, then the lemma is trivial.
Suppose that the lemma holds for
$\varphi _0$
and
$\varphi _1$
. It is easy to show that
$\varphi _0 \land \varphi _1$
and
$\varphi _0 \lor \varphi _1$
are equivalent to one of the eight formulas. The following list of equivalences shows that
$\Box \varphi _0$
and
$\Diamond \varphi _0$
are also equivalent to some of the eight formulas.
Here, we are ready to prove the theorem.
Theorem 9.2. Let L be any logic satisfying
$\Gamma (\mathbf {LP}_2, 1, \omega ) \subseteq L \subseteq \Gamma (\mathbf {LS}, 1, 2)$
. Then, L does not have LIP. In particular, each of the logics
$\Gamma (\mathbf {LP}_2, 1, \omega )$
,
$\Gamma (\mathbf {LP}_2, 1, 2)$
,
$\Gamma (\mathbf {LV}, 1, \omega )$
,
$\Gamma (\mathbf {LV}, 1, 2)$
,
$\Gamma (\mathbf {LS}, 1, \omega )$
, and
$\Gamma (\mathbf {LS}, 1, 2)$
has CIP but does not have LIP.
The frame of
$\Gamma (\mathbf {LS}, 1, 2)$
.
The implications between the eight formulas over
$\mathbf {S4}$
.
Proof. At first, we prove
$$\begin{align*}\Gamma(\mathbf{LP}_2, 1, \omega) \vdash p \land \Box(\Box \neg p \lor p) \to \Box (p \lor q \lor \Box \neg q). \end{align*}$$
Let
$(W, R, \Vdash )$
be any finite Kripke model whose frame is of the form shown in Figure 26. The logic
$\Gamma (\mathbf {LP}_2, 1, \omega )$
is characterized by the class of all such Kripke frames.
A frame of
$\Gamma (\mathbf {LP}_2, 1, \omega )$
.
Let F be the set of all final elements of the model, and I be the cluster
$W \setminus F$
of inner elements. It suffices to show that
$p \land \Box (\Box \neg p \lor p) \to \Box (p \lor q \lor \Box \neg q)$
is valid in
$(W, R, \Vdash )$
. For
$x \in F$
, we have
$x \Vdash p \land \Box (\Box \neg p \lor p) \to \Box (p \lor q \lor \Box \neg q)$
because
$x \Vdash p \to \Box p$
. For
$x \in I$
, assume
$x \Vdash p \land \Box (\Box \neg p \lor p)$
. Let
$y \in W$
be any element such that
$x R y$
. If
$y \in I$
, then
$y \Vdash \Diamond p \land (\Box \neg p \lor p)$
, and so
$y \Vdash p$
. If
$y \in F$
, then
$y \Vdash q \lor \Box \neg q$
holds. Hence, we obtain
$x \Vdash \Box (p \lor q \lor \Box \neg q)$
. We have shown that
$p \land \Box (\Box \neg p \lor p) \to \Box (p \lor q \lor \Box \neg q)$
is valid in
$(W, R, \Vdash )$
.
Suppose, towards a contradiction, that the logic L has LIP. Then, there would exist a Lyndon interpolant
$\theta $
of
$p \land \Box (\Box \neg p \lor p) \to \Box (p \lor q \lor \Box \neg q)$
. Since
$L \subseteq \Gamma (\mathbf {LS}, 1, 2)$
, we would have:
-
1.
$\Gamma (\mathbf {LS}, 1, 2) \vdash p \land \Box (\Box \neg p \lor p) \to \theta $
. -
2.
$\Gamma (\mathbf {LS}, 1, 2) \vdash \theta \to \Box (p \lor q \lor \Box \neg q)$
. -
3.
$v^{+}(\theta ) \subseteq \{p\}$
and
$v^{-}(\theta ) = \emptyset $
.
Here, we consider the model
$M_0 = (W_0, R_0, \Vdash _0)$
of
$\Gamma (\mathbf {LS}, 1, 2)$
as drawn in Figure 27:
The model
$M_0$
.
It is easy to see that
$(M_0, x_0) \Vdash _0 p \land \Box (\Box \neg p \lor p)$
. Thus, we have
$(M_0, x_0) \Vdash _0 \theta $
because
$\Gamma (\mathbf {LS}, 1, 2) \vdash p \land \Box (\Box \neg p \lor p) \to \theta $
. On the other hand, since
$(M_0, x_0) \nVdash _0 \Box \Diamond p$
, we have that
$\theta $
is equivalent to one of p,
$p \lor \Box \Diamond p$
,
$\Diamond p$
, and
$\top $
over
$\Gamma (\mathbf {LS}, 1, 2)$
by Lemma 9.1. So,
$\Gamma (\mathbf {LS}, 1, 2) \vdash p \to \theta $
.
Next, we consider the model
$M_1 = (W_0, R_0, \Vdash _1)$
of
$\Gamma (\mathbf {LS}, 1,2)$
as drawn in Figure 28.
The model
$M_1$
.
Since
$(M_1, x_0) \Vdash _1 p$
, we have
$(M_1, x_0) \Vdash _1 \theta $
. On the other hand,
$(M_1, x_1) \nVdash _1 p$
,
$(M_1, x_1) \nVdash _1 q$
, and
$(M_1, x_1) \nVdash _1 \Box \neg q$
imply that
$(M_1, x_0) \nVdash _1 \Box (p \lor q \lor \Box \neg q)$
. This contradicts
$\Gamma (\mathbf {LS}, 1, 2) \vdash \theta \to \Box (p \lor q \lor \Box \neg q)$
.
Therefore, L does not have LIP.
10 LIP and ULIP for intermediate propositional logics
In this section, we discuss LIP and ULIP for intermediate propositional logics. In particular, we will prove the following theorem.
Theorem 10.1. For any intermediate propositional logic L, the following are equivalent:
-
1. L has CIP.
-
2. L has UIP.
-
3. L has LIP.
-
4. L has ULIP.
The equivalence
$(1 \Leftrightarrow 2)$
is already known [Reference Maksimova17]. So, we will prove the equivalences
$(1 \Leftrightarrow 3)$
and
$(1 \Leftrightarrow 4)$
.
First, we consider LIP. LIP for intermediate logics directly follows from LIP for modal logics through Gödel’s translation.
Definition 10.2 (Gödel’s translation).
We define the translation
$\mathsf {T}$
from formulas of intermediate logic to formulas of modal logic as follows:
-
•
$\mathsf {T}(p) = \Box p$
for propositional variables p, -
•
$\mathsf {T}(\bot ) = \bot $
, -
•
$\mathsf {T}(\varphi \land \psi ) = \mathsf {T}(\varphi ) \land \mathsf {T}(\psi )$
, -
•
$\mathsf {T}(\varphi \lor \psi ) = \mathsf {T}(\varphi ) \lor \mathsf {T}(\psi )$
, -
•
$\mathsf {T}(\neg \varphi ) = \Box \neg \mathsf {T}(\varphi )$
, -
•
$\mathsf {T}(\varphi \to \psi ) = \Box (\mathsf {T}(\varphi ) \to \mathsf {T}(\psi ))$
.
For any intermediate logic L and normal modal logic M extending
$\mathbf {S4}$
, we say that M is a modal companion of L iff for any formula
$\varphi $
of intermediate logic,
$L \vdash \varphi \iff M \vdash \mathsf {T}(\varphi )$
.
Fact 10.3 (Maksimova [Reference Maksimova15]).
For any intermediate propositional logic L, if some modal companion of L has LIP, then L also has LIP.
For example, LIP for
$\mathbf {Cl}$
,
$\mathbf {LS}$
,
$\mathbf {LP}_2$
,
$\mathbf {KC}$
, and
$\mathbf {Int}$
follows from LIP for
$\mathbf {S5}$
,
$\mathbf {GW.2}$
,
$\mathbf {GW}$
,
$\mathbf {S4.2}$
, and
$\mathbf {S4}$
, respectively. Since all modal companions of
$\mathbf {LC}$
do not have CIP [Reference Maksimova14], Kuznets and Lellmann [Reference Kuznets and Lellmann9, Reference Kuznets and Lellmann10] directly proved LIP for
$\mathbf {LC}$
without using Fact 10.3. Among the intermediate logics having CIP, only the logic
$\mathbf {LV}$
was not known to have LIP or not (cf. [Reference Maksimova17]). Since we proved that a modal companion
$\mathbf {GV}$
of
$\mathbf {LV}$
has LIP (Theorem 7.1), we obtain the following corollary, which yields the equivalence
$(1 \Leftrightarrow 3)$
of Theorem 10.1.
Corollary 10.4.
$\mathbf {LV}$
has LIP.
Next, we consider ULIP. We say that a logic L is locally tabular iff for any finite set P of propositional variables, there are finitely many formulas built from variables in P up to L-provable equivalence. For example, it is known that
$\mathbf {Cl}$
,
$\mathbf {LS}$
,
$\mathbf {LV}$
,
$\mathbf {LP}_2$
, and
$\mathbf {LC}$
are locally tabular. For locally tabular logics, LIP and ULIP coincide.
Fact 10.5 (Kurahashi [Reference Kurahashi6, Proposition 3]).
If a locally tabular logic L has LIP, then L also has ULIP.
So, we obtain the following corollary.
Corollary 10.6. The logics
$\mathbf {Cl}$
,
$\mathbf {LS}$
,
$\mathbf {LV}$
,
$\mathbf {LP}_2$
, and
$\mathbf {LC}$
have ULIP.
Therefore, we only need to consider ULIP for
$\mathbf {Int}$
and
$\mathbf {KC}$
. Here, we prove an analogue of Fact 10.3.
Proposition 10.7. For any intermediate propositional logic L, if some modal companion of L has ULIP, then L also has ULIP.
Proof. Suppose that a modal companion M of L has ULIP. Let
$\varphi $
be any formula and
$P^{+}, P^{-}$
be any finite sets of propositional variables. Let
$\theta $
be a uniform Lyndon interpolant of
$(\mathsf {T}(\varphi ), P^{+}, P^{-})$
in M. Let
$\mathsf {s}$
be the uniform substitution such that
$\mathsf {s}(p) = \Box p$
. It is easy to show that there exists a formula
$\xi $
of intermediate logic satisfying the following conditions (cf. [Reference Chagrov and Zakharyaschev1, Theorem 14.9]):
-
1.
$\mathbf {S4} \vdash \Box \mathsf {s}(\theta ) \leftrightarrow \mathsf {T}(\xi )$
, -
2.
$v^{\circ }(\xi ) = v^{\circ }(\theta )$
for
$\circ \in \{+, -\}$
.
We show that
$\xi $
is a uniform Lyndon interpolant of
$(\varphi , P^{+}, P^{-})$
in L.
1. Since
$M \vdash \mathsf {T}(\varphi ) \to \theta $
and
$\mathbf {S4} \vdash \mathsf {T}(\varphi ) \leftrightarrow \Box \mathsf {T}(\varphi )$
, we have
$M \vdash \mathsf {T}(\varphi ) \to \Box \theta $
. Since M is closed under applying uniform substitutions and
$\mathbf {S4} \vdash \mathsf {T}(\varphi ) \leftrightarrow \mathsf {s} \left (\mathsf {T}(\varphi ) \right )$
, we obtain
$M \vdash \mathsf {T}(\varphi ) \to \Box \mathsf {s}(\theta )$
. Hence,
$M \vdash \mathsf {T}(\varphi ) \to \mathsf {T}(\xi )$
, and so
$M \vdash \mathsf {T}(\varphi \to \xi )$
. Since M is a modal companion of L, we get
$L \vdash \varphi \to \xi $
.
2. For
$\circ \in \{+, -\}$
, we have
$v^{\circ }(\xi ) = v^{\circ }(\theta ) \subseteq v^{\circ }\left (\mathsf {T}(\varphi ) \right ) \setminus P^{\circ } = v^{\circ }(\varphi ) \setminus P^{\circ }$
.
3. Let
$\psi $
be any formula such that
$L \vdash \varphi \to \psi $
and
$v^{\circ }(\psi ) \cap P^{\circ } = \emptyset $
. Then,
$M \vdash \mathsf {T}(\varphi ) \to \mathsf {T}(\psi )$
. Since
$v^{\circ }\left (\mathsf {T}(\psi ) \right ) \cap P^{\circ } = v^{\circ }(\psi ) \cap P^{\circ } = \emptyset $
, we obtain
$M \vdash \theta \to \mathsf {T}(\psi )$
. Then, in a similar way as above, we obtain
$M \vdash \mathsf {T}(\xi \to \psi )$
. Therefore,
$L \vdash \xi \to \psi $
.
It was proved in [Reference Kurahashi6] that a modal companion
$\mathbf {Grz}$
of
$\mathbf {Int}$
has ULIP. So, we immediately obtain the following corollary.
Corollary 10.8.
$\mathbf {Int}$
has ULIP.
Finally, we focus on ULIP for
$\mathbf {KC}$
. For this, it suffices to prove ULIP for a modal companion
$\mathbf {Grz.2}$
of
$\mathbf {KC}$
. Let
$\alpha (p)$
be the formula
$\Box (\Box \Diamond p \leftrightarrow \Diamond \Box p)$
, then
$\mathbf {Grz.2}$
is the least normal extension of
$\mathbf {Grz}$
containing
$\alpha (p)$
. We use the following facts.
Fact 10.9 (Cf. [Reference Gabbay and Maksimova5, Lemma 5.32 and Proposition 5.35]).
For any formula
$\varphi $
with
$v(\varphi ) = \{q_0, \ldots , q_{k-1}\}$
, if
$\mathbf {Grz.2} \vdash \varphi $
, then
$$\begin{align*}\mathbf{Grz} \vdash \alpha(\bot) \land \alpha(q_0) \land \cdots \land \alpha(q_{k-1}) \to \varphi. \end{align*}$$
Fact 10.10 (Cf. [Reference Gabbay and Maksimova5, Lemma 5.33]).
Let L be a normal modal logic and
$\varphi (p), \psi $
and
$\rho $
be any formulas such that
$L \vdash \psi \to \rho $
.
-
1. If
$p \notin v^{-}(\varphi )$
, then
$L \vdash \varphi (\psi ) \to \varphi (\rho )$
. -
2. If
$p \notin v^{+}(\varphi )$
, then
$L \vdash \varphi (\rho ) \to \varphi (\psi )$
.
Theorem 10.11.
$\mathbf {Grz.2}$
has ULIP.
Proof. Let
$\varphi $
be any formula and
$P^{+}, P^{-}$
be any finite sets of propositional variables. If
$\circ $
is
$+$
(resp.
$-$
), then let
$\bullet $
denote
$-$
(resp.
$+$
). Let X be the union of the following three sets:
$$\begin{align*}v^{+}(\varphi) \cap v^{-}(\varphi), \quad (v^{+}(\varphi) \setminus v^{-}(\varphi)) \cap P^{-}, \quad (v^{-}(\varphi) \setminus v^{+}(\varphi)) \cap P^{+}. \end{align*}$$
Also let Y be the union of the following two sets:
$$\begin{align*}v^{+}(\varphi) \setminus (v^{-}(\varphi) \cup P^{-}), \quad v^{-}(\varphi) \setminus (v^{+}(\varphi) \cup P^{+}). \end{align*}$$
Then,
$v(\varphi )$
is the disjoint union of X and Y.
By ULIP for
$\mathbf {Grz}$
, we find a uniform Lyndon interpolant
$\theta $
of
$$\begin{align*}\left(\alpha(\bot) \land \bigwedge_{p \in X}\alpha(p) \land \varphi, P^{+}, P^{-} \right) \end{align*}$$
in
$\mathbf {Grz}$
. We prove that
$\theta $
is also a uniform Lyndon interpolant of
$\left (\varphi , P^{+}, P^{-} \right )$
in
$\mathbf {Grz.2}$
.
1. Since
$\mathbf {Grz} \vdash \alpha (\bot ) \land \bigwedge _{p \in X}\alpha (p) \land \varphi \to \theta $
, we get
$\mathbf {Grz.2} \vdash \varphi \to \theta $
.
2. We have:
$$ \begin{align*} v^{\circ}(\theta) & \subseteq v^{\circ} \left(\alpha(\bot) \land \bigwedge_{p \in X}\alpha(p) \land \varphi \right) \setminus P^{\circ} \\ & = \big[ v^{\circ}(\varphi) \cup \big\{\big((v^\bullet(\varphi) \setminus v^{\circ}(\varphi)\big) \cap P^{\circ} \big\} \big] \setminus P^{\circ} \\ & = v^{\circ}(\varphi) \setminus P^{\circ}. \end{align*} $$
3. Let
$\psi $
be any formula such that
$\mathbf {Grz.2} \vdash \varphi \to \psi $
and
$v^{\circ }(\psi ) \cap P^{\circ } = \emptyset $
. By Fact 10.9, we have
$$\begin{align*}\mathbf{Grz} \vdash \alpha(\bot) \land \bigwedge_{p \in v(\varphi) \cup v(\psi)} \alpha(p) \land \varphi \to \psi. \end{align*}$$
Since
$v(\varphi ) \cup v(\psi )$
is the disjoint union of X, Y, and
$v(\psi ) \setminus v(\varphi )$
, we obtain
$$ \begin{align} \mathbf{Grz} \vdash \alpha(\bot) \land \bigwedge_{p \in X} \alpha(p) \land \varphi \to \big(\bigwedge_{q \in Y \cup (v(\psi) \setminus v(\varphi))} \alpha(q) \to \psi \big). \end{align} $$
Let
$\mathsf {s}$
be the uniform substitution defined as follows:
$$\begin{align*}\mathsf{s}(p) : = \begin{cases} \top & \text{if}\ p \notin v^{-}(\varphi) \cup v^{+}(\psi), \\ \bot & \text{else if}\ p \notin v^{+}(\varphi) \cup v^{-}(\psi), \\ p & \text{otherwise.} \end{cases} \end{align*}$$
Since
$\mathbf {K} \vdash p \to \top $
and
$\mathbf {K} \vdash \bot \to p$
, by Fact 10.10, we have
$\mathbf {K} \vdash \varphi \to \mathsf {s}(\varphi )$
and
$\mathbf {K} \vdash \mathsf {s}(\psi ) \to \psi $
. Since
$\mathbf {Grz} \vdash \alpha (\top )$
, we have
$$\begin{align*}\mathbf{Grz} \vdash \alpha(\bot) \land \bigwedge_{p \in X} \alpha(p) \land \varphi \to \mathsf{s} \left(\alpha(\bot) \land \bigwedge_{p \in X} \alpha(p) \land \varphi\right). \end{align*}$$
Let Z be the intersection of the following three sets:
$$\begin{align*}Y \cup (v(\psi) \setminus v(\varphi)), \quad v^{-}(\varphi) \cup v^{+}(\psi), \quad v^{+}(\varphi) \cup v^{-}(\psi). \end{align*}$$
Then, it is shown that Z is included in the union of the following three sets:
$$\begin{align*}(v^{+}(\varphi) \cap v^{+}(\psi)) \setminus (v^{-}(\varphi) \cup P^{-}), \quad & (v^{-}(\varphi) \cap v^{-}(\psi)) \setminus (v^{+}(\varphi) \cup P^{+}), \quad \\ & (v^{+}(\psi) \cap v^{-}(\psi)) \setminus v(\varphi). \end{align*}$$
Moreover, since
$v^{\circ }(\psi ) \cap P^{\circ } = \emptyset $
, we have
$Z \subseteq (v^{+}(\psi ) \setminus P^{-}) \cup (v^{-}(\psi ) \setminus P^{+})$
. Then, by applying the uniform substitution
$\mathsf {s}$
to (3), it follows from the above observations that
$$\begin{align*}\mathbf{Grz} \vdash \alpha(\bot) \land \bigwedge_{p \in X} \alpha(p) \land \varphi \to \left(\bigwedge_{\substack{q \in v^{+}(\psi) \setminus P^{-} \\ \text{or}\ q \in v^{-}(\psi) \setminus P^{+}}} \alpha(q) \to \psi \right). \end{align*}$$
We have:
$$ \begin{align*} & v^{\circ} \left(\bigwedge_{\substack{q \in v^{+}(\psi) \setminus P^{-} \\ \text{or}\ q \in v^{-}(\psi) \setminus P^{+}}} \alpha(q) \to \psi \right) \cap P^{\circ} \\ & = \big[ (v^{+}(\psi) \setminus P^{-}) \cup (v^{-}(\psi) \setminus P^{+}) \cup v^{\circ}(\psi) \big] \cap P^{\circ} \\ & = \big[(v^\bullet(\psi) \setminus P^{\circ}) \cup v^{\circ}(\psi) \big] \cap P^{\circ} \\ & = v^{\circ}(\psi) \cap P^{\circ} \\ & = \emptyset. \end{align*} $$
Therefore, we obtain
$$\begin{align*}\mathbf{Grz} \vdash \theta \to \left(\bigwedge_{\substack{q \in v^{+}(\psi) \setminus P^{-} \\ \text{or}\ q \in v^{-}(\psi) \setminus P^{+}}} \alpha(q) \to \psi \right). \end{align*}$$
We conclude
$\mathbf {Grz.2} \vdash \theta \to \psi $
.
Corollary 10.12.
$\mathbf {KC}$
has ULIP.
We have proved the equivalence
$(1 \Leftrightarrow 4)$
of Theorem 10.1.
Acknowledgments
The author would like to thank Tatsuya Shimura for his valuable comments and information.
Funding
This work was supported by JSPS KAKENHI Grant Number JP23K03200.
