Manuel Kauers Introduction to Modal Logics

Syntax: Formulas of Prepositional Modal Logic

• Let Σ be a set of boolean variables

• The formula set MFor is defined by – Σ ⊆ MFor,

– true, false ∈ MFor,

– A, B ∈ MFor ⟹ (A → B), (A ∧ B), (A ∨ B) ∈ MFor,

– A ∈ MFor ⟹ ¬A, □A, ◇A ∈ MFor.

• □A “Box”: A is necessary

• ◇A “Diamond”: A is possible

• ◇A :↔ ¬□¬A

• Examples: □p → □□p, ◇p ∧ ¬□q ∨ (q ↔ p), etc.

Interpretations of Box and Diamond

• There are several possibilities

Name  □F  ◇F

classic modal F is necessarily true

F is possibly true

temporal F is true from now on

F will become true at some point

deontic F is obligatory

F is permitted

doxastic An agent believes F F is consistent with the things an

agent believes

epistemic An agent knows F An agent does not know that F is

false

dynamic F is true after each execution of a program There is an execution of a program after which F is true

“automaton” F is true in all reachable states There is a reachable state in which F

is true.

“Leibniz” F is true “in all worlds”

There is “a world” where F is true

Axiom Candidates

• What tells us the intuition?

□(F → G)
□F  F → □F □F → F □F → ◇F □F → □□F → (□F → □G)

F is necessarily true, F is true from now on An agent believes F An agent knows F F is obligatory F is true after each execution of a program F is true in all reachable states

Manuel Kauers Introduction to Modal Logics

Axiom Candidates

• What tells us the intuition?

□(F → G)
□F  F → □F □F → F □F → ◇F □F → □□F → (□F → □G)
F is necessarily true,  yes  yes  yes  yes  yes
F is true from now on  yes  no  no  yes  yes
An agent believes F  yes  no  yes  yes  yes
An agent knows F  yes  yes  yes  yes  yes
F is obligatory  yes  no  yes  no  yes

F is true after each

execution of a program  yes  no  no  no  yes
F is true in all reachable states  yes  no  no  no  yes

Axiom Systems

• Various axiom systems are defined

• The simples one is K.

– Axioms of K:

∗ All prepositional tautologies ∗ □(A → B) → (□A → □B)

– Deduction rules of K:

∗ Modus Ponens (MP): \frac{A, A → B}{B} ∗ Necessitation (N): \frac{A}{□A}

• Other systems are obtained by adding further axioms to K.

• For instance T is K plus □A → A.

• Logic consequences can be proven from axioms and rules. Examples: – □A ∧ □B ↔ □(A ∧ B) in K

– □A ∨ □B → □(A ∨ B) in K

Three Philosophers With Hats I

• Three philosophers named 1, 2, 3, are sitting aroud.

• Each is wearing a hat which is black or white.

• There is at least one black hat.

• Everybody can see the color of the others’ hats.

• No. 1 says he doesn’t know the color of his hat.

• No. 2 says he deosn’t know either.

• But no. 3 says that he must then have a black hat.

• How is this possible?

• Formalize and prove it in an appropriate modal logic!

Three Philosophers With Hats II

• Formalisation in multimodal logic.

• □_{i}A means “No. i knows A.”

• B_{i} be a boolean variable expressing that i’s hat is black.

• One hat is black: B_{1} ∨ B_{2} ∨ B_{3}.

• Everybody can see the others’ hats: B_{1} → □_{2}B_{1}, ¬B_{1} → □_{2}¬B_{1}, etc.

• The first doesn’t know: ¬□_{1}B_{1}

• The second doesn’t know: ¬□_{2}B_{2}

• To prove: □_{3}B_{3}.

Manuel Kauers Introduction to Modal Logics

Three Philosophers With Hats III

• Proof:

1 (F)  B_{1} ∨ B_{2} ∨ B_{3}  10 (9)  ¬B_{3} → B_{2}
2 (1)  (¬B_{2} ∧ ¬B_{3}) → B_{1}  11 (10)  □_{2}(¬B_{3} → B_{2})
3 (2)  □_{1}((¬B_{2} ∧ ¬B_{3}) → B_{1})  12 (11)  □_{2}¬B_{3} → □_{2}B_{2}
4 (3)  □_{1}(¬B_{2} ∧ ¬B_{3}) → □_{1}B_{1}  13 (F)  ¬□_{2}B_{2}
5 (F)  ¬□_{1}B_{1}  14 (12, 13) ¬□_{2}¬B_{3}
6 (4, 5)  ¬□_{1}(¬B_{2} ∧ ¬B_{3})  15 (F)  ¬B_{3} → □_{2}¬B_{3}
7 (F)  (¬B_{2} ∧ ¬B_{3}) → □_{1}(¬B_{2} ∧ ¬B_{3})  16 (14, 15) B_{3}
8 (6, 7)  ¬(¬B_{2} ∧ ¬B_{3})  17 (16)  □_{3}B_{3}
9 (8)  B_{2} ∨ B_{3}

Semantics: Kripke Structures

• Kripke Frame: pair (G, R) with a set G and a relation R on G. More or less a “graph.”

• Signature Σ: A set of boolean variables

• Kripke Structure: triple K = (G, R, v) where (G, R) is a Kripke frame, and v: Σ × G → {0, 1} is a valuation.

• Example:

[figure: ¬p, ¬q; a; b; p, ¬q]

[figure]

[figure: p, q; d; c; ¬p, q]

• G may or may not be finite

• There are no restrictions on R in general

Semantics: Interpretation

• Let K = (G, R, v) be a Kripke structure, g ∈ G, F ∈ MFor.

• g ⊧ F (“F holds in g”) is defined by structural induction – g ⊧ p iff v(g, p) = 1

– g ⊧ ¬A iff not g ⊧ A

– g ⊧ A ∨ B iff g ⊧ A or g ⊧ B

– g ⊧ A ∧ B iff g ⊧ A and g ⊧ B

– g ⊧ A → B iff g ⊧ B or not g ⊧ A

– g ⊧ □A if ∀ h ∈ G : (R(g, h) ⟹ h ⊧ A)

– g ⊧ ◇A if ∃ h ∈ G : (R(g, h) ∧ h ⊧ A)

• K ⊧ F means that g ⊧ F for all g ∈ G.

• Semantic Consequences: Let A, B ∈ MFor – A ⊧_{L} B (local consequence) iff ∀ K = (G, R, v) ∀ g ∈ G : (g ⊧ A ⟹ g ⊧ B)

– A ⊧_{G} B (global consequence) iff ∀ K = (G, R, v) : (∀g ∈ G : g ⊧ A ⟹ ∀ g ∈ G : g ⊧ B)

Syntax vs. Semantics

• Why is semantics defined like this?

• Because then A ⊢_{K} B ⟺ A ⊧_{G} B

• “⇐” To show: Axioms and rules work.

– K ⊧ A if A is prepositional tautology

– K ⊧ □(A → B) → (□A → □B)

– If K ⊧ A and K ⊧ A → B then K ⊧ B

– If K ⊧ A then K ⊧ □A

• “⇒” nontrivial.

• Application: ⊬_{K} □(A ∨ B) → (□A ∨ □B) can be shown by providing the following counterexample:

[figure: h_{1}] p, ¬q
[figure: g]
[figure] [figure: h_{2}] ¬p, q

Semantics for other Axiom Systems

• Kripke Structures turned out to be adequate for K

• What about other axiom systems?

• Other systems are obtained by extending K by further axioms.

• Adding axioms corresponds to restricting the class of admissible frames

• Example: T is K plus □A → A.

• ⊢_{T} A iff K ⊧_{G} A for all K whose underlying frames are reflexive.

• More general: There is a “relationship” between the formula □p → p in MFor and the formula ∀ x : R(x, x) in predicate logic.

• Correspondence theory studies this kind of correspondence in depth and leads to interesting insights.

Other Aspects of Modal Logics

• Correspondence Theory

• Tense Logic

• Completness results

• Decidability and Automated Theorem Proving • Modal Predicate Logic

• Specification Languages

• Dynamic Logic

• …