Logica voor AI Correspondentie Bisimulatie Nietkaraktersiseerbaarh Correspondentie, bisimulatie, niet-karakteriseerbaarheid Albert Visser [email protected] 26 november en 3 december 2014 1 Kripke Semantiek Correspondentie De taal Lm van de modale propositielogica ϕ ::= p | ⊥ | > | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | ϕ ↔ ϕ | ϕ | ^ϕ Bisimulatie Nietkaraktersiseerbaarh Blokje en ruitje I ϕ: het is noodzakelijk dat ϕ I ^ϕ: het is mogelijk dat ϕ 2 Kripke Semantiek Modelstructuur (of frame) Correspondentie 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 Bisimulatie Nietkaraktersiseerbaarh 3 Kripke Semantiek Kripke Model Een Kripke model is een geordend drietal M = hW, R, Vi, waarbij Correspondentie Bisimulatie Nietkaraktersiseerbaarh I hW, Ri een modelstructuur en I V : W → Pow (VAR ) een interpretatiefunctie is. 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) 4 Frame eigenschappen Zij R ⊆ W × W een bereikbaarheidsrelatie. De kwantoren hieronder lopen steeds over W. Correspondentie R is reflexief R is irreflexief R is symmetrisch R is asymmetrisch R is anti-symmetrisch R is transitief R is euclidisch R is dicht R is deterministisch R is voortzettend R is disconnected R is universeel ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ Bisimulatie ∀w w Rw Niet∀w ¬ w Rw karaktersiseerbaarh ∀w ∀v (w Rv → v Rw ) ∀w ∀v (w Rv → ¬v Rw ) ∀w ∀v ((w Rv ∧ w , v ) → ¬v Rw ) ∀w ∀v ∀z ((w Rv ∧ v Rz ) → w Rz ) ∀w ∀v ∀z ((w Rv ∧ w Rz ) → v Rz ) ∀w ∀v (w Rv → ∃z (w Rz ∧ z Rv )) ∀w ∀v ∀z ((w Rv ∧ w Rz ) → v = z ) ∀w ∃v w Rv ∀w ∀v ¬ v Rw ∀w ∀v w Rv 5 Frame eigenschappen Correspondentie Bisimulatie I Een modelstructuur F = hW, Ri heet reflexief (symmetrisch, transitief, etc.) desda R reflexief (symmetrisch, transitief, etc.) is of W. I Een model M = hW, R, Vi heet reflexief (symmetrisch, transitief, etc.) desda F = hW, Ri reflexief (symmetrisch, transitief, etc.) is. Nietkaraktersiseerbaarh 6 Correspondentie Geldigheid in een model: M ϕ Een formule ϕ is geldig in een Kripke model M = hW, R, Vi, notatie: M ϕ, desda voor alle werelden w ∈ W geldt M, w ϕ Correspondentie Bisimulatie Nietkaraktersiseerbaarh Geldigheid in een modelstructuur: F ϕ Een formule ϕ is geldig in een modelstructuur F = hW, Ri, notatie: F ϕ, desda voor alle modellen M = hW, R, Vi geldt M ϕ Geldigheid in een klasse van modelstructuren: C ϕ Een formule ϕ is geldig in een klasse C van modelstructuren, notatie: C ϕ, desda voor alle modelstructuren F = hW, Ri ∈ C geldt F ϕ. 7 Correspondentie Karakteriseerbaarheid Correspondentie Een verzameling formules Γ ⊆ Lm karakteriseert een klasse C van modelstructuren desda Bisimulatie Nietkaraktersiseerbaarh voor alle modelstructuren F geldt: F ∈C desda F ψ voor alle ψ ∈ Γ. Modale definieerbaarheid Een klasse C van modelstructuren is modaal definieerbaar desda er is een verzameling modale formules Γ ⊆ Lm die deze klasse karakteriseert. 8 Correspondentie Correspondentie Transitiviteit Bisimulatie De klasse van alle transitieve modelstructuren is modaal definieerbaar. Nietkaraktersiseerbaarh De formule p → p karakteriseert de klasse van alle transitieve modelstructuren. Zij F = hW, Ri een modelstructuur. F is transitief desda F p → p . 9 Correspondentie Transitiviteit Zij F = hW, Ri een modelstructuur. Dan, F is transitief desda F p → p. Bewijs: “⇒” Stel dat F = hW, Ri transitief is. Zij M = hW, R, Vi een willekeurig model op F en zij w ∈ W een willekeurige wereld. Stel dat M, w p. We moeten laten zien dat M, w p. Stel dat w Rv. We moeten laten zien dat M, v p. Stel dat v Ru. We moeten laten zien dat M, u p. We hebben w Rv en v Ru. Dus met transitiviteit w Ru. Omdat M, w p, volgt dat M, u p. Correspondentie Bisimulatie Nietkaraktersiseerbaarh Daar dit voor alle w , v , u ∈ W met w Rv en v Ru geldt, volgt: M p → p. Aangezien M willekeurig gekozen was, geldt: F p → p. 10 Correspondentie Correspondentie Transitiviteit Zij F = hW, Ri een modelstructuur. We hebben: F is transitief desda F p → p. Bisimulatie Nietkaraktersiseerbaarh “⇐” We bewijzen deze richting met contrapositie. Stel dat F = hW, Ri niet transitief is. Dan zijn er werelden w , u, v ∈ W zodanig dat w Ru en uRv maar niet w Rv. Beschouw M = hW, R, Vi met p ∈ V(x ) desda wRx. Dan: M, w p en M, v 2 p. Dus M, u 2 p en daarom ook M, w 2 p. Ergo, M 2 p → p en daarmee F 2 p → p. 11 Correspondentie Zij F = hW, Ri een modelstructuur. Correspondentie F p → p (of F p → ^p) desda F is reflexief F p (of F ⊥) desda F is disconnected karaktersiseerbaarh F ^p → p (of F p → ^p) desda F is symmetrisch F p → p (of F ^^p → ^p) desda F is transitief F ^p → ^p (of F ^p → p) desda F is euclidisch F p → p (of F ^p → ^^p) desda F is dicht F ^p → p desda F is deterministisch F p → ^p (of F ^>) desda F is voortzettend Bisimulatie Niet- 12 Correspondentie Verschillende modaliteiten I epistemisch I doxastisch I deontisch I temporeel Correspondentie Bisimulatie Nietkaraktersiseerbaarh Verschillende principes I (D) ϕ → ^ϕ I (T) ϕ → ϕ I (B) ^ϕ → ϕ I (4) ϕ → ϕ I (5) ^ϕ → ^ϕ 13 Correspondentie Correspondentie Niet-karakteriseerbaarheid De klasse van I irreflexieve I intransitieve I asymmetrische I anti-symmetrische I universele Bisimulatie Nietkaraktersiseerbaarh modelstructuren is niet karakteriseerbaar. 14 Bisimulatie Correspondentie 0 (p) 1 (p) 2 (p) 3 (p) ... Bisimulatie a (p) P I Voor alle ϕ ∈ Lm : M, 0 ϕ desda M0 , a ϕ I Voor alle ϕ ∈ Lm : M ϕ desda M0 ϕ I Voor alle ϕ ∈ Lm : als F ϕ dan F 0 ϕ Nietkaraktersiseerbaarh 15 Bisimulatie Bezie Kripke modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i. Een bisimulatie tussen M en M0 is een relatie Z ⊆ W × W0 zodanig dat: Als w Zw 0 , dan: Correspondentie Bisimulatie atomaire clausule: V(w ) = V(w 0 ), Nietkaraktersiseerbaarh zig: als w Rv, dan is er een v 0 z.d.d. w 0 R0 v 0 en v Zv 0 ; v R w Z Z v0 R0 w0 zag: als w 0 R0 v 0 , dan is er een v z.d.d. w Rv en v Zv 0 . v R w Z Z v0 R0 0 w 16 Bisimulatie Correspondentie Bisimulatie Voorbeeld 0 (p) I 1 (p) Nietkaraktersiseerbaarh 2 (p) 3 (p) ... a (p) P Z = {h0, a i, h1, a i, h2, a i, h3, a i, . . . } 17 Bisimulatie Correspondentie Bisimulatie M0 hW0 , R0 , V0 i. Bezie Kripke modellen M = hW, R, Vi en = Zij Z een bisimulatie tussen M en M0 met w Zw 0 . Nietkaraktersiseerbaarh Dan geldt voor alle formules ϕ ∈ Lm : M, w ϕ desda M0 , w 0 ϕ Bewijs: formule inductie. 18 Bisimulatie Formule inductie Bezie Kripke modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i. Zij Z een bisimulatie tussen M en M0 met w Zw 0 . Stelling: Voor alle ϕ ∈ Lm : M, w ϕ I I I desda M0 , w 0 ϕ Correspondentie Bisimulatie Nietkaraktersiseerbaarh Inductiebasis: Voor alle atomaire proposities p ∈ VAR : M, w p desda M0 , w 0 p Inductie-eigenschap IE(ψ): voor alle w , w 0 met w Zw 0 : M, w ψ desda M0 , w 0 ψ Inductiestap: Als IE(ψ) en IE(θ), dan hebben we voor ϕ := ¬ψ | ψ ∨ θ | ψ ∧ θ | ψ → θ | ψ ↔ θ | ψ | ^ψ dat IE(ϕ). 19 Bisimulatie Bezie Kripke modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i. Zij Z een bisimulatie tussen M en M0 . Dan geldt, voor alle ϕ ∈ Lm en voor all w , w 0 met w Zw 0 , dat M, w ϕ desda M0 , w 0 ϕ. I I w Zw 0 . Basis: Zij p ∈ VAR en Dan geldt: M, w p desda 0 p ∈ V(w ). Omdat w Zw , geldt: V(w ) = V(w 0 ). Daaruit volgt: p ∈ V(w ) desda p ∈ V(w 0 ). Dus: M, w p desda M0 , w 0 p. Correspondentie Bisimulatie Nietkaraktersiseerbaarh Stap voor ¬. Zij ϕ := ¬ ψ en vooronderstel dat IE(ψ). We hebben voor w Zw 0 dat: M, w ¬ ψ ⇔ M, w 2 ψ ⇔ M0 , w 0 2 ψ ⇔ M0 , w 0 ¬ ψ 20 Bisimulatie I Stap voor ∧. Zij ϕ := ψ ∧ θ en vooronderstel dat IE(ψ) en IE(θ) en w Zw 0 . We hebben: Correspondentie Bisimulatie M, w ψ ∧ θ ⇔ M, w ψ en M, w θ ⇔ M0 , w 0 ψ en M0 , w 0 θ Nietkaraktersiseerbaarh ⇔ M0 , w 0 ψ ∧ θ I Stap voor ^. Zij ϕ := ^ψ en vooronderstel dat IE(ψ) en w Zw 0 . Stel dat M, w ^ψ. Dan is er een v met w Rv and M, v ψ. Met de zig eigenschap volgt dat er een v 0 is met w 0 Rv 0 en v Zv 0 . Er volgt nu met IE(ψ) dat M0 , v 0 ψ. Omdat w 0 Rv 0 hebben we M0 , w 0 ^ψ. De andere richting gaat hetzelfde. I De rest gaat analoog. 21 Bisimulatie Correspondentie Complete bisimulatie Bisimulatie Bezie Kripke modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i. Een bisimulatie Z tussen M en M0 heet compleet voor M0 desda voor alle w 0 ∈ W0 is er een w ∈ W met w Zw 0 . Nietkaraktersiseerbaarh Voorbeeld: 0 (p) 1 (p) 2 (p) 3 (p) ... a (p) P 22 Bisimulatie Correspondentie Bezie M = hW, R, Vi en M0 = hW0 , R0 , V0 i. Zij Z een bisimulatie tussen M en M0 die compleet is voor M0 . Dan geldt: M ϕ ⇒ M0 ϕ. Bisimulatie Nietkaraktersiseerbaarh Bewijs: Stel dat M ϕ. M.a.w., voor alle w ∈ W geldt M, w ϕ. Zij w 0 ∈ W0 een willekeurige wereld in M0 . Omdat de bisimulatie Z compleet is voor M0 , geldt: er is een w ∈ W zodanig dat w Zw 0 . Aangezien M, w ϕ, volgt M0 , w 0 ϕ. Daar w 0 willekeurig gekozen was, volgt: M0 ϕ. 23 Bisimulatie Bezie frames F = hW, Ri en F 0 = hW0 , R0 i. Als er voor elke valuatie V0 op F 0 een valuatie V op F is zodanig dat er een bisimulatie Z ⊆ W × W0 tussen de resulterende modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i is die compleet is voor M0 , dan geldt: Correspondentie Bisimulatie Nietkaraktersiseerbaarh F ϕ ⇒ F0 ϕ Bewijs: Stel dat F ϕ. Daaruit volgt: voor alle M = hW, R, Vi geldt M ϕ. Zij V0 een willekeurige valuatie op F 0 . Dan volgt uit de aanname dat er een valuatie V op F is zodanig dat er een bisimulatie Z ⊆ W × W0 tussen de resulterende modellen M = hW, R, Vi en M0 = hW0 , R0 , V0 i is die compleet is voor M0 . Aangezien M ϕ, volgt M0 ϕ. Daar V0 (en dus M0 ) willekeurig gekozen was, volgt: F 0 ϕ 24 Niet-karakteriseerbaarheid Correspondentie Stelling van Goldblatt-Thomason: Als een frame eigenschap E in de taal van de predicatenlogica kan worden uitgedrukt, dan is deze eigenschap E modaal definieerbaar desda I E is gesloten onder gegenereerde subframes; I E is gesloten onder disjoint unions; I E is gesloten onder p-morfismen; I het complement van E is gesloten onder ultrafilter extensions. Bisimulatie Nietkaraktersiseerbaarh 25 Niet-karakteriseerbaarheid De relatie R∗ Zij R ⊆ W × W een bereikbaarheidsrelatie. R∗ = {hw , v i : er zijn u1 , . . . , un zodat w Ru1 R . . . Run Rv }. Voorbeeld: I I v t w u Correspondentie Bisimulatie Nietkaraktersiseerbaarh R = {hw , w i, hw , v i, hv , v i, hv , t i, ht , t i, hu, w i, hu, t i} R∗ = {hw , w i, hw , v i, hw , t i, hv , v i, hv , t i, ht , t i, hu, w i, hu, v i, hu, t i} 26 Niet-karakteriseerbaarheid Gegenereerde subframes Zij F = hW, Ri een modelstructuur en zij w ∈ W een wereld. Het w-gegenereerde subframe van F is de modelstructuur Fw = hWw , Rw i, waarbij I I Correspondentie Bisimulatie Nietkaraktersiseerbaarh Ww = {v ∈ W : v = w of w R∗ v } en Rw = R ∩ (Ww × Ww ) = {hv , w i ∈ R : v ∈ Rw en w ∈ Rw }. Voorbeeld: v t v w u w t 27 Niet-karakteriseerbaarheid Correspondentie Gegenereerde subframes Zij F = hW, Ri een modelstructuur, w ∈ W een wereld, Fw = hWw , Rw i het w-gegenereerde subframe van F en Mw = hWw , Rw , Vw i een model op Fw . Dan is er een model M = hW, R, Vi op F zodanig dat er een bisimulatie Z tussen M en Mw is die compleet is voor Mw . Bisimulatie Nietkaraktersiseerbaarh Bewijs: Definieer V(v ) = Vw (v ) voor alle v ∈ Ww . Z = {hv , v i : v ∈ Ww } is een bisimulatie tussen M en Mw die compleet is voor Mw . 28 Niet-karakteriseerbaarheid Correspondentie Gegenereerde subframes Zij F = hW, Ri een modelstructuur, w ∈ W een wereld en Fw = hWw , Rw i het w-gegenereerde subframe van F . Bisimulatie Nietkaraktersiseerbaarh Dan geldt voor alle formules ϕ ∈ Lm F ϕ ⇒ Fw ϕ Hoe kan je met behulp van gegenereerde subframes laten zien dat een frame eigenschap niet modaal definieerbaar is? 29 Niet-karakteriseerbaarheid Gegenereerde subframes Hoe kan je met behulp van gegenereerde subframes laten zien dat een frame eigenschap niet modaal definieerbaar is? Je geeft een modelstructuur F = hW, Ri welke de gewenste eigenschap heeft en een wereld w ∈ W zodanig dat het w-gegenereerde subframe Fw van F die eigenschap niet heeft. I Stel dat de klasse C van alle modelstructuren die de gewenste eigenschap hebben modaal definieerbaar was. I Dan is er een Γ zodanig dat voor alle modelstructuren F geldt: F Γ desda F ∈ C I Als F ∈ C, dan geldt: F Γ. I Daaruit volgt: Fw Γ I Als Fw < C, dan kan Γ geen karakteriserende formule verzameling voor de klasse C zijn. Correspondentie Bisimulatie Nietkaraktersiseerbaarh 30 Niet-karakteriseerbaarheid Gegenereerde subframes Correspondentie Bisimulatie Nietkaraktersiseerbaarh Voorbeeld: Fw F v t v w u w t 31 Niet-karakteriseerbaarheid Disjoint unions Correspondentie Bezie F1 = hW1 , R1 i en F2 = hW2 , R2 i. De disjoint union van F1 en F2 is de modelstructuur F1 t F2 = hW, Ri, waarbij I W = {(w , i ) : w ∈ Wi , i ∈ {1, 2}} I R = {h(w , i ), (v , i )i : w Ri v , i ∈ {1, 2}} Bisimulatie Nietkaraktersiseerbaarh Voorbeeld: v F1 t F2 F2 F1 w w t (v , 1) (w , 1) (w , 2) (t , 2) 32 Niet-karakteriseerbaarheid Disjoint unions Bezie F1 = hW1 , R1 i en F2 = hW2 , R2 i. Zij F1 t F2 = hW, Ri de disjoint union van F1 en F2 . Bewijs: F1 t F2 ϕ ⇔ F1 ϕ en F2 ϕ Correspondentie Bisimulatie Nietkaraktersiseerbaarh “⇒” Zij V1 een valuatie op F1 . Definieer V(w , 1) = V1 (w ) voor alle w ∈ W1 . Z = {h(w , 1), w i : w ∈ W1 } ⊆ W × W1 is een bisimulatie tussen M en M1 die compleet is voor M1 . Analoog voor F2 . “⇐” Stel F1 t F2 2 ϕ. Dan is er een valuatie V op F1 t F2 en een wereld (w , i ) ∈ W zodanig dat M, (w , i ) 2 ϕ. Definieer Vi (w ) = V(w , i ) voor alle w ∈ Wi Z = {h(w , i ), w i : w ∈ Wi } ⊆ W × Wi is een bisimulatie tussen M en Mi . Aangezien M, (w , i ) 2 ϕ volgt Mi , w 2 ϕ, en dus Fi 2 ϕ. 33 Niet-karakteriseerbaarheid Disjoint unions Hoe kan je met behulp van disjoint unions laten zien dat een frame eigenschap niet modaal definieerbaar is? Je geeft een modelstructuur F = hW, Ri welke de gewenste eigenschap heeft en zodanig is dat de disjoint union F t F die eigenschap niet heeft. I Stel dat de klasse C van alle modelstructuren die de gewenste eigenschap hebben modaal definieerbaar was. I Dan is er een Γ zodanig dat voor alle modelstructuren F geldt: F Γ desda F ∈ C I Als F1 , F2 ∈ C, dan geldt: Fi Γ. I Daaruit volgt: F1 t F2 Γ I Als F1 t F2 < C, dan kan Γ geen karakteriserende formule verzameling voor de klasse C zijn. Correspondentie Bisimulatie Nietkaraktersiseerbaarh 34 Niet-karakteriseerbaarheid Correspondentie Bisimulatie Nietkaraktersiseerbaarh Disjoint unions Voorbeeld: De disjuncte vereniging van twee universele modellen is niet universeel. Daarom is universaliteit niet definieerbaar. 35 Niet-karakteriseerbaarheid p-morfismen Bezie F = hW, Ri en F 0 = hW0 , R0 i. Een p-morfisme tussen F en F 0 is een functie f : W → W0 zodanig dat f is een surjectie; I als w Rv, dan f (w )R0 f (v ); R w I Bisimulatie Nietkaraktersiseerbaarh I v Correspondentie f f v0 R0 0 w p als f (w )R0 v 0 , dan is er een v ∈ W met wRv en f (v ) = v 0 . v R w f f v0 R0 w0 p 36 Niet-karakteriseerbaarheid Correspondentie p-morfismen Bisimulatie Nietkaraktersiseerbaarh Voorbeeld: 0 I 1 2 3 ... a f (n) = a voor alle n ∈ N 37 Niet-karakteriseerbaarheid Correspondentie p-morfismen Zijn F = hW, Ri en F 0 = hW0 , R0 i modelstructuren. Zij f : W → W0 een p-morfisme tussen F en F 0 . Zij M0 = hW0 , R0 , V0 i en model op F 0 . Bisimulatie Nietkaraktersiseerbaarh Dan is er model M = hW, R, Vi op F zodanig dat er een bisimulatie is tussen M en M0 die compleet is voor M0 . Bewijs: Definieer V(w ) = V0 (f (w )) voor alle w ∈ W. De relatie Z = {hw , f (w )i : w ∈ W} is een bisimulatie tussen M en M0 die compleet is voor M0 . 38 Niet-karakteriseerbaarheid Correspondentie Bisimulatie p-morfismen Nietkaraktersiseerbaarh Zijn F = hW, Ri en F 0 = hW0 , R0 i modelstructuren. Zij f : W → W0 een p-morfisme tussen F en F 0 . Dan geldt voor alle formules ϕ ∈ Lm : F ϕ ⇒ F0 ϕ 39 Niet-karakteriseerbaarheid p-morfismen Hoe kan je met behulp van p-morfismen laten zien dat een frame eigenschap niet modaal definieerbaar is? Je geeft een modelstructuur F = hW, Ri welke de gewenste eigenschap heeft en een modelstructuur F 0 = hW0 , R0 i welke die eigenschap niet heeft zodanig dat er een p-morfisme f : W → W0 tussen F en F 0 is. I Stel dat de klasse C van alle modelstructuren die de gewenste eigenschap hebben modaal definieerbaar was. I Dan is er een Γ zodanig dat voor alle modelstructuren F geldt: F Γ desda F ∈ C I Als F ∈ C, dan geldt: F Γ. I Daaruit volgt: F 0 Γ I Correspondentie Bisimulatie Nietkaraktersiseerbaarh Als F 0 < C, dan kan Γ geen karakteriserende verzameling formules voor de klasse C zijn. 40 Niet-karakteriseerbaarheid Correspondentie p-morfismen Bisimulatie Nietkaraktersiseerbaarh Voorbeeld: Irreflexiviteit en asymmetrie en intransitiviteit zijn niet modaal definieerbaar. 0 I 1 2 3 ... a f (n) = a voor alle n ∈ N 41
© Copyright 2024 ExpyDoc