Is $p \rightarrow \lozenge (q \rightarrow q)$ a tautology in K?

Question

Intuitively, it is a tautology. Imagine two possible worlds $m0$ and $m1$, such that $m1$ is accessible from $m0$, i.e., we have the folowing scheme of possible worlds: $m0 \rightarrow m1$. Whatever is the truth value of $q$ in $m1$, $\lozenge(q \rightarrow q)$ is true in $m0$. It follows that $p\rightarrow \lozenge(q\rightarrow q)$ is true in $m0$, wathever is the truth value of $p$ in $m0$ and $m1$. It is a tautology. But I've avaliated this expression by using MOLTAP, and the result was NOT VALID. Is MOLTAP wrong?

Answer 1

Yet another way to see that $p\rightarrow\Diamond(q\rightarrow q)$ is not a tautology in $K$ is as follows: if it is, then $T\rightarrow\Diamond(q\rightarrow q)$ is a theorem, then so is $\Diamond(q\rightarrow q)$ i.e. $\Diamond T$, where $T$ stands for $true$. But $\Diamond T$ is not a theorem in $K$. It is only a theorem in modal logic $D$, which corresponds to serial frames. In fact $\Diamond T$ is equivalent to the $D$ axiom $\Box p \rightarrow \Diamond p$, see answer to 3-rd question below this one.