Logika dla informatyków/Zdaniowa logika dynamiczna

Zdaniowa logika dynamiczna

Zdaniowa logika dynamiczna (PDL, od angielskiej nazwy Propositional Dynamic Logic) została zaproponowana przez V. Pratta w 1976r. Jest ona eleganckim i zwięzłym formalizmem pozwalającym badać rozumowania dotyczące programów iteracyjnych. Formalizm ten rozszerza logikę modalną poprzez wprowadzenie modalności dla każdego programu z osobna. W tej części pokażemy jedynie dwie podstawowe własności PDL: własność małego modelu oraz pełność aksjomatyzacji. Z własności małego modelu natychmiast wynika rozstrzygalność problemu spełnialności dla PDL. System o podobnym charakterze, o nazwie Logika Algorytmiczna, został zaproponowany w roku 1970 przez A. Salwickiego.

Składnia i semantyka PDL

Syntaktycznie PDL jest mieszaniną trzech klasycznych składników: logiki zdaniowej, logiki modalnej oraz algebry wyrażeń regularnych. Język PDL zawiera wyrażenia dwóch rodzajów: zdania (lub formuły) $\phi ,\psi ,\dots$ oraz programy $\alpha ,\beta ,\gamma ,\dots$. Zakładamy, że mamy do dyspozycji przeliczalnie wiele atomowych symboli każdego rodzaju. Programy atomowe są oznaczane przez $a,b,c,\dots$, a zbiór wszystkich atomowych programów oznaczamy przez ${\mathrm{\Pi }}_0$.

Programy są budowane z programów atomowych przy użyciu operacji złożenia $(;)$, niedeterministycznego wyboru $(\cup )$ oraz iteracji ${(}^{*})$. Intuicyjnie wykonanie programu $\alpha ;\beta$ oznacza wykonanie $\alpha$, a następnie wykonanie na danych wyprodukowanych przez $\alpha$ programu $\beta$. Wykonanie programu $\alpha \cup \beta$ oznacza niedeterministyczny wybór wykonania $\alpha$ lub $\beta$. Natomiast wykonanie programu ${\alpha }^{*}$ oznacza wykonanie $\alpha$ pewną liczbę razy, być może zero. Ponadto mamy operację testowania tworzącą z każdej formuły $\phi$ nowy program $\phi ?$. Wykonanie programu $\phi ?$ jest możliwe tylko wtedy, gdy warunek $\phi$ zachodzi. Z drugiej strony, formuły mogą odwoływać się do dowolnego programu $\alpha$ poprzez modalność konieczności $[\alpha ]$: dla dowolnego zdania $\phi$, napis

$[\alpha ]\phi$

czytamy "po (każdym) wykonaniu programu $\alpha$ koniecznie musi zajść $\phi$".

Definicja 10.1

Definicja formuł i programów jest wzajemnie rekurencyjna. Definiujemy zbiór programów $\mathrm{\Pi }$ oraz zbiór formuł $\mathrm{\Phi }$ jako najmniejsze zbiory spełniające następujące warunki

• $ZZ\subseteq \mathrm{\Phi }$
• ${\mathrm{\Pi }}_0\subseteq \mathrm{\Pi }$
• jeśli $\phi ,\psi \in \mathrm{\Phi }$, to $\phi \to \psi \in \mathrm{\Phi }$ oraz $\mathrm{\perp }\in \mathrm{\Phi }$
• jeśli $\alpha ,\beta \in \mathrm{\Pi }$, to $(\alpha ;\beta )$,$(\alpha \cup \beta )$, oraz ${\alpha }^{*}\in \mathrm{\Pi }$
• jeśli $\alpha \in \mathrm{\Pi }$ oraz $\phi \in \mathrm{\Phi }$, to $[\alpha ]\phi \in \mathrm{\Phi }$
• jeśli $\phi \in \mathrm{\Phi }$, to $\phi ?\in \mathrm{\Pi }.$

Aby uniknąć pisania zbyt wielu nawiasów, stosujemy następujące priorytety:

• Jednoargumentowe operatory (wliczając $[\alpha ]$ ) wiążą silniej niż dwuargumentowe.
• Operator $;$ wiąże silniej niż $\cup$.
• Spójniki logiczne mają takie same priorytety jak zdefiniowano wcześniej.

Tak więc wyrażenie

$[\alpha ;{\beta }^{*}\cup {\gamma }^{*}]\phi \vee \psi$

odpowiada następującemu wyrażeniu z nawiasami

$([(\alpha ;{\beta }^{*})\cup {\gamma }^{*}]\phi )\vee \psi .$

Ponieważ operatory $;$ oraz $\cup$ okażą się być łączne, więc zwyczajowo będziemy opuszczać nawiasy w wyrażeniach typu $\alpha ;\beta ;\gamma$ lub $\alpha \cup \beta \cup \gamma$.

Przypomnijmy, że negacja $\mathrm{\neg }\phi$ jest skrótem formuły $\phi \to \mathrm{\perp }$. Dualnie do [ ] definiujemy modalność możliwości

$⟨\alpha ⟩\phi :=\mathrm{\neg }[\alpha ]\mathrm{\neg }\phi .$

Zdanie $⟨\alpha ⟩\phi$ czytamy "istnieje obliczenie programu $\alpha$, które zatrzymuje się w stanie spełniającym formułę $\phi$". Istotną różnicą pomiędzy modalnościami [ ] i $⟨⟩$ jest to, że $⟨\alpha ⟩\phi$ implikuje iż program $\alpha$ się zatrzymuje, podczas gdy $\left[\alpha \right]\phi$ nie gwarantuje zatrzymania się programu $\alpha$. W szczególności formuła $[\alpha ]\mathrm{\perp }$ wyraża własność mówiącą, że żadne obliczenie programu $\alpha$ nie zatrzymuje się. Natomiast formuła $⟨\alpha ⟩\mathrm{\perp }$ jest zawsze fałszywa.

Przejdziemy teraz do zdefiniowania semantyki. Podstawową strukturą semantyczną dla PDL jest tzw. struktura Kripkego.

Definicja 10.2

Struktura Kripkego jest uporządkowaną parą Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathfrak{K} = \langle K,\mathrm{m}_{\mathfrak{K}\rangle} , gdzie $K$ jest zbiorem elementów $u,v,w,\dots$ zwanych stanami, a Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathrm{m}_{\mathfrak{K}} jest funkcją przyporządkowującą każdemu atomowemu zdaniu $p\in ZZ$, podzbiór Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(p)\subseteq K} oraz każdemu atomowemu programowi $a\in {\mathrm{\Pi }}_0$ relację binarną Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(a)\subseteq K\times K} .

Poniżej funkcję Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathrm{m}_{\mathfrak{K}} rozszerzymy do dowolnych formuł i dowolnych programów. Intuicyjnie dla formuły $\phi$, zbiór stanów Parser nie mógł rozpoznać (nieznana funkcja „\vrphi”): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(\vrphi)} jest zbiorem wszystkich stanów struktury $\mathfrak{𝔎}$, w których $\phi$ jest spełniona. Natomiast dla programu $\alpha$, relacja Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(\alpha)} jest tzw. relacją wejścia-wyjścia programu $\alpha$ w strukturze $\mathfrak{𝔎}$.

Definicja 10.3

${\mathrm{m}}_{\mathfrak{𝔎}}(\phi \to \psi )$	$:=(K-{\mathrm{m}}_{\mathfrak{𝔎}}(\phi )\cup {\mathrm{m}}_{\mathfrak{𝔎}}(\psi )$
${\mathrm{m}}_{\mathfrak{𝔎}}(\mathrm{\perp })$	$:=\mathrm{\varnothing }$
${\mathrm{m}}_{\mathfrak{𝔎}}([\alpha ]\phi )$	$:=\{u|\mathrm{\forall }v\in K(⟨u,v⟩\in {\mathrm{m}}_{\mathfrak{𝔎}}(\alpha )\Rightarrow v\in {\mathrm{m}}_{\mathfrak{𝔎}}(\phi ))\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(\alpha ;\beta )$	$:=\{⟨u,v⟩|\mathrm{\exists }w\in K(⟨u,v⟩\in {\mathrm{m}}_{\mathfrak{𝔎}}(\alpha )\wedge ⟨w,v⟩\in {\mathrm{m}}_{\mathfrak{𝔎}}(\beta ))\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(\alpha \cup \beta )$	$:={\mathrm{m}}_{\mathfrak{𝔎}}(\alpha )\cup {\mathrm{m}}_{\mathfrak{𝔎}}(\beta )$
${\mathrm{m}}_{\mathfrak{𝔎}}({\alpha }^{*})$	$:=\bigcup _{n\ge 0}{\mathrm{m}}_{\mathfrak{𝔎}}(\alpha {)}^n$
${\mathrm{m}}_{\mathfrak{𝔎}}(\phi ?)$	Parser nie mógł rozpoznać (błąd składni): {\displaystyle := \left\{\langle u,v\rangle | u \in {\mathrm{m}_\mathfrak{K}}(\varphi)\right}.}

Definicja 10.4

Powiemy, że formuła $\phi$ jest spełniona w stanie $u$ struktury $\mathfrak{𝔎}$, gdy $u\in {\mathrm{m}}_{\mathfrak{𝔎}}(\phi )$. Podobnie jak w logice pierwszego rzędu spełnianie zapisujemy następująco $(\mathfrak{𝔎},u)\models \phi$. Gdy z kontekstu wynika o jaką strukturę chodzi, to możemy po prostu pisać $u\models \phi$.

Powiemy, że formuła $\phi$ jest prawdziwa w strukturze $\mathfrak{𝔎}$, gdy jest spełniona w każdym stanie tej struktury. Zapisujemy to $\mathfrak{𝔎}\models \phi$. Formuła $\phi$ jest tautologią PDL, gdy jest ona prawdziwa w każdej strukturze Kripkego. Wreszcie powiemy, że formuła $\phi$ jest spełnialna, gdy istnieje struktura Kripkego $\mathfrak{𝔎}$, taka że $\phi$ jest spełniona w przynajmniej jednym stanie $\mathfrak{𝔎}$.

Przykład 10.5

Niech $p$ będzie zmienną zdaniową oraz niech $a$ będzie atomowym programem. Niech $\mathfrak{𝔎}=(K,{\mathrm{m}}_{\mathfrak{𝔎}})$ będzie taką strukturą Kripkego, że

$K$	$=\{u,v,w\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(p)$	$=\{u,v\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(a)$	$=\{⟨u,v⟩,⟨u,w⟩,⟨v,w⟩,⟨w,v⟩\}$.

Nastepujący diagram ilustruje $\mathfrak{𝔎}$.

W tej strukturze mamy $u\models ⟨a⟩\mathrm{\neg }p\wedge ⟨a⟩p$, ale $v\models [a]\mathrm{\neg }p$ oraz $w\models [a]p$. Ponadto każdy stan struktury $\mathfrak{𝔎}$ spełnia następującą formułę

$⟨a^{*}⟩[(aa{)}^{*}]p\wedge ⟨a^{*}⟩[(aa{)}^{*}]\mathrm{\neg }p$

.

Przykład 10.6

Niech $p,q$ będą zmiennymi zdaniowymi i niech $a,b$ będą atomowymi programami. Ponadto niech $\mathfrak{𝔎}=(K,{\mathrm{m}}_{\mathfrak{𝔎}})$ będzie strukturą Kripkego zdefiniowaną następująco

$K$	$=\{s,t,u,v\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(p)$	$=\{u,v\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(q)$	$=\{t,v\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(a)$	$=\{⟨t,v⟩,⟨v,t⟩,⟨s,u⟩,⟨u,s⟩\}$
${\mathrm{m}}_{\mathfrak{𝔎}}(b)$	$=\{⟨u,v⟩,⟨v,u⟩,⟨s,t⟩,⟨t,s⟩\}$

Następujący rysunek ilustruje $\mathfrak{𝔎}$.

Następujące formuły są prawdziwe w $\mathfrak{𝔎}$.

$p\leftrightarrow [(a{b}^{*}a{)}^{*}]p$ $q\leftrightarrow [(b{a}^{*}b{)}^{*}]q.$

Ponadto niech $\alpha$ będzie programem

$\alpha =(aa\cup bb\cup (ab\cup ba)(aa\cup bb{)}^{*}(ab\cup ba){)}^{*}.(14)$

Program $\alpha$ traktowany jako wyrażenie regularne, generuje wszystkie słowa nad alfabetem $\{a,b\}$ o parzystej liczbie wystąpień $a$ oraz $b$. Można pokazać, że dla dowolnego zdania $\phi$, formuła $\phi \leftrightarrow [\alpha ]\phi$ jest prawdziwa w $\mathfrak{𝔎}$. Zauważmy, że operator ${*}^{}$ jest z natury infinitarny. Z definicji domknięcie zwrotne i przechodnie relacji jest nieskończoną sumą. Z tego względu twierdzenie o zwartości nie zachodzi dla PDL. Istotnie, zbiór

$\{⟨{\alpha }^{*}⟩\phi \}\cup \{\mathrm{\neg }\phi ,\mathrm{\neg }⟨\alpha ⟩\phi ,\mathrm{\neg }⟨{\alpha }^2⟩\phi ,\dots \}$

jest skończenie spełnialny (tzn. każdy skończony podzbiór jest spełnialny), ale cały zbiór nie jest spełnialny.

Przykłady tautologii PDL

W tej części przedstawimy przykłady tautologii PDL. Wszystkie dowody, jako łatwe pozostawimy Czytelnikowi. Pierwsza grupa tautologii to schematy znane z logiki modalnej.

Twierdzenie 10.7

Następujące formuły są tautologiami PDL.

$(i)⟨\alpha ⟩(\phi \vee \psi )\leftrightarrow ⟨\alpha ⟩\phi \vee ⟨\alpha ⟩\psi$

$(ii)[\alpha ](\phi \wedge \psi )\leftrightarrow [\alpha ]\phi \wedge [\alpha ]\psi$

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iii)\ \ \ [\alpha](\varphi\rightarrow\psi) \ \ \rightarrow\ \ ([\alpha]\varphi\rightarrow[\alpha]\psi)}

$(iv)⟨\alpha ⟩(\phi \wedge \psi )\to ⟨\alpha ⟩\phi \wedge ⟨\alpha ⟩\psi$

$(v)[\alpha ]\phi \vee [\alpha ]\psi \to [\alpha ](\phi \vee \psi )$

$(vi)⟨\alpha ⟩\mathrm{\perp }\leftrightarrow \mathrm{\perp }$

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vii)\ \ \ [\alpha]\varphi \ \ \leftrightarrow\ \ \ \neg\langle\alpha\rangle\neg\varphi} .

Implikacje odwrotne w Twierdzeniu 10.7 $(iii)-(v)$ nie zachodzą. Przykładowo implikacja odwrotna do $(iv)$ nie jest spełniona w stanie $u$ następującej struktury Kripkego.

Następna grupa tautologii, specyficzna dla PDL, dotyczy spójników programotwórczych $;$ i $\cup$ oraz testu $?$.

Twierdzenie 10.8

Następujące formuły są tautologiami PDL.

$(i)⟨\alpha \cup \beta ⟩\phi \leftrightarrow ⟨\alpha ⟩\phi \vee ⟨\beta ⟩\phi$

$(ii)[\alpha \cup \beta ]\phi \leftrightarrow [\alpha ]\phi \wedge [\beta ]\phi$

$(iii)⟨\alpha ;\beta ⟩\phi \leftrightarrow ⟨\alpha ⟩⟨\beta ⟩\phi$

$(iv)[\alpha ;\beta ]\phi \leftrightarrow [\alpha ][\beta ]\phi$

$(v)⟨\phi ?⟩\psi \leftrightarrow (\phi \wedge \psi )$

$(vi)[\phi ?]\psi \leftrightarrow (\phi \to \psi )$.

Ostatnia grupa tautologii dotyczy operatora iteracji ${*}^{}$.

Twierdzenie 10.9

Nastepujące formuły są tautologiami PDL.

$(i)[{\alpha }^{*}]\phi \to \phi$

$(ii)\phi \to ⟨{\alpha }^{*}⟩\phi$

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iii)\ \ [\alpha^*]\varphi\ \ \rightarrow\ \ [\alpha]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iv)\ \ \ \langle\alpha\rangle\varphi\ \ \rightarrow\ \ \langle\alpha^*\rangle\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (v)\ \ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^*\alpha^*]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vi)\ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \langle\alpha^*\alpha^*\rangle\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vii)\ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^{**}]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (viii)\ \langle\alpha^*\rangle\varphi\ \leftrightarrow\ \ \langle\alpha^{**}\rangle\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (ix)\ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ \varphi\wedge[\alpha][\alpha^*]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (x)\ \ \ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \varphi\vee\langle\alpha\rangle\langle\alpha^*\rangle\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (xi)\ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ \varphi\wedge[\alpha^*](\varphi\rightarrow[\alpha]\varphi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (xii)\ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \varphi\vee\langle\alpha^*\rangle(\neg\varphi\wedge\langle\alpha\rangle\varphi)} .

Własność $(ii)$ mówi, że ${\alpha }^{*}$ jest semantycznie relacją zwrotną. Przechodniość relacji ${\alpha }^{*}$ jest wyrażona w $(vi)$. Natomiast fakt, że ${\alpha }^{*}$ zawiera relację $\alpha$, jest wyrażony w $(iv)$. Implikacja $\leftarrow$ w $(xi)$ wyraża zasadę indukcji. Bazą jest założenie, że własność $\phi$ jest spełniona w pewnym stanie $u$. Warunek indukcyjny mówi, że w każdym stanie osiągalnym z $u$ poprzez skończoną liczbę iteracji programu $\alpha$, kolejne wykonanie $\alpha$ zachowuje własność $\phi$. Teza stwierdza, że wówczas $\phi$ jest spełnione we wszystkich stanach osiągalnych w skończonej liczbie iteracji $\alpha$.

Własność małego modelu

W tej części udowodnimy własność małego modelu dla PDL. Własność ta mówi, że jeśli $\phi$ jest spełnialna, to jest spełniona w pewnej skończonej strukturze Kripkego. Co więcej, jak będzie wynikało z dowodu, struktura ta ma co najwyżej $2^{|\phi |}$ stanów, gdzie $|\phi |$ oznacza rozmiar formuły $\phi$. Wynika stąd natychmiast rozstrzygalność problemu spełnialności dla PDL. Technika zastosowana w dowodzie twierdzenia o małym modelu nosi nazwę filtracji i jest od dawna stosowana w logikach modalnych. W przypadku PDL sytuację komplikuje fakt, że definicja formuł i programów jest wzajemnie rekurencyjna, co powoduje że indukcyjne rozumowania są nieco bardziej delikatne. Własność małego modelu dla PDL została udowodniona w 1977r. przez M. Fischera i R. Ladnera. Zaczniemy od definicji domknięcia Fischera-Ladnera. Zdefiniujemy dwie funkcje

$FL$	$:\mathrm{\Phi }\to 2^{\mathrm{\Phi }}$
$F{L}^{◻}$	$:\{[\alpha ]\phi |\alpha \in \mathrm{\Psi },\phi \in \mathrm{\Phi }\}\to 2^{\mathrm{\Phi }}$

przez wzajemną indukcję

$(a)FL(p):=\{p\}$, gdy $p$ jest zmienną zdaniową

$(b)FL(\phi \to \psi ):=\{\phi \to \psi \}\cup FL(\phi )\cup FL(\psi )$

$(c)FL(\mathrm{\perp }):=\{\mathrm{\perp }\}$

$(d)FL([\alpha ]\phi ):=F{L}^{◻}([\alpha ]\phi )\cup FL(\phi )$

$(e)F{L}^{◻}([a]\phi ):=\{[a]\phi \}$, gdy $a$ jest atomowym programem

$(f)F{L}^{◻}([\alpha \cup \beta ]\phi ):=\{[\alpha \cup \beta ]\phi \}\cup F{L}^{◻}([\alpha ]\phi )\cup F{L}^{◻}([\beta ]\phi )$

$(g)F{L}^{◻}([\alpha ;\beta ]\phi ):=\{[\alpha ;\beta ]\phi \}\cup F{L}^{◻}([\alpha ][\beta ]\phi )\cup F{L}^{◻}([\beta ]\phi )$

$(h)F{L}^{◻}([{\alpha }^{*}]\phi ):=\{[{\alpha }^{*}]\phi \}\cup F{L}^{◻}([\alpha ][{\alpha }^{*}]\phi )$

$(i)F{L}^{◻}([\psi ?]\phi ):=\{[\psi ?]\phi \}\cup FL(\psi )$

Zbiór $FL(\phi )$ jest nazywany domknięciem Fischera-Ladnera. Zauważmy, że definicja $FL(\phi )$ jest indukcyjna ze względu na budowę formuły $\phi$, natomiast pomocnicza funkcja $F{L}^{◻}$ jest określona jedynie na formułach postaci $[\alpha ]\phi$ i jej definicja jest indukcyjna ze względu na budowę programu $\alpha$. Tak więc chociaż w warunku $(h)$ formuła po prawej stronie definicji jest dłuższa niż po lewej, to program $\alpha$ w zewnętrznej modalności jest prostszy niż ${\alpha }^{*}$ i dlatego definicja ta jest dobrze ufundowana.

Niech $|\alpha |$ oraz $|\phi |$ oznaczają długość programu $\alpha$ i formuły $\phi$ rozumianą jako liczbę wystąpień symboli nie licząc nawiasów. Następujący lemat podaje ograniczenie górne na moc domknięcia Fischera-Ladnera.

Lemat 10.10

$(i)$ Dla dowolnej formuły $\phi$ mamy $|FL(\phi )|\le |\phi |$.

$(ii)$ Dla dowolnej formuły $[\alpha ]\phi$ mamy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle |FL^{\Box}([\alpha]\varphi}| \leq |\alpha|} .

Dowód

Dowód jest przez jednoczesną indukcję ze względu na schemat definiujący $FL$ oraz $F{L}^{◻}$. Pozostawimy go Czytelnikowi jako ćwiczenie.

Następny lemat ma charakter techniczny. Będzie wykorzystany w dowodzie lematu o filtracji.

Lemat 10.11

$(i)$ Jeśli $\sigma \in FL(\phi )$, to $FL(\sigma )\subseteq FL(\phi )$.

$(ii)$ Jeśli $\sigma \in F{L}^{◻}([\alpha ]\phi )$, to

$FL(\sigma )\subseteq F{L}^{◻}([\alpha ]\phi )\cup FL(\phi )$.

Dowód

Dowodzimy (i) oraz (ii) przez jednoczesną indukcję. Szczegóły pozostawiamy Czytelnikowi jako ćwiczenie.

Następujące własości $FL$ są bezpośrednią konsekwencją Lematu 10.11.

Lemat 10.12

$(i)$ Jeśli $[\alpha ]\psi \in FL(\phi )$, to $\psi \in FL(\phi )$.

$(ii)$ Jeśli $[\rho ?]\psi \in FL(\phi )$, to $\rho \in FL(\phi )$.

$(iii)$ Jeśli $[\alpha \cup \beta ]\psi \in FL(\phi )$, to $[\alpha ]\psi \in FL(\phi )$ oraz $[\beta ]\psi \in FL(\phi )$.

$(iv)$ Jeśli $[\alpha ;\beta ]\psi \in FL(\phi )$, to $[\alpha ][\beta ]\psi \in FL(\phi )$ oraz $[\beta ]\psi \in FL(\phi )$.

$(v)$ Jeśli $[{\alpha }^{*}]\psi \in FL(\phi )$, to $[\alpha ][{\alpha }^{*}]\psi \in FL(\phi )$.

Dla danej formuły $\phi$ oraz struktury Kripkego $\mathfrak{𝔎}=(K,{\mathrm{m}}_{\mathfrak{𝔎}})$ definiujemy nową strukturę $\mathfrak{𝔎}/FL(\phi )=⟨K/FL(\phi ),{\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}⟩$, zwaną filtracją struktury $\mathfrak{𝔎}$ przez $FL(\phi )$. Najpierw definiujemy binarną relację $\equiv$ w zbiorze stanów $\mathfrak{𝔎}$.

$u\equiv v$ wtedy i tylko wtedy, gdy $\mathrm{\forall }\psi \in FL(\phi )(u\in {\mathrm{m}}_{\mathfrak{𝔎}}(\psi )⟺v\in {\mathrm{m}}_{\mathfrak{𝔎}}(\psi )).$

Innymi słowy, utożsamiamy stany $u$ oraz $v$ jeśli są one nierozróżnialne przez żadną formułę ze zbioru $FL(\varphi )$. Filtracja struktury jest zwykłą konstrukcją ilorazową. Niech

$[u]$	$:=\{v|v\equiv u\}$
$K/FL(\phi )$	$:=\{[u]|u\in K\}$
${\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(p)$	$:=\{[u]|u\in {\mathrm{m}}_{\mathfrak{𝔎}}(p)\}$, gdy $p$ jest zmienną losową
${\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(a)$	$:=\{⟨[u],[v]⟩|⟨u,v⟩\in {\mathrm{m}}_{\mathfrak{𝔎}}(a)\}$, gdy $a$ jest atomowym programem.

Przekształcenie ${\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}$ rozszerza się w zwykły sposób na wszystkie formuły i programy.

Następujący lemat pokazuje związek pomiędzy strukturami $\mathfrak{𝔎}$ oraz $\mathfrak{𝔎}/FL(\phi )$. Główna trudność techniczna polega tu na sformułowaniu poprawnego założenia indukcyjnego. Sam dowód (jednoczesna indukcja) jest zupełnie rutynowy i dlatego pozostawimy go Czytelnikowi jako ćwiczenie.

Lemat 10.13 (o filtracji)

Niech $u,v$ będą stanami w strukturze Kripkego $\mathfrak{𝔎}$.

$(i)$ Dla dowolnej formuły $\psi \in FL(\phi )$, mamy $u\in {\mathrm{m}}_{\mathfrak{𝔎}}(\psi )⟺[u]\in {\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(\psi )$.

$(ii)$ Dla dowolnej formuły $[\alpha ]\psi \in FL(\phi )$ zachodzi

$(a)$ jeśli $⟨u,v⟩\in {\mathrm{m}}_{\mathfrak{𝔎}}(\alpha )$, to $⟨[u],[v]⟩\in {\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(\alpha )$;

$(a)$ jeśli $⟨[u],[v]⟩\in {\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(\alpha )$ oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle u\in\mathrm{m}_{\mathfrak{K}([\alpha]\psi)} , to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle v\in\mathrm{m}_{\mathfrak{K}(\psi)} .

Z lematu o filtracji natychmiast dostajemy twierdzenie o małym modelu.

Twierdzenie 10.14 (Własność małego modelu)

Niech $\phi$ będzie spełnialną formułą PDL. Wówczas $\phi$ jest spełniona w strukturze Kripkego mającej co najwyżej $2^{|\phi |}$ stanów.

Dowód

Jeśli $\phi$ jest spełnialna, to istnieje struktura Kripkego $\mathfrak{𝔎}$ oraz stan $u\in \mathfrak{𝔎}$, taki że $u\in {\mathrm{m}}_{\mathfrak{𝔎}}(\phi )$. Niech $FL(\phi )$ będzie domknięciem Fischera-Ladnera formuły $\phi$. Na mocy Lematu 10.13 o filtracji mamy $[u]\in {\mathrm{m}}_{\mathfrak{𝔎}/FL(\phi )}(\phi )$. Ponadto $\mathfrak{𝔎}/FL(\phi )$ ma nie więcej stanów niż liczba wartościowań przypisujących wartości logiczne formułom z $FL(\phi )$. Tych ostatnich jest, na mocy Lematu 10.10 $(i)$, co najwyżej $2^{|\phi |}$.

Z powyższego twierdzenia natychmiast wynika rozstrzygalność problemu spełnialności dla formuł PDL. Naiwny algorytm polegający na przeszukiwaniu wszystkich struktur Kripkego o co najwyżej $2^{|\varphi |}$ stanach ma złożoność podwójnie wykładniczą względem długości formuły. Używając nieco sprytniejszej metody można rozstrzygnąć problem spełnialności w czasie pojedynczo wykładniczym. Złożoność ta jest najlepsza możliwa, można bowiem pokazać, że problem spełnialności dla PDL jest zupełny w deterministycznym czasie wykładniczym.

Aksjomatyzacja PDL

Podamy teraz system formalny dla PDL i naszkicujemy dowód jego pełności. Jest to system w stylu Hilberta.

Aksjomaty

$(P0)$ Aksjomaty logiki zdaniowej

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P1) \ \ [\alpha](\varphi\to\psi)\ \ \to\ \ ([\alpha]\varphi\to[\alpha]\psi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P2) \ \ [\alpha](\varphi\wedge\psi)\ \ \leftrightarrow\ \ ([\alpha]\varphi\wedge[\alpha]\psi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P3) \ \ [\alpha\cup\beta]\varphi\ \ \leftrightarrow\ \ ([\alpha]\varphi\wedge[\beta]\varphi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P4) \ \ [\alpha;\beta]\varphi\ \ \leftrightarrow\ \ ([\alpha][\beta]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P5) \ \ [\psi?]\varphi\ \ \leftrightarrow\ \ (\psi\to\varphi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P6) \ \ \varphi\wedge[\alpha][\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^*]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P7) \ \ \varphi\wedge[\alpha^*](\varphi\to[\alpha]\varphi)\ \ \to\ \ [\alpha^*]\varphi \ \ \ } (aksjomat indukcji)

Reguły dowodzenia

$(MP)\frac{\phi \phi \to \psi }{\psi }$

$(GEN)\frac{\phi }{[\alpha ]\phi }$

Reguła (GEN) nazywana jest regułą modalnej generalizacji. Jeśli $\phi$ daje się wyprowadzić w powyższym systemie poszerzonym o dodanie nowych aksjomatów ze zbioru $\mathrm{\Sigma }$, to będziemy to zapisywać przez $\mathrm{\Sigma }⊢\phi$. Jak zwykle piszemy $⊢\varphi$, gdy $\mathrm{\Sigma }$ jest zbiorem pustym.

Fakt, że wszystkie aksjomaty są tautologiami PDL, wynika z Sekcji: Przykłady tautologii PDL. Pozostawimy Czytelnikowi sprawdzenie, że powyższe reguły zachowują własność bycia tautologią. Tak więc każde twierdzenie powyższego systemu jest tautologią. Naszkicujemy dowód twierdzenia odwrotnego, czyli tzw. twierdzenia o pełności dla PDL. Przypomnijmy, że zbiór formuł $\mathrm{\Sigma }$ jest sprzeczny, gdy $\mathrm{\Sigma }⊢\mathrm{\perp }$. W przeciwnym przypadku mówimy, że $\mathrm{\Sigma }$ jest niesprzeczny. W poniższym lemacie zebrane są podstawowe własności zbiorów niesprzecznych potrzebne do dowodu twierdzenia o pełności.

Lemat 10.15

Niech $\mathrm{\Sigma }$ będzie zbiorem formuł PDL. Wówczas

$(i)\mathrm{\Sigma }$ jest niesprzeczny wtedy i tylko wtedy, gdy $\mathrm{\Sigma }\cup \{\phi \}$ jest niesprzeczny lub $\mathrm{\Sigma }\cup \{\mathrm{\neg }\phi \}$ jest niesprzeczny;

$(ii)$ jeśli $\mathrm{\Sigma }$ jest niesprzeczny, to $\mathrm{\Sigma }$ jest zawarty w maksymalnym niesprzecznym zbiorze formuł.

Ponadto, jeśli $\mathrm{\Sigma }$ jest maksymalnym niesprzecznym zbiorem formuł, to

$(iii)\mathrm{\Sigma }$ zawiera wszystkie twierdzenia PDL;

$(iv)$ jeśli $\phi \in \mathrm{\Sigma }$ oraz $\phi \to \psi \in \mathrm{\Sigma }$, to $\psi \in \mathrm{\Sigma }$;

$(v)\phi \vee \psi \in \mathrm{\Sigma }$ wtedy i tylko wtedy, gdy $\phi \in \mathrm{\Sigma }$ lub $\psi \in \mathrm{\Sigma }$;

$(vi)\phi \wedge \psi \in \mathrm{\Sigma }$ wtedy i tylko wtedy, gdy $\phi \in \mathrm{\Sigma }$ oraz $\psi \in \mathrm{\Sigma }$;

$(vii)\phi \in \mathrm{\Sigma }$ wtedy i tylko wtedy, gdy $\mathrm{\neg }\phi \in ̸\mathrm{\Sigma }$;

$(viii)\mathrm{\perp }\in ̸\mathrm{\Sigma }$.

Z powyższego lematu natychmiast dostajemy następującą własność.

Lemat 10.16

Niech $\mathrm{\Sigma }$ oraz $\mathrm{\Gamma }$ będą maksymalnymi niesprzecznymi zbiorami formuł oraz niech $\alpha$ będzie dowolnym programem. Następujące dwa warunki są równoważne:

$(a)$ Dla dowolnej formuły $\psi$, jeśli $\psi \in \mathrm{\Gamma }$, to $⟨\alpha ⟩\psi \in \mathrm{\Sigma }$.

$(b)$ Dla dowolnej formuły $\psi$, jeśli $[\alpha ]\psi \in \mathrm{\Sigma }$, to $\psi \in \mathrm{\Gamma }$.

Struktura, którą za chwilę zbudujemy przy użyciu maksymalnych niesprzecznych zbiorów formuł nie będzie strukturą Kripkego z tego względu, że znaczeniem programu ${\alpha }^{*}$ nie będzie musiało być domknięcie przechodnie i zwrotne relacji wyznaczonej przez $\alpha$. Spełnione będą nieco słabsze własności, wystarczające jednak do przeprowadzenia dowodu twierdzenia o pełności.

Definicja 10.17

Niestandardową strukturą Kripkego nazwiemy każdą strukturę $\mathfrak{𝔑}=(N,{\mathrm{m}}_{\mathfrak{𝔑}})$ spełniającą wszystkie warunki struktury Kripkego podane w definicjach 10.2 oraz 10.3 za wyjątkiem warunku (14). Zamiast tego warunku żądamy, aby ${\mathrm{m}}_{\mathfrak{𝔑}}({\alpha }^{*})$ było relacją zwrotną i przechodnią, zawierało relację ${\mathrm{m}}_{\mathfrak{𝔑}}(\alpha )$ oraz spełniało aksjomaty $(P6)$ i $(P7)$. Tzn. zamiast warunku

${\mathrm{m}}_{\mathfrak{𝔑}}({\alpha }^{*}):=\bigcup _{n\ge 0}{\mathrm{m}}_{\mathfrak{𝔑}}(\alpha {)}^n,(15)$

żądamy, aby dla każdego programu $\alpha$, relacja ${\mathrm{m}}_{\mathfrak{𝔑}}({\alpha }^{*})$ była zwrotna, przechodnia, zawierała ${\mathrm{m}}_{\mathfrak{𝔑}}(\alpha )$ oraz spełniała następujące dwa warunki dla dowolnej formuły $\phi$

${\mathrm{m}}_{\mathfrak{𝔑}}([{\alpha }^{*}]\phi )={\mathrm{m}}_{\mathfrak{𝔑}}(\phi \wedge [\alpha ;{\alpha }^{*}]\phi )(16)$

${\mathrm{m}}_{\mathfrak{𝔑}}([{\alpha }^{*}]\phi )={\mathrm{m}}_{\mathfrak{𝔑}}(\phi \wedge [{\alpha }^{*}](\phi \to [\alpha ]\phi )).(17)$

Wracamy teraz do konstrukcji struktury z maksymalnych niesprzecznych zbiorów formuł. Zdefiniujemy niestandardową strukturę Kripkego $\mathfrak{𝔑}=(N,{\mathrm{m}}_{\mathfrak{𝔑}})$ następująco

$N$	$:=\{$ maksymalnie niesprzeczne zbiory formuł PDL $\}$
${\mathrm{m}}_{\mathfrak{𝔑}}(\phi )$	$:=\{s|\phi \in s\}$
${\mathrm{m}}_{\mathfrak{𝔑}}(\alpha )$	$:=\{⟨s,t⟩|$ dla wszystkich $\phi$, jeśli $\phi \in t$, to $⟨\alpha ⟩\phi \in s\}$
	$:=\{⟨s,t⟩|$ dla wszystkich $\phi$, jeśli $[\alpha ]\phi \in s$, to $\phi \in t\}$

Z Lematu Lematu 10.16 wynika, że obydwie definicje ${\mathrm{m}}_{\mathfrak{𝔑}}(\alpha )$ są równoważne. Dowód nastepującego twierdzenia pozostawimy Czytelnikowi.

Twierdzenie 10.18

Struktura $\mathfrak{𝔑}$ jest niestandardową strukturą Kripkego.

Dowód

Fakt, że $\mathfrak{𝔑}$ spełnia własności (16) oraz (17) wynika natychmiast z Lematu 10.15 $(iii)$ oraz z aksjomatów (P6) i (P7). Sprawdzenie pozostałych warunków pozostawimy Czytelnikowi jako ćwiczenie.

Istotną cechą niestandardowych struktur Kripkego jest to, że daje się przenieść na nie lemat o filtracji (Lemat 10.13).

Lemat 10.19 (o filtracji dla niestandardowych struktur Kripkego)

Niech $\mathfrak{𝔑}$ będzie niestandardową strukturą Kripkego i niech $u,v$ będą stanami w $\mathfrak{𝔑}$.

$(i)$ Dla dowolnej formuły $\psi \in FL(\phi )$, mamy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle u\in \mathrm{m}_{\mathfrak{N}}(\psi) \ \iff \ [u]\in \mathrm{m}_{\mathfrak{N}/FL(\varphi)}(\psi)} .

$(ii)$ Dla dowolnej formuły $[\alpha ]\psi \in FL(\phi )$ zachodzi

$(a)$ jeśli $⟨u,v⟩\in {\mathrm{m}}_{\mathfrak{𝔑}}(\alpha )$, to $⟨[u],[v]⟩\in {\mathrm{m}}_{\mathfrak{𝔑}/FL(\phi )}(\alpha );$

$(b)$ jeśli $⟨[u],[v]⟩\in {\mathrm{m}}_{\mathfrak{𝔑}/FL(\phi )}(\alpha )$ oraz $u\in {\mathrm{m}}_{\mathfrak{𝔑}}([\alpha ]\psi )$ to $v\in {\mathrm{m}}_{\mathfrak{𝔑}}(\psi )$.

Dowód

Szczegóły dowodu tego lematu pomijamy, zachęcając jednocześnie Czytelnika do spróbowania własnych sił. Różnica w dowodzie tego lematu w stosunku do dowodu Lematu 10.13 polega na tym, że w dowodze kroku indukcyjnego dla części $(ii)$ dla przypadku, gdy $\alpha$ jest programem postaci ${\beta }^{*}$ wykorzystujemy jedynie własności (16) oraz (17), zamiast (15).

Możemy już teraz zakończyć dowód twierdzenia o pełności.

Twierdzenie 10.20 (Pełność dla PDL)

Każda tautologia PDL jest twierdzeniem systemu: dla dowolnej formuły $\phi$, jeśli $\models \phi$, to $⊢\phi$.

Dowód

Rozumujemy przez sprzeczność. Jeśli $⊬\phi$, to $\{\mathrm{\neg }\phi \}$ jest zbiorem niesprzecznym. Zatem na mocy Lematu 10.15 $(ii)$ istnieje maksymalny niesprzeczny zbiór $u$ formuł PDL zawierający $\mathrm{\neg }\phi$. Na mocy lematu o filtracji dla niestandardowych struktur Kripkego (Lemat 10.19) stwierdzamy, że $\mathrm{\neg }\phi$ jest spełniona w stanie $[u]$ skończonej struktury $\mathfrak{𝔑}/FL(\phi )$. Łatwo jest zauważyć, że skończona niestandardowa struktura Kripkego jest zwykłą strukturą Kripkego (tzn. taką, w której zachodzi (15)). Tak więc $\phi$ nie jest tautologią. To kończy dowód twierdzenia o pełności.