## 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 thecurrentstate 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 thecurrentstate $w$, you have a pawn on the board

$K(w)$ = in thecurrentstate $w$, you have a king on the board

$B(w)$ = in thecurrentstate $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.