Logica voor AI eserved@d = *@let@token

Logica voor AI
Logica voor AI
Modale Logica
De taal Lm
Inleiding modale logica en Kripke semantiek
Kripke Semantiek
Geldigheid
Albert Visser
[email protected]
12 november 2014
1
Logica voor AI
Deel 1: Modale logica
semantiek en syntax van verschillende modale logica’s
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Deel 2: (Dynamische) epistemische logica en
toepassingen
kennislogica, kennis-geloof-interactie, common knowledge,
distributed knowledge, gedistribueerde systemen, weak modal
logics, interpreted systems, public announcement, product
update, . . .
2
Logica voor AI
Hoorcollege
Logica voor AI
Modale Logica
I
woensdag 13.15 - 15.00, BBG 161
De taal Lm
I
vrijdag 11.00 - 12.45, BBG 161
Kripke Semantiek
Geldigheid
Werkcollege
I
woensdag 15.15 - 17.00, BBG 079
I
vrijdag 13.15 - 15.00, BBG 065
Assistenten: Hein Duif, Jetze Baumfalk, Mandy Filet.
3
Logica voor AI
Huiswerkopgaven
Aangereikt uiterlijk woensdag, inleveren op de volgende
woensdag.
Het gemiddelde van de cijfers van de huiswerkopgaven wordt
voor 20% meegeteld (10% voor elk Deel). De deeltoetsen tellen
elk voor 40%.
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Tentamens
I
Deel 1: vrijdag 12/12/2014, ??
I
Deel 2: vrijdag 30/01/2015, 13.30 – 16.30, Ruppert Blauw
Dit jaar zullen de delen iets meer door elkaar lopen.
4
Logica voor AI
Website
Logica voor AI
Modale Logica
I
http://www.cs.uu.nl/education/vak.php?vak=INFOLAI
De taal Lm
I
http://www.cs.uu.nl/docs/vakken/lai/
Kripke Semantiek
Geldigheid
Literatuur
I
Deel 1: Modal Logic — collegeaantekeningen van Rosja
Mastop
I
Deel 2: H. van Ditmarsch, W. van der Hoek, B. Kooi.
Dynamic Epistemic Logic. Springer, 2007.
5
Logica voor AI
Logica voor AI
Programma
I
woe 12/11/14 (AV): inleiding modale logica, Kripke
semantiek
I
vrij 14/11/14 (AV): Geldigheid, Logisch Gevolg
I
woe 19/11/14 (JB): Epistemische Logica
I
vrij 21/11/14 (JB): Common Knowledge
I
woe 26/11/14: (AV) Correspondentietheorie
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
6
Modale Logica
Dat is de logica die zich bezig houdt met de logische analyse
van uitspraken en redeneringen waarin modaliteiten zoals ‘het
is noodzakelijk dat’ en ‘het is mogelijk dat’ voorkomen
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Modaliteiten
I
alethisch: noodzakelijkheid
I
epistemisch: kennis
I
doxastisch: geloof
I
deontisch: verplichting
I
temporeel: tijd
Geldigheid
7
Modale Logica
Propositielogica
De connectieven van de propositielogica zijn
waarheidsfunctioneel.
p q p∧q
p ¬p
1 1
1
1
0
1 0
0
0
1
0 1
0
0 0
0
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Modale logica
Modale operatoren zijn geen waarheidsfunctionele
connectieven.
Vergelijk:
(i) Het is noodzakelijk dat 2+2=4.
(ii) Het is noodzakelijk dat ik schoenen draag.
8
Geschiedenis van de Modale Logica
Logica voor AI
Aristoteles (384–322 BCE): Analytica Priora:
Dualiteit
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
I
Het is noodzakelijk dat A
desda
het is niet mogelijk dat niet A .
I
Het is mogelijk dat A
desda
het is niet noodzakelijk dat niet A .
9
Geschiedenis van de Modale Logica
C.I. Lewis (1883–1964):
¨ (→) vs. strikte implicatie (J)
Materiele
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
I
Als de maan van groene kaas is gemaakt, dan is Jan
Klaassen geen vrijgezel.
I
Als Katrijn de vrouw van Jan Klaassen is, dan is Jan
Klaassen geen vrijgezel.
A JB
desda
Geldigheid
het is noodzakelijk dat (A → B ).
10
Geschiedenis van de Modale Logica
R. Carnap (1891–1970):
Modale operatoren als kwantoren (1947)
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
I
Het is noodzakelijk dat A
desda
Geldigheid
A is in alle mogelijke situaties (of toestanden) waar.
I
Het is mogelijk dat A
desda
´ mogelijke situatie (of toestand) waar.
A is in tenminste e´ en
Verband met Leibniz idee van mogelijke werelden. Carnap
dacht eerder aan een soort modellen.
11
Geschiedenis van de Modale Logica
Logica voor AI
Modale Logica
Arthur Prior (1914–1969): Tijdslogica
De taal Lm
Kripke Semantiek
I
Het is altijd het geval geweest dat A
desda
Geldigheid
A is in alle eerdere tijdstippen waar.
I
Het is ooit geval geweest dat A
desda
´ eerder tijdstip waar.
A is in tenminste e´ en
12
Geschiedenis van de Logica
Logica voor AI
Relatieve modaliteit
I
Voorbeeld: Schaakspel
Modale Logica
De taal Lm
Kripke Semantiek
Niet iedere spelsituatie (toestand op het bord) kan vanuit
´ zet (van zwart of
´ wit) bereikt
iedere spelsituatie met e´ en
worden en vanuit verschillende spelsituaties kunnen
verschillende spelsituaties bereikt worden.
I
Ik weet niet of het morgen regent, maar ik weet dat ik het
niet weet.
I
A weet dat B weet dat C weet . . . .
Geldigheid
13
Geschiedenis van de Modale Logica
Saul Kripke (1940):
Kripke modellen (1959, 1963)
Logica voor AI
Modale Logica
I
Verzameling mogelijke werelden
De taal Lm
I
Bereikbaarheidsrelatie(s) tussen de mogelijke werelden
Kripke Semantiek
I
Valuatie
Geldigheid
Relatieve modaliteit
I
Het is noodzakelijk dat A
desda
ϕ is in elke bereikbare wereld waar.
I
Het is mogelijk dat A
desda
´ bereikbare wereld waar.
ϕ is in tenminste e´ en
14
Geschiedenis van de Modale Logica
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Figure: Saul Kripke
15
Geschiedenis van de Modale Logica
The muddy children
I
I
Situatie: Er zijn 3 kinderen waarvan er 2 modder op hun
voorhoofd hebben.
Aankondiging van de vader:
´ kind dat modder op zijn voorhoofd
“Er is tenminste e´ en
heeft. Over vijf minuten stapt iedereen naar voren die weet
dat hij modder op zijn voorhoofd heeft.”
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Wat gebeurt er vijf minuten later?
I
Vader opnieuw:
“Over vijf minuten stapt iedereen naar voren die weet dat
hij modder op zijn voorhoofd heeft.”
Wat gebeurt er vijf minuten later?
Jan gaat dit volgende week behandelen.
16
De taal Lm van de modale propositielogica
Blokje en ruitje
I
ϕ: het is noodzakelijk dat ϕ
I
^ϕ: het is mogelijk dat ϕ
I
Epistemische logica: Ka ϕ: a weet dat ϕ (ipv )
I
Doxastische logica: Ba ϕ: a gelooft dat ϕ (ipv )
I
Deontische logica: O ϕ: het is verplicht dat ϕ (ipv )
I
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Temporele logica: P ϕ: het is ooit zo geweest dat ϕ (ipv ^)
F ϕ: het zal eens zo zijn dat ϕ (ipv ^)
17
De taal Lm van de modale propositielogica
Logica voor AI
Het alphabet van Lm
I
propositieletters: VAR = {p , q, r , . . . }
I
logische constanten: ⊥, >, ¬, ∨, ∧, →, ↔, , ^
I
hulpssymbolen: (, )
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
De taal Lm
ϕ ::= p | ⊥ | > | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | ϕ ↔ ϕ | ϕ | ^ϕ
18
Kripke Semantiek
Modelstructuur (of frame)
Logica voor AI
Een modelstructuur (of frame) is een geordend paar
F = hW, Ri, waarbij
I
W , ∅ een verzameling mogelijke werelden en
I
R ⊆ W × W een bereikbaarheidsrelatie is.
w
v
u
t
s
r
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
19
Kripke Semantiek
Modelstructuur (of frame)
Logica voor AI
Een modelstructuur (of frame) is een geordend paar
F = hW, Ri, waarbij
I
W , ∅ een verzameling mogelijke werelden en
I
R ⊆ W × W een bereikbaarheidsrelatie is.
w
v
u
t
s
r
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
20
Kripke Semantiek
Kripke Model
Een Kripke model is een geordend drietal M = hW, R, Vi,
waarbij
Logica voor AI
Modale Logica
De taal Lm
I
hW, Ri een modelstructuur en
I
V : W → Pow (VAR ) een interpretatiefunctie is.
Kripke Semantiek
Geldigheid
Een propositie p is waar in een wereld w desda p ∈ V(w ).
(p , q)
(p)
(q)
w
v
u
t
s
r
(q)
(p)
(q)
21
Kripke Semantiek
De semantische regels voor en ^
I
ϕ is waar in wereld w in model M
desda
voor iedere wereld v met wRv geldt: ϕ is waar in v.
Logica voor AI
Modale Logica
De taal Lm
I
^ϕ is waar in wereld w in model M
desda
´ wereld v met wRv geldt: ϕ is waar in v.
voor tenminste e´ en
Kripke Semantiek
Geldigheid
Dualiteit
I
ϕ ↔ ¬^¬ϕ
I
^ϕ ↔ ¬¬ϕ
Vergelijk:
I
∀x ϕ(x ) ↔ ¬∃x ¬ϕ(x )
I
∃x ϕ(x ) ↔ ¬∀x ¬ϕ(x )
22
Kripke Semantiek
Waarheid in een wereld: M, w ϕ
Zij ϕ ∈ Lm een formule, M = hW, R, Vi een Kripke model en
w ∈ W een wereld.
I
M, w p desda p ∈ V(w )
I
M, w 2 ⊥
I
M, w ¬ϕ desda M, w 2 ϕ
I
M, w ϕ ∧ ψ desda M, w ϕ en M, w ψ
I
M, w ϕ ∨ ψ desda M, w ϕ en/of M, w ψ
I
M, w ϕ → ψ desda M, w 2 ϕ en/of M, w ψ
I
M, w ϕ desda voor iedere v met wRv geldt M, v ϕ
I
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
´ v met wRv geldt
M, w ^ϕ desda voor tenminste e´ en
M, v ϕ
23
Kripke Semantiek
(p , q)
(p)
(q)
w
v
u
Logica voor AI
Modale Logica
t
s
r
(q)
(p)
(q)
De taal Lm
Kripke Semantiek
Geldigheid
I
I
I
I
I
I
I
M, w
M, w
M, w
M, w
M, w
M, w
M, w
^p want wRv en M, v p
^¬p want wRt en M, t ¬p
^p ∧ ^¬p want M, w ^p en M, w ^¬p
2 p, d.w.z. M, w ¬p, want wRt en M, t 2 p
2 q want wRv en M, v 2 q
2 p ∨ q want M, w 2 p en M, w 2 q
(p ∨ q) want M, w p ∨ q, M, v p ∨ q,
M, t p ∨ q en w , v , t zijn de
enige werelden x met wRx
24
Kripke Semantiek
(p , q)
(p)
(q)
w
v
u
Logica voor AI
Modale Logica
t
s
r
(q)
(p)
(q)
I
M, t ^p
want tRv en M, v p
I
M, t p
want v is de enige wereld x met tRx
I
M, u ^^p
I
M, u ^^p → ^p
want M, u ^^p en M, u ^p
I
M, u ^p → ¬p
want M, u ^p en M, u ¬p,
omdat uRu en M, u 2 p
I
M, u p → q
De taal Lm
Kripke Semantiek
Geldigheid
want uRu en M, u ^p, omdat uRv en
M, v p
want M, u 2 p
25
Kripke Semantiek
(p , q)
(p)
(q)
w
v
u
Logica voor AI
Modale Logica
De taal Lm
t
s
r
(q)
(p)
(q)
I
M, r ⊥
want r is een blinde wereld
I
M, r 2 ^>
want r is een blinde wereld
I
M, v p
want v is een blinde wereld
I
M, v ((^q ∧ (p ∨ q)) → q)
Kripke Semantiek
Geldigheid
Algemeen:
I
M, x ϕ voor alle ϕ ∈ Lm desda er is geen z met xRz
I
M, x 2 ^ϕ voor alle ϕ ∈ Lm desda er is geen z met xRz
26
Geldigheid
Geldigheid in een model: M ϕ
Zij ϕ ∈ Lm een formule en M = hW, R, Vi een Kripke model.
ϕ is geldig in het model M, notatie: M ϕ,
desda
voor alle werelden w ∈ W geldt M, w ϕ
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
(p , q)
(p)
(q)
w
v
u
I
M (p ∨ q)
I
M (p ∨ ¬p )
I
M ^q → ¬q
t
s
r
I
M ^^p → ^p
(q)
(p)
(q)
27
Geldigheid
Geldigheid in een model
Hoe laat je zien dat een formule ϕ niet geldig is in een model
M = hW, R, V i?
Je laat zien dat er een wereld w ∈ W is zodanig dat M, w 2 ϕ.
(p , q)
(p)
(q)
w
v
u
t
s
r
(q)
(p)
(q)
I
M 2 ^p
want M, w 2 ^p, omdat wRv en v is
een blinde wereld
I
M 2 ⊥
want M, t 2 ⊥, omdat tRv en M, v 2 ⊥
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
28
Geldigheid
Geldigheid in een modelstructuur: F ϕ
Zij ϕ ∈ Lm een formule en F = hW, Ri een modelstructuur.
Logica voor AI
Modale Logica
De taal Lm
ϕ is geldig in een modelstructuur F , notatie: F ϕ,
voor alle modellen M = hW, R, Vi geldt M ϕ
I
F ^^p → ^p
I
F (p ∨ ¬p )
I
F 2 (p ∨ q)
I
F 2 ^q → ¬q
desda
Kripke Semantiek
Geldigheid
w
v
u
t
s
r
29
Geldigheid
Geldigheid in een modelstructuur
Hoe laat je zien dat een formule ϕ niet geldig is in een
modelstructuur F = hW, Ri?
Je geeft een valuatie V op de modelstructuur zodanig dat voor
´ wereld w in het model M = hW, R, Vi geldt
tenminste e´ en
M, w 2 ϕ.
(p , q)
(p , q)
()
u
w
v
I
I
t
s
r
(q)
(p)
(q)
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
F 2 (p ∨ q)
want M, u 2 (p ∨ q),
omdat uRu en M, u 2 p ∨ q
F 2 ^q → ¬q want M, t 2 ^q → ¬q,
omdat M, t ^q en M, t q
30
Geldigheid
Algemene modaallogische geldigheid: ϕ
Zij ϕ ∈ Lm een formule.
Logica voor AI
Modale Logica
ϕ is algemeen modaallogisch geldig, notatie: ϕ,
voor alle modelstructuren F = hW, Ri geldt F ϕ
I
(p ∨ ¬p )
I
2 ^^p → ^p
(p , q)
(p)
(q)
w
v
u
t
s
r
(q)
(p)
(q)
De taal Lm
desda
Kripke Semantiek
Geldigheid
31
Geldigheid
Algemene modaallogische geldigheid
ϕ is algemeen modaallogisch geldig
desda
ϕ is in alle modelstructuren F = hW, Ri geldig
desda
ϕ is in alle modellen M = hW, R, Vi geldig
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Hoe laat je zien dat een formule ϕ niet algemeen modaallogisch
geldig is?
Je geeft een model M = hW, R, Vi zodanig dat in tenminste
´ wereld w ∈ W geldt M, w 2 ϕ.
e´ en
(p) w
I
2 ^^p → ^p
v ()
omdat M, w ^^p en M, w 2 ^p
32
Geldigheid
Logica voor AI
Geldige gevolgtrekking: Γ ϕ
Modale Logica
De taal Lm
Een formule ϕ ∈ Lm is een geldige gevolgtrekking uit een
verzameling van formules Γ ⊆ Lm , notatie: Γ ϕ, desda
Kripke Semantiek
Geldigheid
voor alle modellen M = hW, R, Vi en alle werelden w ∈ W
geldt: Als voor alle ψ ∈ Γ, M, w ψ, dan M, w ϕ.
I
∅ϕ
I
{ψ} ϕ
desda
desda
ϕ
ψ→ϕ
33
Geldigheid
Logica voor AI
Modale Logica
Geldige gevolgtrekking
Hoe laat je zien dat een formule ϕ een geldige gevolgtrekking
uit een verzameling Γ is?
De taal Lm
Kripke Semantiek
Geldigheid
Je neemt een willekeurige Kripke model M = hW, R, Vi en
een willekeurige wereld w ∈ W waarin de formules uit Γ
allemaal waar zijn (d.w.z. M, w ψ voor alle ψ ∈ Γ) en laat zien
dat de formule ϕ vervolgens ook waar is in w (d.w.z. M, w ϕ).
34
Geldigheid
Geldige gevolgtrekking
Logica voor AI
Modale Logica
Voorbeeld: {(ϕ → ψ), ϕ} ψ
Zij M = hW, R, Vi een willekeurige Kripke model en w ∈ W
een willekeurige wereld zodanig dat M, w (ϕ → ψ) en
M, w ϕ.
De taal Lm
Kripke Semantiek
Geldigheid
Zij v een willekeurige wereld met wRv.
Aangezien M, w (ϕ → ψ) geldt M, v ϕ → ψ.
Aangezien M, w ϕ geldt M, v ϕ.
Daaruit volgt: M, v ψ.
Daar dit voor alle v met wRv geldt, volgt: M, w ψ.
35
Geldigheid
Geldige gevolgtrekking
Hoe laat je zien dat een formule ϕ geen geldige gevolgtrekking
uit een verzameling Γ is?
Je geeft een model M = hW, R, Vi zodanig dat er in tenminste
´ wereld w ∈ W alle formules uit Γ waar zijn (d.w.z.
e´ en
M, w ψ voor alle ψ ∈ Γ) en ϕ onwaar is (d.w.z. M, w 2 ϕ).
Logica voor AI
Modale Logica
De taal Lm
Kripke Semantiek
Geldigheid
Voorbeeld: {(p ∨ q)} 2 p ∨ q
v (p)
(p , q) w
I
M, w (p ∨ q)
I
M, w 2 p ∨ q
u (q)
want M, w 2 p en M, w 2 q
36
Geldigheid
Geldigheid van Necessitatie
Als ϕ, dan ϕ
Logica voor AI
Modale Logica
De taal Lm
Bewijs:
Kripke Semantiek
Stel dat ϕ.
Geldigheid
Zij M = hW, R, Vi een willekeurige Kripke model en w ∈ W
een willekeurige wereld.
Zij v een willekeurige wereld met wRv.
Aangezien ϕ geldt M, v ϕ.
Daar dit voor alle v met wRv geldt, volgt M, w ϕ.
Omdat dit weer voor elke w ∈ W geldt, is ϕ geldig in M.
En aangezien M willekeurig gekozen was, volgt ϕ.
37
Geldigheid
Geldigheid van Necessitatie
Logica voor AI
Modale Logica
Let op: ϕ 2 ϕ
De taal Lm
Kripke Semantiek
v (p)
Geldigheid
(p) w
t ()
I
M, w p
I
M, w 2 p
want wRt en M, w 2 p
38
Geldigheid
Logica voor AI
Modale Logica
Geldigheid van vervanging van equivalenten
De taal Lm
Kripke Semantiek
Zij θ[ϕ/p ] diegene formule die uit θ ontstaat als elk voorkomen
van p in θ door ϕ wordt vervangen.
Geldigheid
Als ϕ ↔ ψ, dan θ[ϕ/p ] ↔ θ[ψ/p ].
Let op: ϕ ↔ ψ 2 θ[ϕ/p ] ↔ θ[ψ/p ]
39

Download Report