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
Related
