Logika matematyczna zajmuje si¦ modelami w ogólno±ci. Informatyka teo-retyczna zajmuje si¦ tylko modelami sko«czonymi tj. okre±lonymi na zonych no±nikach. Pomysª, aby systematycznie bada¢ tylko rodziny sko«c-zonych modeli rozwin¡ª si¦ w latach 70-tych XX-wieku. Jest on powi¡zany z teori¡ relacyjnych baz danych oraz z teori¡ zªo»ono±ci obliczeniowej (al-gorytmów poszukiwania odpowiedzi na pytania formuªowane w systemach relacyjnych baz danych). Najwa»niejszym prekursorem tej dziedziny infor-matyki teoretycznej jest Ronald Fagin.
12.1 Pewne ró»nice dla sko«czonych modeli
Wiadomo, »e wiele twierdze« teorii modeli jest nieprawdziwych, gdy speª-nialno±¢ |= ograniczymy do sko«czonych modeli.
Jedenym z fundamentalnych przykªadów tego typu jest twierdzenie Gödla o peªno±ci.
Twierdzenie 12.1 (O peªno±ci) Formuªa ϕ jest prawdziwa we wszystkich modelach teorii T wtw, gdy ϕ ma dowód w T .
Standardowym wnioskiem z tego twierdzenia i opisu systemu Hilberta jest
Wniosek 12.2 Zbór T h(Mod((F, C, R))) wszystkich zda« ustalonego j¦zyka b¦d¡cych twierdzeniami rachunku kwanty katorów jest rekurencyjnie przeliczalny.
Dowód Poniewa» nietrudno udowodni¢, »e zbiór wszystkich dowodów w systemie Hilberta jest rekurencyjny i rozstrzygalny jest predykat R(x, y) stwierdzaj¡cy, »e x jest ci¡giem formuª, który jest dowodem formuªy y, a
y ∈ T h(M od((F , C, R))) ⇔ ∃xR(x, y) mamy tez¦.
Twierdzenie Churcha, które w ogólnej postaci brzmi nast¦puj¡co:
Twierdzenie 12.3 (Church 1936) Dla j¦zyków (F, C, R) posiadaj¡cych sym-bole relacyjne, które nie s¡ jednoargumentowe zbiór T h(Mod((F, C, R))) wszys-tkich zda« prawdziwych w ka»dym modelu j¦zyka (F, C, R) nie jest rekuren-cyjny.
implikuje, »e
Wniosek 12.4 Zaªó»my, »e j¦zyk (F, C, R) ma symbole relacyjne, które nie s¡ jednoargumentowe. Wtedy dopeªnienie zbioru T h(Mod((F, C, R))) wszys-tkich zda« prawdziwych w ka»dym modelu j¦zyka (F, C, R) nie jest rekuren-cyjnie przeliczalny.
Ciekawe, »e dla sko«czonych modeli sytuacja jest zupeªnie inna.
Twierdzenie 12.5 (Trakhtenbrot) Zaªó»my, »e j¦zyk (F, C, R) ma sym-bole relacyjne, które nie s¡ jednoargumentowe. Wtedy zbiór T h(ModF((F , C, R))) wszystkich zda« prawdziwych w ka»dym modelu sko«czonym j¦zyka (F, C, R) nie jest rekurencyjnie przeliczalny, ale jego dopeªnienie jest rekurencyjnie przeliczalne.
Zauwa»my, »e bardzo ªatwo wykaza¢, »e zbiór zda«, które nie s¡ twierdzeni-ami teorii sko«czonych modeli jest r.e., gdy» wystarczy opracowa¢ procedur¦
wyliczaj¡c¡ wszystkie sko«czone modele danego j¦zyka i posªu»y¢ si¦ ni¡ w poszukiwaniu modelu, w którym dane zdanie nie jest prawdziwe. Dowód twierdzenia nie jest jednak banalny!
Z twierdzenia Trakhtenbrota wynika, »e nie istnieje system dowodzenia np. w stylu Hilberta twierdze« teorii sko«czonych modeli, dla którego za-chodzi twierdzenie o peªno±ci. Dlaczego? Z powy»szych rozwa»a« wiemy, »e jego istnienie poci¡ga, »e zbiór T h(ModF((F , C, R)))jest r.e.
Z twierdzenia o peªno±ci wynika
Twierdzenie 12.6 (O zwarto±ci) Nich T b¦dzie zbiorem zda« I-go rz¦du.
Je±li ka»dy sko«czony podzbiór T jest niesprzeczny, to T jest niesprzeczny.
Wobec twierdzenia Henkina, »e ka»dy niesprzeczny zbiór zda« ma model otrzymujemy drug¡ wersj¦ twierdzenia.
Twierdzenie 12.7 (O zwarto±ci) Nich T b¦dzie zbiorem zda« I-go rz¦du.
Je±li ka»dy sko«czony podzbiór T ma model, to T ma model.
Twierdzenie to nie jest prawdziwe, gdy ograniczymy si¦ do sko«czonych modeli, co pokazuje przyklad.
Przykªad Niech tnb¦dzie zdaniem, które mówi, »e model ma przynajm-niej n elementóe i T = {tn, n ∈ n}. Jasne jest, »e ka»dy sko«czony podzbiór T ma sko«czony model, ale T nie ma takiego modelu.
Z powy»szych rozwa»a« wida¢, »e teoria sko«czonych modeli ró»ni si¦
bardzo o uniwersalnej teorii modeli. Musiaªa wi¦c wypracowa¢ oryginalne metody badawcze.
12.2 Opisowa teoria zªo»ono±ci, twierdzenie Fagina
Twierdzenie Cooka, jest dowodem ±cisªego zwi¡zku logiki ze zªo»ono±ci¡.
Twierdzenie Fagina pokazuje, »e jest on bardzo gªeboki.
W rozdziale tym b¦dziemu rozwa»a¢ nie tylko formuªy I-go rz¦du, ale i formuªy II-go rz¦du postaci
∃Pϕ
gdzie P jest symbolem relacyjnym wyst¦puj¡cym w j¦zyku formuªy ϕ, s¡
tzw. Σ11- formuªy lub egzystencjalne formuªy II-go rz¦du. Nietrudo wykaza¢,
»e postawienie wi¦kszej ilo±ci kwanty katorów typu ∃Q daje formuª¦, która jest logicznie równowa»na z Σ11-formuª¡.
Dla prostoty b¦dziemy te» zakªada¢, »e zajmujemy si¦ teori¡ grafów, czyli modeli z jedn¡ relacj¡ binarn¡.
Twierdzenie 12.8 Dla dowolnej formuªy II-go rz¦du ∃Pϕ zbiór wszystkich grafów b¦d¡cych jej modelami nale»y do klasy NP.
Dowód Dla danego grafu G = (V, E) niedeterministyczna MT mo»e
¹gadn¡¢"interpretacj¦ PG predykatu P i nast¦pnie mo»e bada¢ determin-istycznie i we wielomianowym czasie, czy powstaª model formuªy ϕ.
Poka»emy, »e zachodzi te» implikacja w drug¡ stron¦, czyli
Twierdzenie 12.9 (Fagin) Klasa wªasno±ci grafowych wyra»alnych w Σ11 -logice jest równa NP.
Dowód jest podobny do dowodu tw. Cooka. Dla MT dziaªaj¡cej w czasie nk i lewostronnie ograniczonej rozstrzygaj¡cej pewien zbiór grafów skonstru-ujemy »¡dan¡ formuª¦. Ponownie rozwa»ymy tablic¦ kwadratow¡ rozmiaru nk. Przypomnijmy, »e w dowodzie wprowadzili±my zbiór zmiennych zdan-iowych Ti,j,Y potrójnie indeksowany krokiem obliczenia i, numerem komórki j i jej zawarto±ci¡ Y ∈ Γ. Tutaj wprowadzimy:
1. predykaty TY(x, y), które b¦dziemy podobnie interpretowa¢: symbol Y jest w j-tej komórce i-tego wiersza, o ile x, y s¡ zapisami liczb i, j;
2. predykaty C0, . . . , Cq−1 odpowiadaj¡ce za wybór m-tej instrukcji;
3. zapis k-cyfrowych liczb naturalnych w systemie o podstawie n, czyli pozwalaj¡cy na ªiczenieód 0 do nk− 1;
4. predykaty Sj(x, y) dla j = 1, . . . k pozwalaj¡ce na interpretacj¦ funkcji nast¦pnika dla j-cyfrowych zapisów.
Wtedy poszukiwana formuªa jest postaci:
∃S1∃TY 1. . . ∃TY m∃C0. . . ∃Cq−1ϕ
gdzie m jest moc¡ zbioru Γ. Po pierwsze musimy pami¦ta¢, »e dla ustalonego grafu o n wierzchoªkach zmienne, które wprowadzomy b¦d¡ przyjmowa¢
warto±ci ze zbioru wierzchoªków, czyli mo»emy przyj¡¢, »e ze zbioru {0, 1, . . . , n−
1}. St¡d j-cyfrowy zapis w systemie o podstawie n mo»emy traktowa¢ jak warto±ciowanie j zmiennych.
Jak zwykle w takich rozumowaniach ϕ jest koniunkcj¡ formuª. Poni»ej opiujemy co wa»niejsze skªadniki.
1. S1(x, y) jest funkcj¡ nast¦pnika, przykªadowo
∀x∀y,zS1(x, y) ∧ S1(x, z) ⇒ y = z to jest funkcja cz¦±ciowa (2)
∀x∀y,zS1(y, x) ∧ S1(z, x) ⇒ y = z która jest ró»nowarto±ciowa (3)
∀y¬S1(y, x)de nicja zera, ozn.ζ(x) (4)
∀y¬S1(x, y)de nicja n − 1, η(x) (5)
2. Formuªy uniwersalne opisuj¡ce relacje 2j-argumentowe Sj(x, y) de ni-ujemy indukcyjnie:
Sj(x, y) ⇔ ((S1(xj, yj) ∧ x1 = y1∧ . . . ∧ xj−1 = yj−1)∨
(η(xj) ∧ ζ(yj) ∧ Sj−1(x1, . . . , xj−1, y1, . . . , yj−1))
3. Pierwszy wiersz tablicy opisuje kon guracj¦ pocz¡tkow¡, a ka»dy nast¦pny jest wypeªniony zgodnie z intsrukcjami maszyny. Przykªadowo, relacj¦
przej±cia mo»na przedstawi¢ jako zbiór pi¡tek (x, y, z, c, d), gdzie c jest wyborem kolejnej instrukcji, a d symbolem w komórce j, który tam si¦
pojawi po jej wykonaniu; x, y, z opisuj¡ zawarto±¢ komórek j−1, j, j+1 przed jej wykonaniem. Dla ka»dej takiej pi¡tki tworzymy formuª¦ uni-wersaln¡ (dopisz kwanty katory "dla ka»dego"):
(Sk(x0, x)∧Sk(y0, y)∧Sk(y, y00)∧Tx(x0, y0)∧Ty(x0, y)∧Tz(x0, y00)∧Cc(x0))
⇒ Td(x, y)
Trzeba jeszcze zapewni¢ jednoznaczno±¢ wyboru:
(C0(x) ∨ . . . Cq−1(x)) ∧ (
q−1
_
j=0
¬Cj(x))
Na koniec mo»emy sobie postawi¢ pytanie, czy istnieje charakteryzacja logiczna klasy P?
Tak¡ charakteryzacj¦ podali niezale»nie Imermann, Vardi i Papadim-itriou. Aby j¡ uzyska¢ nale»y zastanowi¢ si¦, co si¦ zmieni w dowodzie twierdzenia Fagina, gdy b¦dziemy rozwa»a¢ maszyny deterministyczne? Zniknie formuªa zapewniaj¡ca jednoznaczno±¢ wyboru i predykaty, które w niej wys-t¦puj¡. Mo»na zauwa»y¢, »e skªadniki formuªy ϕ opisuj¡ce obliczenia maszyny b¦d¡ uniwersalnymi formuªami hornowskimi. St¡d zachodzi
Twierdzenie 12.10 Klasa wªasno±ci grafowych wyra»alnych w egzystencjal-nej logice hornowskiej drugiego rz¦du z nast¦pnikiem równa jest klasie P.
Uniwersaln¡ formuªe I-go rz¦du nazywamy hornowsk¡, je±li po usuni¦ciu kwanty katorów jest ona alternatyw¡ literaªów, z których co najwy»ej je-den jest pozytywny tj. nie jest negacj¡ formuªy atomowej. W twierdzeniu
tym zakªada si¦, »e wªasno±ci nast¦pnika s¡ aksjomatami. Zauwa»my, »e nie s¡ one hornowskie! Przykªadowo, formuªa:
∀x¬ζ(x) ⇒ ∃yS1(y, x)
stwierdzaj¡ca, »e ka»dy element ró»ny od zera jest nast¦pnikem, nie jest formuª¡ hornowsk¡.