0

I want to prove that $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5

I have S5 definition :

\begin{align*} T&:\Box p\rightarrow p\\ 5&:\Diamond p\rightarrow \Box\Diamond p\\ K&:\Box (p\rightarrow q)\rightarrow(\Box p\rightarrow \Box \phi)\\ Nec&:\frac{\phi}{\Box\phi} \end{align*}

And theorem definition :

A formula is a theorem of S5 $\Leftrightarrow\phi$ is valid in all frames where R is an equivalence relation

\begin{align} &\neg (\phi\rightarrow\neg\Box\neg\phi),w_i\mbox{ as an hypothesis}\\ &\phi,w_i \mbox{ from }R_\neg \mbox{ on } 1\\ &\Diamond\phi,w_i\mbox{ from }R_\neg \mbox{ on } 1\\ \end{align}

I'm not sure I have here an equivalence relation to conclude that

Therefore $\phi$ is valid in all frames and $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5

Third attempt

\begin{align} \neg\phi\rightarrow\Box\neg\phi,w_i \mbox{ contrapositive of }T\\ \neg\neg\phi\rightarrow\neg\Box\neg\phi,w_i \mbox{ negation of }1 \end{align}

Therefore $\phi$ is valid and $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5

Revolucion for Monica
  • 1,511

1 Answers1

2

1) $\Box\neg\phi\to\neg\phi$, obtained by substituting $\neg\phi$ for $p$ in the $\mathbf{T}$ axiom.

2) $\neg\neg\phi\to\neg\Box\neg\phi$, by contraposition from (1).

3) $\phi\to\neg\neg\phi$, by classical logic (a tautology).

4) $\phi\to\neg\Box\neg\phi$, by syllogism from (3) and (2).

That's it.

Evgeny Zolin
  • 148
  • 8