# Negative introspection axiom and Euclidean property of accessibility relation

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.

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