Modal logic formalization of chess

modal_logic_of_chess.txt

# Text used in the video
#
# https://youtu.be/E6wr0MtbKrY

A         ... Predicate
A(x)      ... One reading: "A is satisfied by x."
              Here: "The state x forces A to hold."

Modalities: Model necessity, knowledge, believe, persistence, obligation, ...
◻
◊ ≡ ¬◻¬

◻A        ... another Predicate
◻A(x)     ... One reading: "A is necessarily satisfied by x."
              Here: "The state x necessarily forces A to hold persistently (forever)."
◊A(x)     ... One reading: "A is not necessarily not satisfied by x (A is possible for x)."
              Here: "It's still possible for x to allow for A."

Semantics:
⟨W, R⟩              ... Kripke frame
W                   ... type of states (worlds)
R : W × W → {T, F}  ... Binary accessibility relation
                        Reading: R(s, t) ... "The state t is accessible from the state s"

◻A(s) ... ∀t. R(s, t) → A(t) ... Akin to an all-quantor over a poset of which s is the bottom.

## Chess example
W := The legal board configurations in chess
R(s, t) := There is a game development from s to t.
Call i the initial position for which ∀s. R(i, s)

We use modal operators on predicates of the current state to from predicates
of what might happen, as in:
◻A(s) := From the state s on, A will necessarily hold till the end of the game.
◊A(s) := From the state s on, there will possibly be some state in which A holds.

P(s) := In the state s, you have a pawn on the board.
K(s) := In the state s, you have a king on the board.
B(s) := In the state s, you have a dark-squared bishop on the board.

We can formulate:
B(i)                          == At the start of the game, you have a dark-squared bishop
◻K(i)                         == In all possible states, you do have a king on the board.
¬◻P(i)                        == It's not a given that any of you pawns will stay
                                 on the board till the end.
◊¬P(i)                        == Equivalently, it might happen that at one point after the start,
                                 you have no pawns on the board.

### A Derivation
∀s. (¬B(s) ∧ ¬P(s)) → ◻¬B(s)  == If you have no dark-squared bishop and no pawn
                                 on the board, then, till the end of the game,
                                 you'll have no dark-squared bishop.
(¬B(c) ∧ ¬P(c)) → ◻¬B(c)
¬◻¬B(c) → ¬(¬B(c) ∧ ¬P(c))      via   X → Y       |-  ¬Y → ¬X
◊B(c) → (¬¬B(c) ∨ ¬¬P(c))       via   ¬(X ∧ Y)    |-  ¬X ∨ ¬Y
◊B(c) → (¬B(c) → P(c))          via   ¬X ∨ Y      |-  X → Y
(◊B(c) ∧ ¬B(c)) → P(c)          via   X → Y → Z   |-  (X ∧ Y) → Z

As it's the case that
"if you have no dark-squared bishop and no pawn on the board,
then, till the end of the game, you'll have no dark-squared bishop."
it is also the case that
"if it's still possible that you can have a dark-squared bishop on the board
despite not having one now, then you have a pawn on the board."