Logika dla informatyków/Logika w informatyce

Wykład 13 (link z wykł. 3)

Logika w informatyce

W tym rozdziale naszkicujemy skrótowo kilka nie wspomnianych dotychczas zagadnień logiki, które wiążą ją z informatyką. Wybór jest dość arbitralny, a opisy niezbyt wyczerpujące. Stanowią one raczej zaproszenie do dalszych, własnych poszukiwań, niż zamknięty wykład prezentowanych zagadnień.

Zdaniowe logiki trójwartościowe

Logika klasyczna, o której mowa w Wykładzie 1, jest \textit{logiką dwuwartościową}.

Pierwsze \textit{logiki trójwartościowe} skonstruowali niezależnie od siebie polski logik Jan Łukasiewicz i amerykański \begin{eqnarray*}ale\boldsymbol{s}}\def\blank{\hbox{\sf Brodzony w Augustowie\end{eqnarray*} logik i matematyk Emil Post. Motywacje Posta były raczej kombinatoryczne, natomiast Łukasiewicz swoją konstrukcję poparł głębokim wywodem filozoficznym. Argumentował między innymi, że zdania o przyszłości, typu ,,jutro pójdę do kina, nie są dzisiaj jeszcze ani prawdziwe, ani fałszywe, bo przypisanie im którejś z tych wartości zaprzeczałoby istnieniu wolnej woli. \iffalse Podobnie, przypisanie już dziś prawdy lub fałszu zdaniu ,,Obraz, który namaluję jutro będzie piękny przeczyłoby naszej zdolności do tworzenia, bo skoro już dziś można ocenić to, co stworzymy dopiero jutro, to znaczy że nie będziemy tworzyć, tylko odtwarzać coś już zdeterminowanego.

Łukasiewicz wierzył głęboko w wolną wolę i twórczość, więc\boldsymbol{s}}\def\blank{\hbox{\sf Bważał, że \fi Aby logika mogła jakoś zdać sprawę ze statusu zdań o przyszłości, musi im przypisać inną, trzecią wartość logiczną.

Trzeba tu zaznaczyć, że zupełnie inną propozycją rozwiązania tego samego problemu jest stworzona przez Brouwera logika intuicjonistyczna, którą poznaliśmy w Wykładzie #logint.

Zanim przejdziemy do części trochę bardziej formalnej, rozważmy jeszcze dwa przykłady wzięte z żywej informatyki, gdzie także naturalnie pojawia się trzecia wartość logiczna.

Przykład

Rozważmy dwie deklaracje funkcji w Pascalu:

function f(x,y:boolean):boolean;

begin

...

end;

function g(x,y:boolean):boolean;

begin

...

end;

a następnie ich\boldsymbol{s

\def\blank{\hbox{\sf Bżycie

function f(x,y:boolean):boolean;

begin

...

end;

function g(x,y:boolean):boolean;

begin

...

end;

if f(x,y) and g(x,y) then ... else ...;

Wydaje się na pierwszy rzut oka, że to sytuacja rodem z logiki klasycznej, ale nie: przecież i \verb+f+ i \verb+g+ mogą dać w wyniku obliczenia wartości \verb+true+, \verb+false+ lub się zapętlić, które to zdarzenie jest formą trzeciej wartości logicznej. Sposób, w jaki się z nią obejdzie funkcja \verb+and+ zależy od wyboru programisty: może on zastosować albo krótkie albo długie wyliczenie w swoim programie. }}

Przykład

Inna sytuacja to tabela stworzona za pomocą następującej instrukcji SQL w relacyjnej bazie danych:

function f(x,y:boolean):boolean;

begin

...

end;

function g(x,y:boolean):boolean;

begin

...

end;

if f(x,y) and g(x,y) then ... else ...;

CREATE TABLE A (

id INTEGER PRIMARY KEY auto_increment,

...

valid BOOLEAN,

...

);

Przy takiej deklaracji, tabela \verb+A+ będzie mogła w kolumnie \verb+valid+ zawierać \textit{trzy} wartości logiczne: \verb+TRUE+, \verb+FALSE+ i \verb+NULL+, a logika trójwartościowa objawi swoje działanie przy wykonaniu np.\ zapytania

function f(x,y:boolean):boolean;

begin

...

end;

function g(x,y:boolean):boolean;

begin

...

end;

if f(x,y) and g(x,y) then ... else ...;

CREATE TABLE A (

id INTEGER PRIMARY KEY auto_increment,

...

valid BOOLEAN,

...

);

SELECT *

FROM A AS A1, A AS A2

WHERE A1.valid and A2.valid

Definicja

\textit{Zbiór formuł zdaniowej logiki trójwartościowej} to zbiór tych formuł zdaniowej logiki klasycznej \begin{eqnarray*}patrz Definicja #radamalpa, w których występują tylko spójniki $\mathrm{\neg },\vee$ i $\wedge .$

Wywołane w ten sposób zawężenie składni zrekompensujemy niezwłocznie po stronie semantyki.

Przez trójwartościowanie zdaniowe\/ rozumiemy dowolną funkcję Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho:\\mbox{\small ZZ}\to\{0,\frac12,1\}} , która zmiennym zdaniowym przypisuje wartości logiczne 0, $\frac{1}{2}$ i 1.

Wartość formuły\/ zdaniowej $\alpha$ przy trójwartościowaniu $\varrho$ oznaczamy przez Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz\alpha\varrho} i określamy przez indukcję:

• Parser nie mógł rozpoznać (nieznana funkcja „\wf”): {\displaystyle \wf\prooftree p \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree=\varrho\begin{eqnarray*}p\end{eqnarray*}} , gdy $p$ jest symbolem zdaniowym;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz{\neg\alpha}\varrho=F_\lnot\begin{eqnarray*}\wfz{\alpha}\varrho\end{eqnarray*}} ;
• </math>\wf\prooftree \alpha\lor\beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*

\endprooftree=F_\land\begin{eqnarray*}\wf\prooftree \alpha \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree,

\wf\prooftree \beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\end{eqnarray*}</math>;

• </math>\wf\prooftree \alpha\land\beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree=F_\lor\begin{eqnarray*}\wf\prooftree \alpha \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree,

\wf\prooftree \beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\end{eqnarray*}</math>;

• Parser nie mógł rozpoznać (nieznana funkcja „\wf”): {\displaystyle \wf\prooftree \lnot\alpha \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree=F_\lnot\begin{eqnarray*}\wfz\alpha\varrho\end{eqnarray*}.}

}}

Różne wybory funkcji $F_{\vee },F_{\wedge }:\{0,\frac{1}{2},1\}\times \{0,\frac{1}{2},1\}\to \{0,\frac{1}{2},1\}$ i $F_{\mathrm{\neg }}:\{0,\frac{1}{2},1\}\to \{0,\frac{1}{2},1\}$ prowadzą do różnych logik trójwartościowych.

Zaczniemy od logiki najstarszej, zwanej dziś logiką Heytinga-Kleene-Łukasiewicza:

Parser nie mógł rozpoznać (nieznana funkcja „\conn”): {\displaystyle \conn{F_\land}0000\mbox{\rm\texttt<}\frac12\mbox{\rm\texttt>}\mbox{\rm\texttt<}\frac12\mbox{\rm\texttt>}\ \ \conn{F_\lor}0\mbox{\rm\texttt<}\frac12\mbox{\rm\texttt>}11\mbox{\rm\texttt<}\frac12\mbox{\rm\texttt>}1\ \ \ {\begi\prooftree array \justifies |c|c| \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hline \multicolum\prooftree 2}{|c| \justifies F_\lnot \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \\\hline\hline x&\\\hline 0&1\\\hline 1&0\\\hline{\frac12}&{\frac12}\\\hline\end{array}} }

Jest to logika niewątpliwie nadająca się do rozwiązania zadania, które sobie Łukasiewicz postawił. Sposób traktowania wartości logicznej $\frac{1}{2}$ jest taki, że należy ją rozumieć jako ,,jeszcze nie wiadomo.

Warto zauważyć, że w przypadku tej logiki zachodzą równości

• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz{\neg\alpha}\varrho=1-\wfz{\alpha}\varrho} ,
• </math>\wf\prooftree \alpha\vee\beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree=\max\{\wf\prooftree \alpha \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree,

\wf\prooftree \beta \justifies \varrho}\ \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree</math>,

• </math>\wf\prooftree \alpha\wedge\beta \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree=\min\{\wf\prooftree \alpha \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree,

\wf\prooftree \beta \justifies \varrho}\ \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree</math>,

znane z Definicji #zesiesmieli, tak więc mozna ją traktować jako literalne\boldsymbol{s}}\def\blank{\hbox{\sf Bogólnienie logiki klasycznej.

Zachowanie stałych i operacji logicznych w języku SQL rządzi się właśnie prawami logiki Heytinga-Kleene-Łukasiewicza.

Zupełnie inną logikę zaproponował Bochvar:

Parser nie mógł rozpoznać (nieznana funkcja „\conn”): {\displaystyle \conn{F_\land}0\mbox{\rm\texttt<}\frac12}0\prooftree \frac12}{\frac12 \justifies \frac12 \using \textrm{\begin{eqnarray*}W\end{eqnarray*}\mbox{\rm\texttt>}\endprooftree\ \ \ \conn{F_\lor}0\mbox{\rm\texttt<}\frac12}1\prooftree \frac12}{\frac12 \justifies \frac12 \using \textrm{\begin{eqnarray*}W\end{eqnarray*}\mbox{\rm\texttt>}\endprooftree\ \ \ {\begi\prooftree array \justifies |c|c| \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hline \multicolum\prooftree 2}{|c| \justifies F_\lnot \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \\\hline\hline x&\\\hline 0&1\\\hline 1&0\\\hline{\frac12}&{\frac12}\\\hline\end{array}} }

Czytelnik bez trudu rozpozna, że jest logika właściwa dla Przykładu #paskal, gdy programista wybierze długie wyliczenie wyrażeń logicznych. W sensie tej logiki stała $\frac{1}{2}$ oznacza awarię lub błąd.

Dalej mamy dość\Delta\vdashgzotycznie wyglądającą logikę Sobocińskiego:

Parser nie mógł rozpoznać (nieznana funkcja „\conn”): {\displaystyle \conn{F_\land}00001101\ \ \ \ \conn{F_\lor}01011101\ \ \ \ {\begi\prooftree array \justifies |c|c| \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hline \multicolum\prooftree 2}{|c| \justifies F_\lnot \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \\\hline\hline x&\\\hline 0&1\\\hline 1&0\\\hline{\frac12}&{\frac12}\\\hline\end{array}} }

Jednak i ona ma swój poważny sens. W niej stała logiczna $\frac{1}{2}$ oznacza ,,nie dotyczy lub ,,nieistotne. Wszyscy odruchowo wręcz stosujemy tę logikę przy okazji wypełniania różnych formularzy i kwestionariuszy. Odpowiadając na różne pytania sformułowane ,,tak lub nie w niektórych polach na odpowiedzi\boldsymbol{s}}\def\blank{\hbox{\sf Bmieszczamy ,,nie dotyczy a potem podpisujemy się pod dokumentem mimo ostrzeżenia ,,Świadomy/ma odpowiedzialności karnej za składanie fałszywych zeznań \dots oświadczam że wszystkie odpowiedzi w tym formularzu są zgodne ze stanem faktycznym. Po prostu stosujemy tu logikę Sobocińskiego, w której koniunkcja kilku wyrazów o wartości 1 i kilku wyrazów o wartości $\frac{1}{2}$ daje wynik 1. Na szczęście, organy kontrolne chyba też znają ten rachunek zdań i stosują go do oceny naszych zeznań\dots

Przechodząc do logik wyglądających na pierwszy rzut oka jeszcze niezwyklej, natrafiamy na logikę z nieprzemienną koniunkcją i alternatywą, która opisuje spójniki logiczne w Pascalu, wyliczane w sposób krótki:

Parser nie mógł rozpoznać (nieznana funkcja „\conn”): {\displaystyle \conn{F_\land}0000\prooftree \frac12}{\frac12 \justifies \frac12 \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\ \ \ \conn{F_\lor}0\mbox{\rm\texttt<}\frac12}11\prooftree \frac12 \justifies \frac12 \using \textrm{\begin{eqnarray*}W\end{eqnarray*}\mbox{\rm\texttt>}\endprooftree\ \ \ {\begi\prooftree array \justifies |c|c| \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hline \multicolum\prooftree 2}{|c| \justifies F_\lnot \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \\\hline\hline x&\\\hline 0&1\\\hline 1&0\\\hline{\frac12}&{\frac12}\\\hline\end{array}} }

Dla każdego z powyższych rachunków logicznych zasadne i interesujące są pytania o to czym jest tautologia, o aksjomatyzacje i systemy dowodzenia. Tak samo jest z innymi logikami wielowartościowymi, bo Czytelnik juz zapewne zauważył, że o ile jest jedna sensowna logika dwuwartościowa i kilka, wzajemnie konkurencyjnych sensownych logik trójwartościowych, to zapewne przy wzroście liczby wartości logicznych, liczba sensownych logik też rośnie. Tytułem przykładu: można sobie bez trudu wyobrazić logikę, w której chcielibyśmy mieć jednocześnie dwie różne stałe odpowiadające ,,nie wiadomo i ,,nie dotyczy. Taka logika miałaby więc co najmniej cztery wartości logiczne. Jak łatwo się domyślić, ogromnym obszarem zastosowań logik wielowartościowych jest sztuczna inteligencja i reprezentacja wiedzy.

Logika intucjonistyczna też może być w pewnych sytuacjach traktowana jako logika wielowartościowa. W tym przypadku potrzeba tych wartości nieskończenie wiele. Odpowiednio staranne spojrzenie na Definicję Twierdzenie #zwawo pozwala w nim dojrzeć właśnie opis zbioru tautologii zdaniowej logiki intucjonistycznej jako zbioru tautologii logiki nieskończeniewielo\-war\-toś\-ciowej, w której zbiór wartości logicznych to rodzina podzbiorów otwartych $\mathbb{ℝ}$. Trzeba jednak zaznaczyć, że podejście to zatraca pewne istotne intuicje.

Tw. Codda

Twierdzenie Codda łączy ze sobą świat logiki i świat relacyjnych baz danych. Zostanie ono sformułowane i dowiedzione w tym rozdziale. Orzeka ono, że logika pierwszego rzędu i algebra relacyjna, znana z wykładu baz danych, są wzajemnie na siebie przekładalne, przy założeniu dla logiki pierwszego rzędu tzw. semantyki dziedziny aktywnej.

Na potrzeby niniejszego rozważania zakładamy i\boldsymbol{s}}\def\blank{\hbox{\sf Bstalamy skończoną sygnaturę $\mathrm{\Sigma },$ złożoną wyłącznie z symboli relacji i stałych, jak to zwykle ma miejsce w bazach danych.

Definicja

{{{3}}}

Jak wiadomo, AR jest teoretycznym modelem języka zapytań do relacyjnych baz danych. Pokażemy teraz, że algebra relacyjna jest ściśle powiązana z logiką pierwszego rzędu, a we wszystkich sytuacjach naturalnych z punktu widzenia teorii baz danych, jest jej nawet równoważna.

Dla danej formuły $\alpha$ logiki pierwszego rzędu takiej, że Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv{\alpha}=\{x_{i_1},\dots x_{i_n}\}} , oraz struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA=\<A,\dots\>} określimy interpretację tej formuły w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , oznaczaną Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\\seml \alpha \semr} , jak następuje:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\\seml \alpha \semr=\{\<a_1,\dots,a_n\>\in }

Intuicyjnie, Parser nie mógł rozpoznać (nieznana funkcja „\wf”): {\displaystyle \wf\alpha} to relacja definiowana przez formułę $\alpha$ w danej strukturze.

Definicja

\textit{Aktywną dziedziną} struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nazwiemy podzbiór

Parser nie mógł rozpoznać (błąd składni): {\displaystyle ad\begin{eqnarray*}\strA\end{eqnarray*}\subseteq A} jej\boldsymbol{s

\def\blank{\hbox{\sf Bniwersum, złożony z wszystkich\Delta\vdashlementów

które są wartościami stałych z sygnatury bądź występują jako współrzędna w co najmniej jednej krotce należącej do interpretacji jakiegoś symbolu relacyjnego z sygnatury. }}

Jak łatwo zauważyć, interpretacje wszystkich wyrażeń algebry relacyjnej obliczane w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} są w istocie relacjami w dziedzinie aktywnej.

Inaczej jest w logice pierwszego rzędu:\boldsymbol{s}}\def\blank{\hbox{\sf Bżycie negacji prowadzi natychmiast do formuł, których interpretacje zawierają\Delta\vdashlementy spoza aktywnej dziedziny.

Zatem w pełnej ogólności są formuły logiki pierwszego rzędu, dla których nie istnieje wyrażenie algebry relacyjnej o tej samej interpretacji w każdej strukturze.

Jednak gdy założymy, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle A=ad\begin{eqnarray*}\strA\end{eqnarray*},} to sytuacja sie zmienia. Wyrazem tego jest poniższe twierdzenie.

Twierdzenie Codd

Dla każdego wyrażenia $E$ algebry relacyjnej istnieje taka formuła ${\alpha }_E$ logiki pierwszego rzędu, że dla każdej struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} spełniającej Parser nie mógł rozpoznać (błąd składni): {\displaystyle A=ad\begin{eqnarray*}\strA\end{eqnarray*},} zachodzi Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\\seml \alpha \semr=\\\seml E \semr.}

Dla każdej formuły $\alpha$ logiki pierwszego rzędu istnieje wyrażenie $E_{\alpha }$ algebry relacyjnej takie, że dla każdej struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} spełniającej Parser nie mógł rozpoznać (błąd składni): {\displaystyle A=ad\begin{eqnarray*}\strA\end{eqnarray*},} zachodzi Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\\seml E \semr=\\\seml \alpha \semr.}

Dowód

{{{3}}}

\def\blank{\hbox{\sf Btraty

ogólności założyć, że </math>i=n+1$.Wtedy$E_{\exists x_i\alpha;n}</math> jest zdefiniowane jako ${\pi }_{1,\dots ,n}{E}_{\alpha ;n+1}.$

We wszystkich przypadkach kroki dowodu indukcyjnego są oczywiste. }}

Twierdzenie Codda jest już w pewnym stopniu częścią folkloru w teorii baz danych. Dziś wszyscy wiedzą, że algebra relacyjna to właściwie to samo, co logika pierwszego rzędu. W związku z tym, od wielu lat na konferencjach naukowych dotyczących teorii baz danych, systematycznie prezentowane są prace, których tematem jest logika pierwszego rzędu i nikt się już temu nie dziwi ani niczego nie musi\boldsymbol{s}}\def\blank{\hbox{\sf Bzasadniać.

W szczególności badania dotyczące gier Ehrenfeuchta oraz charakteryzacji obliczeniowych logiki pierwszego rzędu \begin{eqnarray*}w duchu twierdzeń B\"uchi i Fagina\end{eqnarray*} są generalnie postrzegane jako wyniki należące do teorii baz danych.

Rozstrzygalność i nierozstrzygalność teorii

W tym rozdziale przedyskutujemy zagadnienie rozstrzygalności teorii matematycznych \begin{eqnarray*}rozumianych jako zbiorów zdań\end{eqnarray*}. Przykładem teorii nierozstrzygalnej jest arytmetyka Peano \begin{eqnarray*}Twierdzenie #przescieradlo\end{eqnarray*}. Przykład teorii rozstrzygalnej prezentujemy poniżej.

Twierdzenie

Teoria gęstych porządków liniowych które nie mają\Delta\vdashlementów maksymalnych ani minimalnych jest rozstrzygalna.

{{dowod||

Niech ${𝒜}$ będzie klasą wszystkich gęstych porządków liniowych które nie mają\Delta\vdashlementów maksymalnych ani minimalnych. Z Wniosku [[#zupa} wiemy, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle '''Th]]\begin{eqnarray*}\mathcal{A'''\end{eqnarray*}} jest zupełna. Ponadto zauważmy, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle '''Th}\begin{eqnarray*}\mathcal{A}\end{eqnarray*}=\{\alpha&nbsp;|&nbsp;\Delta\models\alpha\'''} , gdzie $\mathrm{\Delta }$ to następujący zbiór zdań: \begin{gather*} \forall x\forall y \ \begin{eqnarray*}x\leq y \land y\leq x\end{eqnarray*}\to x=y\\ \forall x\forall y \forall z\ \begin{eqnarray*}x\leq y \land y\leq z\end{eqnarray*}\to x\leq z\\ \forall x\forall y \ x\leq y \lor y\leq x\\ \forall x\exists y\ x< y\\ \forall x\exists y\ y< x\\ \forall x\forall y\ \begin{eqnarray*}x < y\end{eqnarray*}\to \begin{eqnarray*}\exists z\ x < z \land z<y\end{eqnarray*} \end{gather*} gdzie </math>x<yParser nie mógł rozpoznać (błąd składni): {\displaystyle jest oczywistym skrótem notacyjnym dla formuły } x\leq y \land x\neq y.</math>

Na mocy twierdzenia o pełności \[\{\alpha | \Delta\models\alpha\}=\{\alpha | \Delta\vdash_H\alpha\}.\] Pozostaje więc wykazać rozstrzygalność Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{\alpha&nbsp;|&nbsp;\Delta\vdash_H\alpha\}.}

Procedura rozstrzygająca jest następująca: Dla danej formuły $\alpha$ systematycznie generujemy wszystkie dowody w systemie Hilberta, poszukując wśród nich albo dowodu $\mathrm{\Delta }{⊢}_H\alpha ,$ albo dowodu $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\alpha .$ Wobec zaobserwowanej przez nas zupełności, jeden z nich w końcu się znajdzie. Jeśli będzie to ten pierwszy, to procedura\boldsymbol{s}}\def\blank{\hbox{\sf Bdzieli wówczas odpowiedzi: ,,TAK, a jeśli ten drugi, to ,,NIE. }}

Przeprowadzony przez nas dowód jest całkiem prosty, ale prowadzi do algorytmu rozstrzygającego, o którego złożoności nic rozsądnego powiedzieć nie\boldsymbol{s}}\def\blank{\hbox{\sf Bmiemy.

Istnieją bardziej zaawansowane technicznie metody dowodzenia rozstrzygalności, które pozwalają oszacować złożoność tworzonych przez nie algorytmów. Jednak można\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić, że żaden taki algorytm nie może mieć złożoności mniejszej niż {\sc Pspace}, o ile tylko działa poprawnie dla wszystkich formuł zawierających symbole równości.

Twierdzenie Stockmeyer

Następujący problem jest {\sc Pspace}-trudny: czy dane zdanie logiki pierwszego rzędu nad sygnaturą zawierającą wyłącznie symbol równości jest tautologią?

Wobec naszej wiedzy o klasach złożoności, wątpliwe jest zatem istnienie algorytmów o wielomianowej złożoności czasowej nawet dla teorii jeszcze prostszych niż ta rozpatrywana w poprzednim twierdzeniu.

Dowód

{{{3}}}

Szczególnie interesujące jest następujące twierdzenie:

Twierdzenie Tarski

Teoria\boldsymbol{s

\def\blank{\hbox{\sf Bporządkowanego ciała liczb rzeczywistych, tj. teoria struktury

\mbox{Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\RR,+,*,0,1,\leq\>} } jest rozstrzygalna. }}

Jej znaczenie dla informatyki zasadza się na fakcie, że ta teoria to w istocie znana wszystkim ze szkoły \textit{geometria analityczna}. Poważną część algorytmicznych badań w zakresie geometrii obliczeniowej można streścić jako\boldsymbol{s}}\def\blank{\hbox{\sf Blepszanie algorytmu rozstrzygającego teorię \mbox{Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\RR,+,*,0,1,\leq\>} } dla różnych szczególnych klas formuł, pojawiających się w praktyce.

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

Udowodnić, że logiki trójwartościowe Heytinga-Kleene-Łukasiewicza, Bochvara i Sobocińskiego spełniają prawa de Morgana.

Podać przykład zdania logiki pierwszego rzędu, które nie jest tautologią, ale jest prawdziwe we wszystkich strukturach Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} takich, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle A=ad\begin{eqnarray*}\strA\end{eqnarray*}.}

1. Udowodnić, że zbiór tautologii logiki pierwszego rzędu nad

sygnaturą składającą się tylko z równości jest rozstrzygalny.

{\em Wskazówka:\/} Niech $\alpha$ będzie formułą o randze kwantyfikatorowej $q$. Udowodnić, że każde dwie struktury o mocy co najmniej $q$ nad powyższą sygnaturą są $q$-elementarnie równoważne. Wywnioskować stąd, że aby sprawdzić, czy $\alpha$ jest tautologią wystarczyć sprawdzić to w strukturach o mocy co najwyżej $q.$

1. Zbadać złożoność obliczeniową algorytmu zaproponowanego powyżej

i\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić, że zbiór tautologii logiki pierwszego rzędu nad sygnaturą składającą się tylko z równości jest {\sc Pspace}-zupełny.

1. Udowodnić, że zbiór tautologii logiki pierwszego

rzędu nad sygnaturą składającą się tylko z równości i skończenie wielu symboli stałych jest rozstrzygalny.

{\em Wskazówka:\/} Rozwiązać najpierw zadanie #rJ1, a stałe zasymulować jako relacje\boldsymbol{s}}\def\blank{\hbox{\sf Bnarne będące singletonami.

\end{small}