Transcript Modal Logic - CSE, IIT Bombay

Modal Logic
CS 621
Seminar
Group no.: 10
Kiran Sawant (114057001)
Joe Cheri Ross (114050001)
Sudha Bhingardive (114050002)
Modes of Truth
• Propositional logic is decidable but too restrictive.
• FOL and HOL have high expressivity but are not decidable.
• Modal logic extends PL to add expressivity without losing
decidability.
Consider the following:
• Either it rains or it does not rain.
• It may rain today.
• Dr. Manmohan Singh is Prime Minister of India.
• I believe that Ram believes that I know that he did it.
The truth value of some of these sentences depends on the
place, time and judgement of the person who uttered it.
What is Modal Logic?
 Study of modal propositions and logic relationships
 Modal propositions are propositions about what is necessarily
the case and what is possibly the case
Ex:
It is possible for humans to travel to Mars
It is necessary that either it is raining or it is not raining
Modal Operators: □ and ◊
□ is read as “necessarily”
◊ is read as “possibly”
p: It will rain tomorrow
□p: It is necessary that it will rain tomorrow
◊p: It is possible that it will rain tomorrow
□p ↔ ¬◊¬p
Syntax
The formulas of basic modal logic φ are defined by the following
Backus Naur form (BNF):
φ := p | ⊥ | ¬φ | φ ∧ ψ | φ ∨ ψ | φ → ψ | φ ↔ ψ | □φ | ◊φ
where "p" is any atomic formula
Example:
□p →□ □ p
p ∧ ◊(p → □¬r)
□((◊q ∧ ¬r) → □p)
Meanings of the Modal Operators
□
◊
Alethic logic
p is necessarily
true
p is possibly true
Deontic logic
p is obligatory
p is permitted
Temporal logic
p will always be true
p will become true
Sometime in future
Epistemic logic
p knows that
P believes that
Semantics
Kripke structures (possible worlds structures) are models of
basic modal logic.
A Kripke structure is a tuple M = (W,R,L) where
 W is a non-empty set (possible Worlds)
 R ⊆ WΧW is an accessibility relation (wRv)
L : W →P, {true, false} is a labelling function
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Truth of Modal Formulas
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Example of Kripke Structure
Inference Rules
lUS – Rule of Uniform Substitution: The result of uniformly replacing any variables p1,
…, pn in a theorem by any WFF φ1, …, φn respectively, is itself a theorem
lMP – Modus Ponens
lNR – Rule of Necessitation: If φ is a theorem, so is □φ
Axioms and their Corresponding
Properties on Accessibility Relations
Axiom
Formula Scheme
Property on R
K
□ (φ → ψ) → (□φ → □ψ )
T
□φ → φ
Reflexive
B
φ → □◊φ
Symmetric
D
□φ → ◊φ
Serial
4
□φ → □□φ
Transitive
5
◊φ → □◊φ
Euclidean
□φ ↔ ◊φ
Functional
Some modal logic systems take only a subset of this set
All general, problem independent theorems can be derived
from only these axioms and some additional, problem
specific axioms describing the research problem
Which Formula Schemes Should
Hold for these Readings of □?
□φ
K
T
D
4
5
It is necessarily true that φ
Y
Y
Y
Y
Y
It will always be true that φ
Y
It ought to be that φ
Y
Y
Agent Q believes that φ
Y
Y
Y
Y
Agent Q knows that φ
Y
Y
Y
Y
Y
Y
Axiomatic Systems
Systems:
K := K + N
T := K + T
S4 := T + 4
S5 := S4 + 5
D := K + D
Example of Inference in Modal
Logic
Given: □(p → q) and □p
Infer: □q
where, p: It rained. q: Grass is wet.
1.□(p → q) [Given]
2.□p
[Given]
3.□p → □q [K, 1]
4.□q
[MP, 3 and 2]
Muddy Children
Problem Statement
Two children a and b coming to mother after playing
Mother says “Atleast one of you has dirty forehead”
She asks each one “Do you know whether your
forehead is dirty ? “
If b says “yes”: a's forehead is not muddy
If b says “no”: both foreheads are muddy
Muddy Children
Kripke Structure
(A,B)
W4
(1 1)
a
(0 1)
b
W3
W2
b
a
W1
(0 0)
(1 0)
Muddy Children
Formalization
A: a's forehead is dirty
B: b's forehead is dirty
Ki : Child i knows

Initial: Ka Kb (A ∨ B)
After first query: Ka ¬Kb B
Final: Ka A
Muddy Children
Proof
1.
2.
3.
4.
1.
Ka Kb(¬A → B)
Ka (Kb ¬A → Kb B)
Ka¬KbB → Ka¬Kb¬A
Ka¬KbB
Ka¬Kb¬A
6. Ka(¬Kb¬A → KbA)
7. Ka Kb A
8. Ka A
Premise (Mother said)
K- Axiom
(p→q)(¬q → ¬p), K- Axiom
After 1st query
3,4- MP
Premise(Init)
5,6- Axiom K and MP
7- Axiom T
Conclusion
• Modal logic forms the basis for other kinds of logic.
• Modal logic extends the expressivity propositional logic.
• Modal logic is a non-numeric alternative to different logics
like fuzzy logic, probabilistic logic, multiple-valued logic.
• Fuzzy logic operations on uncertainties derive uncertainties
(better or worse), whereas in modal logic one can derive
certainties from uncertainties.
• Relevant in various fields such as knowledge
representation[6], linguistics[5], verification.
References
1.P. Blackburn, et. al., Modal Logic, Cambridge: Cambridge
University Press, 2001
2.P. Blackburn, et. al., Handbook of Modal Logic, New York:
Elsevier Science Inc, 2006
3.S. A. Kripke, "A Completeness Theorem in Modal Logic",
The Journal of Symbolic Logic, vol. 24, no. 1, 1-14, Mar.
1959
4.J. Doyle, "A Truth Maintenance System", Artificial
Intelligence, vol. 12, no. 3, 231-272, 1979
5.L. S. Moss and H. Tiede, "Applications of Modal Logic in
Linguistics", Elsevier Science. Linguistics, 1031-1077, 2006
6.R. Rosati, "Multi-modal Nonmonotonic Logics of Minimal
Knowledge", Annals of Mathematics and Artificial
Intelligence, vol. 48, no. 3-4, 169-185, Dec. 2006
BACKUP
Example 1:
Example 1:
Example 1:
Example 1:
Example 2:
Example 2:
Example 2:
Cards game: Kripke structure
Wise Men Puzzle
Problem description

3 Wise men

There are 3 Red hats and 2 white hats



The King puts a hat on each of them and
ask sequentially the color of their hat on
their head
1st man and 2nd man say he doesn't know
We have to prove whether 3rd man now
knows his hat is red
Wise Men Puzzle
Solution Method

Initially:W
RRR
RRW RWR RW
WRR WRW WWR
WWW
After 1st man says he doesn't know:-
RRR
RRW RWR WRR WRW
WWR RWW
After 2nd man says he doesn't know:RRR RRW RWR WRR WRW
WWR RWW
Wise Men Puzzle
Initial Knowledge
Pi means man i has red hat.
¬Pi means man i has white hat.
Kj Pi means agent/man j knows that man i
has a red hat.
Let Γ be set of formulas:{C(p1 ∨ p2 ∨ p3),
C(p1 → K2 p1), C(¬p1 → K2 ¬p1),
C(p1 → K3 p1), C(¬p1 → K3 ¬p1),
C(p2 → K1 p2), C(¬p2 → K1 ¬p2),
Wise Men Puzzle
Formalisation
Naive approach
Γ, C(¬K1 p1 ∧ ¬K1 ¬p1), C(¬K2 p2
∧ ¬K2 ¬p2) |− K3 p3


This doesn't capture time between events
(2nd man answers after 1st)
To formalise correctly this has to be broken into 2
entailments, corresponding to each
announcement
Wise Men Puzzle
Correct Formalisation


1. Γ, C(¬K1 p1 ∧ ¬K1 ¬p1) |−
C(p2 ∨ p3).
2. Γ, C(p2 ∨ p3), C(¬K2 p2,∧¬K2
¬p2) |− K3 p3.
Wise Men Puzzle
Proof of Entailment 1




1 C(p1 ∨ p2 ∨ p3)
premise
2 C(pi → Kj pi)
premise, (i= j)
3 C(¬pi → Kj ¬pi)
(i = j)
premise,
4 C¬K1 p1
premise

5 C¬K1 ¬p1

6 C
premise

13 K1

14 ¬p2
K1e 11

15 ¬p3
K1e 12

16 ¬p2 ∧ ¬p3
∧i 14, 15

17 p1 ∨ p2 ∨ p3
Ce 1

18 p1
prop 16, 17

19 K1 p1
K1i 13−18

20 ¬K1 p1
Ce 4

21 ⊥
¬e 19, 20
Wise Men Puzzle
Proof of Entailment 2

1 C(p1 ∨ p2 ∨ p3)

2 C(pi → Kj pi)
premise, (i = j)

3 C(¬pi → Kj ¬pi)
premise, (i = j)

4 C¬K2 p2
premise

5 C¬K2 ¬p2
premise

6 C(p2 ∨ p3)
premise

7 K3

8 ¬p3
assumption

9 ¬p3 → K2 ¬p3
CK 3 (i, j) = (3, 2)

10 K2 ¬p3
→e 9, 8
premise

11 K2

12 ¬p3
K2e 10

13 p2 ∨ p3
Ce 6

14 p2
prop 12, 13

15 K2 p2
K2i 11−14

16 Ki ¬K2 p2
CK 4, for each i

17 ¬K2 p2
KT 16

18 ⊥

19 p3
PBC 8−18

20 K3 p3
K3i 7−19
¬e 15, 17