Modal Logic
Framework
Modal operators
◻R … necessarily
◊R=¬◻R¬ … possibly
Semantics
⟨W,R⟩ … “Kripke frame”
where
W … (type of) worlds
R⊆W×W … binary accessibility relation
wRv … “v is accessible from w”
P(w) … predicate
(◻RP)(w) … ∀v.wRv→P(v)
(◊RP)(w) … ∃v.wRv∧P(v)
The modal operators are similar to ∀ and ∃, except instead of mapping predicates P(w) to propositions (as in ∀w.P(w)), they map predicates to predicates (as in (◻P)(w)).
An example I cooked up:
W := legal board configurations in chess
wRv := there is a game development from w to v
call w0 the initial position for which ∀v.w0Rv
We use modal operators on predicates of the current state to form predicates of what might happen
◻ = will hold till the end of the game
◊ = 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(w0) … at the start, you have a dark-squared bishop
∀v.(◻K)(v) … in all possible states, you do have a king on the board
¬(◻P)(w0) … it's not a given that some of your pawns will stay on the board till the end
(◊¬P)(w0) … equivalently, it might happen that at one point you have no pawns on the board
∀v.(¬P(v)∧¬B(v))→(◻¬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:
(¬P(v)∧¬B(v))→(◻¬B)(v) | postulate |
¬P(v)→¬B(v)→(◻¬B)(v) | currying |
¬(¬B(v)→(◻¬B)(v))→¬¬P(v) | A implies B ⊢ not B implies not A |
¬(¬B(v)→(◻¬B)(v))→P(v) | ¬¬ A ⊢ A |
¬(¬¬B(v)∨(◻¬B)(v))→P(v) | A implies B ⊢ not A or B |
¬(B(v)∨(◻¬B)(v))→P(v) | ¬¬ A ⊢ A |
(¬B(v)∧¬(◻¬B)(v))→P(v) | neither A nor B ⊢ not A and not B |
(¬B(v)∧(◊B)(v))→P(v) | ¬◻¬A⊢◊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.