Why the statement:

Premise:$$(\exists x)(\diamond Px\vee\square Qx) $$


$$\diamond(\exists x)(Px\vee Qx)$$ is not valid in $K$ system of modal logic, but it's true in the $T$ system and also in $S4$ and $S5$? Thanks


I'll briefly recall a few basic facts to clearly state my assumptions.

The semantics of $\Box \varphi$ in first-order modal logic is defined with respect to a Kripke structure $K = \langle W, \rho, D, \mathcal{I} \rangle$, where $W$ is the (nonempty) set of worlds, $\rho$ is the world accessibility relation, $D$ is the (nonempty) domain, and $\mathcal{I}$ is the interpretation, which assigns a relation over $D$ of the appropriate arity to every relation symbol in every world in $W$. Specifically,

$$ K,w \models \Box \varphi $$

if and only if $\varphi$ holds in all worlds $w'$ accessible from $w$ in $K$; that is, if and only if $K, w' \models \varphi$ in every world $w'$ such that $(w,w') \in \rho$.

From the definition of $\Diamond \varphi$ as $\neg \Box \neg \varphi$ we get that $K, w \models \Diamond \varphi$ if and only if there is a world $w'$ in $W$ that is accessible from $w$ and where $\varphi$ holds.

This definition of $\Box \varphi$ has two important features:

  1. It causes the axioms of $K$ to hold in every Kripke structure.
  2. It does not impose any restriction on $\rho$ (other than being a subset of $W \times W$).

Consider a world $w$ such that for all $w' \in W$, $(w,w') \not\in \rho$.

Then in this world $\Box \varphi$ holds regardless of $\varphi$, but $\Diamond \varphi$ is false.

Now observe that in $T$ we have the axiom $\Box \psi \rightarrow \psi$, which is missing from $K$. From $\Box \neg\varphi \rightarrow \neg\varphi$, by contraposition, we derive $\varphi \rightarrow \Diamond \varphi$, which together with $\Box \varphi \rightarrow \varphi$, implies

$$ \Box \varphi \rightarrow \Diamond \varphi \enspace. $$

So, the extra axiom cannot hold in all Kripke structures. If $\rho$ is reflexive, though, "dead-end worlds," from which no worlds are accessible, are not possible, and $\Box \varphi \rightarrow \Diamond \varphi$ holds.

Given $\Box \varphi \rightarrow \Diamond \varphi$ it is a simple matter to show that

$$ \Diamond (\exists x)(P x \vee Q x) $$

can be derived from

$$ (\exists x)(\Diamond P x \vee \Box Q x) \enspace. $$

It is also not difficult to come up with a Kripke structure with a "dead-end world," where the premise holds (because $\Box Qx$ holds vacuously) but the consequence is false. Since the axioms of $K$ hold in this structure, we have shown that the derivation is not possible from the axioms of $K$.

To finish things off, since $S4$ and $S5$ are stronger than $T$, what can be proved in $T$ can be proved in $S4$ and $S5$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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