# One-Variable Unification in K

Stéphane P. Desarzens

► To cite this version:

Stéphane P. Desarzens. One-Variable Unification in K. UNIF 2023 - 37th International Workshop on Unification, Veena Ravishankar; Christophe Ringeissen, Jul 2023, Rome, Italy. hal-04128048v2

HAL Id: hal-04128048

https://inria.hal.science/hal-04128048v2

Submitted on 27 Jun 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# One-Variable Unification in K

Stéphane P. Desarzens

University of Bern, Switzerland
stephane.desarzens@unibe.ch

## Abstract

We give an algorithm which decides unifiability in the modal logic K of single variable formulas of modal degree one. For this we introduce a finite Kripke frame which characterises unifiability for such formulas. We also present an example suggested to the author by E. Jeřábek, showing that this approach does not directly generalise to multiple variables.

## 1 Introduction

The question whether there exists an effective algorithm which decides for modal formulas if they are unifiable in the modal logic K has been called “the big open problem for unification in modal logics.” [1] Two main motivations for studying this problem are to understand admissible inference rules in K and to solve unification problems with constants in description logics like ALC.

It has been shown that no such algorithm exists if K is extended by the universal modality [7], and that the unification type of K is nullary [6]. The latter paper also shows that the techniques that were used in [5] to study the same question for transitive modal logics do not directly apply to K.

Our approach to the problem tries to use the observation that a formula $\varphi$ is unifiable in K iff for every Kripke frame $F$ there is a ground-definable valuation $V$ on $F$ which makes $\varphi$ true at every point of $F$. For formulas of modal degree one in one variable we present a finite frame which characterises unifiability using this approach. An example of Jeřábek shows that a similar technique does not work in the case of two variables and non-zero modal degree.

## 2 Preliminaries

We fix the notation and recall some facts about modal logic, referring the reader to [2] for further details. We build the set $Fm$ of (modal) formulas inductively as follows: for each $n \in \mathbb{N}$ the propositional variable $p_n$ is in $Fm$, the constant symbol $\top$ is in $Fm$, and if $\varphi, \psi \in Fm$ then $\neg\varphi, \varphi \wedge \psi, \Box\varphi \in Fm$. For $\varphi, \psi \in Fm$ we define the notations $\perp := \neg\top, \varphi \lor \psi := \neg(\neg\varphi \wedge \neg\psi), \varphi \rightarrow \psi := \neg\varphi \lor \psi, \varphi \leftrightarrow \psi := (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)$ and $\diamond\varphi := \neg\Box\neg\varphi$.

We define $\text{md}: Fm \rightarrow \mathbb{N}$, the modal degree of a formula, recursively by $\text{md}(p_n) := \text{md}(\top) := 0$ for all $n \in \mathbb{N}$, $\text{md}(\neg\varphi) := \text{md}(\varphi)$, $\text{md}(\varphi \wedge \psi) := \max(\text{md}(\varphi), \text{md}(\psi))$ and $\text{md}(\Box\varphi) := \text{md}(\varphi) + 1$ for all $\varphi, \psi \in Fm$.

For a set $L \subseteq \{p_n | n \in \mathbb{N}\}$ and $n \in \mathbb{N}$, let $Fm(L, n)$ be the set of modal formulas with variables in $L$ of modal degree at most $n$.

A Kripke frame is a pair $(F, R)$ where $F$ is a set and $R$ is a binary relation on $F$. We will only write $F$ for the Kripke frame $(F, R)$ if the relation is clear from the context.

A valuation on a Kripke frame $F$ is a map $V: \{p_n | n \in \mathbb{N}\} \rightarrow \mathcal{P}(F)$. For a Kripke frame $F$ with relation $R$ and a valuation $V$ on $F$, we define what it means for a formula $\varphi$
to be true at a point $w \in F$, written $\langle F, V \rangle$, $w \Vdash \varphi$, recursively by

$$ \langle F, V \rangle, w \Vdash p_n \text{ iff } w \in V(p_n) $$

$$ \langle F, V \rangle, w \Vdash \top \text{ holds for all } w $$

$$ \langle F, V \rangle, w \Vdash \neg \varphi \text{ iff not } \langle F, V \rangle, w \Vdash \varphi $$

$$ \langle F, V \rangle, w \Vdash \varphi \wedge \psi \text{ iff } \langle F, V \rangle, w \Vdash \varphi \text{ and } \langle F, V \rangle, w \Vdash \psi $$

$$ \langle F, V \rangle, w \Vdash \Box \varphi \text{ iff for all } v \in F, \text{Rwv implies } \langle F, V \rangle, v \Vdash \varphi $$

A pair $\langle F, V \rangle$, where $F$ is a Kripke frame and $V$ is a valuation on $F$, is called a *Kripke model*. A formula $\varphi$ is called *valid* (in K) if $\langle F, V \rangle$, $w \Vdash \varphi$ for all frames $F$, valuations $V$ on $F$ and $w \in F$. Two formulas $\varphi, \psi \in Fm$ are called *equivalent* if the formula $\varphi \leftrightarrow \psi$ is valid.

A *substitution* is a map $\sigma: Fm \to Fm$ which commutes with all connectives. Each substitution is uniquely determined by its values on propositional variables, thus when defining a substitution we will only specify how it acts on these and use $p$ to denote an arbitrary variable. For example $(p \mapsto \diamond \top \wedge p_0)$ denotes the substitution $\sigma$ which satisfies $\sigma(p_n) = \diamond \top \wedge p_0$ for all $n \in \mathbb{N}$.

A formula $\varphi$ is *unified* by a substitution $\sigma$ if $\sigma(\varphi)$ is valid. In this case $\sigma$ is called a unifier of $\varphi$. A formula which has a unifier is called unifiable.

A formula is called *ground* if it does not contain any variables. Note that for $F$ a Kripke frame and $\varphi$ a ground formula, the truth of $\varphi$ at $w \in F$ does not depend on the valuation on $F$. So the notation $F, w \Vdash \varphi$ is well-defined as $\langle F, V \rangle, w \Vdash \varphi$ for some/all valuations $V$ on $F$. A ground formula $\varphi$ is called *valid in the frame $F$*, if $F, w \Vdash \varphi$ for all $w \in F$. A substitution $\sigma$ is called *ground* if for all $n \in \mathbb{N}$ the formula $\sigma(p_n)$ is ground. Equivalently, a substitution $\sigma$ is ground iff $\sigma(\varphi)$ is ground for all formulas $\varphi$.

For a Kripke frame $F$ and a ground substitution $\sigma$, we define the valuation $V_\sigma$ on $F$ by $V_\sigma(p) := \{w \in F \mid F, w \Vdash \sigma(p)\}$ for each variable $p$.

**Lemma 2.1** (Special case of [2, Lemma 3.25]). Let $F$ be a Kripke frame, $w \in F$. For any ground substitution $\sigma$ and formula $\varphi$ we have $F, w \Vdash \sigma(\varphi)$ iff $\langle F, V_\sigma \rangle, w \Vdash \varphi$.

The following observation inspired our approach to the problem.

**Proposition 2.2.** A formula $\varphi \in Fm$ is unifiable iff for every Kripke frame $F$ there exists a ground substitution $\sigma$ such that for all $w \in F$, $\langle F, V_\sigma \rangle, w \Vdash \varphi$.

*Proof.* The implication from left to right follows directly using Lemma 2.1. For the converse direction, let $F$ be a frame such that a ground formula $\psi \in Fm$ is valid iff $F, w \Vdash \psi$ for all $w \in F$. For example $F$ may be the frame of the canonical model of K or the disjoint union of all frames $F(\emptyset, n)$ which are described later. If $\sigma$ is a ground substitution with $\langle F, V_\sigma \rangle, w \Vdash \varphi$ for all $w \in F$, we obtain by Lemma 2.1 that $F, w \Vdash \sigma(\varphi)$ for all $w \in F$. Hence $\sigma(\varphi)$ is valid. $\square$

We recall the normal forms of K. Fine [3] and S. Ghilardi [4].

**Definition 2.3.** Let $X$ be a set. For each $n \in \mathbb{N}$ define the set $T_n^X$ of $X$-labelled (commutative idempotent) trees of degree $n$ by $T_0^X := X$ and $T_{n+1}^X := X \times \mathcal{P}(T_n^X)$.

If $X = \mathcal{P}(L)$ for some finite $L \subseteq \{p_n \mid n \in \mathbb{N}\}$, we can interpret each $X$-labelled tree of finite degree as a modal formula as follows.

**Definition 2.4.** Let $L \subseteq \{p_n \mid n \in \mathbb{N}\}$ be a finite set. For each $n \in \mathbb{N}$ define $\iota_n: T_n^{\mathcal{P}(L)} \to Fm(L, n)$ by

$$ \iota_0: T_0^{\mathcal{P}(L)} \to Fm(L, 0); A \mapsto \bigwedge_{p \in A} p \wedge \bigwedge_{p \in L \setminus A} \neg p, $$

$$ \iota_{n+1}: T_{n+1}^{\mathcal{P}(L)} \to Fm(L, n+1); \langle A, B \rangle \mapsto \iota_0(A) \wedge \bigwedge_{t \in B} \diamond \iota_n(t) \wedge \Box \bigvee_{t \in B} \iota_n(t). $$
Note that for each $\langle A, B \rangle \in T_{n+1}^{\mathcal{P}(L)}$ the formula $\iota_{n+1}(\langle A, B \rangle)$ is equivalent to $\iota_0(A) \wedge \bigwedge_{t \in B} \diamond \iota_n(t) \wedge \bigwedge_{t \in T_n^{\mathcal{P}(L)} \setminus B} \neg \diamond \iota_n(t)$. We require $L$ to be finite, because otherwise $\iota_0$ would not be well-defined.

This construction has the following properties:

**Theorem 2.5 ([3, 4])**. Let $L$ be a finite subset of $\{p_n \mid n \in \mathbb{N}\}$.

(1) For each Kripke frame $F$, valuation $V$ on $F$, $w \in F$ and $n \in \mathbb{N}$ there exists a unique $t \in T_n^{\mathcal{P}(L)}$ such that $\langle F, V \rangle, w \models \iota_n(t)$.

(2) For each $n \in \mathbb{N}$ there is a Kripke model $F(L, n)$ whose set of points is $T_n^{\mathcal{P}(L)}$, such that for each $t \in T_n^{\mathcal{P}(L)}$ we have $F(L, n), t \models \iota_n(t)$.

(3) For each formula $\varphi$ with variables in $L$ there exists a set $\Phi \subseteq T_{\mathrm{md}(\varphi)}^{\mathcal{P}(L)}$ such that $\bigvee_{t \in \Phi} \iota_{\mathrm{md}(\varphi)}(t)$ is equivalent to $\varphi$.

*Proof sketch of (1).* Let $R$ be the relation of the frame $F$ and proceed by induction on $n$. For $n=0$ set $t := \{p_i \in L \mid w \in V(p_i)\}$. For the inductive step set $t := \{\langle p_i \in L \mid w \in V(p_i) \rangle, \{t \in T_n^{\mathcal{P}(L)} \mid \langle F, V \rangle, v \models \iota_n(t) \text{ and } R w v \text{ for some } v \in F \}\}$. Correctness and uniqueness of this construction is straightforward to check. $\square$

Note that [3] presented Theorem 2.5 (2) using a Kripke model whose set of points is $\bigcup_{k \le n} T_k^{\mathcal{P}(L)}$. We omit how the model needs to be adapted to obtain the statement presented here.

We introduce the following notation for elements of $T_n^X$ to remove some of the notational burden and to simplify the computation of “is $\iota_n(t)$ true at a given point of a Kripke model?” for $t \in T_n^{\mathcal{P}(L)}$ represented in this notation. For $t \in T_0^X$ we write $\boxed{t}$. For

$\langle l, \{t_1, \dots, t_k\} \rangle \in T_{n+1}^X$ we write $\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}] 
  
  \node (l) at (0,0) {};
  \node (r) at (4,0) {};
  \draw (l) -- (r);
  \node at (0.5,0.5) {$l$};
  \node at (3.5,0.5) {$t_1$};
  \node at (0.5,-0.5) {$t_1$};
  \node at (3.5,-0.5) {$t_k$};
  \draw[->] (l) -- (r);
\end{tikzpicture}$ where each $t_i$ is written using this notation.

For example for $X = \{a, b, c, d\}$ we write $\langle a, \{\langle a, \{b, c\}\rangle, \langle d, \emptyset\rangle\} \rangle \in T_2^X$ as

<figure><img src="image_2.png" /></figure>

If $X = \mathcal{P}(\{p_0\})$, instead of labelling the nodes with $\emptyset$ and $\{p_0\}$ we colour them white and black respectively. For example we write $\langle \{p_0\}, \{\langle \emptyset, \emptyset \rangle, \langle \emptyset, \{\emptyset, \{p_0\}\} \rangle \rangle \rangle \in T_2^{\mathcal{P}(\{p_0\})}$ as

<figure><img src="image_3.png" /></figure>

## 3 Unifiability of one-variable formulas of degree one

We first introduce sets of trees which characterise being unified by a given substitution. Then we slightly modify the frame $F(\emptyset, 2)$ to obtain the frame $F$ with which we can characterise unifiability of one-variable formulas of degree one.

For each finite $L \subseteq \{p_n \mid n \in \mathbb{N}\}$, ground substitution $\sigma$ and $n \in \mathbb{N}$ we can compute a set $\Phi(L, \sigma, n) \subseteq T_n^{\mathcal{P}(L)}$ with the property that for each set $\Psi \subseteq T_n^{\mathcal{P}(L)}$, the formula $\bigvee \iota_n[\Psi]$ is unified by $\sigma$ iff $\Phi(L, \sigma, n) \subseteq \Psi$. For example we can compute that

$$ \Phi(\{p_0\}, p \mapsto \top, 1) = \{ \bullet, \bullet \rightarrow \Box \}, $$

$$ \Phi(\{p_0\}, p \mapsto \Box \bot, 1) = \{ \bullet, \circ \rightarrow \Box, \circ \rightarrow \Box, \circ \rightarrow \Box \}. $$
Write $T_2^{\mathcal{P}(\emptyset)} = \{a, b, c, d\}$ such that $a = \langle \emptyset, \emptyset \rangle$, $b = \langle \emptyset, \{a, d\} \rangle$, $c = \langle \emptyset, \{d\} \rangle$ and $d = \langle \emptyset, \{a\} \rangle$. Then the frame $F(\emptyset, 2)$ looks as depicted in Figure 1. For the rest of this section, let $F = \langle T_2^{\mathcal{P}(\emptyset)}, R \rangle$ be the Kripke frame with the relation $R = \{\langle b, b \rangle, \langle b, a \rangle, \langle d, a \rangle, \langle c, c \rangle\}$. This frame is depicted in Figure 2. Note that $F, t \models \iota_2(t)$ for all $t \in T_2^{\mathcal{P}(\emptyset)}$.

<figure><img src="image_4.png" /><figcaption>Figure 1: The frame $F(\emptyset, 2)$</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 2: The frame $F$</figcaption></figure>

**Theorem 3.1.** Let $\varphi$ be a formula of modal degree one such that the only variable occurring in $\varphi$ is $p_0$. The following are equivalent:

(1) $\varphi$ is unifiable.

(2) $\varphi$ is unified by a ground substitution $\sigma$ for which $\sigma(p_0)$ has degree at most one.

(3) $\varphi$ is unified by one of the following substitutions: $p \mapsto \top$, $p \mapsto \bot$, $p \mapsto \Box\bot$, $p \mapsto \Diamond\top$.

(4) There is a valuation $V$ on $F$ such that for all $w \in F$ we have $\langle F, V \rangle$, $w \models \varphi$.

This theorem gives two ways of deciding whether a one-variable formula of modal degree one is unifiable. First, since validity in $K$ is decidable, it is decidable whether a given substitution unifies a given formula. Hence (3) can be used to decide unifiability. Second, truth of a formula at a point of a Kripke model is decidable and there are only finitely many valuations on the frame $F$, since $F$ is finite. Hence (4) can also be used to decide unifiability.

*Proof.* The implications (3) ⇒ (2) ⇒ (1) are trivial. For (1) ⇒ (4) let $\sigma$ be a substitution which unifies $\varphi$ and $\tau$ any ground substitution. We claim that the valuation $V_{\tau\circ\sigma}$ on $F$ has the desired property. Let $w \in F$. Since $\sigma$ unifies $\varphi$ we have $\langle F, V_\tau \rangle$, $w \models \sigma(\varphi)$. Hence by Lemma 2.1, $F, w \models \tau(\sigma(\varphi))$. Applying Lemma 2.1 again yields $\langle F, V_{\tau\circ\sigma} \rangle$, $w \models \varphi$ as desired.

The hard part of the proof is (4) ⇒ (3). Assume that $V$ is a valuation on the frame $F$ such that $\langle F, V \rangle$, $w \models \varphi$ for all $w \in F$. We make the following claims, from which (3) follows immediately:

(a) if $a \in V(p_0)$ then $\varphi$ is unified by $p \mapsto \top$ or $p \mapsto \Box\bot$,

(b) if $a \notin V(p_0)$ then $\varphi$ is unified by $p \mapsto \bot$ or $p \mapsto \Diamond\top$.

We first prove (a). By Theorem 2.5, there is a set $\Phi \subseteq T_1^{\mathcal{P}(\{p_0\})}$ such that $\bigvee \iota_1[\Phi]$ is equivalent to $\varphi$. We obtain $\langle F, V \rangle$, $w \models \bigvee \iota_1[\Phi]$ for all $w \in F$. By the definition of truth at a point, there must be for each $w \in F$ some $t_w \in \Phi$ with $\langle F, V \rangle$, $w \models \iota_1(t_w)$.

For each $w \in F$ there is some unique $Q_w \in \mathcal{P}(\{p_0\}) = T_0^{\mathcal{P}(\{p_0\})}$ such that $\langle F, V \rangle$, $w \models \iota_0(Q_w)$. By Theorem 2.5 (1), the $t_w$ are uniquely determined by $\langle F, V \rangle$. So we can retrace the existence part of the proof of Theorem 2.5 (1) to compute

$$t_a = \boxed{Q_a}, \quad t_b = \boxed{\begin{array}{@{}c@{\quad}c@{}} \boxed{Q_b} & \boxed{Q_a} \\ \diagdown & \diagup \end{array}}, \quad t_c = \boxed{Q_c} \rightarrow \boxed{Q_c}, \quad t_d = \boxed{Q_d} \rightarrow \boxed{Q_a} \in \Phi.$$

Since $a \in V(p_0)$, it follows that $Q_a = \{p_0\}$. If $Q_b = \{p_0\}$ or $Q_c = \{p_0\}$ or $Q_d = \{p_0\}$ then $\Phi(\{p_0\}, p \mapsto \top, 1) \subseteq \{t_a, t_b, t_c, t_d\} \subseteq \Phi$ and hence $\bigvee \iota_1[\Phi]$ and $\varphi$ are unified by $p \mapsto \top$. Otherwise $Q_b = Q_c = Q_d = \emptyset$ and $\Phi(\{p_0\}, p \mapsto \Box\bot, 1) = \{t_a, t_b, t_c, t_d\} \subseteq \Phi$ and hence $\bigvee \iota_1[\Phi]$ and $\varphi$ are unified by $p \mapsto \Box\bot$. In either case (a) follows.

One can prove (b) using an analogous approach, considering $\Phi(\{p_0\}, p \mapsto \bot, 1)$ and $\Phi(\{p_0\}, p \mapsto \Diamond\top, 1)$ instead. In addition, we present an alternate proof which uses (a).
Assume that $a \notin V(p_0)$. Let $\tau$ be the substitution satisfying $\tau(p_n) = \neg p_n$ for all $n \in \mathbb{N}$. The valuation $V'$ on $F$, defined by $V'(p_n) := F \setminus V(p_n)$ for all $n \in \mathbb{N}$, has the property that $\langle F, V' \rangle, w \Vdash \tau(\varphi)$ for all $w \in F$. Since $a \in V'(p_0)$, we can apply (a) to obtain that $\tau(\varphi)$ is unified by $p \mapsto \top$ or $p \mapsto \Box\bot$. Note that for every unifier $\sigma$ of $\tau(\varphi)$, the substitution $\sigma \circ \tau$ is a unifier of $\varphi$. Hence $\varphi$ is unified by $(p \mapsto \top) \circ \tau = (p \mapsto \bot)$ or $(p \mapsto \Box\bot) \circ \tau = (p \mapsto \diamond\top)$. $\Box$

**Remark 3.2.** The above theorem is applicable precisely to the formulas that can be represented via **Theorem 2.5 (3)** as subsets of $T_1^{P(\{p_0\})}$. Elementary computations show that there are up to equivalence $2^8 = 256$ such formulas.

It might be, that one can obtain similar results for formulas of higher degrees in one variable, by adapting the relation of $F(\emptyset, n)$ for large enough $n$.

**Example 3.3.** The formula $q \leftrightarrow \neg\Box q$ is not unifiable, because for all valuations $V$ on $F$ we have $\langle F, V \rangle$, $c \Vdash q \leftrightarrow \neg\Box q$. Indeed, if $c \in V(q)$ then $\langle F, V \rangle$, $c \Vdash q$ and $\langle F, V \rangle$, $c \Vdash \neg\Box q$, and if $c \notin V(q)$ then $\langle F, V \rangle$, $c \Vdash q$ and $\langle F, V \rangle$, $c \Vdash \neg\Box q$.

# 4 Beyond one variable

Above, we described a finite frame $F$ such that each $\varphi \in Fm(\{p_0\}, 1)$ is unifiable iff there is a valuation on $F$ which makes $\varphi$ true at every point of $F$. An example of Jeřábek<fnref n="1" /> shows that we cannot find a similar finite frame for the two variable case of degree one. We repeat his proofs here. Let $p, q$ be any two distinct propositional variables. Consider the formula $\varphi := (\Box p \rightarrow p) \wedge (p \rightarrow (q \leftrightarrow \neg\Box q))$ and the following propositions.

**Proposition 4.1.** The formula $\varphi$ is not unifiable.

**Proposition 4.2.** For every finite frame $F$ there exists a ground substitution $\sigma$ such that for all $w \in F$ we have $\langle F, V_\sigma \rangle, w \Vdash \varphi$.

To prove these results, we need an intermediate result. Define the sequence $(\xi_i)_{i \in \mathbb{N}} \subseteq Fm$ by $\xi_0 := \bot$ and $\xi_{i+1} := \neg\Box\xi_i$ for each $i \in \mathbb{N}$.

**Proposition 4.3.** Let $F$ be a frame and $n \in \mathbb{N}$ such that for every $w \in F$ we have $F, w \Vdash \Box^n \bot$. Let $\sigma$ be a valuation with $\sigma(q) = \xi_n$. Then the valuation $V_\sigma$ makes $q \leftrightarrow \neg\Box q$ true at every point of $F$.

*Proof.* By induction on $n$. $\Box$

*Proof of Proposition 4.1.* Assume that $\sigma$ is a unifier of $\varphi$. Then $\sigma$ is a unifier of $\Box p \rightarrow p$ and of $p \rightarrow (q \leftrightarrow \neg\Box q)$. Thus $\Box\sigma(p) \rightarrow \sigma(p)$ is valid, which by Löb's rule implies that $\sigma(p)$ is valid. I.e., $\sigma$ is a unifier of $p$. Hence $\sigma$ is also a unifier of $q \leftrightarrow \neg\Box q$. But by **Example 3.3** this is impossible. $\Box$

*Proof of Proposition 4.2.* Let $F$ be a finite frame. Define $W_i := \{w \in F \mid F, w \Vdash \Box^i \bot\}$ for each $i \in \mathbb{N}$. Since $W_i \subseteq W_{i+1}$ for each $i \in \mathbb{N}$ and $F$ is finite, there exists $n \in \mathbb{N}$ such that $W_n = \bigcup_{i \in \mathbb{N}} W_i$. Note that $W_n$ is the largest converse well-founded generated subframe of $F$. Now the substitution $\sigma$ defined by $\sigma(p) := \Box^n \bot$ and $\sigma(q) := \xi_n$ has the desired property. Indeed, $\Box^{n+1} \bot \rightarrow \Box^n \bot$ is valid in $F$. By **Proposition 4.3** and **Lemma 2.1**, $\xi_n \leftrightarrow \neg\Box\xi_n$ is valid in $W_n$. This precisely means that $\Box^n \bot \rightarrow (\xi_n \leftrightarrow \neg\Box\xi_n)$ is valid in $F$. Hence $(\Box^{n+1} \bot \rightarrow \Box^n \bot) \wedge (\Box^n \rightarrow (\xi_n \leftrightarrow \neg\Box\xi_n)) = \sigma(\varphi)$ is valid in $F$ as claimed. $\Box$

<footnote n="1">¹Emil Jeřábek. *Existence of certain formulas in modal logic*. K. MathOverflow. Version: 2023-03-06. URL: https://mathoverflow.net/q/442159. Answering a question posed by the author.</footnote>
References

[1] Franz Baader and Silvio Ghilardi. 'Unification in Modal and Description Logics'. In: *Logic Journal of the IGPL* 19.6 (2011), pp. 705-730. DOI: 10.1093/jigpal/jzq008.

[2] Patrick Blackburn, Maarten de Rijke and Yde Venema. *Modal Logic*. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. DOI: 10.1017/CBO9781107050884.

[3] Kit Fine. 'Normal forms in modal logic.' In: *Notre Dame Journal of Formal Logic* 16.2 (1975), pp. 229-237. DOI: 10.1305/ndjfl/1093891703.

[4] Silvio Ghilardi. 'An algebraic theory of normal forms'. In: *Annals of Pure and Applied Logic* 71.3 (1995), pp. 189-245. ISSN: 0168-0072. DOI: 10.1016/0168-0072(93)E0084-2.

[5] Silvio Ghilardi. 'Best Solving Modal Equations'. In: *Annals of Pure and Applied Logic* 102.3 (2000), pp. 183-198. DOI: 10.1016/s0168-0072(99)00032-9.

[6] Emil Jeřábek. 'Blending margins: the modal logic K has nullary unification type'. In: *Journal of Logic and Computation* 25.5 (Oct. 2013), pp. 1231-1240. ISSN: 0955-792X. DOI: 10.1093/logcom/ext055.

[7] Frank Wolter and Michael Zakharyaschev. 'Undecidability of the Unification and Admissibility Problems for Modal and Description Logics'. In: *ACM Trans. Comput. Logic* 9.4 (Aug. 2008). ISSN: 1529-3785. DOI: 10.1145/1380572.1380574.