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



Existence of certain formulas in modal logic K
$\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$.


