3
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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$

$\endgroup$
  • $\begingroup$ Your reasoning looks correct. I added an answer that puts it more succinctly. $\endgroup$ – spaceisdarkgreen Jun 4 at 14:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.