Dynamic Models in Imperative Logic

Warsaw, 21-24. February 2011.

User Tools

Site Tools

Modal logic calculator


W is a nonempty set; R is a binary relation on W, i.e. R\subseteq W\times W; V is valuation function which takes propositional letters (from set A) and delivers subsets of W, showing in which world a letter is true: V: A \to \wp W.

Exercise. Build a model \mathcal{M}=\left<\left<W,R\right>,\mathcal{V}\right>:

  • W=\{w_{1},w_{2},w_{3}\}: press buttons +1, +2, +3;
  • R=\{\langle w_{1},w_{2}\rangle,~\langle w_{1},w_{3}\rangle,~\langle w_{2},w_{1}\rangle,~\langle w_{3},w_{3}\rangle\}: press buttons >2, >3, >1, and >3 in appropriate columns;
  • \mathcal{V}(p)=\{w_{2},w_{3}\}, \mathcal{V}(q)=\{w_{1}\}: press buttons p and q in appropriate columns (the color of the letter in the world changes to green if the letter is true there).

Enter the formula \char{msam10}{03}p \to \char{msam10}{03}\char{msam10}{03}p and see in which worlds it is true (green worlds) and in which false (red worlds). E.g. the formula is true in w_2, and we write \mathcal{M},w_2\models \char{msam10}{03}p \to \char{msam10}{03}\char{msam10}{03}p because being necessarily true means being true in all accessible worlds.

In general:

  • \mathcal{M},w\models \char{msam10}{03}\varphi iff for all v such that Rwv it holds that \mathcal{M},v\models \varphi;
  • \mathcal{M},w\models \diamond\varphi iff for some v such that Rwv it holds that \mathcal{M},v\models \varphi.

There are number of ways to define logical truth in possible worlds semantics:

  • (V1) validity in the model: being true at each world;
  • (V2) validity in the frame: being true at each world in any model built over the frame 1);
  • (V3) validity in the class of frames: being (V2) valid on each frame from the class;
  • (V4) validity in all models.

In modal logic (V3) notion is used. It shows, so to speak, that the semantics of modal operators (e.g. words like 'necessary,' 'obligatory,' 'known' etc.) is captured by diverse structures (their “conceptual space” is given by a particular structure).

"The simplest modal logic of action"

The simplest modal logic of action is obtained by assuming that action sentences contain a 'praxeological' operator D_a which behaves logically in the same way as necessity operator \ldots, and may be read as 'a sees to it that.' The truth conditions of the D-sentences are given by the usual possible worlds semantics for modalities:
(AD) u \models D_a p if and only if w\models p for every w such that R_a(u,w),
where u and w are possible worlds or situations and R_a is an alternativeness relation between possible worlds. \ldots The alternatives to a given world u are its 'practical' alternatives: they are worlds in which the agent behaves in the same way as in u. The first semantical analysis of this kind was given by Brian Chellas2) (1969).

Hilpinen, Risto. 1997. On action and agency. in Logic, Action and Cognition – Essays in Philosophical Logic, E. Ejerhed and S. Lindström (eds.), 3–27, Kluwer.

Praxeological axioms?

Characterization of worlds

  • An praxeological logic is normal just in case these principles are valid:
    • (necessitation) \top \to D_a\top,
    • (K) D_a(p\to q)\to(D_a p \to D_a q).
    • The two principles show the character of the possible worlds. Worlds are deductively closed: making true all tutologies and all tautological consequences of the facts that obtain in them.

Characterization of accessibility relation

Praxeological variant of T axiom D_a p \to p reads 'if agent a sees to that p is the case, then p is the case (what is done, it is the case). The axiom T characterizes reflexive frames, i.e. strucrures \langle W,R\rangle:
If R is reflexive, then for each frame \langle W,R\rangle it holds that for any w and any V: \langle \langle W,R\rangle V\rangle,w \models D_a p \to p, i.e. D_a p \to p is (V3)-valid in the class of reflexive frames.

1) This kind of validity can be checked using calculator by changing valuations.
2) In his dissertation.