===== Modal Logic =====
==== Framework ====

>**Modal operators**
>$\Box_R$ ... necessarily
>$\Diamond_R=\neg\Box_R\neg$ ... possibly
>
>**Semantics**
>$\langle W,R\rangle$ ... "Kripke frame"
>where
>$W$ ... (type of) worlds
>$R\subseteq W\times W$ ... binary accessibility relation
>$wRv$ ... "$v$ is accessible from $w$"
>
>$P(w)$ ... predicate
>$(\Box_R P)(w)$ ... $\forall v.\, wRv\rightarrow P(v)$
>$(\Diamond_R P)(w)$ ... $\exists v.\, wRv\land P(v)$
>
>The modal operators are similar to $\forall$ and $\exists$, except instead of mapping predicates $P(w)$ to propositions (as in $\forall w.\,P(w)$), they map predicates to predicates (as in $(\Box P)(w)$).

An **example** I cooked up:

>$W$ := legal board configurations in chess
>$wRv$ := there is a game development from $w$ to $v$
>call $w_0$ the initial position for which $\forall v.\,w_0Rv$ 
>
>We use modal operators on predicates of the //current// state to form predicates of what might happen
>$\Box$ = will hold till the end of the game
>$\Diamond$ = might occur till the end of the game
>(this makes for sort of temporal logic which is trivial in that it has no time steps)
>
>$P(w)$ = in the //current// state $w$, you have a pawn on the board
>$K(w)$ = in the //current// state $w$, you have a king on the board
>$B(w)$ = in the //current// state $w$, you have a dark-squared bishop
>
>we can formulate:
>$B(w_0)$ ... at the start, you have a dark-squared bishop
>$\forall v.\,(\Box K)(v)$ ... in all possible states, you do have a king on the board
>$\neg(\Box P)(w_0)$ ... it's not a given that some of your pawns will stay on the board till the end
>$(\Diamond \neg P)(w_0)$ ... equivalently, it might happen that at one point you have no pawns on the board
>$\forall v.\,(\neg P(v)\land\neg B(v))\rightarrow (\Box\neg B)(v)$ ... if you have no pawn on the board and no dark-squared bishop, then, till the end of the game, you'll have no dark-squared bishop
>
>From the last line, using classical predicate logic on the body, we can make the following derivation:

| $(\neg P(v)\land\neg B(v))\rightarrow (\Box\neg B)(v)$ | postulate |
| $\neg P(v)\rightarrow\neg B(v)\rightarrow (\Box \neg B)(v)$ | currying |
| $\neg(\neg B(v)\rightarrow (\Box\neg B)(v))\rightarrow \neg \neg P(v)$ | A implies B $\vdash$ not B implies not A |
| $\neg(\neg B(v)\rightarrow (\Box\neg B)(v))\rightarrow P(v)$ | $\neg \neg$ A $\vdash$ A |
| $\neg(\neg\neg B(v)\lor (\Box\neg B)(v))\rightarrow P(v)$ | A implies B $\vdash$ not A or B |
| $\neg(B(v)\lor (\Box\neg B)(v))\rightarrow P(v)$ | $\neg \neg$ A $\vdash$ A |
| $(\neg B(v)\land \neg(\Box\neg B)(v))\rightarrow P(v)$ | neither A nor B $\vdash$ not A and not B |
| $(\neg B(v)\land (\Diamond B)(v))\rightarrow P(v)$ | $\neg\Box \neg A\vdash \Diamond A$ |

>... if you have no dark-squared bishop but it's still possible that it might happen, then you have a pawn on the board.

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Modal_logic|Modal logic]]

nLab:
[[http://ncatlab.org:8080/nlab/show/necessity%20and%20possibility|necessity and possibility]]

-----
=== Related ===
[[Logic]]