Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia

Logika pierwszego rzędu. Sposób użycia.

Przyjrzyjmy się teraz kilku ważnym tautologiom.

Fakt 3.1

Następujące formuły są tautologiami (dla dowolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$).

1. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x(\var\varphi\to\psi)\to(\exists x\var\varphi\to\exists x\psi)} ;
2. $\mathrm{\exists }x\phi \to \phi$, o ile $x\in ̸FV(\phi )$;
3. $\phi (s/x)\to \mathrm{\exists }x\phi$;
4. $\mathrm{\neg }\mathrm{\forall }x\phi \leftrightarrow \mathrm{\exists }x\mathrm{\neg }\phi$;
5. $\mathrm{\neg }\mathrm{\exists }x\phi \leftrightarrow \mathrm{\forall }x\mathrm{\neg }\phi$;
6. $\mathrm{\forall }x(\phi \wedge \psi )\leftrightarrow \mathrm{\forall }x\phi \wedge \mathrm{\forall }x\psi$;
7. $\mathrm{\exists }x(\phi \vee \psi )\leftrightarrow \mathrm{\exists }x\phi \vee \mathrm{\exists }x\psi$;
8. $\mathrm{\forall }x(\phi \vee \psi )\leftrightarrow \phi \vee \mathrm{\forall }x\psi$, o ile $x\in ̸FV(\phi )$;
9. $\mathrm{\exists }x(\phi \wedge \psi )\leftrightarrow \phi \wedge \mathrm{\exists }x\psi$, o ile $x\in ̸FV(\phi )$;
10. $\mathrm{\forall }x\phi \to \mathrm{\exists }x\phi$;
11. $\mathrm{\forall }x\mathrm{\forall }y\phi \leftrightarrow \mathrm{\forall }y\mathrm{\forall }x\phi$;
12. $\mathrm{\exists }x\mathrm{\exists }y\phi \leftrightarrow \mathrm{\exists }y\mathrm{\exists }x\phi$;
13. $\mathrm{\exists }x\mathrm{\forall }y\phi \to \mathrm{\forall }y\mathrm{\exists }x\phi$;

Dowód

Ćwiczenie.

Formuły (1-3) powyżej wyrażają własności kwantyfikatora szczegółowego i są odpowiednikami formuł z Faktu 2.7. Zauważmy, że zamiast rozdzielności kwantyfikatora szczegółowego, mamy tu jeszcze jedno prawo rozkładu kwantyfikatora ogólnego. Zakłóca to nieco symetrię pomiędzy $\mathrm{\forall }$ i $\mathrm{\exists }$, wyrażoną prawami de Morgana (4) i (4).

Kolejne dwie tautologie przypominają o bliskim związku kwantyfikatora ogólnego z koniunkcją i kwantyfikatora szczegółowego z alternatywą. (Uwaga: zmienna $x$ może być wolna w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$.) Analogiczna rozdzielność kwantyfikatora ogólnego względem alternatywy (8) i kwantyfikatora szczegółowego względem koniunkcji (9) nie zawsze jest prawdą, ale zachodzi pod warunkiem, że zmienna wiązana kwantyfikatorem nie występuje w jednym z członów formuły. (Prawo (8) nazywane bywa prawem Grzegorczyka.)

Formuła (10) jest odbiciem naszego założenia o niepustości świata. Jest to tautologia, ponieważ umówiliśmy się, że rozważamy tylko struktury o niepustych nośnikach.

Prawa (11)--(13) charakteryzują możliwości permutowania kwantyfikatorów. Implikacja odwrotna do (13) zazwyczaj nie jest tautologią.

Stosując równoważności (4--9) możemy każdą formułę sprowadzić do postaci, w której wszystkie kwantyfikatory znajdują się na początku.

Definicja 3.2

Mówimy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest w preneksowej postaci normalnej, gdy

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi = Q_1y_1Q_2y_2\ldots Q_ny_n\,\psi} ,

gdzie każde z $Q_i$ to $\mathrm{\forall }$ lub $\mathrm{\exists }$, a $\psi$ jest formułą otwartą. (Oczywiście $n$ może być zerem.)

Fakt 3.3

Dla każdej formuły pierwszego rzędu istnieje równoważna jej formuła w preneksowej postaci normalnej.

Dowód

Indukcja (ćwiczenie).

Przykład 3.3

Formuła $\mathrm{\exists }yp(y)\to \mathrm{\forall }zq(z)$ jest równoważna każdej z następujących formuł:

$\mathrm{\neg }\mathrm{\exists }yp(y)\vee \mathrm{\forall }zq(z)$;

$\mathrm{\forall }y\mathrm{\neg }p(y)\vee \mathrm{\forall }zq(z)$;

$\mathrm{\forall }y(\mathrm{\neg }p(y)\vee \mathrm{\forall }zq(z))$;

$\mathrm{\forall }y\mathrm{\forall }z(\mathrm{\neg }p(y)\vee q(z))$;

$\mathrm{\forall }y\mathrm{\forall }z(p(y)\to q(z))$.

Logika formalna i język polski

Systemy logiki formalnej są, jak już mówiliśmy, tylko pewnymi modelami, czy też przybliżeniami rzeczywistych sposobów wyrażania różnych stwierdzeń i wnioskowania o ich poprawności. Poziom dokładności takich przybliżeń może być większy lub mniejszy. Większy tam, gdzie mamy do czynienia z dobrze określoną teorią matematyczną, lub językiem programowania. Mniejszy wtedy, gdy używamy logiki do weryfikacji poprawności stwierdzeń języka potocznego, choćby takiego jak podręcznikowy przykład: Janek idzie do szkoły. Oczywiście przypisanie temu stwierdzeniu wartości logicznej jest zgoła niemożliwe, nie wiemy bowiem, który Janek do jakiej ma iść szkoły i czy może już doszedł? Więcej sensu ma zastosowanie logiki predykatów do analizy np. takiego rozumowania:

Każdy cyrulik sewilski goli tych wszystkich mężczyzn w Sewilli, którzy się sami nie golą.

Ale nie goli żadnego z tych, którzy golą się sami.

A zatem w Sewilli nie ma ani jednego cyrulika.

W tym przypadku aparat logiki formalnej może być pomocny. Łatwiej zrozumieć o co chodzi, tłumacząc nasz problem na język logiki predykatów, i przedstawiając go jako pytanie o poprawność pewnego stwierdzenia postaci Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma \models\var\varphi} . Można więc zapytać, czy

$\mathrm{\forall }x(C(x)\wedge S(x)\to \mathrm{\forall }y(G(x,y)\leftrightarrow S(y)\wedge \mathrm{\neg }G(y,y)))\models \mathrm{\neg }\mathrm{\exists }x(C(x)\wedge S(x))?$

Stwierdziwszy poprawność powyższego stwierdzenia, wywnioskujemy, że w Sewilli cyrulika nie ma. I będzie to wniosek ... błędny, bo cyrulik być może jest kobietą.

W powyższym przykładzie po prostu źle\boldsymbol{s}}\def\blank{\hbox\mathsf{ B ustalono logiczną interpretację naszego zadania, zapominając o jednym z jego istotnych elementów. Błąd ten można łatwo naprawić, co jest zalecane jako ćwiczenie. Ale nie zawsze język logiki formalnej wyraża ściśle to samo, co p\leftrightarrow potoczny język polski, a nawet język w którym pisane są prace matematyczne. Zarówno składnia jak i semantyka tych języków rządzi się zupełnie innymi prawami, i o tym należy pamiętać tłumacząc jeden na drugi.

Implikacja materialna i związek przyczynowo-skutkowy

Implikacja, o której mówimy w logice klasycznej, to tzw. implikacja materialna. Wartość logiczna, którą przypisujemy wyrażeniu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi \to\psi} zależy wyłącznie od wartości logicznych przypisanych jego częściom składowym Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$. Nie zależy natomiast zupełnie od treści tych wyrażeń, czy też jakichkolwiek innych związków pomiędzy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$. W szczególności, wypowiedzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$ mogą mówić o zajściu jakichś zdarzeń i wtedy wartość logiczna implikacji Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\psi} nie ma nic wspólnego z ich ewentualnym następstwem w czasie, lub też z tym, że jedno z tych zdarzeń spowodowało drugie. W języku polskim stwierdzenie "jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} to $\psi$" oczywiście sugeruje taki związek, np. w zdaniu:

Jeśli zasilanie jest włączone, to terminal działa.

Tymczasem implikacja materialna nie zachodzi, o czym dobrze wiedzą użytkownicy terminali. Co więcej, w istocie materialną prawdą jest stwierdzenie odwrotne:

Jeśli terminal działa, to zasilanie jest włączone.

Natomiast zdanie

Terminal działa, ponieważ zasilanie jest włączone,

stwierdza nie tylko związek przyczynowo-skutkowy, ale też faktyczne zajście wymienionych zdarzeń i w ogóle nie ma odpowiednika w logice klasycznej.

Inne spójniki w mniejszym stopniu grożą podobnymi nieporozumieniami. Ale na przykład spójnik "i"" w języku polskim może też sugerować następstwo czasowe <ref name="szesc">W językach programowania jest podobnie, ale to już inna historia.</ref> zdarzeń: "Poszedł i zrobił." A wyrażenie "A, chyba że B" ma inny odcień znaczeniowy niż proste "A lub B". Przy tej okazji zwróćmy uwagę na to, że słowo "albo" bywa czasem rozumiane w znaczeniu alternatywy wykluczającej. My jednak umawiamy się, że rozumiemy je tak samo jak "lub".

Konfuzje składniowe

Przy tłumaczeniu z języka polskiego na język logiki formalnej i na odwrót można łatwo popełnić błąd nawet wtedy, gdy nie powstają problemy semantyczne. Składnia tych języków jest oparta na innych zasadach. Na przykład te dwa zdania mają bardzo podobną budowę:

Każdy kot ma wąsy.
Pewien kot ma wąsy.

Ale ich tłumaczenia na język rachunku predykatów nie są już takie podobne:

$\mathrm{\forall }x(Kot(x)\to$MaWąsy$(x))$;

$\mathrm{\exists }x(Kot(x)\wedge$MaWąsy$(x))$.

Dość częstym błędem jest właśnie mylenie koniunkcji z implikacją w zasięgu działania kwantyfikatora. A oto inny przykład: Zdania

Liczba $n$ jest parzysta; Liczba $n$ jest dwukrotnością pewnej liczby

oznaczają to samo. Zaprzeczeniem pierwszego z nich jest oczywiście zdanie

Liczba $n$ nie jest parzysta,

ale zaprzeczeniem drugiego nie jest zdanie

Liczba $n$ nie jest dwukrotnością pewnej liczby,

otrzymane przecież przez analogiczną operację "podstawienia". Użycie słowa "pewnej" powoduje bowiem, że to zdanie rozumiemy jako $\mathrm{\exists }x(\mathrm{\neg }n=2x)$, a nie jako $\mathrm{\neg }\mathrm{\exists }x(n=2x)$.

Innym popularnym błędem jest mylenie koniunkcji z alternatywą w przesłance implikacji, zwłaszcza gdy występuje tam negacja. Mamy bowiem skłonność do powtarzania słowa "nie" w obu członach założenia i nie razi nas zdanie

Kto nie ma biletu lub nie jest pracownikiem teatru, ten nie wejdzie na przedstawienie.

Ale od tekstu matematycznego oczekujemy więcej ścisłości i w takim tekście zdanie:

Jeśli $x$ nie jest równe $2$ lub nie jest równe 3 to $x^2-5x+6$ nie jest zerem.

może wprowadzić czytelnika w błąd. ""Dosłowne" tłumaczenie tego zdania na język logiki predykatów, to przecież formuła

$\mathrm{\neg }(x=2)\vee \mathrm{\neg }(x=3)\to \mathrm{\neg }(x^2-5x+6=0)$,

a nie formuła

$\mathrm{\neg }(x=2\vee x=3)\to \mathrm{\neg }(x^2-5x+6=0)$.

Wielu takich dwuznaczności unikniemy, gdy przypomnimy sobie, że w języku polskim istnieją takie słowa jak ani i żaden.

Siła wyrazu logiki pierwszego rzędu

Język logiki pierwszego rzędu, dzięki możliwości używania kwantyfikatorów, jest dość elastyczny. Można z jego pomocą wyrazić wiele nietrywialnych własności obiektów matematycznych. W szczególności interesować nas może definiowanie elementów i wyodrębnianie struktur o pewnych szczególnych własnościach, czy też formułowanie kryteriów odróżniających jakieś struktury od innych.

Przykład 3.5

Przypuśćmy, że sygnatura składa się z dwóch jednoargumentowych symboli relacyjnych $R$ i $S$, i dwuargumentowego symbolu funkcyjnego $f$. Wtedy formuła

$\mathrm{\forall }x\mathrm{\forall }y(R(x)\wedge S(y)\to R(f(x,y))\wedge S(f(x,y))$

jest prawdziwa dokładnie w tych modelach $A=<A,f^A,R^A,S^A>$, w których obraz iloczynu kartezjańskiego $R^A\times S^A$ przy przekształceniu $f$ zawiera się w zwykłym iloczynie $R^A\cap S^A$

Przykład 3.6

Teraz niech nasza sygnatura składa się z jednej operacji dwuargumentowej $\cdot$ i z jednej stałej $\epsilon$. Zdanie

$\mathrm{\exists }{x}_1\mathrm{\exists }{x}_2\mathrm{\forall }y(\mathrm{\forall }{z}_1\mathrm{\forall }{z}_2(y=z_1\cdot z_2\to y=z_1\vee y=z_2)\to y=x_1\vee y=x_2\vee y=\epsilon )$

jest prawdziwe w strukturze $<\{a,b{\}}^{*},\cdot ,\epsilon >$ słów nad alfabetem $\{a,b{\}}^{*}$ z konkatenacją i słowem pustym, ale nie w modelu słów nad alfabetem trzyliterowym $<{a,b,c}^{*},\cdot ,\epsilon >$. Inaczej mówiąc, nasze zdanie rozróżnia te dwie struktury.

Nierozstrzygalność

Niestety, konsekwencją znacznej siły wyrazu logiki pierwszego rzędu jest jej nierozstrzygalność. Dokładniej, nierozstrzygalny jest następujący problem decyzyjny:<ref name="siedem">W istocie, nazwa 'problem decyzyjny" (Entscheidungsproblem) została użyta po raz pierwszy właśnie w tym kontekście.</ref>Czy dana formuła logiki pierwszego rzędu jest tautologią? Aby wykazać, że tak jest, posłużymy się znaną nam nierozstrzygalnością problemu stopu dla maszyn Turinga.

Przypomnijmy, że (deterministyczną, jednotaśmową) maszynę Turinga nad alfabetem $A$ można zdefiniować jako krotkę $M=<\mathrm{\Delta },Q,\delta ,q_0,q_a>$, gdzie:

• $\mathrm{\Delta }$ jest skończonym alfabetem, zawierającym $A$ oraz symbol $B\in ̸A$ (blank);
• $Q$ jest skończonym zbiorem stanów;
• $q_0\in Q$ jest stanem początkowym;
• $q_f\in Q$ jest stanem końcowym lub akceptującym;
• $\delta :(Q-\{q_f\})\times \mathrm{\Delta }\to \mathrm{\Delta }\times Q\times \{-1,0,+1\}$jest funkcją przejścia.

Zakładając, że zbiory $\mathrm{\Delta }$ i $Q$ są rozłączne, można zdefiniować konfigurację maszyny jako słowo postaci $wqv$, gdzie $q\in Q$ oraz $w,v\in {\mathrm{\Delta }}^{*}$, przy czym utożsamiamy konfiguracje $wqv$ i Parser nie mógł rozpoznać (nieznana funkcja „\blank”): {\displaystyle wqv\blank} . Interpretacja tej definicji jest następująca. Taśma maszyny jest nieskończona w prawo. Na początku taśmy zapisane jest słowo $wv$, dalej w prawo są same blanki, a głowica maszyny "patrzy" na pierwszy znak na prawo od $w$. Konfigurację postaci $C_w=q_{0}w$, gdzie $w\in A^{*}$, nazywamy początkową, a konfigurację postaci $w{q}_{f}v$ nazywamy końcową lub akceptującą.

Relację ${\to }_M$ na konfiguracjach definiuje się tak:

• Jeśli $\delta (q,a)=(b,p,+1)$, to $wqav{\to }_{M}wbpv$;
• Jeśli $\delta (q,a)=(b,p,0)$, to $wqav{\to }_{M}wpbv$;
• Jeśli $\delta (q,a)=(b,p,-1)$, to $wcqav{\to }_{M}wpcbv$ oraz $qav{\to }_{M}pbv$ (gdy ruch w lewo jest niemożliwy.)

Symbolem ${\Rightarrow }_M$ oznaczamy przechodnio-zwrotne domknięcie relacji ${\to }_M$. Jeżeli $C_w{\Rightarrow }_M{C}^{\prime }$, gdzie $C^{\prime }$ jest konfiguracją akceptującą to mówimy, że maszyna akceptuje słowo $w$.

W naszej konstrukcji skorzystamy z następującej postaci problemu stopu: Czy dana maszyna Turinga akceptuje słowo puste? Nietrudno jest zredukować do niego ogólny przypadek problemu stopu (ćwiczenie).

Następujący lemat będzie przydatny w dowodzie nierozstrzygalności.

Lemat 3.7

Niech $\vartheta$ oznacza koniunkcję następujących formuł

• $\mathrm{\forall }y\mathrm{\neg }P(y,c)$
• $\mathrm{\forall }x\mathrm{\exists }yP(x,y)$
• $\mathrm{\forall }x\mathrm{\forall }y(P(x,y)\to R(x,y))$
• $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(R(x,y)\to (R(y,z)\to R(x,z)))$
• $\mathrm{\forall }x\mathrm{\neg }R(x,x)$

Zdanie $\vartheta$ jest spełnialne, a każdy jego model $\mathfrak{𝔄}$ zawiera nieskończony ciąg różnych elementów $c^{\mathfrak{𝔄}}=a_0,a_1,a_2,\dots$, takich że $(a_i,a_{i+1})\in P^{\mathfrak{𝔄}}$ dla każdego $i$.

Dowód

Ćwiczenie.

Twierdzenie 3.8

Nie istnieje algorytm rozstrzygający, czy dana formuła logiki pierwszego rzędu jest tautologią.

Dowód

Naszym celem jest efektywna konstrukcja, która dla dowolnej maszyny Turinga $M$ utworzy formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_\M} o takiej własności:

$M$akceptuje słowo puste wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M} jest tautologią.

Stąd natychmiast wynika teza twierdzenia. W przeciwnym razie taka konstrukcja pozwalałaby bowiem na rozstrzyganie problemu stopu.

W istocie, wygodniej będzie skonstruować taką formułę ${\psi }_M$, że

$M$ zapętla się na słowie pustym wtedy i tylko wtedy, gdy ${\psi }_M$ jest spełnialna,

i na koniec przyjąć Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M=\neg \psi_M} . Sygnatura naszej formuły będzie zależała od maszyny $M$ (bo tak jest łatwiej) chociaż tak być nie musi (Ćwiczenie 13). Składa się ona z:

• jednoargumentowych symboli relacyjnych $S_q$, dla wszystkich stanów $q\in Q$;
• dwuargumentowych symboli relacyjnych $C_a$, dla wszystkich symboli $a\in \mathrm{\Delta }$;
• dwuargumentowego symbolu relacyjnego $G$;
• stałej $c$ i symboli $P$ i $Q$ występujących w formule $\vartheta$ z Lematu 3.7.

Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\M} jest koniunkcją złożoną z wielu składowych, które teraz opiszemy. Pierwszą składową jest formuła $\vartheta$ z Lematu 3.7. Każdy model tej formuły zawiera różnowartościowy ciąg $a_0,a_1,a_2,\dots$, który posłuży nam jako substytut ciągu liczb naturalnych (o elemencie $a_i$ myślimy jak o liczbie $i$). Intuicyjny sens formuł atomowych naszej sygnatury jest taki:

• Formułę $S_q(x)$ czytamy: po $x$ krokach obliczenia maszyna jest w stanie $q$.
• Formułę $G(x,y)$ czytamy: po $x$ krokach głowica maszyny znajduje się w pozycji $y$.
• Formułę $C_a(x,y)$ czytamy: po $x$ krokach na pozycji $y$ znajduje się symbol $a$.

Dalsze składowe naszej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M} są tak dobrane, aby każdy jej model reprezentował nieskończone obliczenie maszyny zaczynające się od słowa pustego. Oto te składowe:

1. $S_{q_0}(c)\wedge G(c,c)\wedge \mathrm{\forall }x{C}_{\mathsf{B}}(c,x)$;
2. $\mathrm{\forall }x(\underset{q\in Q}{\bigvee }{S}_q(x))$;
3. $\mathrm{\forall }x(S_q(x)\to \mathrm{\neg }{S}_p(x))$, dla $q,p\in Q$, $q\ne p$;
4. $\mathrm{\forall }x\mathrm{\forall }y(\underset{a\in \mathrm{\Delta }}{\bigvee }{C}_a(x,y))$;
5. $\mathrm{\forall }x\mathrm{\forall }y(C_a(x,y)\to \mathrm{\neg }{C}_b(x,y))$, dla $a,b\in \mathrm{\Delta }$,$a\ne b$;
6. $\mathrm{\forall }x\mathrm{\exists }yG(x,y)$;
7. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(G(x,y)\wedge G(x,z)\to y=z)$;
8. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(S_q(x)\wedge G(x,y)\wedge C_a(x,y)\wedge P(x,z)\to S_p(z)\wedge C_b(z,y))$, gdy $\delta (q,a)=(p,b,i)$;
9. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(\mathrm{\neg }G(x,y)\wedge C_a(x,y)\wedge P(x,z)\to C_a(z,y))$;
10. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z\mathrm{\forall }v(S_q(x)\wedge G(x,y)\wedge P(x,z)\wedge P(y,v)\to G(z,v))$, gdy $\delta (q,a)=(p,b,+1)$;
11. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(S_q(x)\wedge G(x,y)\wedge P(x,z)\to G(z,y))$, gdy $\delta (q,a)=(p,b,0)$;
12. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z\mathrm{\forall }v(S_q(x)\wedge G(x,y)\wedge P(x,z)\wedge P(v,y)\to G(z,v))$, gdy $\delta (q,a)=(p,b,-1)$;
13. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z\mathrm{\forall }v(S_q(x)\wedge G(x,c)\wedge P(x,z)\to G(z,c))$, gdy $\delta (q,a)=(p,b,-1)$;
14. $\mathrm{\forall }x\mathrm{\neg }{S}_{q_f}(x)$.

Przypuśćmy teraz, że maszyna $M$ ma nieskończone obliczenie dla pustego słowa wejściowego. Zbudujemy model $\mathfrak{𝔄}$ dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M} . Dziedziną tego modelu jest zbiór $\mathbb{\mathbb{N}}$ liczb naturalnych. Stałą $c$ interpretujemy jako zero, relacja $P^{\mathfrak{𝔄}}$ to relacja następnika, a $R^{\mathfrak{𝔄}}$ to (ostra) relacja mniejszości. Relacje $S_q^A$, $C_a^A$ i $G^A$ określamy zgodnie z ich intuicyjną interpretacją na podstawie przebiegu nieskończonego obliczenia maszyny. Nietrudno się przekonać, że wszystkie człony koniunkcji są prawdziwe w $\mathfrak{𝔄}$, czyli zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M} jest spełnialne.

Przystąpmy więc do trudniejszej części dowodu. Załóżmy mianowicie, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi_M} dla pewnej struktury $\mathfrak{𝔄}$. Wtedy także $\mathfrak{𝔄}\models \vartheta$, niech więc $a_i$ będą elementami $\mathfrak{𝔄}$, o których mowa w Lemacie 3.7. Struktura $\mathfrak{𝔄}$ spełnia też wszystkie pozostałe składowe formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_M} . Składowe (2) i (3) gwarantują, że każdy z elementów $a_i$ należy do dokładnie jednej z relacji $S_q$. Podobnie, każda para $(a_i,a_j)$ należy do dokładnie jednej z relacji $C_a$, oraz każde $a_i$ jest w relacji $G$ z dokładnie jednym elementem struktury $\mathfrak{𝔄}$ --- tu używamy składowych (4)--(7).

Rozpatrzmy obliczenie maszyny $M$ dla słowa pustego. Pokażemy, że jest to obliczenie nieskończone.

Jeśli obliczenie maszyny $M$ składa się z co najmniej $n$ kroków, to przez $q_n$ oznaczmy stan, w którym znajduje się maszyna $M$ po wykonaniu tych $n$ kroków, a przez $k_n$ pozycję głowicy w tym momencie. Zawartością $m$-tej komórki taśmy po $n$-tym kroku obliczenia niech zaś będzie symbol $b_{nm}$.

Przez indukcję ze względu na $n$ dowodzimy, że dla dowolnego $n\in \mathbb{\mathbb{N}}$ obliczenie składa się z co najmniej $n$ kroków, oraz:

$a_n\in S_{q_n}^{\mathfrak{𝔄}}$ $(a_n,a_m)\in C_{b_{nm}}^{\mathfrak{𝔄}}$$(a_n,a_{k_n})\in G^{\mathfrak{𝔄}}$.

Inaczej mówiąc, model $\mathfrak{𝔄}$ prawidłowo reprezentuje kolejne konfiguracje maszyny. Dla $n=0$ powyższe związki wynikają wprost z prawdziwości członu (1) naszej koniunkcji. W kroku indukcyjnym skorzystamy przede wszystkim z członu (14), który gwarantuje, że stan $q_n$ nie jest końcowy. Określona jest więc wartość funkcji przejścia $\delta (q_n,b_{m{k}_n})$. Możemy więc odwołać się do składowych (9--12), które zapewniają poprawną zmianę stanu i symbolu pod głowicą (8), zachowanie bez zmian reszty taśmy (9) i przesunięcie głowicy (10--12). Szczegóły dowodu pozostawiamy Czytelnikowi.

Twierdzenie 3.8 można wzmocnić, pokazując (Ćwiczenie 13), że problem jest nierozstrzygalny nawet dla formuł nad pewną ustaloną sygnaturą. W istocie, jest tak dla większości sygnatur, z wyjątkiem bardzo "ubogich" przypadków. Dwa takie przypadki są przedmiotem Ćwiczeń 2 i 5 do Logika dla informatyków/Logika w informatyce.

Przypisy

<references/>