Processing math: 100%

Framework

Modal operators
R … necessarily
R=¬R¬ … possibly

Semantics
W,R … “Kripke frame”
where
W … (type of) worlds
RW×W … binary accessibility relation
wRv … “v is accessible from w

P(w) … predicate
(RP)(w)v.wRvP(v)
(RP)(w)v.wRvP(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) ¬¬AA
… 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

Link to graph
Log In
Improvements of the human condition