About the unification type of simple symmetric modal logics

TL;DR

This paper investigates the unification problem in simple symmetric modal logics, demonstrating that certain logics like KB, KDB, and KTB contain formulas with no minimal complete set of unifiers, called nullary formulas.

Contribution

It establishes the existence of nullary formulas in specific simple symmetric modal logics, advancing understanding of unification properties in these systems.

Findings

KB, KDB, and KTB have nullary formulas

Nullary formulas lack minimal complete unifier sets

Results deepen the understanding of unification in modal logics

Abstract

The unification problem in a normal modal logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. We shall say that a set of unifiers of a unifiable formula F is complete if for all unifiers s of F, there exists a unifier t of F in that set such that t is more general than s. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. In this paper, we prove that KB, KDB and KTB possess nullary formulas.

Full text

1 Introduction

The unification problem in a normal modal logic is to determine, given a formula $\varphi$, whether there exists a substitution $\sigma$ such that $\sigma(\varphi)$ is in that logic. In that case, $\sigma$ is a unifier of $\varphi$. 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 [1, 16]: 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 unitary, or finitary, or infinitary depending on the cardinalities of its minimal complete sets of unifiers. A normal modal logic is called nullary if it possesses a nullary formula. Otherwise, it is called unitary, or finitary, or infinitary depending on the types of its unifiable formulas. We usually distinguish between elementary unification and unification with parameters. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with parameters, some variables — called parameters — remain unchanged.

It is known that $\mathbf{S}{5}$ is unitary [1], $\mathbf{KT}$ is nullary [6], $\mathbf{KD}$ is nullary [7], $\mathbf{Alt}_{1}$ is nullary [9], $\mathbf{S}{4.3}$ is unitary [18], transitive normal modal logics like ${\mathbf{K}}4$ are finitary [22] and $\mathbf{K}$ is nullary [26], though the nullariness character of $\mathbf{KT}$ and $\mathbf{KD}$ has only been obtained within the context of unification with parameters. Taking a look at the literature about unification types in normal modal logics [1, 16], one will quickly notice that much remains to be done. For instance, the types of simple Church-Rosser normal modal logics like $\mathbf{KG}$, $\mathbf{KDG}$ and $\mathbf{KTG}$ are unknown111In this paper, we follow the same conventions as in [11, 12, 13] for talking about normal modal logics: $\mathbf{S}{5}$ is the least normal modal logic containing the formulas usually denoted $(\mathbf{T})$, $(\mathbf{4})$ and $(\mathbf{B})$, $\mathbf{KT}$ is the least normal modal logic containing the formula usually denoted $(\mathbf{T})$, etc.. Even, for all $k\in\mathbb{N}$ such that $k\geq 2$, the type of the least normal modal logic containing $\Box^{k}\bot$ is unknown. In this paper, we adapt to $\mathbf{KB}$, $\mathbf{KDB}$ and $\mathbf{KTB}$ the argument of Jer̆ábek [26] showing $\mathbf{K}$ is nullary, though the nullariness character of $\mathbf{KB}$, $\mathbf{KDB}$ and $\mathbf{KTB}$ will only be obtained within the context of unification with parameters. We assume the reader is at home with tools and techniques in modal logic. For more on this, see Blackburn et al. [11], or Chagrov and Zakharyaschev [12], or Chellas [13].

2 Syntax

In this section, we present the syntax of normal modal logics.

Formulas

Let $\mathit{VAR}$ be a nonempty countable set of propositional variables (with typical members denoted $x$, $y$, etc) and $\mathit{PAR}$ be a nonempty countable set of propositional parameters (with typical members denoted $p$, $q$, etc). Atoms (denoted $\alpha$, $\beta$, etc) are variables or parameters. The set $\mathit{FOR}$ of all formulas (with typical members denoted $\varphi$, $\psi$, etc) is inductively defined as follows:

• •

$\varphi,\psi::=x\mid p\mid\bot\mid\neg\varphi\mid(\varphi\vee\psi)\mid\Box\varphi$.

We adopt the standard rules for omission of the parentheses. The Boolean connectives $\top$, $\wedge$, $\rightarrow$ and $\leftrightarrow$ are defined by the usual abbreviations. For all parameters $p$, we write “$p^{0}$” to mean “$\neg p$” and we write “$p^{1}$” to mean “$p$”. From now on,

[TABLE]

Let $\boxplus$ and $\boxminus$ be the modal connectives defined as follows:

• •

$\boxplus\varphi::=(p^{0}\wedge q^{0}\rightarrow\Box(p^{1}\wedge q^{0}\rightarrow\Box(p^{0}\wedge q^{1}\rightarrow\Box(p^{0}\wedge q^{0}\rightarrow\varphi))))$,

• •

$\boxminus\varphi::=(p^{0}\wedge q^{0}\rightarrow\Box(p^{0}\wedge q^{1}\rightarrow\Box(p^{1}\wedge q^{0}\rightarrow\Box(p^{0}\wedge q^{0}\rightarrow\varphi))))$.

For all $k\in\mathbb{N}$, the modal connectives $\boxplus^{k}$ and $\boxminus^{k}$ are inductively defined as follows:

• •

$\boxplus^{0}\varphi::=\varphi$,

• •

$\boxplus^{k+1}\varphi::=\boxplus\boxplus^{k}\varphi$,

• •

$\boxminus^{0}\varphi::=\varphi$,

• •

$\boxminus^{k+1}\varphi::=\boxminus\boxminus^{k}\varphi$.

For all $k\in\mathbb{N}$, the modal connectives $\boxplus^{<k}$ and $\boxminus^{<k}$ are inductively defined as follows:

• •

$\boxplus^{<0}\varphi::=\top$,

• •

$\boxplus^{<k+1}\varphi::=(\boxplus^{<k}\varphi\wedge\boxplus^{k}\varphi)$,

• •

$\boxminus^{<0}\varphi::=\top$,

• •

$\boxminus^{<k+1}\varphi::=(\boxminus^{<k}\varphi\wedge\boxminus^{k}\varphi)$.

Degrees

The degree of a formula $\varphi$ (in symbols $\deg(\varphi)$) is the nonnegative integer inductively defined as follows:

• •

$\deg(x)=0$,

• •

$\deg(p)=0$,

• •

$\deg(\bot)=0$,

• •

$\deg(\neg\varphi)=\deg(\varphi)$,

• •

$\deg(\varphi\vee\psi)=\max\{\deg(\varphi),\deg(\psi)\}$,

• •

$\deg(\Box\varphi)=\deg(\varphi)+1$.

Lemma 1

Let $\varphi$ be a formula.

$\deg(\boxplus(\varphi)=\deg(\varphi)+3$, 2. 2.

$\deg(\boxminus(\varphi)=\deg(\varphi)+3$, 3. 3.

for all $k\in\mathbb{N}$, $\deg(\boxplus^{k}\varphi)=\deg(\varphi)+3k$, 4. 4.

for all $k\in\mathbb{N}$, $\deg(\boxminus^{k}\varphi)=\deg(\varphi)+3k$, 5. 5.

for all $k\in\mathbb{N}$, if $k=0$ then $\deg(\boxplus^{<k}\varphi)=0$ else $\deg(\boxplus^{<k}\varphi)=\deg(\varphi)+3(k-1)$, 6. 6.

for all $k\in\mathbb{N}$, if $k=0$ then $\deg(\boxminus^{<k}\varphi)=0$ else $\deg(\boxminus^{<k}\varphi)=\deg(\varphi)+3(k-1)$.

Proof: $(1)$ and $(2)$: Left to the reader.

$(3)$–$(6)$: By induction on $k$.  $\dashv$

Substitutions

A substitution is a function $\sigma$ associating to each variable $x$ a formula $\sigma(x)$. Following the standard assumption considered in the literature about the unification problem in normal modal logics [1, 16], we will always assume that substitutions move at most finitely many variables. For all formulas $\varphi(x_{1},\ldots,x_{m},p_{1},\ldots,p_{n})$, let $\sigma(\varphi(x_{1},\ldots,x_{m},p_{1},\ldots,p_{n}))$ be $\varphi(\sigma(x_{1}),\ldots,\sigma(x_{m}),p_{1},\ldots,p_{n})$. The composition $\sigma\circ\tau$ of the substitutions $\sigma$ and $\tau$ is the substitution associating to each variable $x$ the formula $\tau(\sigma(x))$.

3 Semantics

In this section, we present the semantics of normal modal logics.

Frames and models

A frame is a couple $F=(W,R)$ where $W$ is a non-empty set of states and $R$ is a relation on $W$. We shall say that a frame $F=(W,R)$ is symmetric if for all $s,t\in W$, if $sRt$ then $tRs$. We shall say that a frame $F=(W,R)$ is serial if for all $s\in W$, there exists $t\in W$ such that $sRt$. We shall say that a frame $F=(W,R)$ is reflexive if for all $s\in W$, $sRs$. Remark that reflexive frames are serial. A model based on a frame $F=(W,R)$ is a triple $M=(W,R,V)$ where $V$ is a function assigning to each variable $x$ a subset $V(x)$ of $W$ and to each parameter $p$ a subset $V(p)$ of $W$. Given a model $M=(W,R,V)$, the satisfiability of a modal formula $\varphi$ at $s\in W$ (in symbols $M,s\models\varphi$) is inductively defined as follows:

• •

$M,s\models x$ iff $s\in V(x)$,

• •

$M,s\models p$ iff $s\in V(p)$,

• •

$M,s\not\models\bot$,

• •

$M,s\models\neg\varphi$ iff $M,s\not\models\varphi$,

• •

$M,s\models\varphi\vee\psi$ iff $M,s\models\varphi$, or $M,s\models\psi$,

• •

$M,s\models\Box\varphi$ iff for all $t\in W$, if $sRt$ then $M,t\models\varphi$.

Truth and validity

We shall say that a formula $\varphi$ is true in a model $M=(W,R,V)$ if $\varphi$ is satisfied at all $s\in W$. We shall say that a formula $\varphi$ is valid in a frame $F$ if $\varphi$ is true in all models based on $F$. We shall say that a formula $\varphi$ is valid in a class $C$ of frames if $\varphi$ is valid in all frames of $C$. Let $\mathbf{KB}$ be the set of all formulas valid in the class of all symmetric frames. Let $\mathbf{KDB}$ be the set of all formulas valid in the class of all serial symmetric frames. Let $\mathbf{KTB}$ be the set of all formulas valid in the class of all reflexive symmetric frames. Obviously, $\mathbf{KB}\subseteq\mathbf{KDB}\subseteq\mathbf{KTB}$. Moreover, $\mathbf{KB}$ is the least normal modal logic containing all formulas of the form $\neg\varphi\rightarrow\Box\neg\Box\varphi$, $\mathbf{KDB}$ is the least normal modal logic containing all formulas of the form $\Box\neg\varphi\rightarrow\neg\Box\varphi$ and $\neg\varphi\rightarrow\Box\neg\Box\varphi$ and $\mathbf{KTB}$ is the least normal modal logic containing all formulas of the form $\Box\varphi\rightarrow\varphi$ and $\neg\varphi\rightarrow\Box\neg\Box\varphi$. From now on,

[TABLE]

Lemma 2

For all $k\in\mathbb{N}$,

$\boxplus^{k}\top\in\mathbf{KB}$, 2. 2.

$\boxminus^{k}\top\in\mathbf{KB}$, 3. 3.

$\boxplus^{<k}\top\in\mathbf{KB}$, 4. 4.

$\boxminus^{<k}\top\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 3

For all $k\in\mathbb{N}$,

$\boxplus^{k}\bot\not\in\mathbf{KB}$, 2. 2.

$\boxminus^{k}\bot\not\in\mathbf{KB}$.

Proof: Let $k\in\mathbb{N}$. Let $F=(W,R)$ where $W=\{0,\ldots,3k\}$ and $R=\{(i,j):\ {\mid}j-i{\mid}\leq 1\}$. Let $M=(W,R,V)$ where $V(p)=\{i:\ i=1\mod 3\}$, $V(q)=\{i:\ i=2\mod 3\}$ and for all atoms $\alpha$, if $\alpha\not=p$ and $\alpha\not=q$ then $V(\alpha)=\emptyset$. The reader may easily verify that $M,0\not\models\boxplus^{k}\bot$ and $M,3k\not\models\boxminus^{k}\bot$. Hence, $\boxplus^{k}\bot\not\in\mathbf{KB}$ and $\boxminus^{k}\bot\not\in\mathbf{KB}$.  $\dashv$

In the proof of Lemma 3, remark that the frame $F=(W,R)$ is reflexive.

Lemma 4

Let $\varphi$ be a formula. For all $k\in\mathbb{N}$,

$(\boxplus^{<k+1}\varphi\leftrightarrow\varphi\wedge\boxplus\boxplus^{<k}\varphi)\in\mathbf{KB}$, 2. 2.

$(\boxminus^{<k+1}\varphi\leftrightarrow\varphi\wedge\boxminus\boxminus^{<k}\varphi)\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 5

For all $k,l\in\mathbb{N}$,

if $k>l$ then $(\boxplus^{k}\bot\rightarrow\boxplus^{l}\bot)\not\in\mathbf{KB}$, 2. 2.

if $k>l$ then $(\boxminus^{k}\bot\rightarrow\boxminus^{l}\bot)\not\in\mathbf{KB}$.

Proof: Let $k\in\mathbb{N}$. Suppose $k>l$. Let $F=(W,R)$ where $W=\{0,\ldots,3l\}$ and $R=\{(i,j):\ {\mid}j-i{\mid}\leq 1\}$. Let $M=(W,R,V)$ where $V(p)=\{i:\ i=1\mod 3\}$, $V(q)=\{i:\ i=2\mod 3\}$ and for all atoms $\alpha$, if $\alpha\not=p$ and $\alpha\not=q$ then $V(\alpha)=\emptyset$. The reader may easily verify that $M,0\not\models(\boxplus^{k}\bot\rightarrow\boxplus^{l}\bot)$ and $M,3l\not\models(\boxminus^{k}\bot\rightarrow\boxminus^{l}\bot)$. Hence, $(\boxplus^{k}\bot\rightarrow\boxplus^{l}\bot)\not\in\mathbf{KB}$ and $(\boxminus^{k}\bot\rightarrow\boxminus^{l}\bot)\not\in\mathbf{KB}$.  $\dashv$

In the proof of Lemma 5, remark that the frame $F=(W,R)$ is reflexive.

Lemma 6

For all formulas $\varphi$, $(\varphi\rightarrow\boxplus\varphi)\in\mathbf{KB}$ iff $(\neg\varphi\rightarrow\boxminus\neg\varphi)\in\mathbf{KB}$.

Proof: Let $\varphi$ be a formula such that $(\varphi\rightarrow\boxplus\varphi)\not\in\mathbf{KB}$ and $(\neg\varphi\rightarrow\boxminus\neg\varphi)\in\mathbf{KB}$, or $(\varphi\rightarrow\boxplus\varphi)\in\mathbf{KB}$ and $(\neg\varphi\rightarrow\boxminus\neg\varphi)\not\in\mathbf{KB}$.

— Case “$(\varphi\rightarrow\boxplus\varphi)\not\in\mathbf{KB}$ and $(\neg\varphi\rightarrow\boxminus\neg\varphi)\in\mathbf{KB}$”: Let $F=(W,R)$ be a frame, $M=(W,R,V)$ be a model based on $F$ and $s\in W$ be such that $M,s\not\models(\varphi\rightarrow\boxplus\varphi)$. Hence, $M,s\models\varphi$ and $M,s\not\models\boxplus\varphi$. Let $t,u,v\in W$ be such that $sRt$, $tRu$, $uRv$, $M,s\models p^{0}\wedge q^{0}$, $M,t\models p^{1}\wedge q^{0}$, $M,u\models p^{0}\wedge q^{1}$, $M,v\models p^{0}\wedge q^{0}$ and $M,v\not\models\varphi$. Thus, $tRs$, $uRt$ and $vRu$. Moreover, $M,v\models\neg\varphi$. Since $(\neg\varphi\rightarrow\boxminus\neg\varphi)\in\mathbf{KB}$, therefore $M,v\models(\neg\varphi\rightarrow\boxminus\neg\varphi)\in\mathbf{KB}$. Since $M,v\models\neg\varphi$, therefore $M,v\models\boxminus\neg\varphi$. Since $tRs$, $uRt$, $vRu$, $M,s\models p^{0}\wedge q^{0}$, $M,t\models p^{1}\wedge q^{0}$, $M,u\models p^{0}\wedge q^{1}$ and $M,v\models p^{0}\wedge q^{0}$, therefore $M,s\models\neg\varphi$. Consequently, $M,s\not\models\varphi$: a contradiction.

— Case “$(\varphi\rightarrow\boxplus\varphi)\in\mathbf{KB}$ and $(\neg\varphi\rightarrow\boxminus\neg\varphi)\not\in\mathbf{KB}$”: Let $F=(W,R)$ be a frame, $M=(W,R,V)$ be a model based on $F$ and $s\in W$ be such that $M,s\not\models(\neg\varphi\rightarrow\boxminus\neg\varphi)$. Hence, $M,s\models\neg\varphi$ and $M,s\not\models\boxminus\neg\varphi$. Let $t,u,v\in W$ be such that $sRt$, $tRu$, $uRv$, $M,s\models p^{0}\wedge q^{0}$, $M,t\models p^{0}\wedge q^{1}$, $M,u\models p^{1}\wedge q^{0}$, $M,v\models p^{0}\wedge q^{0}$ and $M,v\not\models\neg\varphi$. Thus, $tRs$, $uRt$ and $vRu$. Moreover, $M,v\models\varphi$. Since $(\varphi\rightarrow\boxplus\varphi)\in\mathbf{KB}$, therefore $M,v\models(\varphi\rightarrow\boxplus\varphi)\in\mathbf{KB}$. Since $M,v\models\varphi$, therefore $M,v\models\boxplus\varphi$. Since $tRs$, $uRt$, $vRu$, $M,s\models p^{0}\wedge q^{0}$, $M,t\models p^{0}\wedge q^{1}$, $M,u\models p^{1}\wedge q^{0}$ and $M,v\models p^{0}\wedge q^{0}$, therefore $M,s\models\varphi$. Consequently, $M,s\not\models\neg\varphi$: a contradiction.  $\dashv$

4 Unification

In this section, we present unification in $\mathbf{KB}$.

Unification problem

We shall say that a substitution $\sigma$ is equivalent to a substitution $\tau$ (in symbols $\sigma\simeq\tau$) if for all variables $x$, $(\sigma(x)\leftrightarrow\tau(x))\in\mathbf{KB}$. We shall say that a substitution $\sigma$ is more general than a substitution $\tau$ (in symbols $\sigma\preceq\tau$) if there exists a substitution $\upsilon$ such that $\sigma\circ\upsilon\simeq\tau$. Obviously, $\preceq$ contains $\simeq$. Moreover,

Proposition 1** (Baader and Ghilardi [1], Dzik [16])**

The binary relation $\simeq$ is reflexive, symmetric and transitive on the set of all substitutions, 2. 2.

the binary relation $\preceq$ is reflexive and transitive on the set of all substitutions.

We shall say that a set $\Sigma$ of substitutions is minimal if for all $\sigma,\tau\in\Sigma$, if $\sigma\preceq\tau$ then $\sigma\simeq\tau$. We shall say that a formula $\varphi$ is unifiable if there exists a substitution $\sigma$ such that $\sigma(\varphi)\in\mathbf{KB}$. In that case, $\sigma$ is a unifier of $\varphi$.

Proposition 2

Let $\varphi$ be a formula. For all unifiers $\sigma$ of $\varphi$, there exists a unifier $\tau$ of $\varphi$ such that $\tau\preceq\sigma$ and for all variables $x$, if $x$ does not occur in $\varphi$ then $\tau(x)=x$.

Proof: Left to the reader.  $\dashv$

We shall say that a set $\Sigma$ of unifiers of a unifiable formula $\varphi$ is complete if for all unifiers $\sigma$ of $\varphi$, there exists $\tau\in\Sigma$ such that $\tau\preceq\sigma$.

Unification types

An important question is the following: when a formula is unifiable, has it a minimal complete set of unifiers? When the answer is “yes”, how large is this set? We shall say that a unifiable formula

• •

$\varphi$ is nullary if there exists no minimal complete set of unifiers of $\varphi$,

• •

$\varphi$ is unitary if there exists a minimal complete set of unifiers of $\varphi$ with cardinality $1$,

• •

$\varphi$ is finitary if there exists a finite minimal complete set of unifiers of $\varphi$ but there exists no with cardinality $1$,

• •

$\varphi$ is infinitary if there exists a minimal complete set of unifiers of $\varphi$ but there exists no finite one.

5 Playing with substitutions

For all $k\in\mathbb{N}$, let $\sigma_{k}$ and $\tau_{k}$ be the substitutions inductively defined as follows:

• •

$\sigma_{0}(x)=\bot$,

• •

for all variables $y$ distinct from $x$, $\sigma_{0}(y)=y$,

• •

$\tau_{0}(x)=\top$,

• •

for all variables $y$ distinct from $x$, $\tau_{0}(y)=y$,

• •

$\sigma_{k+1}(x)=(x\wedge\boxplus\sigma_{k}(x))$,

• •

for all variables $y$ distinct from $x$, $\sigma_{k+1}(y)=y$,

• •

$\tau_{k+1}(x)=\neg(\neg x\wedge\boxminus\neg\tau_{k}(x))$,

• •

for all variables $y$ distinct from $x$, $\tau_{k+1}(y)=y$.

These substitutions will be used in Section 6 to prove that $\mathbf{KB}$ possesses nullary formulas.

Lemma 7

For all $k\in\mathbb{N}$,

$(\boxplus^{<k}x\wedge\boxplus^{k}\bot\rightarrow\sigma_{k}(x))\in\mathbf{KB}$, 2. 2.

$(\boxminus^{<k}\neg x\wedge\boxminus^{k}\bot\rightarrow\neg\tau_{k}(x))\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 8

For all $k\in\mathbb{N}$,

$(\sigma_{k}(x)\rightarrow x)\in\mathbf{KB}$, 2. 2.

$(\neg\tau_{k}(x)\rightarrow\neg x)\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 9

For all $k\in\mathbb{N}$,

$(\sigma_{k}(x)\rightarrow\boxplus\sigma_{k}(x))\in\mathbf{KB}$, 2. 2.

$(\neg\tau_{k}(x)\rightarrow\boxminus\neg\tau_{k}(x))\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 10

For all $k,l\in\mathbb{N}$,

if $k\leq l$ then $(\sigma_{k}(x)\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$, 2. 2.

if $k\leq l$ then $(\neg\tau_{k}(x)\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 11

For all $k,l\in\mathbb{N}$,

if $k>l$ then $(\sigma_{k}(x)\rightarrow\boxplus^{l}\bot)\not\in\mathbf{KB}$, 2. 2.

if $k>l$ then $(\neg\tau_{k}(x)\rightarrow\boxminus^{l}\bot)\not\in\mathbf{KB}$.

Proof: Let $k,l\in\mathbb{N}$.

$(1)$: Suppose $k>l$ and $(\sigma_{k}(x)\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$. Let $\upsilon$ be the substitution defined as follows:

• •

$\upsilon(x)=\top$,

• •

for all variables $y$ distinct from $x$, $\upsilon(y)=y$.

Since $(\sigma_{k}(x)\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$, therefore $(\upsilon(\sigma_{k}(x))\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$. By Lemma 7, $(\boxplus^{<k}x\wedge\boxplus^{k}\bot\rightarrow\sigma_{k}(x))\in\mathbf{KB}$. Hence, $(\boxplus^{<k}\upsilon(x)\wedge\boxplus^{k}\bot\rightarrow\upsilon(\sigma_{k}(x)))\in\mathbf{KB}$. Since $\upsilon(x)=\top$, therefore by Lemma 2, $(\boxplus^{k}\bot\rightarrow\upsilon(\sigma_{k}(x)))\in\mathbf{KB}$. Since $(\upsilon(\sigma_{k}(x))\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$, therefore $(\boxplus^{k}\bot\rightarrow\boxplus^{l}\bot)\in\mathbf{KB}$. Thus, by Lemma 5, $k\not>l$: a contradiction.

$(2)$: Suppose $k>l$ and $(\neg\tau_{k}(x)\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$. Let $\upsilon$ be the substitution defined as follows:

• •

$\upsilon(x)=\bot$,

• •

for all variables $y$ distinct from $x$, $\upsilon(y)=y$.

Since $(\neg\tau_{k}(x)\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$, therefore $(\upsilon(\neg\tau_{k}(x))\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$. By Lemma 7, $(\boxminus^{<k}\neg x\wedge\boxminus^{k}\bot\rightarrow\neg\tau_{k}(x))\in\mathbf{KB}$. Hence, $(\boxminus^{<k}\neg\upsilon(x)\wedge\boxminus^{k}\bot\rightarrow\upsilon(\neg\tau_{k}(x)))\in\mathbf{KB}$. Since $\upsilon(x)=\bot$, therefore by Lemma 2, $(\boxminus^{k}\bot\rightarrow\upsilon(\neg\tau_{k}(x)))\in\mathbf{KB}$. Since $(\upsilon(\neg\tau_{k}(x))\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$, therefore $(\boxminus^{k}\bot\rightarrow\boxminus^{l}\bot)\in\mathbf{KB}$. Thus, by Lemma 5, $k\not>l$: a contradiction.  $\dashv$

Lemma 12

For all $k,l\in\mathbb{N}$,

$(\boxplus^{k}\bot\vee\neg\tau_{l}(x))\not\in\mathbf{KB}$, 2. 2.

$(\boxminus^{k}\bot\vee\sigma_{l}(x))\not\in\mathbf{KB}$.

Proof: Let $k,l\in\mathbb{N}$.

$(1)$: Suppose $(\boxplus^{k}\bot\vee\neg\tau_{l}(x))\in\mathbf{KB}$. By Lemma 8, $(\neg\tau_{l}(x)\rightarrow\neg x)\in\mathbf{KB}$. Since $(\boxplus^{k}\bot\vee\neg\tau_{l}(x))\in\mathbf{KB}$, therefore $(\boxplus^{k}\bot\vee\neg x)\in\mathbf{KB}$. Let $\upsilon$ be the substitution defined as follows:

• •

$\upsilon(x)=\top$,

• •

for all variables $y$ distinct from $x$, $\upsilon(y)=y$.

Since $(\boxplus^{k}\bot\vee\neg x)\in\mathbf{KB}$, therefore $(\boxplus^{k}\bot\vee\neg\upsilon(x))\in\mathbf{KB}$. Since $\upsilon(x)=\top$, therefore $\boxplus^{k}\bot\in\mathbf{KB}$: a contradiction with Lemma 3.

$(2)$: Suppose $(\boxminus^{k}\bot\vee\sigma_{l}(x))\in\mathbf{KB}$. By Lemma 8, $(\sigma_{l}(x)\rightarrow x)\in\mathbf{KB}$. Since $(\boxminus^{k}\bot\vee\sigma_{l}(x))\in\mathbf{KB}$, therefore $(\boxminus^{k}\bot\vee x)\in\mathbf{KB}$. Let $\upsilon$ be the substitution defined as follows:

• •

$\upsilon(x)=\bot$,

• •

for all variables $y$ distinct from $x$, $\upsilon(y)=y$.

Since $(\boxminus^{k}\bot\vee x)\in\mathbf{KB}$, therefore $(\boxminus^{k}\bot\vee\upsilon(x))\in\mathbf{KB}$. Since $\upsilon(x)=\bot$, therefore $\boxminus^{k}\bot\in\mathbf{KB}$: a contradiction with Lemma 3.  $\dashv$

Lemma 13

For all $k,l\in\mathbb{N}$,

if $k\leq l$ then $(\boxplus^{k}\bot\wedge\sigma_{l}(x)\leftrightarrow\sigma_{k}(x))$, 2. 2.

if $k\leq l$ then $(\boxminus^{k}\bot\wedge\neg\tau_{l}(x)\leftrightarrow\neg\tau_{k}(x))$,

Proof: By induction on $k$.  $\dashv$

For all $k\in\mathbb{N}$, let $\lambda_{k}$ and $\mu_{k}$ be the substitutions defined as follows:

• •

$\lambda_{k}(x)=(x\wedge\boxplus^{k}\bot)$,

• •

for all variables $y$ distinct from $x$, $\lambda_{k}(y)=y$,

• •

$\mu_{k}(x)=\neg(\neg x\wedge\boxminus^{k}\bot)$,

• •

for all variables $y$ distinct from $x$, $\mu_{k}(y)=y$.

Lemma 14

For all $k,l\in\mathbb{N}$,

if $k\leq l$ then $(\lambda_{l}(\sigma_{k}(x))\leftrightarrow\sigma_{k}(x))\in\mathbf{KB}$, 2. 2.

if $k\leq l$ then $(\mu_{l}(\tau_{k}(x))\leftrightarrow\tau_{k}(x))\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 15

For all $k,l\in\mathbb{N}$,

if $k\geq l$ then $(\lambda_{l}(\sigma_{k}(x))\leftrightarrow\sigma_{l}(x))\in\mathbf{KB}$, 2. 2.

if $k\geq l$ then $(\mu_{l}(\tau_{k}(x))\leftrightarrow\tau_{l}(x))\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 16

For all $k,l\in\mathbb{N}$,

if $k\leq l$ then $\sigma_{l}\circ\lambda_{k}\simeq\sigma_{k}$, 2. 2.

if $k\leq l$ then $\tau_{l}\circ\mu_{k}\simeq\tau_{k}$.

Proof: By Lemma 15.  $\dashv$

Lemma 17

For all $k,l\in\mathbb{N}$,

if $k\leq l$ then $\sigma_{l}\preceq\sigma_{k}$, 2. 2.

if $k\leq l$ then $\tau_{l}\preceq\tau_{k}$.

Proof: By Lemma 16.  $\dashv$

Lemma 18

For all $k,l\in\mathbb{N}$,

if $k<l$ then $\sigma_{k}\not\preceq\sigma_{l}$, 2. 2.

if $k<l$ then $\tau_{k}\not\preceq\tau_{l}$.

Proof: Let $k,l\in\mathbb{N}$.

$(1)$: Suppose $k<l$ and $\sigma_{k}\preceq\sigma_{l}$. Let $\lambda$ be a substitution such that $\sigma_{k}\circ\lambda\simeq\sigma_{l}$. Hence, $(\lambda(\sigma_{k}(x))\leftrightarrow\sigma_{l}(x))\in\mathbf{KB}$. By Lemma 10, $(\sigma_{k}(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Thus, $(\lambda(\sigma_{k}(x))\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Since $(\lambda(\sigma_{k}(x))\leftrightarrow\sigma_{l}(x))\in\mathbf{KB}$, therefore $(\sigma_{l}(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Consequently, by Lemma 11, $l\not>k$: a contradiction.

$(2)$: Suppose $k<l$ and $\tau_{k}\preceq\tau_{l}$. Let $\mu$ be a substitution such that $\tau_{k}\circ\mu\simeq\tau_{l}$. Hence, $(\mu(\tau_{k}(x))\leftrightarrow\tau_{l}(x))\in\mathbf{KB}$. By Lemma 10, $(\neg\tau_{k}(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Thus, $(\mu(\neg\tau_{k}(x))\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Since $(\mu(\tau_{k}(x))\leftrightarrow\tau_{l}(x))\in\mathbf{KB}$, therefore $(\neg\tau_{l}(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Consequently, by Lemma 11, $l\not>k$: a contradiction.  $\dashv$

Lemma 19

For all $k,l\in\mathbb{N}$,

$\sigma_{k}\not\preceq\tau_{l}$, 2. 2.

$\tau_{k}\not\preceq\sigma_{l}$.

Proof: Let $k,l\in\mathbb{N}$.

$(1)$: Suppose $\sigma_{k}\preceq\tau_{l}$. Let $\upsilon$ be a substitution such that $\sigma_{k}\circ\upsilon\simeq\tau_{l}$. Hence, $(\upsilon(\sigma_{k}(x))\leftrightarrow\tau_{l}(x))\in\mathbf{KB}$. By Lemma 10, $(\sigma_{k}(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Thus, $(\upsilon(\sigma_{k}(x))\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Since $(\upsilon(\sigma_{k}(x))\leftrightarrow\tau_{l}(x))\in\mathbf{KB}$, therefore $(\boxplus^{k}\bot\vee\neg\tau_{l}(x))\in\mathbf{KB}$: a contradiction with Lemma 12.

$(2)$: Suppose $\tau_{k}\preceq\sigma_{l}$. Let $\upsilon$ be a substitution such that $\tau_{k}\circ\upsilon\simeq\sigma_{l}$. Hence, $(\upsilon(\tau_{k}(x))\leftrightarrow\sigma_{l}(x))\in\mathbf{KB}$. By Lemma 10, $(\neg\tau_{k}(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Thus, $(\upsilon(\neg\tau_{k}(x))\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Since $(\upsilon(\tau_{k}(x))\leftrightarrow\sigma_{l}(x))\in\mathbf{KB}$, therefore $(\boxminus^{k}\bot\vee\sigma_{l}(x))\in\mathbf{KB}$: a contradiction with Lemma 12.  $\dashv$

6 About the nullariness of $\mathbf{KB}$

In this section, we prove that the following formula is unifiable and nullary:

• •

$\varphi::=((x\rightarrow\boxplus x)\wedge(\neg x\rightarrow\boxminus\neg x))$.

Lemma 20

Let $\sigma$ be a unifier of $\varphi$. For all $k\in\mathbb{N}$,

$(\sigma(x)\rightarrow\boxplus^{<k}\sigma(x))\in\mathbf{KB}$, 2. 2.

$(\neg\sigma(x)\rightarrow\boxminus^{<k}\neg\sigma(x))\in\mathbf{KB}$.

Proof: By induction on $k$.  $\dashv$

Lemma 21

For all $k\in\mathbb{N}$,

$\sigma_{k}$* is a unifier of $\varphi$,* 2. 2.

$\tau_{k}$* is a unifier of $\varphi$.*

Proof: By Lemmas 6 and 9.  $\dashv$

Lemma 22

Let $\upsilon$ be a substitution. If $\upsilon$ is a unifier of $\varphi$ then

for all $k\in\mathbb{N}$, the following conditions are equivalent: $(a)$ $\sigma_{k}\circ\upsilon\simeq\upsilon$, $(b)$ $\sigma_{k}\preceq\upsilon$, $(c)$ $(\upsilon(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$, 2. 2.

for all $k\in\mathbb{N}$, the following conditions are equivalent: $(d)$ $\tau_{k}\circ\upsilon\simeq\upsilon$, $(e)$ $\tau_{k}\preceq\upsilon$, $(f)$ $(\neg\upsilon(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$.

Proof: Suppose $\upsilon$ is a unifier of $\varphi$.

$(1)$: Let $k\in\mathbb{N}$.

$(a)\Rightarrow(b)$: Suppose $\sigma_{k}\circ\upsilon\simeq\upsilon$. Hence, $\sigma_{k}\preceq\upsilon$.

$(b)\Rightarrow(c)$: Suppose $\sigma_{k}\preceq\upsilon$. Let $\upsilon^{\prime}$ be a substitution such that $\sigma_{k}\circ\upsilon^{\prime}\simeq\upsilon$. Hence, $(\upsilon^{\prime}(\sigma_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$. By Lemma 10, $(\sigma_{k}(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Thus, $(\upsilon^{\prime}(\sigma_{k}(x))\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Since $(\upsilon^{\prime}(\sigma_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$, therefore $(\upsilon(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$.

$(c)\Rightarrow(a)$: Suppose $(\upsilon(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$. Since $\upsilon$ is a unifier of $\varphi$, therefore by Lemma 20, $(\upsilon(x)\rightarrow\boxplus^{<k}\upsilon(x))\in\mathbf{KB}$. Since $(\upsilon(x)\rightarrow\boxplus^{k}\bot)\in\mathbf{KB}$, therefore $(\upsilon(x)\rightarrow\boxplus^{<k}\upsilon(x)\wedge\boxplus^{k}\bot)\in\mathbf{KB}$. By Lemma 7, $(\boxplus^{<k}x\wedge\boxplus^{k}\bot\rightarrow\sigma_{k}(x))\in\mathbf{KB}$. Hence, $(\boxplus^{<k}\upsilon(x)\wedge\boxplus^{k}\bot\rightarrow\upsilon(\sigma_{k}(x)))\in\mathbf{KB}$. Since $(\upsilon(x)\rightarrow\boxplus^{<k}\upsilon(x)\wedge\boxplus^{k}\bot)\in\mathbf{KB}$, therefore $(\upsilon(x)\rightarrow\upsilon(\sigma_{k}(x)))\in\mathbf{KB}$. By Lemma 8, $(\sigma_{k}(x)\rightarrow x)\in\mathbf{KB}$. Thus, $(\upsilon(\sigma_{k}(x))\rightarrow\upsilon(x))\in\mathbf{KB}$. Since $(\upsilon(x)\rightarrow\upsilon(\sigma_{k}(x)))\in\mathbf{KB}$, therefore $(\upsilon(\sigma_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$. Consequently, $\sigma_{k}\circ\upsilon\simeq\upsilon$.

$(2)$: Let $k\in\mathbb{N}$.

$(d)\Rightarrow(e)$: Suppose $\tau_{k}\circ\upsilon\simeq\upsilon$. Hence, $\tau_{k}\preceq\upsilon$.

$(e)\Rightarrow(f)$: Suppose $\tau_{k}\preceq\upsilon$. Let $\upsilon^{\prime}$ be a substitution such that $\tau_{k}\circ\upsilon^{\prime}\simeq\upsilon$. Hence, $(\upsilon^{\prime}(\tau_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$. By Lemma 10, $(\neg\tau_{k}(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Thus, $(\upsilon^{\prime}(\neg\tau_{k}(x))\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Since $(\upsilon^{\prime}(\tau_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$, therefore $(\neg\upsilon(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$.

$(f)\Rightarrow(d)$: Suppose $(\neg\upsilon(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$. Since $\upsilon$ is a unifier of $\varphi$, therefore by Lemma 20, $(\neg\upsilon(x)\rightarrow\boxminus^{<k}\neg\upsilon(x))\in\mathbf{KB}$. Since $(\neg\upsilon(x)\rightarrow\boxminus^{k}\bot)\in\mathbf{KB}$, therefore $(\neg\upsilon(x)\rightarrow\boxminus^{<k}\neg\upsilon(x)\wedge\boxminus^{k}\bot)\in\mathbf{KB}$. By Lemma 7, $(\boxminus^{<k}\neg x\wedge\boxminus^{k}\bot\rightarrow\neg\tau_{k}(x))\in\mathbf{KB}$. Hence, $(\boxminus^{<k}\neg\upsilon(x)\wedge\boxminus^{k}\bot\rightarrow\upsilon(\neg\tau{k}(x)))\in\mathbf{KB}$. Since $(\neg\upsilon(x)\rightarrow\boxminus^{<k}\neg\upsilon(x)\wedge\boxminus^{k}\bot)\in\mathbf{KB}$, therefore $(\neg\upsilon(x)\rightarrow\upsilon(\neg\tau_{k}(x)))\in\mathbf{KB}$. By Lemma 8, $(\neg\tau_{k}(x)\rightarrow\neg x)\in\mathbf{KB}$. Thus, $(\upsilon(\neg\tau_{k}(x))\rightarrow\neg\upsilon(x))\in\mathbf{KB}$. Since $(\neg\upsilon(x)\rightarrow\upsilon(\neg\tau_{k}(x)))\in\mathbf{KB}$, therefore $(\upsilon(\tau_{k}(x))\leftrightarrow\upsilon(x))\in\mathbf{KB}$. Consequently, $\tau_{k}\circ\upsilon\simeq\upsilon$.  $\dashv$

Lemma 23

Let $\sigma$ be a substitution. If $\sigma$ is a unifier of $\varphi$ then there exists $k\in\mathbb{N}$ such that $\sigma_{k}\preceq\sigma$, or $\tau_{k}\preceq\sigma$.

Proof: Suppose $\sigma$ is a unifier of $\varphi$. By Propositions 1 and 2, we can assume that for all variables $y$ distinct from $x$, $\sigma(y)=y$. Let $k\in\mathbb{N}$ be such that $\deg(\sigma(x))\leq 3k$. Suppose $\sigma_{k}\not\preceq\sigma$ and $\tau_{k}\not\preceq\sigma$. Since $\sigma$ is a unifier of $\varphi$, therefore by Lemma 22, $(\sigma(x)\rightarrow\boxplus^{k}\bot)\not\in\mathbf{KB}$ and $(\neg\sigma(x)\rightarrow\boxminus^{k}\bot)\not\in\mathbf{KB}$. Let $F=(W,R)$ be a frame, $M=(W,R,V)$ be a model based on $F$, $s\in W$, $F^{\prime}=(W^{\prime},R^{\prime})$ be a frame, $M^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$ be a model based on $F^{\prime}$ and $s^{\prime}\in W^{\prime}$ be such that $M,s\not\models(\sigma(x)\rightarrow\boxplus^{k}\bot)$ and $M^{\prime},s^{\prime}\not\models(\neg\sigma(x)\rightarrow\boxminus^{k}\bot)$. Hence, $M,s\models\sigma(x)$, $M,s\not\models\boxplus^{k}\bot$, $M^{\prime},s^{\prime}\models\neg\sigma(x)$ and $M^{\prime},s^{\prime}\not\models\boxminus^{k}\bot$. Let $v_{0},t_{1},u_{1},v_{1},\ldots,t_{k},u_{k},v_{k}\in W$ and $v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k}\in W^{\prime}$ be such that $s=v_{0}$, $s^{\prime}=v^{\prime}_{0}$ and for all $i\in\mathbb{N}$, if $i<k$ then

• •

$v_{i}Rt_{i+1}$,

• •

$t_{i+1}Ru_{i+1}$,

• •

$u_{i+1}Rv_{i+1}$,

• •

$v^{\prime}_{i}R^{\prime}t^{\prime}_{i+1}$,

• •

$t^{\prime}_{i+1}R^{\prime}u^{\prime}_{i+1}$,

• •

$u^{\prime}_{i+1}R^{\prime}v^{\prime}_{i+1}$,

• •

$M,v_{i}\models p^{0}\wedge q^{0}$,

• •

$M,t_{i+1}\models p^{1}\wedge q^{0}$,

• •

$M,u_{i+1}\models p^{0}\wedge q^{1}$,

• •

$M,v_{i+1}\models p^{0}\wedge q^{0}$,

• •

$M^{\prime},v^{\prime}_{i}\models p^{0}\wedge q^{0}$,

• •

$M^{\prime},t^{\prime}_{i+1}\models p^{0}\wedge q^{1}$,

• •

$M^{\prime},u^{\prime}_{i+1}\models p^{1}\wedge q^{0}$,

• •

$M^{\prime},v^{\prime}_{i+1}\models p^{0}\wedge q^{0}$.

Let $M_{s}=(W_{s},R_{s},V_{s})$ be the symmetric unravelling of $M$ around $s$ and $M^{\prime}_{s^{\prime}}=(W^{\prime}_{s^{\prime}},R^{\prime}_{s^{\prime}},V^{\prime}_{s^{\prime}})$ be the symmetric unravelling of $M^{\prime}$ around $s^{\prime}$. For more on this, see [11, Definition $4.51$]. Since $M,s\models\sigma(x)$ and $M^{\prime},s^{\prime}\models\neg\sigma(x)$, therefore by [11, Proposition $2.14$ and Lemma $4.52$], $M_{s},(v_{0})\models\sigma(x)$ and $M^{\prime}_{s^{\prime}},(v^{\prime}_{0})\models\neg\sigma(x)$. Let $F^{\prime\prime}=(W^{\prime\prime},R^{\prime\prime})$ be the least frame containing the disjoint union of $(W_{s},R_{s})$ and $(W^{\prime}_{s^{\prime}},R^{\prime}_{s^{\prime}})$ and such that for some new states $t$ and $u$,

• •

$(v_{0},t_{1},u_{1},v_{1},\ldots,t_{k},u_{k},v_{k})R^{\prime\prime}t$,

• •

$tR^{\prime\prime}(v_{0},t_{1},u_{1},v_{1},\ldots,t_{k},u_{k},v_{k})$,

• •

$tR^{\prime\prime}t$,

• •

$tR^{\prime\prime}u$,

• •

$uR^{\prime\prime}t$,

• •

$uR^{\prime\prime}u$,

• •

$uR^{\prime\prime}(v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k})$,

• •

$(v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k})R^{\prime\prime}u$.

Let $M^{\prime\prime}=(W^{\prime\prime},R^{\prime\prime},V^{\prime\prime})$ where

• •

$V^{\prime\prime}(p)=V_{s}(p)\cup V^{\prime}_{s^{\prime}}(p)\cup\{t\}$,

• •

$V^{\prime\prime}(q)=V_{s}(q)\cup V^{\prime}_{s^{\prime}}(q)\cup\{u\}$,

• •

for all atoms $\alpha$, if $\alpha\not=p$ and $\alpha\not=q$ then $V^{\prime\prime}(\alpha)=V_{s}(\alpha)\cup V^{\prime}_{s^{\prime}}(\alpha)$.

Since $\deg(\sigma(x))\leq 3k$, $M_{s},(v_{0})\models\sigma(x)$ and $M^{\prime}_{s^{\prime}},(v^{\prime}_{0})\models\neg\sigma(x)$, therefore M^{\prime\prime},(v_{0})$$\models\sigma(x) and $M^{\prime\prime},(v^{\prime}_{0})\models\neg\sigma(x)$. Since $\sigma$ is a unifier of $\varphi$, therefore $((\sigma(x)\rightarrow\boxplus\sigma(x))\wedge(\neg\sigma(x)\rightarrow\boxminus\neg\sigma(x)))\in\mathbf{KB}$. Since $M^{\prime\prime},(v_{0})\models\sigma(x)$ and $M^{\prime\prime},(v^{\prime}_{0})\models\neg\sigma(x)$, considering that for all $i\in\mathbb{N}$, if $i<k$ then $M,v_{i}\models p^{0}\wedge q^{0}$, $M,t_{i+1}\models p^{1}\wedge q^{0}$, $M,u_{i+1}\models p^{0}\wedge q^{1}$, $M,v_{i+1}\models p^{0}\wedge q^{0}$, $M^{\prime},v^{\prime}_{i}\models p^{0}\wedge q^{0}$, $M^{\prime},t^{\prime}_{i+1}\models p^{0}\wedge q^{1}$, $M^{\prime},u^{\prime}_{i+1}\models p^{1}\wedge q^{0}$ and $M^{\prime},v^{\prime}_{i+1}\models p^{0}\wedge q^{0}$, therefore M^{\prime\prime},(v_{0},t_{1},u_{1},v_{1},\ldots,t_{k},u_{k},$$v_{k})\models\sigma(x) and $M^{\prime\prime},(v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k})\models\neg\sigma(x)$. Since $((\sigma(x)\rightarrow\boxplus\sigma(x))\wedge(\neg\sigma(x)\rightarrow\boxminus\neg\sigma(x)))\in\mathbf{KB}$, considering that $M,v_{k}\models p^{0}\wedge q^{0}$, $M^{\prime\prime},t\models p^{1}\wedge q^{0}$, $M^{\prime\prime},u\models p^{0}\wedge q^{1}$ and $M^{\prime},v^{\prime}_{k}\models p^{0}\wedge q^{0}$, therefore M^{\prime\prime},(v_{0},t_{1},u_{1},v_{1},\ldots,t_{k},$$u_{k},v_{k})\models\neg\sigma(x) and $M^{\prime\prime},(v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k})\models\sigma(x)$. Thus, M^{\prime\prime},(v_{0},t_{1},$$u_{1},v_{1},\ldots,t_{k},u_{k},v_{k})\not\models\sigma(x) and $M^{\prime\prime},(v^{\prime}_{0},t^{\prime}_{1},u^{\prime}_{1},v^{\prime}_{1},\ldots,t^{\prime}_{k},u^{\prime}_{k},v^{\prime}_{k})\not\models\neg\sigma(x)$: a contradiction.  $\dashv$

In the proof of Lemma 23, remark that the symmetric unravellings $M_{s}$ and $M^{\prime}_{s^{\prime}}$ are serial when the models $M$ and $M^{\prime}$ are serial. Moreover, when the models $M$ and $M^{\prime}$ are reflexive, $M_{s}$ and $M^{\prime}_{s^{\prime}}$ can be defined as their reflexive symmetric unravellings.

Proposition 3

$\varphi$* is nullary.*

Proof: Suppose $\varphi$ is not nullary. Let $\Sigma$ be a minimal complete set of unifiers of $\varphi$. By Lemma 21, $\sigma_{0}$ is a unifier of $\varphi$. Since $\Sigma$ is a complete set of unifiers of $\varphi$, therefore let $\sigma\in\Sigma$ be such that $\sigma\preceq\sigma_{0}$. Hence, by Lemma 23, let $k\in\mathbb{N}$ be such that $\sigma_{k}\preceq\sigma$, or $\tau_{k}\preceq\sigma$.

— Case “$\sigma_{k}\preceq\sigma$”: By Lemma 21, $\sigma_{k+1}$ is a unifier of $\varphi$. Since $\Sigma$ is a complete set of unifiers of $\varphi$, therefore let $\sigma^{\prime}\in\Sigma$ be such that $\sigma^{\prime}\preceq\sigma_{k+1}$. Since $\sigma_{k}\preceq\sigma$, therefore by Lemma 17, $\sigma^{\prime}\preceq\sigma$. Since $\Sigma$ is a minimal set of unifiers of $\varphi$, therefore $\sigma^{\prime}\simeq\sigma$. Since $\sigma_{k}\preceq\sigma$ and $\sigma^{\prime}\preceq\sigma_{k+1}$, therefore $\sigma_{k}\preceq\sigma_{k+1}$: a contradiction with Lemma 18.

— Case “$\tau_{k}\preceq\sigma$”: Since $\sigma\preceq\sigma_{0}$, therefore $\tau_{k}\preceq\sigma_{0}$: a contradiction with Lemma 19.  $\dashv$

7 Conclusion

In modal logic, the problem of checking the unifiability of formulas has been introduced as a special case of the problem of checking the admissibility of inference rules [29]. Intuitively, for an axiomatically presented modal logic, the admissibility problem asks whether a given inference rule can be added to the axiomatization of the logic without changing the associated set of derivable formulas. Its computability has been studied — for a limited number of normal modal logics like $\mathbf{K}{4}$, $\mathbf{GL}$ and $\mathbf{S}{4}$ — by Jer̆ábek [25] and Rybakov [27]. Aside from these transitive normal modal logics and for the normal extensions of $\mathbf{S}{5}$, it is still unknown for numerous normal modal logics — for example $\mathbf{K}$, $\mathbf{KD}$ and $\mathbf{KT}$ — whether the problem of checking the admissibility of inference rules is solvable. The significance of the unification type in the research on the problem of checking the unifiability of formulas stems from the fact that if a normal modal logic is unitary, or finitary then the problem of checking the admissibility of inference rules can be reduced to the problem of checking the unifiability of formulas.

In this paper, we have adapted to $\mathbf{KB}$ the argument of Jer̆ábek [26] showing that $\mathbf{K}$ is nullary, though the nullariness character of $\mathbf{KB}$ have only been be obtained within the context of unification with parameters. Seeing that the frames constructed in the proofs of Lemmas 3 and 5 are reflexive and the symmetric unravellings of the models constructed in the proof of Lemma 23 are serial when the considered models are serial, or can be forced to be reflexive when the considered models are reflexive, therefore on checking the proofs of our results, the reader may easily verify that our adaptation also applies in the case of $\mathbf{KDB}$ and $\mathbf{KTB}$ — one has only to replace “$\mathbf{KB}$” by “$\mathbf{KDB}$”, or “$\mathbf{KTB}$”, “frame” by “serial frame”, or “reflexive frame”, etc. The nullariness character of $\mathbf{KB}$, $\mathbf{KDB}$ and $\mathbf{KTB}$ constitutes an answer to questions put forward by Dzik [16]. Nevertheless, much remains to be done, seeing that, for instance, the types of simple Church-Rosser normal modal logics like $\mathbf{KG}$, $\mathbf{KDG}$ and $\mathbf{KTG}$ are unknown and for all $k\in\mathbb{N}$ such that $k\geq 2$, the type of the least normal modal logic containing $\Box^{k}\bot$ is unknown.

Acknowledgements

This paper has been written on the occasion of a $3$-months visit of Çiğdem Gencer during the Fall $2018$ in Toulouse that was financially supported by Université Paul Sabatier (“Professeurs invités 2018”). We make a point of thanking the colleagues of the Institut de recherche en informatique de Toulouse who contributed to the development of the work we present today. Special acknowledgement is also heartily granted to Maryam Rostamigiv (Toulouse University, France) and Tinko Tinchev (Sofia University St. Kliment Ohridski , Bulgaria) for their valuable remarks.