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. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x(\var\varphi\wedge\psi)\\leftrightarrow\forall x\var\varphi\wedge\forall x\psi} ;
4. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x(\var\varphi\vee\psi)\\leftrightarrow\exists x\var\varphi\vee\exists x\psi} ;

o ile Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;

1. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x(\var\varphi\wedge\psi)\\leftrightarrow\var\varphi\wedge\exists x\psi} ,

o ile Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;

Dowód

{{{3}}}

Formuły (#trk1)--(#trk3) powyżej wyrażają własności kwantyfikatora szczegółowego i są odpowiednikami formuł z Faktu #fakt-przyklad-taut. 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 (#trk4) i (#trk5).

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 (#trk8) i kwantyfikatora szczegółowego względem koniunkcji (#trk9) 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 (#trk8) nazywane bywa prawem Grzegorczyka.)

Formuła (#trka) jest odbiciem naszego założenia o niepustości świata. Jest to tautologia, ponieważ\boldsymbol{s}}\def\blank{\hbox{\sf Bmówiliśmy się, że rozważamy tylko struktury o niepustych nośnikach.

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

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

Definicja

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

\hfil 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

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

Dowód

{{{3}}}

Przykład

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

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

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

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

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

\hspace{6cm}$\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\boldsymbol{s}}\def\blank{\hbox{\sf Bżywamy logiki do weryfikacji poprawności stwierdzeń języka p\leftrightarrowcznego, choćby takiego jak podręcznikowy przykład: {\it,,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: \begin{center}\it 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. \end{center} 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

\hfil </math>\forall x (C(x) \wedge S(x) \to \forall y(G(x,y)\\leftrightarrow S(y)\wedge \neg G(y,y))) \models \neg \exists x (C(x) \wedge S(x)) ?</math>

Stwierdziwszy poprawność powyższego stwierdzenia, wywnioskujemy, że w Sewilli cyrulika nie ma. I będzie to wniosek\dots 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.

\subsubsection*{Implikacja materialna i związek przyczynowo-skutkowy}

Implikacja, o której mówimy w logice klasycznej to tzw. \rightarrowlikacja 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 \rightarrowlikacji ,,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:

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

Tymczasem \rightarrowlikacja materialna nie zachodzi, o czym dobrze wiedzą\boldsymbol{s}}\def\blank{\hbox{\sf Bżytkownicy terminali. Co więcej, w istocie materialną prawdą jest stwierdzenie odwrotne:

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

Natomiast zdanie

\hfil 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\footnote{W językach programowania jest podobnie, ale to już inna historia.} zdarzeń: ,,Poszedł i zrobił.'' A wyrażenie ,,A, chyba że B\/ ma inny odcień znaczeniowy niż proste {\it,,A lub B\/}. Przy tej okazji zwróćmy\boldsymbol{s}}\def\blank{\hbox{\sf Bwagę na to, że słowo ,,albo\/ bywa czasem rozumiane w znaczeniu alternatywy wykluczającej. My jednak\boldsymbol{s}}\def\blank{\hbox{\sf Bmawiamy się, że rozumiemy je tak samo jak {\it,,lub}.