Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
modal_logic [2015/08/09 16:40] nikolaj |
modal_logic [2015/08/09 17:37] ben |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| >$W$ ... (type of) worlds | >$W$ ... (type of) worlds | ||
| >$R\subseteq W\times W$ ... binary accessibility relation | >$R\subseteq W\times W$ ... binary accessibility relation | ||
| - | >$wRv$ ... "$w$ is accessibility from $v$" | + | >$wRv$ ... "$v$ is accessible from $w$" |
| > | > | ||
| >$P(w)$ ... predicate | >$P(w)$ ... predicate | ||
| Line 19: | Line 19: | ||
| >The modal operators are similar to $\forall$ and $\exists$, except instead of maping predicates $P(w)$ to propositions (as in $\forall w.\,P(w)$), they map predicates to predicates (as in $(\Box P)(w)$). | >The modal operators are similar to $\forall$ and $\exists$, except instead of maping predicates $P(w)$ to propositions (as in $\forall w.\,P(w)$), they map predicates to predicates (as in $(\Box P)(w)$). | ||
| - | And **Example** I just cooked up: | + | An **example** I cooked up: |
| >$W$ := legal board configurations in chess | >$W$ := legal board configurations in chess | ||
| Line 30: | Line 30: | ||
| >(this makes for sort of temporal logic which is trivial in that it has no time steps) | >(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 field | + | >$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 field | + | >$K(w)$ = in the //current// state $w$, you have a king on the board |
| - | >$B(w)$ = in the //current// state $w$, you have a bishop on a black field | + | >$B(w)$ = in the //current// state $w$, you have a dark-squared bishop |
| > | > | ||
| >we can formulate: | >we can formulate: | ||
| - | >$B(w_0)$ ... at the start, you have a bishop on a black field | + | >$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 field | + | >$\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 | >$\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 | >$(\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 bishop on a black field, then, till the end of the game, you'll have no bishop on a black field | + | >$\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: | >From the last line, using classical predicate logic on the body, we can make the following derivation: | ||
| Line 52: | Line 52: | ||
| | $(\neg B(v)\land (\Diamond B)(v))\rightarrow P(v)$ | $\neg\Box \neg A\vdash \Diamond A$ | | | $(\neg B(v)\land (\Diamond B)(v))\rightarrow P(v)$ | $\neg\Box \neg A\vdash \Diamond A$ | | ||
| - | >... if you have no bishop on a black field but it's still possible that it might happen, then you have a pawn on the field. | + | >... 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 === | === Reference === | ||
