# Proof in T and K system of modal logic

Why the statement:

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

Conclusion:

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