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) $\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){)}^{*}.$

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. Dla dowolnego zbioru $X$, przez $|X|$ oznaczamy moc zbioru $X$. Następujący lemat podaje ograniczenie górne na moc domknięcia Fischera-Ladnera.

k

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