Unification in Modal Logic

Abstract

Let $\varphi _{1},\ldots ,\varphi _{n}$ and $\psi$ be some formulas.

Let $\varphi _{1},\ldots ,\varphi _{n}$ and $\psi$ be some formulas. The figure $\frac{\varphi _{1},\ldots ,\varphi _{n}}{\psi }$ is the inference rule which for all substitutions $\sigma$, derives $\sigma (\psi )$ from $\sigma (\varphi _{1}),\ldots ,\sigma (\varphi _{n})$. It is admissible in a propositional logic L whenever for all substitutions $\sigma$, $\sigma (\psi )\in L$ if $\sigma (\varphi _{1}),\ldots ,\sigma (\varphi _{n})\in L$. It is derivable in L whenever there is a derivation of $\psi$ in L from the hypothesis $\varphi _{1},\ldots ,\varphi _{n}$. It is evident that every derivable rule is also admissible. L is called structurally complete when the converse holds. Some propositional logics — such as Classical Propositional Logic — are structurally complete. Others — like Intuitionistic Propositional Logic — are not. See [14, Chap. 2]. When L is not structurally complete, owing to the importance of the admissibility problem in the mechanization of propositional logics, it is crucial to be able to recognize whether a given inference rule is admissible. The question of the existence of a decidable modal logic with an undecidable admissibility problem has been negatively answered by Wolter and Zakharyaschev [41] within the context of normal modal logics between K and K4 enriched with the universal modality — see also the pioneering article of Chagrov [13] for an earlier example of a decidable modal logic with an undecidable admissibility problem. In some other cases, for instance Intuitionistic Propositional Logic and transitive normal modal logics like K4, the question of the decidability of the admissibility problem has been positively answered by Rybakov [33,34,35]. See also [15, 25, 27, 28, 32]. The truth is that Rybakov’s decidability results are related to the fact that the propositional logics he has considered are finitary [22,23,24].

The finitariness character of a propositional logic L originates in its unification problem. The unification problem in L is to determine, given a formula $\varphi$, whether there exists a substitution $\sigma$ such that $\sigma (\varphi )$ is in L. In that case, $\sigma$ is a unifier of $\varphi$. A formula $\varphi$ is filtering if for all unifiers $\sigma$ and $\tau$ of $\varphi$, there exists a unifier of $\varphi$ which is more general than $\sigma$ and $\tau$. We shall say that a set of unifiers of a formula $\varphi$ is complete if for all unifiers $\sigma$ of $\varphi$, there exists a unifier $\tau$ of $\varphi$ in that set such that $\tau$ is more general than $\sigma$. An important question is the following: when a formula is unifiable, has it a minimal complete set of unifiers? When the answer is “no”, the formula is nullary. When the answer is “yes”, the formula is either infinitary, or finitary, or unitary depending on the cardinalities of its minimal complete sets of unifiers. Filtering formulas are always unitary, or nullary. A propositional logic is called nullary if it possesses a nullary formula. Otherwise, it is called either infinitary, or finitary, or unitary depending on the types of its unifiable formulas. When every formula is filtering, the propositional logic is called filtering. See [3, 17, 26] for details. It is evident that if L is consistent then its unification problem can be reduced to its admissibility problem: a given formula $\varphi$ possesses a unifier in L if and only if the inference rule $\frac{\varphi }{\bot }$ is not admissible. Reciprocally, if L is unitary, or finitary and the elements of the minimal complete sets of unifiers given rise by its unifiable formulas can be computed then its admissibility problem can be reduced to its unification problem: a given inference rule $\frac{\varphi _{1},\ldots ,\varphi _{n}}{\psi }$ is admissible in L if and only if either $\varphi _{1}\wedge \ldots \wedge \varphi _{n}$ is not unifiable, or the substitutions that belong to a minimal complete set of unifiers of $\varphi _{1}\wedge \ldots \wedge \varphi _{n}$ are unifiers of $\psi$.

In accordance with their capacity to talk about relational structures, normal modal logics like epistemic logics, or temporal logics are playing a fundamental role in many applications. By virtue of its close relationships with the admissibility problem, the unification problem lies at the heart of their mechanization. For this reason, as advocated by Babenyshev et al. [7], investigations in the unification problem in normal modal logics can greatly contribute to the development of their applications. Regarding the unification problem in normal modal logics, we usually distinguish between elementary unification and unification with constants. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with constants, some variables — called constants — remain unchanged. In normal modal logics extending KD, the elementary unification problem can be decided in nondeterministic polynomial time, seeing that one can easily decide whether a given variable-free formula is equivalent to $\bot$, or is equivalent to $\top$. In many transitive normal modal logics like K4, solving the elementary unification problem is more difficult. In some other normal modal logics like K, it is even unknown whether the elementary unification problem is decidable. As for the unification problem with constants, it is not known to be decidable even for a simple normal modal logic such as $Alt_{1}$. The truth is that the unification problem with constants is only known to be decidable for a limited number of transitive normal modal logics like K4. In many cases, the decidability of the unification problem is a consequence of the decidability of the corresponding admissibility problem. See [23, 24, 29, 36,37,38,39,40] for details.

Concerning the unification types of normal modal logics, it is known that S5 is unitary [3], KT is nullary [8], KD is nullary [9], $Alt_{1}$ is nullary [11], S4.3 is unitary [19], transitive normal modal logics like K4 are finitary [24] and K is nullary [30], though the nullariness character of KT and KD has only been obtained within the context of unification with constants. For some other normal modal logics such as the normal extensions of K4, they are filtering — therefore they are unitary, or nullary — if and only if they contain the modal translation of the weak law $\lnot p\vee \lnot \lnot p$ of the excluded middle [26]. Taking a look at the literature about unification types in normal modal logics [3, 17, 26], one will quickly notice that much remains to be done. For instance, the types of symmetric normal modal logics like KB, KTB and KDB and the types of Church-Rosser normal modal logics like KG, KTG and KDG are unknown. Even the types of simple normal modal logics such as $K+\Box ^{k}\bot$ are unknown when $k\in \mathbb {N}$ is such that $k\ge 2$. In his proof that K is nullary, Jer̆ábek [30] has taken the formula $(x\rightarrow \Box x)$ and has shown that it has no minimal complete set of unifiers. In this respect, he has mainly used the following properties of the modality $\Box$: for all $k,l\in \mathbb {N}$, if $(\Box ^{l}\bot \rightarrow \Box ^{k}\bot )\in K$ then $l\le k$; for all formulas $\psi$ and for all $k\in \mathbb {N}$, if $(\psi \rightarrow \Box \psi )\in K$ and $\deg (\psi )\le k$ then $\psi \in K$, or $(\psi \rightarrow \Box ^{k}\bot )\in K$. Since for all $k\in \mathbb {N}$, $\lnot \Box ^{k}\bot \in KD$, therefore the adaptation of Jer̆ábek’s argument to KT and KD is not straightforward. It has been done in [8, 9] by taking the formula $(x\rightarrow p)\wedge (y\rightarrow q)\wedge (x\rightarrow \Box (q\rightarrow y))\wedge (y\rightarrow \Box (p\rightarrow x))$ in the case of KT and by taking the formula $(x\rightarrow p)\wedge (x\rightarrow \Box (p\rightarrow x))$ in the case of KD.

In this talk, we will give a survey of the results on unification in modal logic and we will present some of the open problems whose solution will have a great impact on the future of the area. After an introductory part about unification in equational theories, we will consider the case of Boolean unification [1, 31], we will study the unification problem in Intuitionistic Propositional Logic and transitive normal modal logics like K4 [21,22,23, 36, 37], we will introduce the notions of projective and transparent unifiers [16,17,18,19, 24] and we will define filtering unification [26]. Then, we will present the latest results obtained within the context of unification in description logics [2, 4, 5, 20] and in multimodal, tense and epistemic logics [6, 10, 12, 16].

Special acknowledgement is heartily granted to Çiğdem Gencer (Istanbul Aydın University, Turkey), Mojtaba Mojtahedi (Tehran University, Iran), Maryam Rostamigiv (Toulouse University, France) and Tinko Tinchev (Sofia University, Bulgaria) for their feedback: their useful suggestions have been essential for improving a preliminary versions of this talk.