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.

TEST

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

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

a nie formuła

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

Wielu takich dwuznaczności\boldsymbol{s}}\def\blank{\hbox{\sf Bnikniemy, gdy przypomnimy sobie, że w języku polskim istnieją takie słowa jak ani\/ i żaden\/.

Język logiki pierwszego rzędu, dzięki możliwości\boldsymbol{s}}\def\blank{\hbox{\sf Bż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

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 Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A = \<A, f^\A, g^\A, R^\A, S^\A\>} , w których obraz iloczynu kartezjańskiego Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle R^\A\times S^\A} przy przekształceniu $f$ zawiera się w zwykłym iloczynie \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle R^\A\cap S^\A} }.

Przykład

{{{3}}}

Niestety, konsekwencją znacznej siły wyrazu logiki pierwszego rzędu jest jej nierozstrzygalność. Dokładniej, nierozstrzygalny jest następujący problem decyzyjny:\footnote{W istocie, nazwa ,,problem decyzyjny (Entscheidungsproblem) została\boldsymbol{s}}\def\blank{\hbox{\sf Bżyta po raz pierwszy właśnie w tym kontekście.} {\it 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 Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A} \/ można zdefiniować jako krotkę Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \M = \<\Delta, Q, \delta, q_0, q_a\>} , gdzie:

• $\mathrm{\Delta }$ jest skończonym alfabetem, zawierającym Parser nie mógł rozpoznać (nieznana funkcja „\A”): {\displaystyle \A}

oraz symbol Parser nie mógł rozpoznać (nieznana funkcja „\blank”): {\displaystyle \blank\not\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\boldsymbol{s}}\def\blank{\hbox{\sf Btoż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 ${\mathbb{ℂ}}_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ą\/.

\bigbreak Relację Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \to_\M} na konfiguracjach definiuje się tak:

• Jeśli $\delta (q,a)=(b,p,+1)$ to Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle wqav \to_\M wbpv} ;
• Jeśli $\delta (q,a)=(b,p,0)$ to Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle wqav \to_\M wpbv} ;
• Jeśli $\delta (q,a)=(b,p,-1)$ to Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle wcqav \to_\M wpcbv}

oraz Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle qav\to_\M pbv} (gdy ruch w lewo jest niemożliwy.)

Symbolem Parser nie mógł rozpoznać (nieznana funkcja „\rarrow”): {\displaystyle \rarrow_\M} oznaczamy przechodnio-zwrotne domknięcie relacji Parser nie mógł rozpoznać (nieznana funkcja „\M”): {\displaystyle \to_\M} . Jeżeli Parser nie mógł rozpoznać (nieznana funkcja „\rarrow”): {\displaystyle \C_w\rarrow_\M \C'} , gdzie ${\mathbb{ℂ}}^{\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.

\begin{lemat} \parskip=2pt 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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} zawiera nieskończony ciąg różnychelementów Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle c^\strA=a_0, a_1, a_2,\ldots} , takich że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle (a_i,a_{i+1})\in P^\strA} dla każdego $i$. \end{lemat} Dowód

{{{3}}}

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}