Slides

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