0
$\begingroup$

enter image description here

enter image description here

I'm trying to understand how a formula can not be valid but also true in the above question.

$\endgroup$
  • $\begingroup$ See Kripke semantics : Basic definitions: We read $w\Vdash A$ as “w satisfies A”, “A is satisfied in w”. A formula A is valid in a model $\langle W,R,\Vdash \rangle$ , if $w\Vdash A$ for all $w ∈ W$. You have to map "your" true/valid" on "satisfiable/valid in a model". $\endgroup$ – Mauro ALLEGRANZA Apr 7 '18 at 8:26
1
$\begingroup$

So, let's consider your task at hand.

We need to write some “properly satisfiable” formula with modalities which is not valid (i.e., there can be some models wherein it can be false) but true in the model on the picture (i.e., it is true in every world of this model).

We assume that we work in K, i.e. in minimal normal modal logic where there are no additional conditions on reachability relation (arrows). I also assume that you know relational (Kripke) semantics for normal modal logics.

Let's list some modal formulas of one variable that are true in $x_1,\ldots,x_4$.

  • $x_1\vDash\diamond q$ (i.e., you can move one step along an arrow and arrive to $q$); $x_1\vDash\diamond p$ (i.e., you can move one step along an arrow and arrive to $p$);
  • $x_2\vDash\Box\Box q$ (i.e., if you make exactly two steps from $x_2$, you'll arrive to $q$)
  • $x_3\vDash\Box\Box p$ (i.e., if you make exactly two steps from $x_2$, you'll arrive to $p$)
  • $x_4\vDash\Box A$ with $A$ being any formula you want (because, you cannot go anywhere from $x_4$ and formulas with $\Box$ will be vacuously true)

Now, I claim (and leave it to you as an easy exercise) that $$\mathfrak{K}\vDash\diamond q\vee\Box\Box q\vee\Box\Box p\vee\Box A$$ with $\mathfrak{K}$ being your model and $A$ being arbitrary formula.

I also claim (and leave it to you as an a tiny bit more difficult) that this formula is not valid, i.e. we can find a model where it is false (for some $A$).

$\endgroup$
  • $\begingroup$ Thank you so much for your detailed answer. It really helped. $\endgroup$ – Daryn Wilkinson Apr 8 '18 at 8:17
  • $\begingroup$ Tbh, there is an even easier answer: simply write $\Box\neg r$: it will be true in every world of your model. $\endgroup$ – Daniil Kozhemiachenko Apr 8 '18 at 19:01

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.