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

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 [x:=s]\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{\sf Bstalono logiczną interpretację naszego zadania, zapominając o jednym z jego istotnychelementó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\leftrightarrowczny 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 ichewentualnym 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 definiowanieelementó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$, dwuargumentowego symbolu funkcyjnego $f$ i jednoargumentowego symbolu funkcyjnego $g$. 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,g^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 Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle 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

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

Dowód

{{{3}}}

\def\blank{\hbox{\sf Btworzy formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_\M} o takiej własności:

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} akceptuje słowo puste \quad \wtw, gdy\quad 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łę Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \psi_\M} , że

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} zapętla się na słowie pustym \quad \wtw, gdy\quad Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \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 Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} (bo tak jest łatwiej) chociaż tak być nie musi (Ćwiczenie #stalasygnatura). 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 #nieKronecker.

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 #nieKronecker. 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 (oelemencie $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. \Leftrightarrow te składowe:

1. Parser nie mógł rozpoznać (błąd składni): {\displaystyle S_{q_0}(c)\wedge G(c,c)\wedge \forall x\,C_{\sf 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$;

1. $\mathrm{\forall }x\mathrm{\exists }yG(x,y)$;
2. $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(G(x,y)\wedge G(x,z)\to y=z)$;
3. </math>\forall x\forall y\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))</math>, gdy $\delta (q,a)=(p,b,i)$;

1. </math>\forall x\forall y\forall z(\neg G(x,y)\wedge C_a(x,y) \wedge P(x,z)

\to C_a(z,y))</math>;

1. </math>\forall x\forall y\forall z\forall v(S_q(x)\wedge G(x,y)\wedge P(x,z)

\wedge P(y,v)\to G(z,v))</math>, gdy $\delta (q,a)=(p,b,+1)$;

1. </math>\forall x\forall y\forall z(S_q(x)\wedge G(x,y)\wedge P(x,z)

\to G(z,y))</math>, gdy $\delta (q,a)=(p,b,0)$;

1. </math>\forall x\forall y\forall z\forall v(S_q(x)\wedge G(x,y)\wedge P(x,z)

\wedge P(v,y)\to G(z,v))</math>, gdy $\delta (q,a)=(p,b,-1)$;

1. </math>\forall x\forall y\forall z\forall v(S_q(x)\wedge G(x,c)\wedge P(x,z)

\to G(z,c))</math>, gdy $\delta (q,a)=(p,b,-1)$;

1. $\mathrm{\forall }x\mathrm{\neg }{S}_{q_f}(x)$.

Przypuśćmy teraz, że maszyna Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} ma nieskończone obliczenie dla pustego słowa wejściowego. Zbudujemy model Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_\M} . Dziedziną tego modelu jest zbiór Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \NN} liczb naturalnych. Stałą $c$ interpretujemy jako zero, relacja Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle P^\strA} to relacja następnika, a Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle R^\strA} to (ostra) relacja mniejszości. Relacje Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle S_q^\A} , Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle C_a^\A} i Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle 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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , 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 „\strA”): {\displaystyle \strA\models\var\varphi_\M} dla pewnej struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} . Wtedy także Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\vartheta} , niech więc $a_i$ będąelementami Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , o których mowa w Lemacie #nieKronecker. Struktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} 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 zelementó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 jednymelementem struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} --- tu używamy składowych (4)--(7).

Rozpatrzmy obliczenie maszyny Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} dla słowa pustego. Pokażemy, że jest to obliczenie nieskończone.

Jeśli obliczenie maszyny Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} składa się z co najmniej $n$ kroków, to przez $q_n$ oznaczmy stan, w którym znajduje się maszyna Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \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ę \zwn $n$ dowodzimy, że dla dowolnego Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle n\in\NN} obliczenie składa się z co najmniej $n$ kroków, oraz:

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle a_n\in S_{q_n}^\strA} \qquad Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle (a_n,a_m)\in C_{b_{nm}}^\strA} \qquadParser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle (a_n,a_{k_n})\in G^\strA} .

Inaczej mówiąc, model Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} 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 #entscheidungsproblem można wzmocnić, pokazując (Ćwiczenie #stalasygnatura), że problem jest nierozstrzygalny nawet dla formuł nad pewną\boldsymbol{s}}\def\blank{\hbox{\sf Bstaloną sygnaturą. W istocie, jest tak dla większości sygnatur, z wyjątkiem bardzo ,,ubogich przypadków. Dwa takie przypadki są przedmiotem Ćwiczeń #rJ1 i #rJ2 do Rozdziału #trzynasty.

\subsection*{Ćwiczenia}\begin{small}

1. Stosując schematy (#trk6--#9) z Faktu #teerka,

pokazać, że następujące formuły są tautologiami:

1. 1. </math>(\exists y p(y) \to \forall z q(z)) \to

\forall y\forall z(p(y)\to q(z))</math>; %95b

1. 1. </math>(\forall x\exists y r(x,y) \to \exists x\forall y r(y,x))\to

\exists x\forall y(r(x,y) \to r(y,x))</math>; %99a

1. 1. </math>\forall x\exists y((p(x)\to q(y))\to r(y))

\to ((\forall x p(x)\to \forall y q(y))\to \exists y r(y))</math>; %109a

1. 1. </math>\forall x(p(x)\to \exists y q(y))\to

\exists y(\exists x p(x)\to q(y))</math>.% 110a

\item Jak rozumiesz następujące zdania? Jak je sformułować, żeby nie budziły wątpliwości?

1. Nie wolno pić i grać w karty.
2. Nie wolno pluć i łapać.
3. Zabrania się zaśmiecania i zanieczyszczania drogi.\footnote{Kodeks

Drogowy przed nowelizacją w roku 1997.}

1. {\it Zabrania się zaśmiecania lub zanieczyszczania

drogi.}\footnote{Kodeks Drogowy po nowelizacji w roku 1997.}

1. {\it Wpisać, gdy osoba\boldsymbol{s}}\def\blank{\hbox{\sf Bbezpieczona nie posiada numerów identyfikacyjnych

NIP lub \mbox{PESEL}.}\footnote{Instrukcja wypełniania formularza ZUS ZCZA (Zgłoszenie danych o członkach rodziny\dots)}

1. {\it Podaj przykład liczby, która jest pierwiastkiem pewnego

równania kwadratowego o współczynnikach całkowitych i takiej, która nie jest.}

1. Warunek zachodzi dla każdego $x$ i dla pewnego $y$.\/

\item Czy następujące definicje można lepiej sformułować?

1. Zbiór $A$ jest {\sf dobry}, jeśli ma co najmniej 2elementy.
2. Zbiór $A$ jest {\sf dobry, jeśli dla każdego $x\in A$,

jeśli $x$ jest parzyste, to $x$ jest podzielne przez $3$.}

1. Zbiór $A$ jest {\sf dobry, jeśli dla pewnego $x\in A$,

jeśli $x$ jest parzyste, to $x$ jest podzielne przez $3$.}

\item Wskazać błąd w rozumowaniu:

1. {\it Aby wykazać prawdziwość tezy\\

{\sf ,,Dla dowolnego $n$, jeśli zachodzi warunek $W(n)$ to zachodzi warunek $U(n)$}\\ załóżmy, że dla dowolnego $n$ zachodzi $W(n)$\dots}

1. {\it Aby wykazać prawdziwość tezy\\

{\sf ,,Dla pewnego $n$, jeśli zachodzi warunek $W(n)$ to zachodzi warunek $U(n)$}\\ załóżmy, że dla pewnego $n$ zachodzi $W(n)$\dots}

\item Sformułować poprawnie zaprzeczenia stwierdzeń:

• Liczby $m$ i $n$ są pierwsze.
• Liczby $m$ i $n$ są względnie pierwsze.

\item Czy zdanie {\it ,,Liczba $a$ nie jest kwadratem pewnej liczby całkowitej\/} jest poprawnym zaprzeczeniem zdania {\it ,,Liczba $a$ jest kwadratem pewnej liczby całkowitej\/}?

\item Sygnatura $\mathrm{\Sigma }$ składa się z symboli $r,s\in {\mathrm{\Sigma }}_1^R$, $R,S\in {\mathrm{\Sigma }}_2^R$ i $g\in {\mathrm{\Sigma }}_2^F$. Napisać takie zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi}  i $\psi$, że:%61 jest rozwiazanie

1. zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest prawdziwe dokładnie w tych modelach

Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A = \<A, R^\A, S^\A, r^\A, s^\A, g^\A\>} , w których obie relacje Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle R^\A} , Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle S^\A} są przechodnie, ale ich suma nie jest przechodnia;

1. zdanie $\psi$ jest prawdziwe dokładnie w tych modelach

Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A = \<A, R^\A, S^\A, r^\A, s^\A, g^\A\>} , w których Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle s^\A} jest obrazem iloczynu kartezjańskiego Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^\A\times r^\A} przy funkcji Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle g^\A} .

\item Sygnatura $\mathrm{\Sigma }$ składa się z dwuargumentowych symboli relacyjnych $r$ i $s$ oraz dwuargumentowego symbolu funkcyjnego $f$. Napisać (możliwie najkrótsze) zdanie, które jest prawdziwe dok{ł}adnie w tych modelach%77 jest rozwiazanie Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A = \<A, r^{\A}, s^{\A}, f^{\A}\>} , w których:

1. Złożenie relacji Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^{\A}} i Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle s^{\A}} zawiera się w ich iloczynie

Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^\A\cap s^\A} ;

1. Zbiór wartości funkcji Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle f^{\A}} jest rzutem sumy Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^\A\cup s^\A} na

pierwszą współrzędną;

1. Relacja Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^\A} nie jest funkcją z $A$ w $A$;
2. Obraz Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle r^\A} przy funkcji Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle f^\A} jest podstrukturą w Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A} ;
3. Obraz zbioru $A\times A$ przy funkcji Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle f^\A} jest pusty.

\item Dla każdej z par struktur:

1. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\NN,\leq\>} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\{m-{1\over n}\ |\ m,n\in\NN-\{0\}\}, \leq\>} ;
2. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\NN, +\>} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\ZZ, +\>} ;
3. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\NN, \leq\>} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\ZZ, \leq\>} ,

wskaż zdanie prawdziwe w jednej z nich a w drugiej nie.

\item Napisać takie zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$, że:

1. zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest prawdziwe w modelu Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A = \<\ZZ, +, 0 \>} ,

ale nie w modelu Parser nie mógł rozpoznać (nieznana funkcja „\B”): {\displaystyle \B = \<\NN, +, 0 \>} ;

1. zdanie $\psi$ jest prawdziwe w modelu Parser nie mógł rozpoznać (nieznana funkcja „\B”): {\displaystyle \B = \<\ZZ, +, 0 \>} ,

ale nie w modelu Parser nie mógł rozpoznać (błąd składni): {\displaystyle \C = \<\QQ, +, 0 \>} .

\item Wskazać formułę pierwszego rzędu:

1. spełnialną w

ciele liczb rzeczywistych ale nie w ciele liczb wymiernych;

1. spełnialną w algebrze Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \NN} z mnożeniem,

ale nie w algebrze Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \NN} z dodawaniem;

1. spełnialną w Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\{a,b\}^*,\cdot,\varepsilon\>}

ale nie w Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\{a,b,c\}^*,\cdot,\varepsilon\>} .

\item Zmodyfikować konstrukcję z dowodu Twierdzenia #entscheidungsproblem w ten sposób, aby w formule Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \psi_\M} nie występował symbol równości ani stała </math>cParser nie mógł rozpoznać (błąd składni): {\displaystyle . %%{1. Napisać } \forall x\forall y\forall z(G(x,y)\wedge \item Zmodyfikować konstrukcję z dowodu Twierdzenia #entscheidungsproblem w ten sposób, aby Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \psi_\M} była zawsze formułą\boldsymbol{s}}\def\blank{\hbox{\sf Bstalonej sygnatury (niezależnej od maszyny Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M} ). Wywnioskować stąd, że logika pierwszego rzędu nad tą\boldsymbol{s}}\def\blank{\hbox{\sf Bstaloną sygnaturą jest nierozstrzygalna.

\end{small}