Questionable Proofs in Modal LPC

67 Views Asked by At

I'm working through some exercises in Hughes and Cresswell, and it seems that I must be making a mistake - the exercise indicates that (at least some of) the axioms of S5 should be necessary, but the following proofs show that the wff is a theorem of any normal modal logic.

The exercise asks to show that $\exists x \square (\square \varphi x\vee \psi y)\equiv \square \exists x (\square \varphi x\vee \psi y)$ is a theorem of S5. Here are the proofs which show that it is a theorem of any normal modal system:

$\aleph=_{def}\varphi x\rightarrow \square \varphi x$ is a theorem of any normal modal system: \begin{align*} &(1) &&\varphi x\rightarrow \varphi x &PC\\ &(2) &&\square \varphi x \rightarrow \square \varphi x & RPK,(1)\\ &(3) &&\square \varphi x \rightarrow \varphi x & T\\ &(4) &&\varphi x \rightarrow \square \varphi x& (2), (3) \end{align*} $\gimel =_{def} \alpha\rightarrow \exists x \alpha$ is a theorem of any normal modal system: \begin{align*} &(1) &&\forall x\neg \alpha \rightarrow \neg \alpha &\forall 1\\ &(2) &&\alpha \rightarrow \neg \forall x \neg \alpha &PC, (1)\\ &(3) &&\alpha \rightarrow \exists x \alpha &QI, (2)\\ \end{align*}

Consequently, $\exists x \square (\square \varphi x\vee \psi y)\equiv \square \exists x (\square \varphi x\vee \psi y)$ is a theorem of any normal modal system: \begin{align*} &(1) &&(\square \varphi x \vee \psi y) \rightarrow(\square \varphi x \vee \psi y)& PC\\ &(2) &&(\square \varphi x \vee \psi y)\rightarrow \square (\square \varphi x \vee \psi y)&\aleph\\ &(3) &&\square (\square \varphi x \vee \psi y)\rightarrow \exists x \square (\square \varphi x \vee \psi y) &\gimel \\ &(4) &&(\square \varphi x \vee \psi y)\rightarrow \exists x\square (\square \varphi x \vee \psi y)&PC, (2),(3)\\ &(5) &&(\square \varphi x \vee \psi y)\rightarrow \exists x (\square \varphi x \vee \psi y)&\gimel \\ &(6) &&\exists x(\square \varphi x \vee \psi y)\rightarrow \square \exists x (\square \varphi x \vee \psi y)&\aleph\\ &(7) &&(\square \varphi x \vee \psi y)\rightarrow \square \exists x (\square \varphi x \vee \psi y)&PC, (5),(6)\\ &(8) &&\exists x \square (\square \varphi x\vee \psi y)\rightarrow (\square \varphi x\vee \psi y) &PC, (1),(4)\\ & (9) && \exists x \square (\square \varphi x\vee \psi y)\rightarrow \square \exists x (\square \varphi x\vee \psi y) &PC, (8),(7)\\ &(10) &&(\square \varphi x\vee \psi y)\rightarrow \exists x \square (\square \varphi x\vee \psi y) &PC, (1),(4)\\ & (11) && \square \exists x(\square \varphi x\vee \psi y)\rightarrow \exists x \square (\square \varphi x\vee \psi y) &PC, (10), (7)\\ & (12) && \square \exists x(\square \varphi x\vee \psi y)\equiv \exists x \square (\square \varphi x\vee \psi y) &PC, (9), (11) \end{align*}

Is there an obvious error in any of these three?