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 części tej pokażemy jedynie dwie podstawowe własności PDL: własność małego modelu oraz przedstawimy aksjomatyzację i udowodnimy jej pełność. 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) $\varphi ,\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 ($\star$). 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 \star$ oznacza wykonanie $\alpha$ pewną liczbę razy, być może zero. Ponadto mamy operację testowania tworzącą z każdej formuły $\varphi$ nowy program $\varphi ?$. Wykonanie programu $\varphi ?$ jest możliwe tylko wtedy, gdy warunek $\varphi$ zachodzi. Z drugiej strony, formuły mogą odwoływać się do dowolnego programu $\alpha$ poprzez modalność konieczności Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha} : dla dowolnego zdania $\varphi$, napis

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi }

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

Definicja

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

• Parser nie mógł rozpoznać (nieznana funkcja „\zmz”): {\displaystyle \displaystyle \zmz\subs\Phi}
• Parser nie mógł rozpoznać (nieznana funkcja „\subs”): {\displaystyle \displaystyle \Pi_0\subs\Pi}
• je¶li $\varphi ,\psi \in \mathrm{\Phi }$, to Parser nie mógł rozpoznać (nieznana funkcja „\imp”): {\displaystyle \displaystyle \phi\imp\psi\in\Phi} oraz

Parser nie mógł rozpoznać (nieznana funkcja „\false”): {\displaystyle \displaystyle \false\in\Phi}

• je¶li $\alpha ,\beta \in \mathrm{\Pi }$, to $(\alpha ;\beta )$,

$(\alpha \cup \beta )$, oraz $\alpha \star \in \mathrm{\Pi }$

• je¶li $\alpha \in \mathrm{\Pi }$

oraz $\varphi \in \mathrm{\Phi }$, to Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi\in\Phi}

• je¶li $\varphi \in \mathrm{\Phi }$, to $\varphi ?\in \mathrm{\Pi }.$

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

• Jednoargumentowe operatory (wliczaj±c Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\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

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha;\beta\star \cup \gamma\star}\phi\join\psi }

odpowiada następuj±cemu wyrażeniu z nawiasami

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle (\bx{(\alpha;\beta\star)\cup\gamma\star}\phi)\join\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, żę negacja $\mathrm{\neg }\varphi$ jest skrótem formuły Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \phi\arr\false} . Dualnie do Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\,}} definiujemy modalno¶ć możliwo¶ci

Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\phi &\eqdef& \neg\bx{\alpha}\neg\phi.   }
  Zdanie

Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\phi} czytamy "istnieje obliczenie programu $\alpha$, które zatrzymuje się w stanie spełniaj±cym formułę $\varphi$". Istotn± różnic± pomiędzy modalno¶ciami Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\,}} i Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\,}} jest to, że Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\phi} implikuje iż program $\alpha$ się zatrzymuje, podczas gdy Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi} nie gwarantuje zatrzymania się programu $\alpha$. W szczególno¶ci formuła Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\false} wyraża własno¶ć mówi±c±, że żadne obliczenie programu $\alpha$ nie zatrzymuje się. Natomiast formuła Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\false} jest zawsze fałszywa.

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

Definicja

Struktura Kripkego jest uporz±dkowan± par± Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK = \<K,\: \mg K\>} , gdzie $K$ jest zbiorem elementów $u,v,w,\dots$ zwanych stanami, a Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K} jest funkcj± przyporz±dkowuj±c± każdemu atomowemu zdaniu Parser nie mógł rozpoznać (nieznana funkcja „\zmz”): {\displaystyle \displaystyle p\in\zmz} , podzbiór Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K(p)\subs K} oraz każdemu atomowemu programowi $a\in {\mathrm{\Pi }}_0$, relację binarn± Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K(a)\subs K\times K} .

Poniżej funkcję Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K} rozszerzymy do dowolnych formuł i dowolnych programów. Intuicyjnie dla formuły $\varphi$, zbiór stanów Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K(\phi)} jest zbiorem wszystkich stanów struktury Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} , w których $\varphi$ jest spełniona. Natomiast dla programu $\alpha$, relacja Parser nie mógł rozpoznać (nieznana funkcja „\mg”): {\displaystyle \displaystyle \mg K(\alpha)} jest tzw. relacj± wej¶cia-wyj¶cia programu $\alpha$ w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} .

Definicja

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \displaystyle \aligned \Mg K{\phi\imp\psi} &\eqdef& (K-\Mg K \phi)\cup\Mg K \psi\nonumber\\ \Mg K{\false} &\eqdef& \emptyset\nonumber\\ \Mg K{\bx\alpha\phi} &\eqdef& \set u {\forall v\in K(\<u,v\>\in \Mg K\alpha \To v\in\Mg K \phi)} \nonumber\\ \Mg K{\alpha;\beta} &\eqdef& \set{\<u,v\>}{\exists w\in K(\<u,w\>\in \Mg K \alpha \wedge \<w,v\>\in \Mg K \beta)}\nonumber\\ \Mg K{\alpha\cup\beta} &\eqdef& \Mg K \alpha\cup \Mg K \beta\nonumber\\ \Mg K{\alpha\star} &\eqdef& \ \bigcup_{n\geq 0} \Mg K \alpha^n\nonumber\\ \Mg K{\phi?} &\eqdef& \set{\<u,u\>}{u\in\Mg K \phi}.\nonumber \endaligned}

Definicja

Powiemy, że formuła $\varphi$ jest spełniona w stanie $u$ struktury Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} , gdy Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg K\phi} . Podobnie jak w logice pierwszego rzędu spełnianie zapisujemy następuj±co Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \displaystyle \sat \frK u\phi} . Gdy z kontekstu wynika o jak± strukturę chodzi, to możemy po prostu pisać $u\models \varphi$.

Powiemy, że formuła $\varphi$ jest prawdziwa w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} , gdy jest spełniona w każdym stanie tej struktury. Zapisujemy to Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK\models\phi} . Formuła $\varphi$ jest tautologi± PDL, gdy jest ona prawdziwa w każdej strukturze Kripkego. Wreszcie powiemy, że formuła $\varphi$ jest spełnialna, gdy istnieje struktura Kripkego Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} , taka że $\varphi$ jest spełniona w przynajmniej jednym stanie Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} .

Przykład

Niech $p$ będzie zmienn± zdaniow± oraz niech $a$ będzie atomowym programem. Niech Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK = (K,\:\mg K)} będzie tak± struktur± Kripkego, że

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle K &= \{u,v,w\}\\ \Mg K p &= \{u,v\}\\ \Mg K a &= \{\<u,v\>,\<u,w\>,\<v,w\>,\<w,v\>\}.   }
  Nastepuj±cy diagram ilustruje

Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} .

(0,75)(30,-15)
(0,0)Szablon:4 (60,0)Szablon:4

(30,40)Szablon:4 (-2,-2){(0,0)[tr]{$u$

(62,-2){(0,0)[tl]{$v$}} (30,45){(0,0)[b]{$w$}} (30,0){(90,30)} (85,0){(0,0)[t]{$p$}} (0,0){(3,4){30}} (0,0){(1,0){60}} (60,0){(-3,4){30}} (60,0){(3,-4){0}} (30,-3){(0,0)[t]{$a$}} (13,22){(0,0)[br]{$a$}} (47,22){(0,0)[bl]{$a$}}

W tej strukturze mamy Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle u\models\d a\neg p\meet\d a p} , ale Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle v\models\bx a\neg p} oraz Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle w\models\bx a p} . Ponadto każdy stan struktury Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} spełnia następuj±c± formułę Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{a\star}\bx{(aa)\star}p \meet \d{a\star}\bx{(aa)\star}\neg p. } }}

Przykład

Niech $p,q$ będ± zmiennymi zdaniowymi i niech $a,b$ będ± atomowymi programami. Ponadto niech Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK = (K,\mg K)} będzie struktur± Kripkego zdefiniowan± następuj±co Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle K &= \{s,t,u,v\}\\ \Mg K p &= \{u,v\}\\ \Mg K q &= \{t,v\}\\ \Mg K a &= \{\<t,v\>,\<v,t\>,\<s,u\>,\<u,s\>\}\\ \Mg K b &= \{\<u,v\>,\<v,u\>,\<s,t\>,\<t,s\>\}. } Następuj±cy rysunek ilustruje Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} .

(0,85)(25,-13)
(0,0)Szablon:4 (0,50)Szablon:4

(50,0)Szablon:4 (50,50)Szablon:4

(-2,-2){(0,0)[tr]{$u$

(-2,52){(0,0)[br]{$s$}} (52,-2){(0,0)[tl]{$v$}} (52,52){(0,0)[bl]{$t$}} (50,25){(30,75)} (25,0){(75,30)} (72,40){(0,0)[l]{$q$}} (-18,0){(0,0)[r]{$p$}} (0,50){(0,-1){50}} (0,50){(1,0){50}} (0,0){(1,0){50}} (0,0){(0,1){50}} (50,0){(0,1){50}} (50,0){(-1,0){50}} (50,50){(-1,0){50}} (50,50){(0,-1){50}} (25,-3){(0,0)[t]{$b$}} (25,53){(0,0)[b]{$b$}} (-3,25){(0,0)[r]{$a$}} (53,25){(0,0)[l]{$a$}}

Następuj±ce formuły s± prawdziwe w Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} . Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle p &\oto& \bx{(ab\star a)\star}p\\ q &\oto& \bx{(ba\star b)\star}q. } Ponadto niech $\alpha$ będzie programem

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \displaystyle \aligned \alpha &= (aa\cup bb\cup(ab\cup ba)(aa\cup bb)\star(ab\cup ba))\star. \endaligned}

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 $\varphi$, formuła Parser nie mógł rozpoznać (nieznana funkcja „\oto”): {\displaystyle \displaystyle \phi\oto\bx\alpha\phi} jest prawdziwa w Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} . }}

Zauważmy, że operator $\star$ 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

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \displaystyle \aligned \{\d{\alpha\star}\phi\} &\cup& \{\neg\phi,\ \neg\d\alpha\phi,\ \neg\d{\alpha^2}\phi,\ \ldots\} \endaligned}

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

Następuj±ce formuły s± tautologiami { PDL}.

1. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d \alpha (\phi\join\psi) \ \ \oto\ \ \d \alpha\phi\join\d \alpha \psi}
2. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx \alpha (\phi\meet\psi) \ \ \oto\ \ \bx \alpha\phi\meet\bx \alpha\psi}
3. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha(\phi\imp\psi) \ \ \imp\ \ (\bx\alpha\phi\imp\bx\alpha\psi)}
4. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d \alpha(\phi\meet\psi) \ \ \imp\ \ \d \alpha\phi\meet\d \alpha\psi}
5. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx \alpha\phi\join\bx \alpha\psi\ \ \imp\ \ \bx \alpha(\phi\join\psi)}
6. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d \alpha \false \ \ \oto\ \ \ \false}
7. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi \ \ \oto\ \ \ \neg\d\alpha\neg\phi} .

Implikacje odwrotne w Twierdzeniu Uzupelnic thm-PDLmodal1|{eqn-PDLmodal1-4}--{eqn-PDLmodal1-6} nie zachodz±. Przykładowo implikacja odwrotna do {eqn-PDLmodal1-5} nie jest spełniona w stanie $u$ następuj±cej struktury Kripkego.

(0,40)(40,0)
(0,20)Szablon:4 (-5,20){(0,0)[r]{$u$}}

(0,20){(2,1){40}} (0,20){(2,-1){40}} (40,40)Szablon:4 (40,0)Szablon:4 (45,40){(0,0)[l]{Parser nie mógł rozpoznać (nieznana funkcja „\meet”): {\displaystyle \displaystyle \phi\meet\neg\psi} }} (45,0){(0,0)[l]{Parser nie mógł rozpoznać (nieznana funkcja „\meet”): {\displaystyle \displaystyle \psi\meet\neg\phi} }}

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

Twierdzenie

Następuj±ce formuły s± tautologiami { PDL}.

1. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\alpha\cup\beta}\phi\ \ \oto\ \ \d\alpha\phi\join\d\beta\phi}
2. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\cup\beta}\phi\ \ \oto\ \ \bx\alpha\phi\meet\bx\beta\phi}
3. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\comp\alpha\beta}\phi\ \ \oto\ \ \d\alpha\d\beta\phi}
4. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\comp\alpha\beta}\phi\ \ \oto\ \ \bx\alpha\bx\beta\phi}
5. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\phi?}\psi\ \ \oto\ \ (\phi\meet\psi)}
6. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\phi?}\psi \ \ \oto\ \ (\phi\imp\psi)} .

Ostatnia grupa tautologii dotyczy operatora iteracji $\star$.

Twierdzenie

Nastepuj±ce formuły s± tautologiami { PDL}.

1. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \imp\ \ \phi}
2. Parser nie mógł rozpoznać (nieznana funkcja „\imp”): {\displaystyle \displaystyle \phi\ \ \imp\ \ \d{\alpha\star}\phi}
3. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \imp\ \ \bx\alpha\phi}
4. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\phi\ \ \imp\ \ \d{\alpha\star}\phi}
5. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \oto\ \ \bx{\alpha\star\alpha\star}\phi}
6. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\alpha\star}\phi\ \ \oto\ \ \d{\alpha\star\alpha\star}\phi}
7. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \oto\ \ \bx{\alpha\starstar}\phi}
8. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\alpha\star}\phi\ \ \oto\ \ \d{\alpha\starstar}\phi}
9. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \oto\ \ \phi\meet\bx\alpha\bx{\alpha\star}\phi}
10. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\alpha\star}\phi\ \ \oto\ \ \phi\join\d\alpha\d{\alpha\star}\phi}
11. Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\phi\ \ \oto\ \ \phi\meet\bx{\alpha\star}(\phi\imp\bx\alpha\phi)}
12. Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d{\alpha\star}\phi\ \ \oto\ \ \phi\join\d{\alpha\star}(\neg\phi\meet\d\alpha\phi)} .

Własno¶ć {eqn-starprops1-1a} mówi, że $\alpha \star$ jest semantycznie relacj± zwrotn±. Przechodnio¶ć relacji $\alpha \star$ jest wyrażona w {eqn-starprops1-3a}. Natomiast fakt, ze $\alpha \star$ zawiera relację $\alpha$ jest wyrażony w {eqn-starprops1-2a}. Implikacja $\leftarrow$ w {eqn-starprops1-6} wyraża zasadę indukcji. Baz± jest założenie, że własno¶ć $\varphi$ 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 $\varphi$ 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 $\varphi$ 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^{|\varphi |}$ stanów, gdzie $|\varphi |$ oznacza rozmiar formuły $\varphi$. 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 Parser nie mógł rozpoznać (nieznana funkcja „\FLname”): {\displaystyle \displaystyle \FLname &: \Phi\ \ \imp\ \ \powerset{\Phi}\\ \FLpname &: \set{\bx\alpha\phi}{\alpha\in\Psi,\ \phi\in\Phi}\ \ \imp\ \ \powerset{\Phi} } przez wzajemn± indukcję

1. Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL p\ \ \eqdef\ \ \{p\}} , gdy $p$ jest zmienn± zdaniow±
2. Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL{\phi\imp\psi}\ \ \eqdef\ \ \{\phi\imp\psi\}\cup\FL\phi\cup\FL\psi}
3. Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL{\false}\ \ \eqdef\ \ \{\false\}}
4. Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL{\bx\alpha\phi}\ \ \eqdef\ \ \FLp{\bx\alpha\phi}\cup\FL\phi}
5. Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \FLp{\bx a\phi}\ \ \eqdef\ \ \{\bx a\phi\}} , gdy $a$ jest

atomowym programem

1. Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \FLp{\bx{\alpha\cup\beta}\phi}\ \ \eqdef\ \ \{\bx{\alpha\cup\beta}\phi\}\cup\FLp{\bx\alpha\phi}\cup\FLp{\bx\beta\phi}}
2. Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \FLp{\bx{\comp\alpha\beta}\phi}\ \ \eqdef\ \ \{\bx{\comp\alpha\beta}\phi\}\cup\FLp{\bx\alpha\bx\beta\phi}\cup \FLp{\bx\beta\phi}}
3. Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \FLp{\bx{\alpha\star}\phi}\ \ \eqdef\ \ \{\bx{\alpha\star}\phi\}\cup\FLp{\bx\alpha\bx{\alpha\star}\phi}}
4. Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \FLp{\bx{\psi?}\phi}\ \ \eqdef\ \ \{\bx{\psi?}\phi\}\cup\FL\psi} .

Zbiór Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} jest nazywany domknięciem Fischera-Ladnera. Zauważmy, że definicja Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} jest indukcyjna ze względu na budowę formuły $\varphi$, natomiast pomocnicza funkcja Parser nie mógł rozpoznać (nieznana funkcja „\FLpname”): {\displaystyle \displaystyle \FLpname} jest okre¶lona jedynie na formułach postaci Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\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 \star$ i dlatego definicja ta jest dobrze ufundowana.

Niech Parser nie mógł rozpoznać (nieznana funkcja „\len”): {\displaystyle \displaystyle \len\alpha} oraz Parser nie mógł rozpoznać (nieznana funkcja „\len”): {\displaystyle \displaystyle \len\phi} oznaczaj± długo¶ć programu $\alpha$ i formuły $\varphi$ rozumian± jako liczbę wyst±pień symboli nie licz±c nawiasów. Dla dowolnego zbioru $X$, przez $|X|$ oznaczamy moc zbioru $X$. Następuj±cy lemat podaje ograniczenie górne na moc domknięcia Fischera-Ladnera.

Lemat

1. Dla dowolnej formuły $\varphi$ mamy Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle |\FL\phi|\ \leq\ |\phi|} .
2. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi} mamy Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle |\FLp{\bx\alpha\phi}|\ \leq\ \len{\alpha}} .

Dowód

Dowód jest przez jednoczesn± indukcję  schemat definiuj±cy Parser nie mógł rozpoznać (nieznana funkcja „\FLname”): {\displaystyle \displaystyle \FLname} oraz Parser nie mógł rozpoznać (nieznana funkcja „\FLpname”): {\displaystyle \displaystyle \FLpname} . Pozostawimy go Czytelnikowi jako ćwiczenie.

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

Lemat

1. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \sigma\in\FL\phi} , to Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\sigma\subs\FL\phi} .
2. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\FLp”): {\displaystyle \displaystyle \sigma\in\FLp{\bx\alpha\phi}} , to

Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\sigma\subs\FLp{\bx\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 Parser nie mógł rozpoznać (nieznana funkcja „\FLname”): {\displaystyle \displaystyle \FLname} s± bezpo¶redni± konsekwencj± Lematu Uzupelnic lem-FLtrans|.

Lemat

1. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\psi\in\FL\phi} , to Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \psi\in\FL\phi} .
2. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\rho?}\psi\in\FL\phi} , to Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \rho\in\FL\phi} .
3. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\cup\beta}\psi\in\FL\phi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\psi\in\FL\phi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\beta\psi\in\FL\phi} .

1. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\comp\alpha\beta}\psi\in\FL\phi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\bx\beta\psi\in\FL\phi} and Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\beta\psi\in\FL\phi} .

1. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\star}\psi\in\FL\phi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\bx{\alpha\star}\psi\in\FL\phi} .

Dla danej formuły $\varphi$ oraz struktury Kripkego Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK = (K,\:\mg K)} definiujemy now± strukturę Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK/\FL\phi = \<K/\FL\phi,\:\umg{\frK/\FL\phi}\>} , zwan± filtracj± struktury Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} przez Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} . Najpierw definiujemy binarn± relację $\equiv$ w zbiorze stanów Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} . Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle u \equiv v & } , gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle & \forall\psi\in\FL\phi\ (u\in\Mg K{\psi}\Iff v\in\Mg K{\psi}). } Innymi słowy utożsamiamy stany $u$ oraz $v$ je¶li s± one nierozróżnialne przez żadn± formułę ze zbioru Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} . Filtracja struktury jest zwykł± konstrukcj± ilorazow±. Niech

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle [u] &\eqdef& \set v{v \equiv u}\\ K/\FL\phi &\eqdef& \set{[u]}{u\in K}\\ \uMg{\frK/\FL\phi}p &\eqdef& \set{[u]}{u\in\Mg K p},\quad  }
 gdy $p$

jest zmienn± zdaniow± Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \\ \uMg{\frK/\FL\phi}a &\eqdef& \set{\<[u],[v]\>}{\<u,v\> \in \Mg K a},\quad } gdy $a$ jest atomowym programem. Przekształcenie Parser nie mógł rozpoznać (nieznana funkcja „\umg”): {\displaystyle \displaystyle \umg{\frK/\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 Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} oraz Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK/\FL\phi} . Główna trudno¶ć techniczna polega tu sformułowaniu poprawnego założenia indukcyjnego. Sam dowód (jednoczesna indukcja) jest zupełnie rutynowy i dlatego pozostawimy go Czytelnikowi jako ćwiczenie.

Lemat (o filtracji)

Niech $u,v$ będ± stanami w strukturze Kripkego Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} .

1. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \psi\in\FL\phi} , mamy Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg K\psi \ \Iff \ [u]\in\uMg{\frK/\FL\phi}\psi} .
2. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\psi\in\FL\phi} zachodzi
   1. je¶li Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<u,v\>\in \Mg K\alpha} , to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<[u],[v]\>\in \uMg{\frK/\FL\phi}\alpha} ;
   2. je¶li Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<[u],[v]\>\in \uMg{\frK/\FL\phi}\alpha} oraz Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg K{\bx\alpha\psi}} , to Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle v\in\Mg K\psi} .

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

Twierdzenie (Własno¶ć małego modelu)

Niech $\varphi$ będzie spełnialn± formuł± { PDL}. Wówczas $\varphi$ jest spełniona w strukturze Kripkego maj±cej co najwyżej Parser nie mógł rozpoznać (nieznana funkcja „\len”): {\displaystyle \displaystyle 2^{\len{\phi}}} stanów.

Dowód

Je¶li $\varphi$ jest spełnialna, to istnieje struktura Kripkego Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK} oraz stan Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle u\in\frK} , taki że Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg K{\phi}} . Niech Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} będzie domknięciem Fischera-Ladnera formuły $\varphi$. Na mocy Lematu Uzupelnic filtration| o filtracji mamy Parser nie mógł rozpoznać (nieznana funkcja „\uMg”): {\displaystyle \displaystyle [u]\in\uMg{\frK/\FL\phi}{\phi}} . Ponadto Parser nie mógł rozpoznać (nieznana funkcja „\frK”): {\displaystyle \displaystyle \frK/\FL\phi} ma nie więcej stanów niż liczba warto¶ciowań przypisuj±cych warto¶ci logiczne formułom z Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \FL\phi} . Tych ostatnich jest, na mocy Lematu Uzupelnic lem-size|(i), co najwyżej Parser nie mógł rozpoznać (nieznana funkcja „\len”): {\displaystyle \displaystyle 2^{\len{\phi}}} .

Z powyższego twierdzenia natychmiast wynika rozstrzygalo¶ć problemu spełnialno¶ci dla formuł PDL. Naiwny algorytm polegaj±cy na przeszukiwaniu wszystkich struktur Kripkego o co najwyżej Parser nie mógł rozpoznać (nieznana funkcja „\len”): {\displaystyle \displaystyle 2^{\len\phi}} 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

(P1)

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha(\phi\imp\psi)\ \ \imp\ \ (\bx\alpha\phi\imp\bx\alpha\psi)}

(P2)

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha(\phi\meet\psi)\ \ \oto\ \ \bx\alpha\phi\meet\bx\alpha\psi}

(P3)

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\alpha\cup\beta}\phi\ \ \oto\ \ \bx\alpha\phi\meet\bx\beta\phi}

(P4)

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\comp\alpha\beta}\phi\ \ \oto\ \ \bx\alpha\bx\beta\phi}

(P5)

Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx{\psi?}\phi\ \ \oto\ \ (\psi\imp\phi)}

(P6)

Parser nie mógł rozpoznać (nieznana funkcja „\meet”): {\displaystyle \displaystyle \phi\meet\bx\alpha\bx{\alpha\star}\phi\ \ \oto\ \ \bx{\alpha\star}\phi}

(P7)

Parser nie mógł rozpoznać (nieznana funkcja „\meet”): {\displaystyle \displaystyle \phi\meet\bx{\alpha\star}(\phi\imp\bx\alpha\phi)\ \ \imp\ \ \bx{\alpha\star}\phi} (aksjomat indukcji)

Reguły dowodzenia

(MP)

  Parser nie mógł rozpoznać (nieznana funkcja „\imp”): {\displaystyle \displaystyle \displaystyle\frac{\phi \quad \phi\imp\psi}{\psi}}

(GEN)

  Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \displaystyle\frac{\phi}{\bx\alpha\phi}}

Reguła (GEN) nazywana jest reguł± modalnej generalizacji. Je¶li $\varphi$ 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 }⊢\varphi$. Jak zwykle piszemy $⊢\varphi$, gdy $\mathrm{\Sigma }$ jest zbiorem pustym.

Fakt, że wszystkie aksjomaty s± tautologiami PDL wynika z Sekcji Uzupelnic ex-taut-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 Parser nie mógł rozpoznać (nieznana funkcja „\false”): {\displaystyle \displaystyle \Sigma\vdash\false} . 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

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

1. $\mathrm{\Sigma }$ jest niesprzeczny , gdy

$\mathrm{\Sigma }\cup \{\varphi \}$ jest niesprzeczny lub $\mathrm{\Sigma }\cup \{\mathrm{\neg }\varphi \}$ jest niesprzeczny;

1. 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

{enumi}2

1. $\mathrm{\Sigma }$ zawiera wszystkie twierdzenia

{ PDL};

1. je¶li $\varphi \in \mathrm{\Sigma }$ oraz

Parser nie mógł rozpoznać (nieznana funkcja „\imp”): {\displaystyle \displaystyle \phi\imp\psi\in\Sigma} , to $\psi \in \mathrm{\Sigma }$;

1. Parser nie mógł rozpoznać (nieznana funkcja „\join”): {\displaystyle \displaystyle \phi\join\psi\in\Sigma} , gdy

$\varphi \in \mathrm{\Sigma }$ lub $\psi \in \mathrm{\Sigma }$;

1. Parser nie mógł rozpoznać (nieznana funkcja „\meet”): {\displaystyle \displaystyle \phi\meet\psi\in\Sigma} , gdy

$\varphi \in \mathrm{\Sigma }$ oraz $\psi \in \mathrm{\Sigma }$;

1. $\varphi \in \mathrm{\Sigma }$ , gdy

$\mathrm{\neg }\varphi \in ̸\mathrm{\Sigma }$;

1. Parser nie mógł rozpoznać (nieznana funkcja „\false”): {\displaystyle \displaystyle \false\not\in\Sigma} .

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

Lemat

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:

1. Dla dowolnej formuły $\psi$, je¶li $\psi \in \mathrm{\Gamma }$, to

Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\psi\in\Sigma} .

1. Dla dowolnej formuły $\psi$, je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\psi\in\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 \star$ 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

Niestandardow± struktur± Kripkego nazwiemy każd± strukturę Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN = (N,\mg N)} spełniaj±c± wszystkie warunki struktury Kripkego podane w definicjach Uzupelnic def-kripke1| oraz Uzupelnic def-kripke2| za wyj±tkiem warunku (Uzupelnic eqn-Mgdef6|). Zamiast tego warunku ż±damy, aby Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle \Mg N{\alpha\star}} było relacj± zwrotn± i przechodni±, zawierało relację Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle \Mg N{\alpha}} oraz spełniało aksjomaty (P6) i (P7). Tzn. zamiast warunku

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \displaystyle \aligned \Mg N{\alpha\star} &\eqdef& \bigcup_{n\geq 0}\Mg N{\alpha}^n, \endaligned}

ż±damy, aby dla każdego programu $\alpha$, relacja Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle \Mg N{\alpha\star}} była zwrotna, przechodnia, zawierała Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle \Mg N{\alpha}} oraz spełniała następuj±ce dwa warunki dla dowolnej formuły $\varphi$

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \displaystyle \aligned \Mg N{\bx{\alpha\star}\phi} &= \Mg N{\phi\meet\bx{\comp\alpha{\alpha\star}}\phi}\\ \Mg N{\bx{\alpha\star}\phi} &= \Mg N{\phi\meet\bx{\alpha\star}(\phi\imp\bx\alpha\phi)}. \endaligned}

Wracamy teraz do konstrukcji struktury z maksymalnych niesprzecznych zbiorów formuł. Zdefiniujemy niestandardow± strukturę Kripkego Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN = (N,\:\mg N)} następuj±co Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle N &\eqdef& \{ } maksymalne niesprzeczne zbiory formuł PDL Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \}\\ \Mg N \phi &\eqdef& \set{s}{\phi\in s}\\ \Mg N \alpha &\eqdef& \set{\<s,t\>}{ } dla wszystkich $\varphi$, je¶li $\varphi \in t$, to Parser nie mógł rozpoznać (nieznana funkcja „\d”): {\displaystyle \displaystyle \d\alpha\phi\in s\displaystyle }\\ &= \set{\<s,t\>}{ } dla wszystkich $\varphi$, je¶li Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\phi\in s} , to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \phi\in t\displaystyle }. } Z Lematu Uzupelnic lem-progmax| wynika, że obydwie definicje Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle \Mg N \alpha} s± równoważne. Dowód nastepuj±cego twierdzenia pozostawimy Czytelnikowi.

Twierdzenie

Struktura Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN} jest niestandardow± struktur± Kripkego.

Dowód

Fakt, że Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN} spełnia własno¶ci (Uzupelnic eqn-ns1|) oraz (Uzupelnic eqn-ns2|) wynika natychmiast z Lematu Uzupelnic lem-nsmaxconsis|{eqn-nsmaxconsis3a} 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 Uzupelnic filtration|).

Lemat (o filtracji dla niestandardowych struktur Kripkego)

Niech Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN} będzie niestandardow± struktur± Kripkego i niech $u,v$ będ± stanami w Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN} .

1. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\FL”): {\displaystyle \displaystyle \psi\in\FL\phi} , mamy Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg N\psi \ \Iff \ [u]\in\uMg{\frN/\FL\phi}\psi} .
2. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\bx”): {\displaystyle \displaystyle \bx\alpha\psi\in\FL\phi} zachodzi
   1. je¶li Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<u,v\>\in \Mg N\alpha} ,to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<[u],[v]\>\in \uMg{\frN/\FL\phi}\alpha} ;
   2. je¶li Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<[u],[v]\>\in \uMg{\frN/\FL\phi}\alpha} oraz Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle u\in\Mg N{\bx\alpha\psi}} , to Parser nie mógł rozpoznać (nieznana funkcja „\Mg”): {\displaystyle \displaystyle v\in\Mg N\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 Uzupelnic filtration| polega na tym, że w dowodze kroku indukcyjnego dla czę¶ci (ii) dla przypadku, gdy $\alpha$ jest programem postaci $\beta \star$ wykorzystujemy jedynie własno¶ci (Uzupelnic eqn-ns1|) oraz (Uzupelnic eqn-ns2|), zamiast (Uzupelnic eqn-stdstardef|).

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

Twierdzenie (Pełno¶ć dla PDL)

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

Dowód

Rozumujemy przez sprzeczno¶ć. Je¶li $⊬\varphi$, to $\{\mathrm{\neg }\varphi \}$ jest zbiorem niesprzecznym. Zatem, na mocy Lematu Uzupelnic lem-nsmaxconsis|{eqn-nsmaxconsis2} istnieje maksymalny nesprzeczny zbiór $u$ formuł PDL zawieraj±cy $\mathrm{\neg }\varphi$. Na mocy lematu o filtracji dla niestandardowych struktur Kripkego (Lemat Uzupelnic filtration-2|) stwierdzamy, że $\mathrm{\neg }\varphi$ jest spełniona w stanie $[u]$ skończonej struktury Parser nie mógł rozpoznać (nieznana funkcja „\frN”): {\displaystyle \displaystyle \frN/\FL\phi} . Łatwo jest zauważyć, że skończona niestandardowa struktura Kripkego jest zwykł± struktur± Kripkego (tzn. tak±, w której zachodzi (Uzupelnic eqn-stdstardef|)). Tak więc $\varphi$ nie jest tautologi±. To kończy dowód twierdzenia o pełno¶ci.