Negative introspection axiom and Euclidean property of accessibility relation

Question

Revising the modal logic principles, I have encountered an negative introspection axiom: $$ \vDash \neg \square \alpha \longrightarrow \square \neg \square \alpha $$ with additional information, that it is a direct effect from Euclidean property of accessibility relation $\mathbb{R}$. Square operator is defined as follows (for Kripke structure $\kappa = (\mathbb{W}, \mathbb{R}, m)$): $$ \kappa, w \vDash \square \alpha \equiv \forall w' \in \mathbb{W} \quad w\mathbb{R}w' \implies \kappa, w' \vDash \alpha $$

I got stuck in the point where I have to apply the Euclidean property. We basically know that for any Kripke structure $\kappa$ and state $w \in \mathbb{W}$: $$ \exists w' \in \mathbb{W} \quad w\mathbb{R}w' \wedge \kappa, w' \nvDash \alpha$$ and from the fact that $\mathbb{R}$ is Euclidean: $$ \forall w_{1}, w_{2}, w_{3} \in \mathbb{W} \quad w_{1}\mathbb{R}w_{2} \wedge w_{1}\mathbb{R}w_{3} \implies w_{2}\mathbb{R}w_{3} $$

I've tried to make it similarily to this, but there we have all universal quantifiers, so it was moreorless sensible to me. I would be really grateful, if someone would provide a solution or any hint to that.

Answer 1

This is the same thing as $\lozenge \alpha\to \square\lozenge \alpha.$ If $\lozenge \alpha$ holds, then there is some accessible world at which $\alpha$ holds. By the Euclidean property, that world is accessible from every accessible world, so $\lozenge\alpha$ holds at every accessible world. In other words, $\square \lozenge \alpha$ holds.

Answer 2

By the time, I have found a possible solution, I would appreciate some comments:

Let's get any possible world $w \in \mathbb{W}$, such as $\kappa, w \vDash \neg \square \alpha $. Then,from a definition of $\square$: $$ \exists w' \in \mathbb{B} w\mathbb{R}w' \wedge \kappa, w' \vDash \neg \alpha $$ Let's consider any state $w'' \in \mathbb{W}$ such as $w\mathbb{R}w''$. Then, from Euclideanity of $\mathbb{R}$ we have $w\mathbb{R}w'' \wedge w\mathbb{R}w' \implies w''\mathbb{R}w'$. That concludes to the following: $$\forall w'' \in \mathbb{W} \, \exists w' \in \mathbb{W} \, w\mathbb{R}w'' \implies w''\mathbb{R}w' \wedge \kappa, w' \vDash \neg \alpha $$ which is equivalent to: $$ \forall w'' \in \mathbb{W} \,, w\mathbb{R}w'' \implies \kappa, w'' \vDash \neg \square \alpha$$ and is in fact a definition of $\square$ operator: $\kappa, w \vDash \square \neg \square \alpha$. To sum up, for any Kripke structure $\kappa$ and state $w \in \mathbb{W}$ we have $\kappa, w \vDash \neg \square \alpha \implies \kappa, w \vDash \square \neg \square \alpha$, thus thesis: $\vDash \neg \square \alpha \longrightarrow\square \neg \square \alpha$. $\blacksquare$