# Is there an unsatifiable formula in modal logic K whose negation is not valid?

I just stumbled across this. In classic logic, the negation of a valid formula is unsatisfiable and vice versa. Given the usual Kripke semantics definitions of modal logic K (see below), this law seems only to hold in the former direction. But I failed to construct a counterexample for the opposite direction. So do you know a modal formula that is unsatisfiable in K and whose negation is not valid?

Some definitions: A K-model is a structure $$M = (W,R,I)$$ consisting of a non-empty graph of "worlds" $$(W,R)$$ and a family $$I$$ of valuations, providing a pc-valuation for each world $$w \in W$$. For a modal formula $$H$$, let $$(M,w) \models H$$ be defined as usual in K and let $$M \models H$$ iff $$(M,w)\models H$$ holds for all worlds $$w\in W$$. Based on this I call $$H$$ valid iff $$M \models H$$ holds for each K-structure $$M$$ and I call $$H$$ unsatisfiable iff $$M\not\models H$$ holds for each K-structure.

How about $$H = a \land \Diamond \neg a$$, where $$a$$ is some atomic proposition? Consider a model $$M = (W, R, I)$$. If $$M$$ has a world $$w$$ such that $$M, w \models H$$, then there must exist some $$w' \in W$$ (with $$wRw'$$) such that $$M, w' \models \neg a$$, meaning that $$M, w' \not\models H$$. Hence $$H$$ is unsatisfiable.
On the other hand, $$\neg H = \neg a \lor \Box a$$ is clearly not valid, since we can create a model that does not satisfy it.
• You spelled out the conditions for the satisfiability of $H$ as opposed to its unsatisfiability. Sep 9, 2023 at 15:38