# Existence of certain formulas in modal logic K

Does there exist a modal formula $$φ$$ with the following properties?

1. for every finite Kripke frame $$F$$ there is some ground substitution $$\sigma$$ such that for every point $$w \in F$$ we have $$F, w \Vdash \sigma(φ)$$,
2. there exists an infinite Kripke frame $$F$$ such that for every ground substitution $$\sigma$$ there is some point $$w \in F$$ with $$F, w \nVdash \sigma(φ)$$.

A ground substitution is a map $$σ$$ from the set of variables to the set of formulas without variables (also called "ground formulas"). Their domain is naturally extended to the set of all modal formulas, by forcing $$σ$$ to be a homomorphism. This precisely formalises "uniformly substituting" all variables in a formula by formulas without variables.

This question arose when studying unifiability in the modal logic K.

I know the following "in between" property: If there is a finite (intransitive) tree $$F$$ of depth $$m$$ and a ground substitution $$σ$$ such that

• for all variables $$p$$, we have $$md(σ(p)) ≤ m - md(φ)$$
• $$F, w \Vdash \sigma(\varphi)$$ for all $$w \in F$$

then $$\sigma(\varphi)$$ is valid and condition 2. above can not be fulfilled. Here $$md$$ stands for the modal degree of a formula. I.e. the $$σ$$ which exist in condition 1. have to be "very complicated" in comparison to $$F$$ and $$φ$$.

• Note that 2 is equivalent to “$\varphi$ is not unifiable”. If no formula satisfying 1 and 2 exists, then unifiability in K is decidable, which is a major open problem. Mar 6, 2023 at 8:26
• I asked, because I noticed the same thing. I found that there do not exist formulas satisfying 1 and 2 of degree 1 in 1 variable. (In two ways: by enumeration and by considering a certain 4-point frame) And I was curious whether the more general case was known. Mar 6, 2023 at 11:41

$$\def\eq{\leftrightarrow}\def\sset{\subseteq}$$An example of such a formula is $$\phi(p,q)=(\Box p\to p)\land(p\to(q\eq\neg\Box q)).$$

Lemma. The formula $$\phi$$ satisfies condition 1.

Proof: Let $$(F,R)$$ be a finite frame. For all $$i\in\omega$$, let $$W_i=\{w\in F:w\vDash\Box^i\bot\}$$, where $$\Box^i=\underbrace{\Box\cdots\Box}_i$$. Since $$W_0\sset W_1\sset W_2\sset\cdots$$ and $$F$$ is finite, there is an $$n$$ such that $$W_n=\bigcup_{i\in\omega}W_i$$. Note that $$W_n$$ is the largest converse well-founded generated subframe of $$F$$. By well-founded recursion, there exists a unique $$X\sset W_n$$ such that $$x\in X\iff\exists y\,(x\mathrel Ry\land y\notin X)$$ for all $$x\in W_n$$. Then $$F\vDash\phi$$ under the valuation \begin{align*}w\vDash p&\iff w\in W_n,\\w\vDash q&\iff w\in X.\end{align*}

$$W_n$$ is defined in $$F$$ by the ground formula $$\Box^n\bot$$. To see that $$X$$ is also definable by a ground formula, put $$\xi_0=\bot$$ and $$\xi_{i+1}=\neg\Box\xi_i$$ for each $$i$$ (that is, $$\xi_{2i}=(\Diamond\Box)^i\bot$$ and $$\xi_{2i+1}=(\Diamond\Box)^i\Diamond\top$$). By induction on $$i$$, we can show $$\forall x\in W_i\:(x\in X\iff F,x\vDash\xi_i),$$ hence $$X$$ is definable by the formula $$\Box^n\bot\land\xi_n$$. Thus, the substitution $$\sigma(p)=\Box^n\bot$$, $$\sigma(q)=\xi_n$$ satisfies $$F\vDash\sigma(\phi)$$. QED

To see that $$\phi$$ satisfies 2, note that condition 2 is equivalent to “$$\phi$$ is not unifiable”. Since Löb’s rule $$\Box\alpha\to\alpha\mathrel/\alpha$$ is admissible in K, any unifier of $$\phi$$ also unifies $$p$$, hence $$q\eq\neg\Box q$$; but the latter is not unifiable, as it is not satisfiable in nonempty reflexive frames. Let me spell out a more explicit argument for completeness:

Lemma. The formula $$\phi$$ satisfies condition 2.

Proof: Let $$(F,R)=(\mathbb N,\{(n+1,n):n\in\mathbb N\})$$ be the infinite descending irreflexive intransitive chain, and assume for contradiction that $$F\vDash\sigma(\phi)$$ for a ground substitution $$\sigma$$. Then $$F\models\sigma(\Box p\to p)$$ implies $$n\models\sigma(p)$$ for all $$n\in\mathbb N$$ by induction on $$n$$, hence also $$F\models(\sigma(q)\eq\neg\Box\sigma(q))$$. Thus, $$n+1\models\sigma(q)\iff n+1\nvDash\Box\sigma(q)\iff n\nvDash\sigma(q).$$ On the other hand, for every ground formula $$\alpha$$, we can prove by induction on the complexity of $$\alpha$$ that $$\{n\in\mathbb N:n\models\alpha\}$$ or its completement is finite, thus for all sufficiently large $$n\in\mathbb N$$, we have $$n+1\models\sigma(q)\iff n\models\sigma(q).$$ This is a contradiction. QED

The argument actually works for all logics between $$\mathbf K$$ and $$\mathbf{Alt_1=K}\oplus\Diamond p\to\Box p$$.

• I don’t see how $\Box P \to P \vdash P$ is a valid version of Löb’s rule. Isn’t it that $\vdash \Box P \to P$ implies $\vdash P$? Jun 10, 2023 at 14:19
• This is just a matter of notation. A “rule” by itself is just a picture that has several formulas as premises and one formula as a conclusion. There are various ways how rules are written, and one of them is to separate premises from the conclusion with a $\vdash$ symbol. I could have just as well written it as $\Box P\to P\mathrel/P$. The statement that such a rule is admissible means what you wrote: that whenever $\Box P\to P$ is provable in K, then $P$ is also provable in K. Jun 10, 2023 at 16:42
• Come think of it, I will rather write it with $/$ to avoid potential confusion. Jun 10, 2023 at 16:44