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 $φ$.

  • $\begingroup$ 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. $\endgroup$ Mar 6, 2023 at 8:26
  • $\begingroup$ 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. $\endgroup$
    – 8bc3 457f
    Mar 6, 2023 at 11:41

1 Answer 1


$\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$.

  • $\begingroup$ 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$? $\endgroup$
    – PW_246
    Jun 10, 2023 at 14:19
  • $\begingroup$ 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. $\endgroup$ Jun 10, 2023 at 16:42
  • $\begingroup$ Come think of it, I will rather write it with $/$ to avoid potential confusion. $\endgroup$ Jun 10, 2023 at 16:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.