Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
modal_logic [2015/08/09 16:41] nikolaj |
modal_logic [2018/06/16 00:51] nikolaj |
||
---|---|---|---|
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 17: | Line 17: | ||
>$(\Diamond_R P)(w)$ ... $\exists v.\, wRv\land P(v)$ | >$(\Diamond_R P)(w)$ ... $\exists v.\, wRv\land P(v)$ | ||
> | > | ||
- | >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 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: | + | 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 === |