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 logiką dwuwartościową.

Pierwsze logiki trójwartościowe skonstruowali niezależnie od siebie polski logik Jan Łukasiewicz i amerykański (ale urodzony w Augustowie) 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. 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 11.

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 13.1

Rozważmy dwie deklaracje funkcji w Pascalu:

 CREATE TABLE A   (
 id               INTEGER PRIMARY KEY auto_increment,
     ...
 valid            BOOLEAN,
     ... 
 );

Przy takiej deklaracji, tabela Parser nie mógł rozpoznać (nieznana funkcja „\verb”): {\displaystyle \verb+A+} będzie mogła w kolumnie Parser nie mógł rozpoznać (nieznana funkcja „\verb”): {\displaystyle \verb+valid+} zawierać trzy wartości logiczne: Parser nie mógł rozpoznać (nieznana funkcja „\verb”): {\displaystyle \verb+TRUE+} , Parser nie mógł rozpoznać (nieznana funkcja „\verb”): {\displaystyle \verb+FALSE+} i Parser nie mógł rozpoznać (nieznana funkcja „\verb”): {\displaystyle \verb+NULL+} , a logika trójwartościowa objawi swoje działanie przy wykonaniu np. zapytania

 SELECT *
 FROM A AS A1, A AS A2
 WHERE A1.valid and A2.valid

Definicja 13.3

Zbiór formuł zdaniowej logiki trójwartościowej to zbiór tych formuł zdaniowej logiki klasycznej (patrz Definicja 1.1), 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ć (nieznana funkcja „\small”): {\displaystyle \varrho:\small ZZ\to\{0,\frac12,1\}} , która zmiennym zdaniowym przypisuje wartości logiczne 0, $\frac{1}{2}$ 1.

Wartość formuły zdaniowej $\alpha$ przy trójwartościowaniu $\varrho$ oznaczamy przez $[[\alpha ]{]}_{\varrho }$ i określamy przez indukcję:

• Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle [[\prooftree p]]_\varrho =\varrho(p)} , gdy $p$ jest symbolem zdaniowym;

• $[[\alpha \vee \beta ]{]}_{\varrho }=F_{\wedge }([[\alpha ]{]}_{\varrho },[[\beta ]{]}_{\varrho })$;

• $[[\alpha \wedge \beta ]{]}_{\varrho }=F_{\vee }([[\alpha ]{]}_{\varrho },[[\beta ]{]}_{\varrho })$;

• $[[\mathrm{\neg }\alpha ]{]}_{\varrho }=F_{\mathrm{\neg }}([[\alpha ]{]}_{\varrho })$.

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:

$F_{\wedge }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   0   0 0   1   $\frac{1}{2}$ 0   $\frac{1}{2}$   $\frac{1}{2}$

$F_{\vee }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   1   $\frac{1}{2}$ 1   1   1 $\frac{1}{2}$   1   $\frac{1}{2}$

$F_{\mathrm{\neg }}$  $x$      0 1 $\frac{1}{2}$ 1 0 $\frac{1}{2}$

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

• $[[\mathrm{\neg }\alpha ]{]}_{\varrho }=1-[[\alpha ]{]}_{\varrho }$,

• $[[\alpha \vee \beta ]{]}_{\varrho }=\max \{[[\alpha ]{]}_{\varrho },[[\beta ]{]}_{\varrho }\}$,

• $[[\alpha \wedge \beta ]{]}_{\varrho }=\min \{[[\alpha ]{]}_{\varrho },[[\beta ]{]}_{\varrho }\}$,

znane z Definicji 1.2, tak więc mozna ją traktować jako literalne uogó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:

$F_{\wedge }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   0   $\frac{1}{2}$ 0   1   $\frac{1}{2}$ $\frac{1}{2}$   $\frac{1}{2}$   $\frac{1}{2}$

$F_{\vee }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   1   $\frac{1}{2}$ 1   1   $\frac{1}{2}$ $\frac{1}{2}$   $\frac{1}{2}$   $\frac{1}{2}$

$F_{\mathrm{\neg }}$  $x$      0 1 $\frac{1}{2}$ 1 0 $\frac{1}{2}$

Czytelnik bez trudu rozpozna, że jest logika właściwa dla Przykładu 13.1, 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ść egzotycznie wyglądającą logikę Sobocińskiego:

$F_{\wedge }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   0   0 0   1   1 0   1   $\frac{1}{2}$

$F_{\vee }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   1   0 1   1   1 0   1   $\frac{1}{2}$

$F_{\mathrm{\neg }}$  $x$      0 1 $\frac{1}{2}$ 1 0 $\frac{1}{2}$

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 pytania sformułowane "tak lub nie" w niektórych polach na odpowiedzi umieszczamy "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:

$F_{\wedge }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   0   0 0   1   $\frac{1}{2}$ $\frac{1}{2}$   $\frac{1}{2}$   $\frac{1}{2}$

$F_{\vee }(x,y)$ $x$ \ $y$ 0   1   $\frac{1}{2}$ 0 1 $\frac{1}{2}$ 0   1   $\frac{1}{2}$ 1   1   1 $\frac{1}{2}$   $\frac{1}{2}$   $\frac{1}{2}$

$F_{\mathrm{\neg }}$  $x$      0 1 $\frac{1}{2}$ 1 0 $\frac{1}{2}$

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 przy wzroście liczby wartości logicznych, liczba sensownych logik musi rosnąć. 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 Twierdzenie 11.5 pozwala w nim dojrzeć właśnie opis zbioru tautologii zdaniowej logiki intucjonistycznej jako zbioru tautologii logiki nieskończeniewielowartoś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 iustalamy 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 13.4

Tytułem przypomnienia (Czytelnik powinien znać algebrę relacyjną z wykładu baz danych)i dla ustalenia notacji, definiujemy składnię algebry relacyjnej AR nad $\mathrm{\Sigma }$.

• Każdy symbol relacji $n$-argumentowej z $\mathrm{\Sigma }$ z wyjątkiem równości jest $n$-argumentowym wyrażeniem AR.

• Jeśli $E$ i $F$ są $n$-argumentowymi wyrażeniami AR, to $E\cup F,E-F$ też są $n$-argumentowymi wyrażeniami AR.

• Jeśli $E$ i $F$ są $n$-argumentowymi wyrażeniami AR, to $E\cup F,E-F$ też są $n$-argumentowymi wyrażeniami AR.

• Jeśli $E$ jest $n$-argumentowym wyrażeniem AR oraz $i_1,\dots ,i_k$ jest ciągiem różnych ale niekoniecznie wszystkich elementów zbioru $\{1,\dots ,n\}$, to ${\pi }_{i_1,\dots ,i_k}E$ jest $k$-argumentowym wyrażeniem AR. W szczególności ciąg ten może być pusty, zaś $\pi E$ jest wyrażeniem $\text{0-argumentowym}$.

• Jeśli $E$ jest $n$-argumentowym, zaś $F$ jest $m$-argumentowym wyrażeniem AR, to $E\times F$ jest $n+m$-argumentowym wyrażeniem AR.

• Jeśli $E$ jest $n$-argumentowym wyrażeniem AR oraz $\theta$ jest zbiorem równości postaci '$i=j$' lub '$i=c$', gdzie $i,j\in \{1,\dots ,n\}$ zaś $c$ zależy do zbioru symboli stałych z sygnatury $\mathrm{\Sigma }$, to ${\sigma }_{\theta }E$ jest $n$-argumentowym wyrażeniem AR.

Semantyka algebry relacyjnej jest następująca: dla danej struktury $\mathfrak{𝔄}$ nad $\mathrm{\Sigma }$, każdemu $n$-argumentowemu wyrażeniu $E$ algebry relacyjnej przypisujemy $n$-argumentową relację $[[E]]$ w $A$.

Definicja oczywiście przebiega indukcyjnie względem budowy $E$.

• Jeśli $R$ należy do $\mathrm{\Sigma }$, to $[[R]]=R^{\mathfrak{𝔄}}$.

• Parser nie mógł rozpoznać (nieznana funkcja „\cupF”): {\displaystyle [[E\cupF]]=[[E]]\cup[[F]]} oraz $[[E-F]]=[[E]]-[[F]]$.

• $[[{\pi }_{i_1,\dots ,i_k}E]]=\{<a_{i_1},\dots ,a_{i_k}>|<a_1,\dots ,a_k>\in [[E]]\}$.

• $[[E\times F]]=[[E]]\times [[F]]=\{<a_1,\dots ,a_n,b_1\dots ,b_m>|<a_1,\dots ,a_n>\in [[E]]i<b_1\dots ,b_m>\in [[F]]\}$.

• $[[{\sigma }_{\theta }E]]=\{<a_1,\dots ,a_n>\in [[E]]|a_i=a_j,\text{gdy}(i=j)\in \theta \text{oraz}{a}_i=c^{\mathfrak{𝔄}},\text{gdy}(i=c)\in \theta \}$.

Warto zauważyć, że $[[\pi E]]=\{<>\}$ czyli jest zbiorem złożonym z ciągu pustego, gdy $[[E]]$ jest niepusty, oraz jest pusty w przeciwnym wypadku. Z kolei $[[{\sigma }_{\mathrm{\varnothing }}E]]=[[E]]$

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 $FV(\alpha )=\{x_{i_1},\dots x_{i_n}\}$, oraz struktury $\mathfrak{𝔄}=<A,\dots >$ określimy interpretację tej formuły w $\mathfrak{𝔄}$, oznaczaną $[[\alpha ]]$, jak następuje:

$[[\alpha ]]=\{<a_1,\dots ,a_n>\in A^n|(\mathfrak{𝔄},x_i{}_1:a_1,\dots ,x_i{}_n:a_n)\models \alpha \}$

Intuicyjnie, $[[\alpha ]]$ to relacja definiowana przez formułę $\alpha$ w danej strukturze.

Definicja 13.5

Aktywną dziedziną struktury $\mathfrak{𝔄}$ nazwiemy podzbiór $ad(\mathfrak{𝔄})\subseteq A$ jej uniwersum, złożony z wszystkich elementó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 $\mathfrak{𝔄}$ są w istocie relacjami w dziedzinie aktywnej.

Inaczej jest w logice pierwszego rzędu: użycie negacji prowadzi natychmiast do formuł, których interpretacje zawierająelementy 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 $A=ad(\mathfrak{𝔄})$, to sytuacja sie zmienia. Wyrazem tego jest poniższe twierdzenie.

Twierdzenie 13.6 (Codd)

1. Dla każdego wyrażenia $E$ algebry relacyjnej istnieje taka formuła ${\alpha }_E$ logiki pierwszego rzędu, że dla każdej struktury $\mathfrak{𝔄}$ spełniającej $A=ad(\mathfrak{𝔄})$, zachodzi $[[\alpha ]]=[[E]]$.
2. Dla każdej formuły $\alpha$ logiki pierwszego rzędu istnieje wyrażenie $E_{\alpha }$ algebry relacyjnej takie, że dla każdej struktury $\mathfrak{𝔄}$ spełniającej $A=ad(\mathfrak{𝔄})$, zachodzi $[[E]]=[[\alpha ]]$.

Dowód

Obu części twierdzenia będziemy dowodzić przez indukcję ze względu na budowę: w pierwszym punkcie wyrażenia $E$, a w drugim formuły $\alpha$.

Przy konstrukcji ${\alpha }_E$ będziemy dbać o to, żeby $FV{\alpha }_E=\{x_1,\dots ,x_n\}$, gdzie $n$ to liczba argumentów $E$.

Gdy $E$ jest $n$-argumentowym symbolem relacyjnym $R$, to ${\alpha }_E$ ma postać $R(x_1,\dots ,x_n)$, a prawdziwość tezy jest oczywista.

${\alpha }_{E\cup F}$ definiujemy jako ${\alpha }_E\vee {\alpha }_F$, zaś ${\alpha }_{E-F}$ jako ${\alpha }_E\wedge \mathrm{\neg }{\alpha }_F$. I w tym przypadku teza jest oczywista.

Aby skonstruować ${\alpha }_{{\pi }_{i_1,\dots ,i_k}E}$ tworzymy formułę $\mathrm{\exists }{x}_{j_1}\dots \mathrm{\exists }{x}_{j_{n-k}}\alpha$, gdzie $j_1,\dots ,j_{n-k}$ to wypisane w obojętnej kolejności elementy zbioru $\{1,\dots ,n\}-\{i_1,\dots ,i_k\}$. Następnie dokonujemy w niej zamiany nazw zmiennych związanych tak, by ich numery były większe niż $n$, a zmienne wolne przemianowujemy z $x_{i_j}$ na $y_{i_j}$. Niech $\beta$ będzie otrzymaną w ten sposób formułą. Wówczas ${\alpha }_{{\pi }_{i_1,\dots ,i_k}E}$ definiujemy jako $\beta (x_1/y_{i_1},\dots ,x_k/y_{i_k})$. Widać, że ta formuła spełnia tezę.

Przy konstrukcji ${\alpha }_{E\times F}$ postępujemy następująco: dokonujemy zamiany nazw zmiennych związanych w formule ${\alpha }_F$ w ten sposób, by miały one numery większe niż $n+m$, zaś za zmienne wolne $x_1,\dots ,x_m$ podstawiamy kolejno $x_{n+1},\dots ,x_{n+m}$. Niech powstała formuła nazywa się ${\beta }_F$. Wtedy definiujemy ${\alpha }_{E\times F}$ jako ${\alpha }_E\wedge {\beta }_F$. Oczyiście ta formuła spełnia tezę.

Na zakończenie tej cześci dowodu określamy formułę ${\alpha }_{{\sigma }_{\theta }E}$ jako

${\alpha }_E\wedge \underset{\text{'}i=j^{\prime }\in \theta }{\bigwedge }{x}_i=x_j\wedge \underset{\text{'}i=c^{\prime }\in \theta }{\bigwedge }{x}_i=c$.

I tym razem sprawdzenie, że ta formuła spełnia tezę indukcyjną jest natychmiastowe.

Przystępujemy teraz do tłumaczenia formuł logiki pierwszego rzędu na algebrę relacyjną. W tym celu wygodnie jest założyć, że podstawowymi spójnikami logiki są $\vee ,\mathrm{\neg }$ i $\mathrm{\exists }$, a pozostałe są zdefiniowane za ich pomocą i mają status skrótów notacyjnych.

Zaczynamy od konstrukcji jednoargumentowego wyrażenia $AD$ takiego, że dla każdej struktury $\mathfrak{𝔄}$, mamy $[[AD]]=ad(\mathfrak{𝔄})$.

Jest ono $\cup$-sumą wyrażeń ${\pi }_{i}R$ dla wszystkich symboli relacyjnych $R$ w sygnaturze i wszystkich $i$ takich, że $R$ ma co najmniej $i$ argumentów.

Możemy teraz przystąpić do konstrukcji. Dla każdego zadanego $n$ nie mniejszego niż wszystkie numery zmiennych wolnych w $\alpha$ konstruujemy $n$-argumentowe wyrażenie $E_{\alpha ;n}$ takie, że

$[[E_{\alpha };n]]=\{<a_1,\dots ,a_n>\in A^n|(\mathfrak{𝔄},x_1:a_1,\dots ,x_n:a_n)\models \alpha \}$.

Oznacza to, że $E_{\alpha ;n}$ zawiera dodatkowe współrzędne, które pozwalają zarejestrować indeksy zmiennych wolnych występujących w $\alpha$. Aby otrzymać $E_{\alpha }$ wystarczy wziąć rzut ${\pi }_I{E}_{\alpha ;n}$, gdzie $I$ to posortowany rosnąco ciąg numerów zmiennych wolnych $\alpha$, co eliminuje przy okazji zbędne współrzędne.

$E_{x_i=x_j;n}$ to ${\sigma }_{i=j}(\underset{n}{\underbrace{AD\times \dots \times AD}})$.

$E_{R(x_{i_1},\dots ,x_{i_k});n}$ jest zdefiniowane jako ${\pi }_I(R\times \underset{n-k}{\underbrace{AD\times \dots \times AD}})$, gdzie $I$ jest taką permutacją $\{1,\dots ,n\}$, która współrzędne $R$ mieszcza na pozycjach o kolejnych numerach $i_1,\dots ,i_k$.

$E_{\alpha \vee \beta ;n}$ jest zdefiniowane jako $E_{\alpha ;n}\cup E_{\beta ;n}$, natomiast $E_{\mathrm{\neg }\alpha ;n}$ to $(\underset{n}{\underbrace{AD\times \dots \times AD}})-E_{\alpha ;n}$.

Wreszcie w wypadku $E_{\mathrm{\exists }{x}_i\alpha ;n}$ możemy bez utraty ogólności założyć, że $i=n+1$. Wtedy $E_{\mathrm{\exists }{x}_i\alpha ;n}$ 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 uzasadniać.

W szczególności badania dotyczące gier Ehrenfeuchta oraz charakteryzacji obliczeniowych logiki pierwszego rzędu (w duchu twierdzeń Büchi i Fagina)są generalnie postrzegane jako wyniki należące do teorii baz danych.

Rozstrzygalność i nierozstrzygalność teorii

W tym rozdziale przedyskutujemy zagadnienie rozstrzygalności teorii matematycznych (rozumianych jako zbiory zdań). Przykładem teorii nierozstrzygalnej jest arytmetyka Peano (Twierdzenie 9.3). Przykład teorii rozstrzygalnej prezentujemy poniżej.

Twierdzenie 13.7

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

Dowód

Niech ${𝒜}$ będzie klasą wszystkich gęstych porządków liniowych które nie mająelementów maksymalnych ani minimalnych. Z Wniosku 4.15 wiemy, że $Th({𝒜})$ jest zupełna. Ponadto zauważmy, że $Th({𝒜})=\{\alpha |\mathrm{\Delta }\models \alpha \}$, gdzie $\mathrm{\Delta }$ to następujący zbiór zdań:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall x\forall y \ (x\leq y \land y\leq x)\to x=y\\ \forall x\forall y \forall z\ (x\leq y \land y\leq z)\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\ (x < y)\to (\exists z\ x < z \land z<y) }

gdzie $x<y$ jest oczywistym skrótem notacyjnym dla formuły $x\le y\wedge x\ne y$.

Na mocy twierdzenia o pełności $\{\alpha |\mathrm{\Delta }\models \alpha \}=\{\alpha |\mathrm{\Delta }{⊢}_H\alpha \}$.

Pozostaje więc wykazać rozstrzygalność $\{\alpha |\mathrm{\Delta }{⊢}_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 udzieli 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 umiemy.

Istnieją bardziej zaawansowane technicznie metody dowodzenia rozstrzygalności, które pozwalają oszacować złożoność tworzonych przez nie algorytmów. Jednak można udowodnić, że żaden taki algorytm nie może mieć złożoności mniejszej niż PSPACE, o ile tylko działa poprawnie dla wszystkich formuł zawierających symbole równości.

Twierdzenie 13.8 (Stockmeyer)

Następujący problem jest 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

Przeprowadzamy redukcję w pamięci logarytmicznej z problemu QBF kwantyfikowanych formuł Boolowskich do naszego problemu.

Instancjami problemu QBF są zdania postaci $Q_1{p}_1\dots Q_n{p}_n\alpha$, gdzie $Q_i\in \{\mathrm{\exists },\mathrm{\forall }\}$, a $\alpha$ jest formułą zdaniową. Pojęcie prawdziwości takiego zdania jest definiowane w naturalny sposób. Problem QBF jest znanym problemem PSPACE-zupełnym.

Redukcja określona jest jak następuje: w zdaniu powyższym każde wystąpienie $p_i$ zastępujemy przez $x_i=y_i$. Teraz po kolei zastępujemy kwantyfikatory:

• Każdy kwantyfikator $\mathrm{\forall }{p}_i$ zamieniamy na $\mathrm{\forall }{x}_i\mathrm{\forall }{y}_i$.

• Każdy kwantyfikator $\mathrm{\exists }{p}_i$ zamieniamy na $\mathrm{\exists }{x}_i\mathrm{\exists }{y}_i$.

Niech formułą otrzymana po tych operacjach będzie ${\alpha }^{\prime }$. Wtedy wynikiem naszej redukcji jest formuła ${\alpha }^{″}$ $\mathrm{\forall }x\mathrm{\forall }y(x=y\vee {\alpha }^{\prime })$.

Jest oczywiste, że ${\alpha }^{″}$ daje się obliczyć z $\alpha$ w logarytmicznej pamięci.

Widać, że formuły atomowe $x_i=y_i$ pełnią rolę zmiennych zdaniowych $p_i$, przy czym w każdej strukturze o co najmniej dwóch elementach mogą przyjmować obie wartości logiczne. Kwantyfikatory $\mathrm{\forall }{x}_i\mathrm{\forall }{y}_i$ i $\mathrm{\exists }{x}_i\mathrm{\exists }{y}_i$ swoją funkcją wiernie odpowiadają kwantyfikatorom $\mathrm{\forall }{p}_i$ oraz $\mathrm{\exists }{p}_i$. Z kolei klauzula $\mathrm{\forall }x\mathrm{\forall }y(x=y)$ czyni ${\alpha }^{″}$ prawdziwym w strukturach jednoelementowych, niezależnie od postaci $\alpha$.

Z tego wynika, że $\alpha$ jest prawdziwe wtedy i tylko wtedy, gdy ${\alpha }^{″}$ jest tautologią.

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

Twierdzenie 13.9 (Tarski)

Teoria uporządkowanego ciała liczb rzeczywistych, tj. teoria struktury $<\mathbb{ℝ},+,*,0,1,\le >$ jest rozstrzygalna.

Jej znaczenie dla informatyki zasadza się na fakcie, że ta teoria to w istocie znana wszystkim ze szkoły geometria analityczna. Poważną część algorytmicznych badań w zakresie geometrii obliczeniowej można streścić jako ulepszanie algorytmu rozstrzygającego teorię $<\mathbb{ℝ},+,*,0,1,\le >$ dla różnych szczególnych klas formuł, pojawiających się w praktyce.