Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia: Różnice pomiędzy wersjami
Linia 10: | Linia 10: | ||
#<math>\forall x(\var\varphi\to\psi)\to(\exists x\var\varphi\to\exists x\psi)</math>; | #<math>\forall x(\var\varphi\to\psi)\to(\exists x\var\varphi\to\exists x\psi)</math>; | ||
#<math>\exists x\varphi \to \varphi </math>, o ile <math> x \not\in FV(\varphi)</math>; | #<math>\exists x\varphi \to \varphi </math>, o ile <math> x \not\in FV(\varphi)</math>; | ||
#<math>\forall x( | #<math> \varphi[x:=s] \to \exists x\varphi</math>; | ||
#<math>\exists x( | #<math>\neg\forall x\varphi \leftrightarrow \exists x\neg\varphi</math>; | ||
o ile <math>x\not\in FV( | #<math>\neg\exists x\varphi \leftrightarrow \forall x\neg\varphi</math>; | ||
#<math>\exists x( | #<math>\forall x(\varphi\wedge\psi)\leftrightarrow \forall x\varphi\wedge\forall x\psi</math>; | ||
o ile <math>x\not\in FV(\ | #<math>\exists x(\varphi\vee\psi)\leftrightarrow\exists x\varphi\vee\exists x\psi</math>; | ||
#<math>\forall x(\varphi\vee\psi)\leftrightarrow \varphi\vee\forall x\psi</math>,o ile <math>x\not\in FV(\varphi)</math>; | |||
#<math>\exists x(\varphi\wedge\psi)\leftrightarrow\varphi\wedge\exists x\psi</math>, o ile <math>x\not\in FV(\varphi)</math>; | |||
#<math>\forall x\varphi\to\exists x\varphi</math>; | |||
#<math>\forall x\forall y\varphi\leftrightarrow \forall y\forall x\varphi</math>; | |||
#<math>\exists x\exists y\varphi\leftrightarrow\exists y\exists x\varphi</math>; | |||
#<math>\exists x\forall y\varphi\to \forall y\exists x\varphi</math>; | |||
}} | |||
==TEST== | ==TEST== | ||
{{dowod|| | {{dowod|| |
Wersja z 10:33, 21 wrz 2006
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 ).
- Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x(\var\varphi\to\psi)\to(\exists x\var\varphi\to\exists x\psi)} ;
- , o ile ;
- ;
- ;
- ;
- ;
- ;
- ,o ile ;
- , o ile ;
- ;
- ;
- ;
- ;
TEST
Dowód
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 i , 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 może być wolna w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i .) 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 to lub , a jest formułą otwartą. (Oczywiście 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
Przykład
Formuła jest równoważna każdej z następujących formuł:
\hspace{6cm};
\hspace{6cm};
\hspace{6cm};
\hspace{6cm};
\hspace{6cm}.
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 . 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 . W szczególności, wypowiedzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i 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 \/ 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}.