Notatki do wykªadu

Logiki modalne i temporalne

(semestr zimowy 07/08)

Emanuel Kiero«ski

Zgodnie z obietnic¡ przedstawiam list¦ wprowadzonych denicji i twierdze«.

1 J¦zyk podstawowej logiki modalnej

Zakªadamy, »e dysponujemy przeliczalnym zbiorem zmiennych zdaniowych V ar, oznaczanych zazwyczaj

literami p, q, r itp. Poni»sza reguªa deniuje zbiór formuª podstawowej logiki modalnej:

ϕ ::= p | ⊥ | > | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ |

3ϕ | 2ϕ

W rzeczywisto±ci niektóre z powy»szych konstukcji s¡ nadmiarowe i dadz¡ si¦ zdeniowa¢ za pomoc¡

innych. W szczególno±ci 2p ::= ¬3¬ϕ. Minimalna reguªa mo»e wygl¡da¢ tak:

ϕ ::= p | ¬ϕ | ϕ ∨ ϕ |

3ϕ

2 Logika zdaniowa

Denicja 1

(i) Modelem nazwiemy funkcj¦ M : V ar → {0, 1}

(ii) Formuªa ϕ jest speªniona w modelu M... (tu denicja indukcyjna)

(iii) Formuªa jest speªnialna, gdy istnieje model, w którym jest speªniona

(iv) Formuªa jest tautologi¡ je±li jest speªniona w ka»dym modelu

Z wprowadzonymi poj¦ciami wi¡»emy nast¦puj¡ce problemy obliczeniowe:

Denicja 2

(i) Werykacja modelu  sprawdzi¢, czy dana formuªa jest speªniona w danym modelu

(ii) Speªnialno±¢  sprawdzi¢, czy istnieje model, w którym formuªa jest speªniona

(iii) Tautologie  sprawdzi¢, czy dana formuªa jest speªniona w ka»dym modelu

Twierdzenie 3

(i) Problem werykacji modelu dla logiki zdaniowej jest w P.

(ii) Problem speªnialno±ci dla logiki zdaniowej jest w NP.

(iii) Problem bycia tautologi¡ dla logiki zdaniowej jest coNP-zupeªny.

3 Struktury i modele Kripkego

Denicja 4 Struktur¡ (ang. frame) dla podstawowej logiki modalnej nazywamy par¦ F = (W, R), gdzie
W

jest niepustym zbiorem ±wiatów (lub stanów), a R jest relacj¡ binarn¡ na W . Modelem nazwiemy par¦

M

= (F, V )

, gdzie F jest struktur¡, a V : V ar → P (W ).

Denicja 5 Niech w ∈ W , M = (W, R, V ). Deniujemy indukcyjnie poj¦cie: ϕ jest speªnione w stanie w

(ϕ jest prawdziwe w w) modelu M, symbolicznie: M, w |= ϕ.

• M, w |= p

i w ∈ V (p)

• M, w |= ¬ϕ

i nie zachodzi M, w |= ϕ

• M, w |=

3ϕ i dla pewnego v ∈ W , tekiego »e Rwv zachodzi M, v |= ϕ

• M, w |=

2ϕ i dla ka»dego v ∈ W , takiego »e Rwv zachodzi M, v |= ϕ

1

•

(...)

Dodatkowo, dla zbioru formuª Σ, M, w |= Σ, gdy M, w |= ϕ dla ka»dego ϕ ∈ Σ.

Denicja 6 Formuªa jest globalnie prawdziwa w modelu M, M |= ϕ, gdy jest speªniona w ka»dym jego

stanie.

Przykªad 7 Przykªad 1.22 ze str. 18

Denicja 8

(i) Formuªa ϕ jest prawdziwa (ang. valid) w stanie w struktury F, F, w |= ϕ, gdy jest

prawdziewa w tym stanie w ka»dym modelu rozip¦tym na F.

(ii) ϕ jest prawdziwa w F, F |= ϕ, gdy jest prawdziwa w ka»dym stanie F.

(iii) ϕ jest prawdziwa (jest tautologi¡) w klasie struktur F , gdy jest prawdziwa w ka»dej strukturze z tej

klasy

(iv) ϕ jest prawdziwa (albo jest tautologi¡), gdy jest prawdziwa w ka»dej strukturze.

Poj¦cie prawdziwo±ci w strukturach znacz¡co ró»ni si¦ od poj¦cia prawdziwo±ci (speªniania) w modelach

 przykªadowo, je±li ϕ ∨ ψ jest speªnione w stanie w modelu M, to ϕ jest speªnione w w lub ψ jest speªnione

w w. Je±li ϕ ∨ ψ jest prawdziwe w stanie w struktury F, to wcale nie znaczy, »e która± z podformuª jest w

tym stanie prawdziwa.

Przykªad 9

(i) 3(p ∨ q) → (3p ∨ 3q) jest prawdziwa we wszystkich strukturach (inczej mówi¡c jest

tautologi¡)

(ii) 33p → 3p nie jest prawdziwa we wszystkich strukturach. Jest za to prawdziwa w klasie struktur

przechodnich.

4 Konsekwencja semantyczna

Denicja 10 Niech Σ, ϕ, S b¦d¡ odpowiednio zbiorem formuª, formuª¡ i klas¡ modeli. Mówimy, »e ϕ jest

(lokalnie) semantyczn¡ konsekwencj¡ Σ w klasie S (notacja: Σ |=

S

ϕ

), gdy dla ka»dego modelu M z klasy S

i dla ka»dego stanu w ∈ W , je±li M, w |= Σ, to M, w |= ϕ.

Przykªad 11 Niech S b¦dzie klas¡ modeli przechodnich. Wtedy:

{

33p} |=

S

3p.

Oczywi±cie powy»szy fakt nie zachodzi dla S b¦d¡cego klas¡ wszystkich strukur.

5 Konstrukcje niezmiennicze

5.1 Sumy rozª¡czne modeli

Denicja 12 Niech M

i

b¦dzie rodzin¡ modeli, M

i

= (W

i

, R

i

, V )

. Zakªadamy, »e modele nie maj¡ wspól-

nych stanów. Suma rozª¡czna modeli deniowana jest nast¦puj¡co: U

i

M

i

= (W, R, V )

, gdzie W jest sum¡

zbiorów W

i

, R  sum¡ relacji R

i

, a V (p) = U

i

V

i

(p)

.

Fakt 13 M

i

jak wy»ej. Dla ka»dego ϕ, i ka»dego stanu w ∈ W

i

mamy U

i

M

i

, w |= ϕ

i M

i

, w |= ϕ

.

Przykªad 14 Globalnego diamentu nie da si¦ zdeniowa¢. M, w |= Eϕ i M, v |= ϕ dla pewnego v.

5.2 Generowane podmodele

Denicja 15 Mówimy, »e M

0

= (W

0

, R

0

, V

0

)

jest podmodelem gdy M = (W, R, V ), W

0

⊆ W

, R

0

jest

obci¦ciem R do W

0

i V

0

(p) = V (p) ∩ W

0

. M

0

jest generowanym podmodelem M, gdy dodatkowo dla ka»dego

stanu w ∈ W zachodzi: w ∈ W

0

i Rwv, to v ∈ W

0

. Mówimy, »e podmodel jest generowany przez zbiór X

gdy jest najmniejszym generowanym podmodelem zawieraj¡cym X.

Fakt 16 Je»eli M

0

jest generowanym podmodelem M, to dla ka»dego stanu w w M

0

zachodzi M

0

, w |=

ϕ

i M, w |= ϕ dla dowolnego ϕ.

Przykªad 17 Wsteczny diament nie jest deniowalny.

2

5.3 Morzmy ograniczone

Denicja 18 Niech M, M

0

b¦d¡ modelami. Przeksztaªcenie f : W → W

0

jest morzmem ograniczonym

(ang. bounded morphism), gdy:

(i) w i f(w) speªniaj¡ te same zmienne zdaniowe

(ii) f jest homomorzmem (Rwv → R

0

f (w)f (v)

)

(iii) Je±li R

0

f (w)v

0

, to istnieje v ∈ W , takie »e Rwv oraz f(v) = v

0

Przykªad 19 Modele M i M

0

s¡ zdeniowane nast¦puj¡co:

• W = N, Rmn i n = m + 1, p speªnione dla n parzystych

• W

0

= {e, o}

, R

0

= {(e, o), (o, e)

, p prawdziwe w e.

Morzm ograniczony z M w M

0

: parzyste na e, nieparzyste na n.

Fakt 20 Je±li f jest morzmem ograniczonym z M w M

0

, to dla dowolnego ϕ zachodzi M, w |= ϕ i M

0

, f (w) |=

ϕ

.

6 Bisymulacje

Denicja 21 Bisymulacja pomi¦dzy modelami M, M

0

to taka niepusta relacja Z ⊆ W × W

0

, »e:

(i) je±li wZw

0

, to w i w

0

speªniaj¡ te same zmienna zdaniowe

(ii) (tam): je±li wZw

0

i Rwv to istnieje taki v

0

, »e Zvv

0

i R

0

w

0

v

0

(iii) (z powrotem): je±li wZw

0

i R

0

w

0

v

0

, to istnieje taki v, »e Zvv

0

i Rwv.

Notacja: M, w↔M

0

, w

0

; je±li istnieje jakakolwiek bisymulacja to piszemy czasem: M↔M

0

Twierdzenie 22 Je±li M, w↔M

0

, w

0

, to w i w

0

speªnij¡ dokªadnie te same formuªy ( modal formulas are

invariant under bisimulation).

Twierdzenie 23

(i) M

i

, w↔

U

i

M

i

, w

.

(ii) Je±li M

0

jest generowanym podmodelem M, to dla w ∈ W

0

: M

0

, w↔M, w

.

(iii) Je±li f jest morzmem ograniczonym z M w M

0

, to M, w↔M

0

, f (w)

.

Twierdzenie 24 (Hennessy-Milner) Niech M i M

0

b¦d¡ takimi modelami, »e ka»dy ich element ma tylko

sko«czenie wiele nast¦pników. Wtedy w↔w

0

i w, w' speªniaj¡ dokªadnie te same formuªy.

7 Wªasno±¢ modelu sko«czonego

Denicja 25 Mówimy, »e logika modalna ma wªasno±¢ modelu sko«czonego w klasie modeli M, gdy ka»da

formuªa speªnialna w M jest speªnialna w pewnym modelu sko«czonym w M.

Twierdzenie 26 Logika modalna ma wªano±¢ modelu sko«czonego (w klasie wszystkich modeli)

7.1 Filtracja

Dowód twierdzenia 26 przeprowadzimy metod¡ ltracji.

Denicja 27 Mówimy, »e zbiór formuª Σ jest zamkni¦ty na branie podformuª, gdy ϕ ∈ Σ implikuje, »e

wszystkie podformuªy ϕ nale»¡ równie» do Σ.

Denicja 28 Niech M = (W, R, V ) b¦dzie modelem, a Σ zbiorem formuª zamkni¦tym na branie podformuª.

Deniujemy relacj¦ równowa»no±ci ≡

Σ

na stanach modelu M nast¦puj¡co:

w ≡

Σ

w

0

zachodzi, gdy dla wszystkich ϕ ∈ Σ, M, w |= ϕ i M, w

0

|= ϕ.

Klas¦ abstrakcji elementu w oznaczamy przez |w|

Σ

albo po prostu przez |w|. Zaªó»my, »e model M

f

=

(W

f

, R

f

, V

f

)

jest taki, »e:

(a) W

f

= {|w|

Σ

: w ∈ W }

(zbiór klas abstrakcji)

(b) je±li Rwv, to R

f

|w||v|

,

(c) je±li R

f

|w||v|

, to dla ka»dej formuªy 3ϕ ∈ Σ, je±li M, v |= ϕ, to M, w |= 3ϕ.

3

(d) V

f

(p) = {|w| : M, w |= p}

dla p pojawiaj¡cych si¦ w Σ.

Taki model nazywamy ltracj¡ M wzgl¦dem Σ. Czasem ltracj¡ nazywamy te» sam¡ relacj¦ R

f

.

Fakt 29 Filtracja modelu M wzgl¦dem zamkni¦tego na podformuªy Σ ma najwy»ej 2

|Σ|

stanów.

Twierdzenie 30 Niech M

f

b¦dzie ltracj¡ modelu M wzgl¦dem zamkni¦tego na podformuªy Σ. Wtedy dla

ka»dego ϕ ∈ Σ oraz ka»dego w ∈ W zachodzi: M

f

, |w| |= ϕ

i M, w |= ϕ.

Filtracje zawsze istniej¡. Dwie podstawowe deniowane s¡ nast¦puj¡co:

(i) najmniejsza ltracja: R

s

|w||v|

i ∃w

0

∈ |w|, v

0

∈ |v| Rwv

(ii) najwi¦ksza ltracja: R

l

|w||v|

i dla wszystkich 3ϕ ∈ Σ : M, v |= ϕ implikuje M, w |= 3ϕ.

Lemat 31 Najwi¦ksza i najmniejsza ltracja s¡ rzeczywi±cie ltracjami. W dodatku ka»da ltracja zawiera

najmniejsz¡ i zawiera si¦ w najwi¦kszej.

Twierdzenie 32 Logika modalna ma wªasno±¢ modelu sko«czonego. W dodatku ka»da speªnialna formuªa
ϕ

ma model wielko±ci najwy»ej 2

m

, gdzie m jest liczb¡ podformuª ϕ.

8 Standardowy przekªad na logik¦ pierwszego rz¦du

Denicja 33 Rozwa»amy sygnatur¦ pierwszego rz¦du zawieraj¡c¡ binarn¡ relacj¦ R oraz unarne relacje
P

1

, P

2

, . . .

, odpowiadaj¡ce naszym zmiennym zdaniowym. Dla zmiennej pierwszego rz¦du x standardowy

przekªad ST

x

zwraca dla formuªy modalnej formuªe pierwszego rz¦du ze zmienn¡ woln¡ x:

• ST

x

(p) = P x

• ST

x

(¬ϕ) = ¬ST

x

(ϕ)

• ST

x

(ϕ ∨ ψ) = ST

x

(ϕ) ∨ ST

x

(ψ)

• ST

x

(

3ϕ) = ∃y(Rxy ∧ ST

y

(ψ))

W przekªadzie mo»emy ograniczy¢ si¦ do u»ywania na zmian¦ tylko dwóch zmiennych: x, y.

Fakt 34 Dla wszystkich modeli M i stanów w: M, w |= ϕ i M |= ST

x

(ϕ)[w]

Wniosek: (podstawowa) logika modalna jest fragmentam logiki pierwszego rz¦du FO. St¡d, mo»emy wiele

wyników dla FO przenie±¢ do logiki modalnej. Przykªadowo: zwarto±¢ (compactness) - je±li ka»dy sko«czony

podzbiór pewnego zbioru formuª jest speªnialny, to caªy zbiór równie»; dolne tw. Löwenheima-Skolema:

ka»da speªnialna formuªa ma model przeliczalny, itp.

Nale»y jednak podkre±li¢, »e logika modalna jest do±¢ ubogim framentem FO. Problem speªnialno±ci dla

FO jest nierozstrzygalny

Przykªad 35 Rxx nie jest równowa»na »adnej formule modalnej.

9 Deniowalno±¢ wªasno±ci struktur

Denicja 36 Niech ϕ b¦dzie formuª¡ modaln¡, a K klas¡ struktur. Mówimy, »e ϕ deniuje (lub charake-

ryzuje) K, je±li dla ka»dej struktury F, F ∈ K i F |= ϕ. Analogicznie dla zbioru formuª.

Przykªad 37

(i) (T )p → 3p deniuje klas¦ struktur zwrotnych.

(ii) (4)33p → 3p deniuje klas¦ struktur przechodnich.

(iii) (5)3p → 23p deniuj¦ struktury z wªasno±ci¡ eukliedsowo±ci.

Przykªad 38 Formuªa Löba (L): 2(2p → p) → 2p nie ma odpowiednika w FO.

(1) Fakt: (L) deniuje klas¡ struktur, w których R jest przechodnia, a relacja odwrotna do R dobrze

ufundowana (inaczej mówi¡c w R nie ma niesko«czonego ªa«cucha).

(2) Fakt: (L) nie jest deniowalna w FO.

Fakt 39

(i) F, w |= ϕ i F |= ∀P

1

. . . ∀P

n

ST

x

(ϕ)[w]

(ii) F |= ϕ i F |= ∀P

1

. . . ∀P

n

∀xST

x

(ϕ)

F

|= ∀P

1

. . . ∀P

n

∀xST

x

(ϕ)

nazywamy czasem tªumaczeniem ϕ na MSO (tªumaczeniem na poziomie struk-

tur).

4

10 Podej±cie aksjomatyczne, normalne logiki modalne

Denicja 40 K-dowód to sko«czony ci¡g formuª, z których ka»da jest aksjomatem lub powstaje z poprzed-

nich po zastosowaniu reguª dowodzenia. Aksjomaty:

(PC) wszytkie podstawienia tautologii logiki zdaniowej

(K) 2(p → q) → (2p → 2q)

(Dual) 3p ↔ ¬2¬p

Reguªy dowodzenia:

(1) (Modus ponens): je±li dowiedli±my ϕ oraz ϕ → ψ, to mo»emy dowie±¢ ψ
(2) (Podstawienie): je±li dowiedli±my ϕ, to mo»emy dowie±¢ ψ, je±li ψ powstaje z ϕ przez jednorodne

podstawienie formuª za zmienne zdaniowe.

(3) (generalizacja): je±li mamy ϕ, to mamy 2ϕ.

Formuªa ϕ jest K-dowodliwa (`

K

ϕ

) je±li istnieje dowód, w którym pojawia si¦ na ko«cu.

Twierdzenie 41 [poprawno±¢ systemu K]

(i) Ka»dy aksjomat jest prawdziwy w klasie wszystkich modeli.

(ii) Reguªy dowodzenia zachowuj¡ prawdziwo±¢ w klasie wszystkich modeli.

Fakt 42

(i) je±li dowiedli±my α, to mo»emy dowie±¢ α ∨ β.

(ii) je±li dowiedli±my α i β, to mo»emy dowie±¢ α ∧ β.

Fakt 43 Poni»sze formuªy s¡ dowodliwe (na ¢wiczenia):

(a) (2α ∧ 3β) → 3(α ∧ β),

(b) 2(α ∧ β) ↔ (2α ∧ 2β).

Denicja 44

(i) ϕ jest dowodliwe ze zbioru formuª Γ (Γ `

K

ϕ

) gdy istniej¡ takie ψ

1

, . . . ψ

k

∈ Γ

, »e

`

K

(ψ

1

∧ . . . ∧ ψ

k

) → ϕ

.

(ii) Mówimy, »e zbiór formuª Γ jest sprzeczny je±li Γ `

K

⊥

. W przeciwnym wypadku Γ jest niesprzeczny.

(iii) Γ jest maksymalnym zbiorem niesprzecznym (MCS), gdy po doªo»eniu do niego dowolnej formuªy staje

si¦ sprzeczny.

Fakt 45

(i) Γ niesprzeczny i ka»dy jego sko«czony podzbiór niesprzeczny.

(ii) ¬ `

K

ϕ

to ¬ϕ niesprzeczne.

(iii) Je±li Γ jest MCS to dla ka»dego ϕ: dokªadnie jedna z formuª ϕ, ¬ϕ nale»y do Γ.

(iv) ka»da formuªa niesprzeczna jest zawarta w pewnym MCS.

(v) je±li Γ MCS i Γ `

K

ϕ

, to ϕ ∈ Γ.

(vi) ϕ ∨ ψ ∈ Γ i ϕ ∈ Γ lub ψ ∈ Γ.

(vii) ϕ ∧ ψ ∈ Γ i ϕ ∈ Γ i ψ ∈ Γ.

(viii) je±li 3ϕ niesprzeczna, to ϕ niesprzeczna.

Twierdzenie 46 [Twierdzenie o peªno±ci dla logiki K]
`

K

ϕ

i |= ϕ.

Dowód Implikacja w prawo wynika z twierdzenia 41 (o poprawno±ci). W drug¡ stron¦ wynika z lematu 47.

2

Lemat 47 Ka»da formuªa niesprzeczna ma model. Wi¦cej: istnieje model M = {W, R, V }, w którym speª-

niona jest ka»da niesprzeczna formuªa.

Dowód Konstrukcja modelu kanonicznego.

2

Denicja 48 Normaln¡ logik¡ modaln¡ nazwiemy zbiór formuª zamkni¦ty na operacje syntaktyczne (mo-

dus ponens, podstawienie i generalizacj¦), zawieraj¡cy aksjomaty systemu K. Zazwyczaj normaln¡ logik¦

modaln¡ deniuje si¦ podaj¡c po prostu dodatkowe aksjomaty.

Lista ciekawych aksjomatów:

(4) 33p → 3p

5

(T) p → 3p
(B) p → 23p

(D) 2p → 3p

(L) 2(2p → p) → 2p

Ciekawe logiki:

•

K

•

K4

•

T, czyli K+T

•

B, czyli K+B

•

KD

•

S4, czyli K+T+4

•

S5, czyli K+T+4+B

•

KL

Denicja 49 Mówimy, »e logika normalna Λ jest zupeªna w klasie struktur (lub modeli) K je±li: `

Λ

ϕ

i |=

K

ϕ

(czyli ϕ jest prawdziwa w klasie K)

Twierdzenie 50

(i) K jest zupeªna w klasie wszystkich struktur.

(ii) K4 jest zupeªna w klasie struktur przechodnich.

(iii) T jest zupeªna w klasie struktur zwrotnych.

(iv) B jest zupeªna w klasie struktur symetrycznych.

(v) KD jest zupeªna w klasie struktur nieograniczonych w prawo.

(vi) S4 jest zupeªna w klasie struktur zwrotnych i przechodnich.

(vii) S5 jest zupeªna w klasie struktur, których relacja jest równowa»no±ci¡.

(viii) KL jest zupeªna w klasie sko«czonych drzew przechodnich.

Dowód Technika dowodu zazwyczaj polega na pokazaniu, »e odpowiedni model kanoniczny ma odpowiednie

wªasno±ci.

2

6