A total novice here, and exasperated at that. I can translate natural language statements into formulae of modal logic, but their valuation in Kripke model seems elusive, as I'm simply unsure how to apply theory to practice.

Can someone be so kind as to explain me, step by step, how to go about the formula (p & q -> (p -> q)) -> [](p -> q) in order to assign truth values to each variable at each world in a Kripke model?

Thank you

1 Answer 1


Kripke models can be used to prove that a formula is not valid.

Reagrading your example, this means, to show that the antecedent: (p & q → (p → q)) is true in w (the "actual" world) and the consequnr □(p → q) is not, i.e. (p → q) is false in some world w' accessible from w (i.e. such that wRw').

If q is false in w (written: w ⊮ q) we have that p & q is false in w, and thus (p & q → (p → q)) is true.

And if p is true, we have that (p → q) is false in w.

If the "accessibility" relation R is reflexive, i.e. wRw, we have that (p → q) is not true in every w' such that wRw', and this implies that □(p → q) is false.

If instead you have to "evaluate" the truth value of a formula at a specific world, with an assignment of truth values to atoms, e.g.

w ⊩ { p,q }

in this case we simply to apply the semantical specifications.

Clearly, w ⊩ p & q and w ⊩ p → q, and thus w ⊩ (p & q → (p → q)), and so on.

The accessibility relation is needed in order to assess the modal opeartor ; we have that :

w ⊩ □p if and only if w' ⊩ p for all w' such that wRw'.

  • My sincere thanks!!. A couple of further (naive) questions: 1. Why do we have to take as '(our) actual world' the world where q is false and p is true, as it is the case canonically in S5 model (where the s1 world has these values)? Do we per se, or is it done arbitrarely? In my RL example both p and q are certainly true, does it mean I have to take the world where p and q are true as my 'initial world' and then see which worlds are accessible from this world? Nov 26, 2017 at 15:22
  • _cont'd_2. Do I understand it correctly, and each world has only specific kind of accessibility relations to a specific set of other worlds? That is, does the world {p,q} - both values positive - have different accessible worlds than, say, the world {p}, and we have to take only directly accessible worlds into account? Concretely, in this case {p,q}, I cannot arbitrarily decide that my world has, say, 'reflexive' relation to another wold, when it is not the case in the model? Nov 26, 2017 at 15:42
  • cont'd. 3. What do we do when the antecedent itself contains modal operators, as in []p & [] q -> [] (p ->q)? Do we normally translate the formulas into FOL via standard translation? How do we go about that at a world {p,q}? Nov 26, 2017 at 15:59
  • You said: The accessibility relation is needed in order to assess the modal opeartor □; we have that : w ⊩ □p if and only if w' ⊩ p for all w' such that wRw'. And when it is not the case that the relation is reflexive? I thought (just to show you how tenuous my grasp is) that some worlds can have this relation, and some not? And I have to check what relations are there in each case? Nov 26, 2017 at 16:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .