(1)Denicja Niech ZP b¦dzie pewnym niepustym zbiorem, którego elementy nazywa¢ b¦dziemy zdaniami prostymi

Denicja

Niech ZP b¦dzie pewnym niepustym zbiorem, którego elementy nazywa¢ b¦dziemy zdaniami prostymi. Symbole ∨, ∧, ⇒, ¬ zwane alternatyw¡, koniunkcj¡, implikacj¡ i negacj¡, b¦dziemy nazywa¢

spójnikami zdaniotwórczymi.

Zbiór zda« zªo»onych ZZ (zbudowanych ze zda« prostych ZP) deniujemy jako j¦zyk rekurencyjny nad alfabetem

X = ZP ∪ {(, ), ¬, ∧, ∨, ⇒}

wyznaczony przez

1 j¦zyk bazowy ZP

2 i konteksty: (t1∨ t₂), (t₁∧ t₂), (t₁ ⇒ t₂), ¬(t). Inaczej: rozwa»my funkcj¦ F_Z :2^X? 7→2^X? okre±lon¡ wzorem:

FZ(J) = J∪{(p∨q); p, q ∈ J}∪{(p∧q); p, q ∈ J}∪{(p ⇒ q); p, q ∈ J}∪{¬(p); p ∈ J}.

Wtedy ZZ = S_n∈NF_Zⁿ(ZP), gdzie F_Z⁰(J) = J, F_Zⁿ⁺¹=F_Z(F_Zⁿ(J)).

Denicja rekurencyjna ZZ poci¡ga te», »e zachodzi nast¦puj¡ce

Twierdzenie

Zbiór ZZ ⊆ X^? jest najmniejszym j¦zykiem speªniaj¡cym:

1 ZP ⊆ ZZ;

2 je±li p, q ∈ ZZ, to ¬(p), (p ∨ q), (p ∧ q), (p ⇒ q) ∈ ZZ.

Twierdzenie to wykorzystujemy cz¦sto przy dowodzeniu twierdze«

dotycz¡cych zda« zªo»onych i deniowaniu funkcji na zbiorze ZZ.

W dalszych rozwa»aniach zbiory ZP i ZZ s¡ ustalone.

Symbolem 2 oznacza¢ b¦dziemy dwelementow¡ algebr¦ Boole'a o no±niku {0, 1} wyró»nionych elementach 0, 1 i dziaªaniach

opisanych w tabelach:

∧ 0 1 0 0 0 1 0 1

∨ 0 1 0 0 1 1 1 1

⇒ 0 1

0 1 1 1 0 1

¬ 0 1 1 0

Denicja

Ka»d¡ funkcj¦ v : ZP 7→ {0, 1} nazywamy warto±ciowaniem (logicznym) zda« prostych. Ka»d¡ tak¡ funkcj¦ mo»na rozszerzy¢

na zbiór ZZ zda« zªo»onych deniuj¡c v : ZZ 7→ {0, 1} wzorami:

v(z) = v(z) z ∈ ZP

v(¬z) = ¬v(z) z ∈ ZZ

v(pq) = v(p)v(q) p, q ∈ ZZ,  ∈ {∨, ∧, ⇒}

Denicja

Zdanie zªo»one z ∈ ZZ nazywamy speªnialnym, je±li istnieje

warto±ciowanie v : ZP 7→ {0, 1} takie, »e v(z) = 1, mówimy wtedy,

»e z jest speªnione przy warto±ciowaniu v. Zdanie z ∈ ZZ nazywamy tautologi¡, je±li zdanie ¬z nie jest speªnialne.

Zadanie 1. Wyka», »e zdanie z ∈ ZZ jest tautologi¡ wtw, gdy jest speªnialne przy ka»dym warto±ciowaniu.

Zadanie 2. Wyka», »e nast¦puj¡ce zdania s¡ tautologiami; dla p, q ∈ ZZ napis p ⇔ q oznacza zdanie postaci p ⇒ q ∧ q ⇒ p

1 p ∨ ¬p;

2 ¬(¬p) ⇔ p;

3 ¬(p ∨ q) ⇔ (¬p ∧ ¬q);

4 (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))

Zdenujmy dwa j¦zyki SAT i T zda« zªo»onych, które s¡ speªnialne i zda« b¦d¡cych tautologiami. Na wykªadzie b¦dziemy si¦

zastanawia¢ nad zªo»ono±ci¡ czasow¡ problemów:

zdanie zªo»one nale»y do SAT ; zdanie zªo»one nale»y do T .

Bezpo±rednio z denicji wynika algorytm o zªo»ono±ci wykªadniczej.

Oka»e si¦, »e j¦zyk SAT jest bardzo wa»ny w teorii czasowej zªo»ono±ci obliczeniowej. Udowodnimy Twierdzenie Cooka, które mówi, »e problem ten jest NP-zupeªny. Tak wi¦c ustalenie, czy istnieje algorytm o wielomianowej czasowej zªo»ono±ci obliczeniowej

dla nale»enia do SAT pozwoli rozstrzygn¡¢, czy P = NP.

Przypomnijmy, »e problem równo±ci klas zªozono±ci obliczeniowej P i NP jest jednym z siedmiu problemów milenijnych!

Na drodze do znalezienia lepszego algorytmu dla problemu

speªnialno±ci (tautologii) pojawiªo si¦ te» podej±cie syntaktyczne:

budowano systemy formalne, w których ustalenie, czy z ∈ ZZ jest tautologi¡ sprowadza si¦ do analizy skªadniowej z, czyli budowy, ksztaªtu z. Prykªadem takiego systemu jest system Hilberta.

System ma nast¦puj¡ce schematy aksjomatów i reguª wnioskowania:

A ⇒ (B ⇒ A) (1) (A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)) (2)

A ⇒ (B ⇒ (A ∧ B)) (3)

(A ∧ B) ⇒ A (4)

(A ∧ B) ⇒ B (5)

A ⇒ (A ∨ B) (6)

B ⇒ (A ∨ B) (7)

(A ⇒ C) ⇒ ((B ⇒ C) ⇒ ((A ∨ B) ⇒ C)) (8) (¬A ⇒ ¬B) ⇒ (B ⇒ A)) (9)

0 ⇒ A (10)

MP A ⇒ B, A B

Jak wida¢ wyst¦puje tu reguªa wnioskowania Modus Ponens, czyli

reguªa odrywania. Sªowo "schemat" oznacza, »e litery A, B, C mog¡ zast¦powa¢ dowolne zdania zªo»one.

Denicja

Dowodem zdania z w systemie Hilberta nazywamy ci¡g zda«

z₁,z₂, . . . ,z_n=z taki, »e dla ka»dego i ≤ n z_i jest aksjomatem lub dla pewnych j, k ≤ i z_k = (z_j ⇒z_i), czyli z_i mo»na uzyska¢ z z_k,z_j stosuj¡c reguª¦ Modus Ponens.

Przykªad Jako ilustracj¦ rozwa»my ci¡g zda«:

(A ⇒ (B ⇒ (A ∧ B))) ⇒ ((A ⇒ B) ⇒ (A ⇒ (A ∧ B))), A ⇒ (B ⇒ (A ∧ B)),

(A ⇒ B) ⇒ (A ⇒ (A ∧ B))

Zdanie pierwsze jest wykorzystaniem schematu 15, drugie 16, a trzecie otrzymujemy z nich stosuj¡c reguª¦ MP.

Dla systemu Hilberta zachodz¡ dwa wa»ne twierdzenia;

Twierdzenie (O zgodno±ci)

Ka»de zdanie maj¡ce dowód w systemie Hilberta jest tautologi¡.

Twierdzenie (O zupeªno±ci)

Ka»de zdanie b¦d¡ce tautologi¡ ma dowód w systemie Hilberta.

Ustalmy w dalszych rozwa»niach:

niesko«czony, przeliczalny zbiór X = {x, y, z, . . .} zmiennych indywiduowych;

zbiór staªych C;

zbiór F symboli operacyjnych wraz z funkcj¡ arno±ci ar_f : F 7→N \ {0};

zbiór R symboli operacyjnych wraz z funkcj¡ arno±ci arr : R 7→N \ {0}.

Denicja

Trójk¦ (F, C, R) nazywamy j¦zykiem, typem lub sygnatur¡.

Uwaga Czasem deniuje si¦ funkcj¦ ar_f : F 7→N a wtedy

C = ar_f⁻¹(0). Staªe odgrywaj¡ jednak bardzo wa»n¡ rol¦, wi¦c si¦

je wyró»nia. Wprowad»my te» oznaczenia: F_n=ar_f⁻¹(n), R_n=ar_r⁻¹(n).

J¦zyk I-go rz¦du sygnatury (F, C, R) jest j¦zykiem nad alfabetem

Y = X ∪ F ∪ C ∪ R ∪ {∨, ∧, ⇒, ¬, ∀, ∃, (, )}.

Elementy tego j¦zyka dzielimy na termy i formuªy.

Denicja

Zbiór termów FX jest wyznaczony przez

1 j¦zyk bazowy X ∪ C;

2 konteksty q(t₁, . . . , t_n), gdzie n ≥ 1 i q ∈ F_n. Zadanie Udowodnij

Twierdzenie

Zbiór FX ⊆ Y^? jest najmniejszym j¦zykiem speªniaj¡cym warunki:

1 X ∪ C ⊆ FX ;

2 je±li q ∈ Fn,n ≥ 1 oraz t1, . . . ,tn ∈ FX , to q(t1, . . . ,tn) ∈ FX .

Denicja

Zbiór At formuª atomowych j¦zyka (F, C, R) jest najmniejszym j¦zykiem takim, »e:

1 (t = p) ∈ At gdzie t, p ∈ FX ;

2 r(t₁, . . . ,t_n) ∈At, gdzie r ∈ R_ni t₁, . . . ,t_n∈ FX .

Denicja

Zbiór For formuª j¦zyka (F, C, R) jest najmniejszym j¦zykiem takim, »e:

1 At ⊆ For;

2 je±li α, β ∈ For, to (¬α), (α ∨ β), (α ∧ β), (α ⇒ β) ∈ For;

3 jeªi x ∈ X i α ∈ For, to ∀_xα, ∃_xα ∈For.

Uwaga B¦dziemy stosowali uproszczenia w notacji, np. zamiast

∀_x∀_y b¦dzie ∀_x,y. Standardowo kwantykator u»yty do formuªy np.

postaci ϕ ∨ ψ odnosi si¦ do caªej formuª; tak wi¦c formuªy

(∃_x(ϕ ∧ ψ))i (∃_xϕ) ∧ ψ s¡ ró»ne i, jak wyka»emy, nierównowa»ne.

Tym niemniej pierwsza para nawiasów w obu formuªach nie wpªywa na czytelno±¢, wi¦c zwykle jest pomijana. B¦dziemy te» stosowa¢

priorytety operatorów logicznych wymienionych w kolejno±ci od najsilniejszego do najsªabszego:∃ i ∀, ∧, ∨ i ⇒. Przykªadowo p ⇒ q ∧ r jest uproszczonym zapisem formuªy (p ⇒ (q ∧ r)).

Przykªady

1 Teori¦ grup mo»na opisa¢ w j¦zyku z jedn¡ staª¡ 0 i jednym binarnym dziaªaniem +. Wtedy formuªy

∀_x,y,z (x + y) + z = x + (y + z)

∀_x,yx + y = y + x

opisuj¡ prawo ª¡czno±ci i przemienno±ci, a formuªa

∀_x∃_y x + y = 0 istnienie elementu przeciwnego.

2 Cz±ciowe porz¡dki opisane s¡ w j¦zku z jednym binarnym symbolem relacyjnym . Wtedy formuªa

∀_xx  x

opisuje zwrotno±¢ cz¦±ciowego porz¡dku. Jak wygl¡da zbiór termów dla tego j¦zyka?

3 Grupy uporz¡dkowane deniujemy w j¦zyku

({−, +}, {0}, {}), gdzie dodatkowo − jest symbolem arno±ci 1. W j¦zyku tym formuªa

∀_x,y,zx  y ⇒ x + z  y + z

opisuje monotoniczno±¢ dziaªania +.

Symbolem Var(α) oznaczymy zbiór wszystkich zmiennych

wyst¦puj¡cych w formule, termie α. To co odró»nia kwantykatory

∀, ∃od spójników zdaniotwórczych, to fakt, »e "wi¡»¡ zmienne", a dokªadniej pewne ich wyst¡pienia. Zbiór Var(α) zawiera podzbiór Free(α) zmiennych maj¡cych wolne wyst¡pienia w α, który deniowany jest nast¦puj¡co:

Denicja

1 Free(α) = Var(α), jeªi α jest formuª¡ atomow¡.

2 Free(α) = Free(α₁) ∪Free(α₂), je»eli α = α₁ α₂ dla pewnego spójnika zdaniowego ;

3 Free(¬(α)) = Free(α);

4 Free(∀_xα) =Free(∃_xα) =Free(α) \ {x}.

Denicja

Formuª¦ nie posiadaj¡c¡ zmiennych wolnych nazywamy zdaniem.

Przykªad Rozwa»my formuª¦ ϕ postaci x = y ∨ ∃_x(f (x) = 1).

Wtedy x ∈ Free(ϕ), bo nie zawsze pojawia si¦ "w zasi¦gu"

kwantykatora. Takich formuª nie widuje si¦ raczej w

podr¦cznikach, gdy» dla ka»dej formuªy mo»na wyznaczy¢ formuª¦

równowa»n¡ z ni¡, która ma rozªaczne zbiory zmiennych maj¡cych wolne wyst¡piena i maj¡cych wyst¡pienia zwi¡zane

kwantykatorem.

Co to znaczy, »e dwie formuªy s¡ równowa»ne? Odpowiedzi na to pytanie udzielimy wprowadzaj¡c poj¦cie MODELU j¦zyka I-go rz¦du. Równowa»no±¢ formuª oznacza¢ b¦dzie, »e maj¡ one identyczn¡ interpretacj¦ w ka»dym modelu.

Denicja

Modelem j¦zyka (F, C, R) nazywamy system

A =<A, {q^A,q ∈ F}, {c^A,c ∈ C}, {r^A,r ∈ R} >, gdzie

1 A jest zbiorem zwanym no±nikiem;

2 q^A :Aⁿ7→A dla q ∈ F_n;

3 c^A ∈A dla c ∈ C, s¡ wyró»ninymi elementami zbioru A;

4 r^A⊆Aⁿ dla r ∈ R_n.

W denicji modelu nie zakªadamy, »e no±nik jest niepusty, za to nale»y podkre±l¢, »e gdy zbiór C symboli stalych jest niepusty, to no±nik musi by¢ niepusty. Ogólnie: funkcje q^A, elementy c^A i relacje r^A nazywamy interpretacjami symboli funkcyjnych, staªych

itp. w modelu A.

Denicja

Niech A b¦dzie modelem j¦zyka (F, C, R). Warto±ciowaniem zmiennych w modelu A nazywamy ka»d¡ funkcj¦ h : X 7→ A.

Analogicznie jak w rachunku zda« h wyznacza warto±ciowanie termów h : FX 7→ A wzorami:

1 h(x) = h(x), dla x ∈ X ;

2 h(c) = c^a, dla c ∈ C;

3 h(q(t₁, . . . ,t_n)) =q^A(h(t₁), . . . ,h(t_n)).

Denicja

Mówimy, »e formuªa ϕ jest speªniona w modelu A przy warto±ciowaniu h : X 7→ A (ozn (A, h) |= ϕ), je±li

1 ϕjest równo±ci¡ t₁=t₂ i h(t₁) =h(t₂);

2 ϕjest postaci r(t1, . . . ,tn) i r^A(h(t1), . . . ,h(tn));

3 ϕjest postaci ϕ1∧ ϕ₂ oraz (A, h) |= ϕ1 i (A, h) |= ϕ2;

4 ϕjest postaci ϕ₁∨ ϕ₂ oraz (A, h) |= ϕ₁ lub (A, h) |= ϕ₂;

5 ϕjest postaci ϕ₁ ⇒ ϕ₂ oraz (A, h) |= ¬(ϕ₁) lub (A, h) |= ϕ₂;

6 ϕjest postaci ¬(ϕ₁) oraz (A, h) 6|= ϕ₁ ;

7 ϕjest postaci ∃x(ϕ₁)oraz (A, h1) |= ϕ₁ dla pewnego warto±ciowania h₁ :X 7→ A pokrywaj¡cego si¦ z h na zbiorze X \ {x};

8 ϕjest postaci ∀_x(ϕ₁)oraz (A, h₁) |= ϕ₁ dla ka»dego

warto±ciowania h1 :X 7→ A pokrywaj¡cego si¦ z h na zbiorze X \ {x}.

Denicja

Mówimy, »e formuªa ϕ jest prawdziwa w modelu A, je±li jest speªniona w nim przy ka»dym warto±ciowaniu.

Twierdzeniem rachunku I-go rz¦du nazywamy zdanie ϕ prawdziwe w ka»dym modelu.

Zauwa»my, »e w przypadku kwantykacji zmiennej staje si¦ istotne, czy zmienna wyst¦puje wolno w kwantykowanej formule. Mo»na np. wykaza¢, »e zdanie ϕ jest prawdziwe w modelu A wtw, gdy jest w nim speªnione przy pewnym warto±ciowaniu.

B¦dziemy wi¦c stosowa¢ zapis ϕ(x) oznaczaj¡cy, »e x ∈ Free(ϕ).

Najpierw podamy dªug¡ list¦ praw-twierdze«-tautologii

rachunku kwantykatorów: opiszemy ksztaªt formuª niezale»nie od konkretnego j¦zyka, które s¡ speªnione w ka»dym modelu i przy ka»dym warto±ciowaniu.

Przede wszystkim ªatwo zauwa»y¢, »e zachodzi

Twierdzenie

Niech (F, C, R) b¦dzie j¦zykiem i f : ZP 7→ For dowoln¡ funkcj¡.

Wtedy istnieje funkcja f : ZZ 7→ For taka, »e:

1 f (p) = h(p) dla p ∈ ZP;

2 je±li p ∈ ZZ jest tautologi¡ rachunku zda«, to f (p) jest twierdzeniem rachunku kwantykatorów.

Zarys dowodu Nale»y zastanowi¢ si¦ jak powinna by¢ zdeniowana funkcja f . Chyba nikogo nie zdziwi, »e np. dla zdania p postaci p₁∧p₂ nast¦puj¡co:

f (p1∧p2) =f (p1) ∧f (p2)

Ponadto czujemy, »e zmienne, które nie nale»¡ do zbioru Free(ϕ) nie maj¡ wpªywu na speªnialno±¢ formuªy ϕ. Faktycznie zachodzi:

Lemat

Niech ϕ ∈ For b¦dzie formuª¡ i x 6∈ Free(ϕ). Wtedy dla dowolnego modelu A i warto±ciowania h : X 7→ A nast¦puj¡ce warunki s¡

równowa»ne:

1 (A,h) |= ϕ;

2 dla dowolnego warto±ciowania h⁰ :X 7→ A pokrywaj¡cego si¦ z h na zbiorze X \ {x}: (A, h⁰) |= ϕ.

Dowód Oczywi±cie wystarczy wykaza¢, »e pierwszy warunek implikuje drugi. Nale»y najpierw zauwa»y¢, »e dla formuª

atomowych twierdzenie jest prawdziwe. Rozpatrzmy przykªadowo równo±¢ t₁ =t₂. Wtedy h(t) = h⁰(t) dla ka»dego termu t, w którym nie wyst¦puje zmienna x. Równo±ci tej dowodzi si¦ bardzo ªatwo stosuj¡c indukcj¦ ze wzgl¦du na budow¦ termu t. Wtedy h⁰(t₁) =h(t₁) =h(t₂) =h⁰(t₂). Podobnie mo»na przenie±¢ to rozumowanie na dowoln¡ formuª¦.

Twierdzenie

Nast¦puj¡ce formuªy s¡ prawami rachunku kwantykatorów, o ile zaªo»ymy, »e x 6∈ Free(ψ) w punktach 11-17 :

1 ¬∀_xϕ ⇔ ∃_x¬ϕ;

2 ¬∃_xϕ ⇔ ∀_x¬ϕ;

3 ∃_x∀_yϕ ⇒ ∀_y∃_xϕ;

4 ∃_x(ϕ ∨ ψ) ⇔ (∃_xϕ ∨ ∃_xψ);

5 ∃_x(ϕ ∧ ψ) ⇒ (∃_xϕ ∧ ∃_xψ);

6 ∀_x(ϕ ∧ ψ) ⇔ (∀_xϕ ∧ ∀_xψ);

7 (∀_xϕ ∨ ∀_xψ) ⇒ ∀_x(ϕ ∨ ψ);

Twierdzenie

1 ∀_x(ϕ ⇒ ψ) ⇒ (∀_xϕ ⇒ ∀_xψ);

2 ∀_x(ϕ ⇔ ψ) ⇒ (∀_xϕ ⇔ ∀_xψ);

3 ∀_xψ ⇒ ψ;

4 ∀_xψ ⇔ ψ;

5 ∀_x(ϕ ∨ ψ) ⇒ (∀_xϕ ∨ ψ);

6 (ψ ∧ ∃_xϕ) ⇒ ∃_x(ψ ∧ ϕ);

7 (ψ ⇒ ∃_xϕ) ⇒ ∃_x(ψ ⇒ ϕ);

8 (ψ ⇒ ∀_xϕ) ⇒ ∀_x(ψ ⇒ ϕ);

9 (∃_xϕ ⇒ ψ) ⇒ ∀_x(ϕ ⇒ ψ);

10 (∀_xϕ ⇒ ψ) ⇒ ∃_x(ϕ ⇒ ψ);

Dowód Przedstawimy kilka dowodów wybranych praw, reszt¦

pozostawiaj¡c jako (niezbyt trudne) ¢wiczenie.

Zacznijmy od prawa de Morgana rachunku kwantykatorów:

¬∀_xϕ ⇔ ∃_x¬ϕ; dla modelu A mamy:

A |= ∃_x¬ϕi (A, h) |= ∃x¬ϕdla dowolnego warto±ciowania h.

Niech h : X 7→ A b¦dzie dowolnym warto±ciowaniem. Poka»emy, »e (A,h) |= ∃_x¬ϕi (A, h) |= ¬(∀_xϕ).

(A,h) |= ∃_x¬ϕwtedy i tyko wtedy, gdy istnieje warto±ciowanie h⁰ :X 7→ A by¢ mo»e ró»ni¡ce si¦ od h tylko na x takie, »e (A,h⁰) |= ¬ϕ, czyli (A, h⁰) 6|= ϕ, a to jest równowa»ne, »e (A,h) 6|= ∀_xϕ, ale

(A,h) 6|= ∀_xϕi (A, h) |= ¬(∀_xϕ).

Wobec dowolno±ci h otrzymujemy, »e A |= ∃_x¬ϕi A |= ¬(∀_xϕ). Podobnie (A, h) |= ∃x(ϕ ∧ ψ)wtedy i tylko wtedy, gdy

(A,h⁰) |= (ϕ ∧ ψ)dla pewnego warto±ciowania (mo»e) ro»nego od h tylko na x. Ale (A, h⁰) |= (ϕ ∧ ψ) i (A, h⁰) |= ϕi (A, h⁰) |= ψ.

St¡d mamy, »e (A, h) |= ∃xϕ i (A, h) |= ∃xψ, co oznacza z denicji, »e (A, h) |= ∃xϕ ∧ ∃_xψ. Z rozumowania naszego ªatwo wywnioskowa¢, »e formuªa ∃_xϕ ∧ ∃_xψ ⇒ ∃_x(ϕ ∧ ψ) nie jest prawem rachunku kwantykatorów, gdy» fakt, i»

(A,h) |= ∃xϕ ∧ ∃_xψ nie musi poci¡ga¢, »e dla tego samego warto±ciowania h⁰ mamy (A, h⁰) |= ϕi (A, h⁰) |= ψ. Rozpatrzmy np. j¦zyk z dwiema staªymi 0, 1 i zdanie: ∃_xx = 0 ∧ ∃_xx = 1, które jest prawdziwe w ka»dym modelu. Oczywi±cie zdanie

∃_x(x = 0 ∧ x = 1) nie jest prawdziwe w ka»dym modelu j¦zyka, w którym staªe 0, 1 maj¡ ró»ne interpretacje!

Je±li natomiast wiemy, »e x 6∈ Free(ψ), to warunek

(A,h) |= ψ ∧ ∃_xϕpoci¡ga, »e (A, h) |= ψ i (A, h⁰) |= ϕ, dla pewnego warto±ciwania h⁰ pokrywaj¡cego si¦ z h na zbiorze

X \ {x}. Ale z Lematu 1.20 mamy, »e (A, h⁰) |= ψ, co oznacza, »e (A,h) |= ∃_x(ψ ∧ ϕ).

W powy»szym twierdzeniu zebrano najwa»niejsze twierdzenia-prawa rachunku kwantykatorów: formuªy prawdziwe w ka»dym modelu.

Oczywi±cie z matematycznego punktu widzenia bardzo ciekawe te»

jest analizowanie teorii klas modeli.

Denicja

Niech (F, C, R) b¦dzie j¦zykiem i K klas¡ modeli tego j¦zyka.

Symbolem Th(K) oznaczamy teori¦ klasy K: zbiór zda«

prawdziwych w ka»dym modelu z klasy K.

Wiele dziaªów matematyki polega na analizowaniu teorii pewnej klasy moleli. Na pewno du»o ju» wiemy o teorii grup abelowych, czy przestrzeni liniowych nad ustalonym ciaªem. Ka»da z tych klas modeli ma dodatkow¡ wªasno±¢, mianowicie jest elementarna.

Symbolem Mod(F, C, R) oznacza¢ b¦dziemy klas¦ wszystkich modeli j¦zyka (F, C, R).

Denicja

1 Niech T b¦dzie zbiorem formuª j¦zyka (F, C, R) zwanym teori¡. Wtedy

Mod(T ) = {A ∈ Mod(F, C, R); dla ka»degoϕ ∈ T A |= ϕ}

2 Klasa K ⊆ Mod(F, C, R) jest elementarna, je±li istnieje zbiór T formuª taki, »e K = Mod(T ). Zbiór T nazywamy zbiorem aksjomatów klasy K.

W podr¦cznikach algebry zwykle aksjomatyka teorii grup skªada si¦

ze zda«. Np. ∀_x∀_y∀_z x + (y + z) = (x + y) + z to dobrze nam znane prawo ª¡czno±ci dziaªania +, zdanie

∀_x(x + 0 = x ∧ 0 + x = x) orzeka, »e 0 jest elementem neutralnym +. Tym niemniej formuªa

∀_x(x + 0 = x ∧ 0 + x = x) ⇒ (x + 0 = x ∧ 0 + x = x) jest prawem rachunku kwantykatorów. Z drugiej strony prawdziwo±¢ równo±ci x + 0 = x, 0 + x = x w modelu A oznacza ich speªnialno±¢ przy

ka»dym warto±ciowaniu. Aby wykaza¢, »e zdanie

∀_x(x + 0 = x ∧ 0 + x = x) jest te» prawdziwe, rozwa»my warto±ciowanie h : X 7→ A. Wtedy

(A,h⁰) |= (x + 0 = x ∧ 0 + x = x) dla ka»dego warto±ciowania, nie tylko pokrywaj¡cego si¦ z h na zbiorze X \ {x}. Oczywi±cie w rozumowaniu tym nie jest istotne, »e kwantykowali±my formuª¦

(x + 0 = x ∧ 0 + x = x).

Pokazali±my, »e Lemat

Dla dowolnego modelu A i formuªy ϕ:

A |= ∀_xϕ wtw, gdy A |= ϕ.

Zanim opiszemy system (w stylu Hilberta) dla rachunku predykatów trzeba omówi¢ jeszcze jedn¡ wa»n¡ metod¦ budowania formuª, która przy pewnych zaªo»eniach prowadzi od zda« prawdziwych (w danym modelu) do zda« prawdziwych. Zauwa»my, »e do tej pory

nie uwzgl¦dniali±my tego, »e termy opisuj¡ elementy no±nika modelu okre±lonej postaci. Podstawianie polega na zast¦powaniu wolnego wyst¡pienia zmiennej x w formule termem t.

Denicja

Niech p : X 7→ FX b¦dzie funkcj¡ (tak¡, »e p(y) = y dla y 6= x i p(x) = t). Funkcj¦ t¦ mo»emy traktowa¢ jak warto±ciowanie w modelu o no±niku FX , symbolach funkcyjnych q ∈ Fn

interpretowanych jako konteksty q(t₁. . . , t_n) i symbolach relacyjnych interpretowanych jako zbiór pusty. Warto±¢ p(t⁰) b¦dziemy oznacza¢ t⁰(t/x) i nazywa¢ wynikiem podstawienia t za x. Operacj¦ t¦ rozszerzamy na formuªy wzorami:

1 (t₁ =t₂)(t/x) jest formuª¡ t₁(t/x) = t₂(t/x);

2 r(t1, . . . ,tn)(t/x) = r(t1(t/x), . . . , tn(t/x)) dla r ∈ R_n,n ≥ 1;

3 (ϕ  ψ)(t/x) = ϕ(t/x)  ψ(t/x) dla spójnika  arno±ci 2;

4 (¬ϕ)(t/x) = ¬(ϕ((t/x);

5 (∀_xϕ)(t/x) = ∀_xϕi (∀_yϕ)(t/x) = ∀_y(ϕ(t/x));

6 (∃_xϕ)(t/x) = ∃_xϕi (∃_yϕ)(t/x) = ∃_y(ϕ(t/x));

Przykªad Rozwa»my formuª¦ ∃yx = y arytmetyki liczb naturalnych.

Oczywi±cie jest ona twierdzeniem tej arytmetyki. Podstawmy za x term y + 1, otrzymane zdanie ∃_yy + 1 = y nie jest prawdziwe! Jest to mo»liwe poniewa» postawienie to nie jest wªa±ciwe.

Denicja

Term t jest wolny dla zmiennej x i formuªy ϕ, je±li »adne wyst¡pienie zmiennej x w ϕ nie jest w zasi¦gu kwantykatora

∀_y, ∃_y dla zmiennej y wyst¦puj¡cej w t. Wtedy podstawienie t za x w ϕ nazywamy wªa±ciwym.

Lemat

Niech p b¦dzie podstawieniem t za x w ϕ, które jest wªa±ciwe.

Niech h : X 7→ A b¦dzie dowolnym warto±ciowaniem w modelu A, a h^p :X 7→ A warto±ciowaniem takim, »e h^p =hp. Wtedy:

h^p(s) = h(s(t/x)) (11) (A,h) |= ϕ(t/x) i (A, h^p) |= ϕ (12) (A,h) |= ∀_xϕimplies (A, h) |= ϕ(t/x) (13) Dowód oczywi±cie 13 wynika z 12. Dowód 11 prowadzimy

indukcyjnie.

h^p(y) = h^p(y) = (hp)(y) = h(p(y)) = h(y) = h(y(t/x)) dla zmiennej y 6= x. Natomiast h^p(x) = h^p(x) = h(t) = h(x(t/x)), a wtedy dla q ∈ F_n i n ≥ 1 krok indukcyjny dowodu wynika z równo±ci h^p(q(t1, . . . ,tn)) =q^A(h^p(t1), . . . ,h^p(tn)) =q^A(h(t1(t/

x)), . . . , h(t_n(t/x))) = h(q(t₁(t/x) . . . , t_n(t/x))). Przejd»my do dowodu 12. Rozwa»my np. formuª¦ atomow¡ ϕ b¦d¡c¡ równo±ci¡

t1 =t2. Wtedy h^p(ti) =h(ti(t/x)) dla i = 1, 2, wi¦c równo±¢ 12 jest dla ϕ oczywista. Zaªó»my, »e udowodnili±my j¡ dla formuª ϕ₁, ϕ₂ i ϕ = ϕ₁∨ ϕ₂. Wtedy

(A,h) |= ϕ(t/x) i ((A, h) |= ϕ₁(t/x) lub (A, h) |= ϕ₂(t/

x)) i ((A, h^p) |= ϕ₁ lub (A, h^p) |= ϕ₂) i (A, h^p) |= ϕ.

Zauwa»my, »e nie korzystali±my dotychczas z tego, »e podstawienie jest wªa±ciwe dla podanej formuªy ϕ. Rozwa»my wi¦c formuª¦

∀_yϕ(x) i przyjmijmy, »e y 6= x nie wyst¦puje w termie t. Wtedy (A,h) |= (∀_yϕ(x))(t/x) wtw, gdy (A, h) |= ∀_yϕ(t/x) wtw, gdy (A,g) |= ϕ(t/x) dla ka»dego waro±ciowania g identycznego z h na ka»dej zmiennej z 6= y. Poniewa» 12 zachodzi dla ϕ i g mamy:

(A,g) |= ϕ(t/x) i (A, g^p) |= ϕ. Zauwa»my, »e g^p pokrywa si¦ z h na zmiennych ró»nych od x, y i ka»de warto±ciowanie o tej wªasno±ci jest postaci g^p dla warto±ciowania g pokrywaj¡cego si¦ z h na zbiorze X \ {y}, gdy» x 6= y. St¡d otrzymujemy 12 dla formuªy ∀_yϕ(x). Je±li za± x = y, to (∀_xϕ(x))(t/x) = ∀_xϕ, a zmienna x jest zwi¡zana w tej formule. Wtedy 12 wynika z Lematu

1.20.

Teraz mo»emy poda¢ system Hilberta dla rachunku predykatów.

W tym wypadku schematy aksjomatów mo»na dodatkowo opatrzy¢ kwantykatorami ogólnymi "dla ka»dego".

1 Aksjomaty rachunku zda«

A ⇒ (B ⇒ A) (14) (A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)) (15) (¬A ⇒ ¬B) ⇒ (B ⇒ A)) (16)

2 Aksjomaty równo±ci:

t = t (17)

t1 =t2⇒t2 =t1 (18) t₁ =t₂⇒ (t₂=t₃ ⇒t₁=t₃) (19) gdzie t, t₁,t₂,t₃ s¡ dowolnymi termami. Ponadto dla ka»dego symbolu r ∈ R_n, funkcyjnego f ∈ F_m i odpowiedniego ukªadu

termów:

t₁ =s₁ ⇒ (t₂ =s₂ ⇒ (. . . (t_n=s_n⇒ (r(t₁, . . . ,t_n) ⇒r(s₁, . . . ,s_n))) . . .))(20) t1 =s1 ⇒ (t2 =s2 ⇒ (. . . (tm =sm ⇒ (f (t1, . . . ,tm) =f (s1, . . . ,sm))) . . .))(21)

3 Aksjomaty podstawienia: Dla dowolnej formuªy ϕ, zmiennej x i termu t

∀_xϕ ⇒ ϕ(t/x) o ile podstawienie jest wªa±ciwe. (22)

4 Aksjomaty rozdzielno±ci kwantykatora wzgl¦dem implikacji.

Dla dowolnych formuª ϕ, ψ i zmiennej x

∀_x(ϕ ⇒ ψ) ⇒ (∀_xϕ ⇒ ∀_xψ) (23)

5 Doª¡czanie zb¦dnego kwantykatora. Dla formuªy ϕ i zmiennej x 6∈ Free(ϕ)

ϕ ⇒ ∀_xϕ (24)

6 Reguªa wnioskowania:

MP A ⇒ B, A B

Šatwo zauwa»y¢, »e Twierdzenie

Wszystkie aksjomaty s¡ twierdzeniami rachunku predykatów.

Poj¦cie dowodu formuªy deniujemy analogicznie jak dla rachunku zda«. Poniewa» b¦d¡ nas raczej interesowa¢ konkretne teorie, a nie prawa rachunku kwantykatorów, w dowodzie formuªy w teorii T mo»na oprócz powy»szych aksjomatów wykorzystywa¢ zdania z tego zbioru.

Oznaczenia Dla teorii T i formuªy ϕ zapis T ` ϕ stwierdza, »e istnieje dowód ϕ, wykorzystuj¡cy (oporócz aksjomatów) zdania T . Wtedy zbiór

T^∗= {ϕ ∈For; T ` ϕ}

nazywamy zbiorem wszystkich twierdze« tej teorii.

Natomiast zapis T |= ϕ oznacza, »e ϕ ∈ Th(Mod(T )), czyli ϕ jest prawdziwa w ka»dym modelu teorii T .

Twierdzenie (O zgodno±ci: T ` ϕ → T |= ϕ )

Ka»de twierdzenie ϕ teorii T jest prawdziwe w ka»dym modelu teorii T .

Dowód Wobec powy»szego twierdzenia wystarczy zauwa»y¢, »e dla dowolnego modelu A teorii T i warto±ciowania h : X 7→ A takiego,

»e (A, h) |= ϕ, (A, h) |= ϕ ⇒ ψ zachodzi (A, h) |= ψ. Je±li wi¦c formuªy ϕ, ϕ ⇒ ψ s¡ prawdziwe w A, to ψ jest prawdziwa w tym modelu.

Obecnie zajmieny si¦ twierdzeniami rachunku logicznego

dotycz¡cymi dowolnej teorii i dowolnej formuªy. B¦dziemy zamiast T ∪ {ϕ1, . . . , ϕ_n} ` ϕpisa¢ T , ϕ1, . . . , ϕ<sub>n</sub>` ϕ.

Zaczniemy od twierdzenia o dedukcji, które jest wykorzystywane w prawie ka»dym dowodzie. Je±li kto± nie rozumie powy»szgo zdania,

to nale»y mu przypomnie¢, »e zajmujemy si¦ metamatematyk¡.

Zastanawiamy sie jak prowadzi si¦ dowód dowolnego twierdzenia postaci ϕ ⇒ ψ.

Twierdzenie (0 dedukcji)

Dla ka»dej teorii T i formuª ϕ, ψ mamy;

T , ϕ ` ψ i T ` ϕ ⇒ ψ.

Dowód Zacznijmy od prostszej implikacji. Je±li T ` ϕ ⇒ ψ, to tym bardziej T , ϕ ` ϕ ⇒ ψ, a poniewa» T , ϕ ` ϕ, wi¦c i T , ϕ ` ψ.

Dowód implikacji odwrotnej prowadzimy analizuj¡c (indukcyjnie) dowód formuªy ψ. Je±li jest ona aksjomatem, czyli aksjomatem dowolnego systemu lub elementem T , to T ` ψ. Ponadto ψ ⇒ (ϕ ⇒ ψ)jest aksjomatem logiki, wi¦c przez odrywanie dostajemy T ` ϕ ⇒ ψ.

Zaªó»my wi¦c, »e dowód ψ uzyskano przez odrywanie z dowodów

ω ⇒ ψi ω w teorii T ∪ {ϕ}. Z zaªo»enia mamy:

T ` ϕ ⇒ ω i T ` ϕ ⇒ (ω ⇒ ψ).

Poniewa» formuªa (ϕ ⇒ (ω ⇒ ψ)) ⇒ ((ϕ ⇒ ω) ⇒ (ϕ ⇒ ψ)) jest tautologi¡, wi¦c przez dwukrotne odrywanie otrzymujemy

T ` ϕ ⇒ ψ.

Twierdzenie o dedukcji jest nagminnie stosowan¡ metod¡

prowadzenia dowodu implikacji ϕ ⇒ ψ. Inn¡ wa»n¡ metod¡ jest dowodzenie przez zaprzeczenie.

Wniosek (O dowodach przez zaprzeczenie) Je±li T , ¬ψ ` ¬ϕ, to T ` ϕ ⇒ ψ.

Dowód wynika ªatwo z twierdzenia o dedukcji, gdy» mo»emy przyj¡¢, »e T ` ¬ψ ⇒ ¬ϕ, a formuªa (¬ψ ⇒ ¬ϕ) ⇒ (ϕ ⇒ ψ) jest aksjomatem. Pozostaje wykorzysta¢ reguª¦ odrywania.

Wprowadzaj¡c teori¦ nale»y najpierw rozsrzygn¡¢, czy jest ona niesprzeczna.

Denicja

Teori¦ T nazywamy sprzeczn¡, je±li dla pewnej formuªy ϕ zarówno T ` ϕ, jak i T ` ¬ϕ. Teori¦, która nie jest sprzeczna nazywamy niesprzeczn¡.

Zauwa»my, »e taka sytuacja jest niemo»liwa dla konsekwencji |=!

St¡d prosty wniosek:

Wniosek

Je±li teoria T ma model, to jest niesprzeczna.

Inn¡ dosy¢ oczywist¡ wªasno±ci¡ teorii, wynikaj¡c¡ z zaªo»enia, i»

dowód jest sko«czonym ci¡giem formuª, jest tzw. zwarto±¢:

formuªa ϕ ma dowód w T wtw, gdy ma dowód w pewnej sko«czonej podteorii T₁⊆T .

St¡d teoria T jest niesprzeczna wtw, gdy ka»dy jej sko«czony podzbiór jest niesprzeczny.

Zadanie Udowodnij tzw. prawo Dunsa Scota: formuªa

¬ϕ ⇒ (ϕ ⇒ ψ)jest twierdzeniem rachunku kwantykatorów.

Zadanie wykorzystamy w nast¦pnym twierdzeniu.

Twierdzenie

Je±li T jest sprzeczna, to T ` ψ dla ka»dej formuªy ψ.

Dowód Niech ϕ b¦dzie formuª¡ ±wiadcz¡c¡, »e T jest sprzeczn¡

teori¡. Wtedy T ` ϕ, T ` ¬ϕ i T ` ¬ϕ ⇒ (ϕ ⇒ ψ). Stosuj¡c dwukrotnie reguªe odrywania otrzymujemy T ` ψ.

Kilka oznacze« i denicji:

1 ` ϕ oznacza, »e ∅ ` ϕ;

2 ϕ ≡ ψ oznacza, »e ` ϕ ⇒ ψ i ` ψ ⇒ ϕ, czyli formuªy s¡

logicznie równowa»ne;

3 Je±li T ∪ ¬ϕ jest sprzeczna, to mówimy, »e ¬ϕ jest sprzeczna z T .

Zadanie Udowodnij prawa rachunku kwantykatorów:

1 Je±li ` ϕ ⇒ (ϕ ⇒ ψ), to ` ϕ ⇒ ψ.

2 ϕ₁ ⇒ ϕ₂, ψ₁ ⇒ ψ₂ ` (ϕ₂⇒ ψ₁) ⇒ (ϕ₁ ⇒ ψ₂).

3 ϕ ≡ ¬¬ϕ dla ka»dej formuªy ϕ.

4 (ϕ ⇒ ψ) ≡ (¬ψ ⇒ ¬ϕ);

5 ` ¬(ϕ ⇒ ψ) ⇒ ϕ;

6 ` ¬(ϕ ⇒ ψ) ⇒ ¬ψ;

7 ` ϕ ⇒ (ψ ⇒ ¬(ϕ ⇒ ¬ψ)).

8 ` (¬ϕ ⇒ ψ) ⇒ ((¬ϕ ⇒ ¬ψ) ⇒ ϕ). Rozwi¡zania zada« 1, 2 i 8.

Na pocz¡tek bardzo proste twierdzenie: je±li ` ϕ ⇒ (ϕ ⇒ ψ), to stosuj¡c dwukrotnie twierdzenie o dedukcji mamy: ϕ, ϕ ` ψ, a oczywi±cie {ϕ} ∪ {ϕ} = {ϕ} i znów zastosowanie dedukcji daje

` ϕ ⇒ ψ.

Troch¦ trudniej (2): zamiast

ϕ₁ ⇒ ϕ₂, ψ₁⇒ ψ₂` (ϕ<sub>2</sub> ⇒ ψ<sub>1</sub>) ⇒ (ϕ<sub>1</sub> ⇒ ψ<sub>2</sub>) (z tw....) mo»na dowodzi¢ ϕ<sub>1</sub> ⇒ ϕ<sub>2</sub>, ψ<sub>1</sub>⇒ ψ<sub>2</sub>, ϕ<sub>2</sub> ⇒ ψ<sub>1</sub>, ϕ<sub>1</sub> ` ψ₂, co sprowadza si¦

do trzykrotnego zastosowania reguªy odrywania.

Bardzo trudny przykªad (ostatni): z przedostatniego zadnia (wstawiaj¡c za ϕ formuª¦ ¬ϕ) mamy:

¬ϕ, ψ ` ¬(¬ϕ ⇒ ¬ψ) i z dedukcji ψ ` ¬ϕ ⇒ ¬(¬ϕ ⇒ ¬ψ) ale ¬ϕ ⇒ ψ, ¬ϕ ` ψ, wi¦c z 2 ¬ϕ ⇒ ψ, ¬ϕ ` ¬ϕ ⇒ ¬(¬ϕ ⇒ ¬ψ.) Stosuj¡c 1 i twierdzenie o dedukcji otrzymamy:

¬ϕ ⇒ ψ ` ¬ϕ ⇒ ¬(¬ϕ ⇒ ¬ψ)

ale formuªa ¬ϕ ⇒ ¬(¬ϕ ⇒ ¬ψ) jest logicznie równowa»na formule (¬ϕ ⇒ ¬ψ) ⇒ ϕ, co ko«czy dowód.

Twierdzenie (reuctio ad absurdum)

Je±li formuªa ¬ϕ jest sprzeczna z teori¡ T , to T ` ϕ.

Dowód Niech ψ b¦dzie taka, »e T , ¬ϕ ` ψ i T , ¬ϕ ` ¬ψ. Z tw. o dedukcji T ` ¬ϕ ⇒ ψ i T ` ¬ϕ ⇒ ¬ψ, wi¦c stosuj¡c prawo 8 z zadania otrzymujemy T ` ϕ.

Twierdzenie (Henkina)

Ka»dy nieprzeczny zbiór formuª ma model.

Twierdzenie (O peªno±ci)

Je±li formuªa ϕ jest prawdziwa we wszystkich modelach teorii T , to ϕma dowód w T .

Dowód Nie wprost: Jeªi T 6` ϕ, to z 1.35 T ∪ {¬ϕ} jest

niesprzeczn¡ teori¡. W ka»dym modelu tej teorii (a takie istniej¡ z tw. Henkina) formuªy ϕ i ¬ϕ s¡ prawdziwe, co nie jest mo»liwe.

Logika matematyczna zajmuje si¦ modelami w ogólno±ci.

Informatyka teoretyczna zajmuje si¦ tylko modelami sko«czonymi tj.

okre±lonymi na sko«czonych no±nikach. Pomysª, aby

systematycznie bada¢ tylko rodziny sko«czonych 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 (algorytmów poszukiwania odpowiedzi na pytania formuªowane w

systemach relacyjnych baz danych). Najwa»niejszym prekursorem tej dziedziny informatyki teoretycznej jest Ronald Fagin.

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 (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

Zbór Th(Mod((F, C, R))) wszystkich zda« ustalonego j¦zyka b¦d¡cych twierdzeniami rachunku kwantykatoró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 ∈ Th(Mod((F, C, R))) ⇔ ∃_xR(x, y) mamy tez¦.

Twierdzenie Churcha, które w ogólnej postaci brzmi nast¦puj¡co:

Twierdzenie (Church 1936)

Dla j¦zyków (F, C, R) posiadaj¡cych symbole relacyjne, które nie s¡ jednoargumentowe zbiór Th(Mod((F, C, R))) wszystkich zda«

prawdziwych w ka»dym modelu j¦zyka (F, C, R) nie jest rekurencyjny.

implikuje, »e

Wniosek

Zaªó»my, »e j¦zyk (F, C, R) ma symbole relacyjne, które nie s¡

jednoargumentowe. Wtedy dopeªnienie zbioru Th(Mod((F, C, R))) wszystkich zda« prawdziwych w ka»dym modelu j¦zyka (F, C, R) nie jest rekurencyjnie przeliczalny.

Ciekawe, »e dla sko«czonych modeli sytuacja jest zupeªnie inna.

Twierdzenie (Trakhtenbrot)

Zaªó»my, »e j¦zyk (F, C, R) ma symbole relacyjne, które nie s¡

jednoargumentowe. Wtedy zbiór Th(Mod_F((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¡

twierdzeniami 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 zachodzi twierdzenie o peªno±ci. Dlaczego? Z powy»szych rozwa»a« wiemy, »e jego istnienie poci¡ga, »e zbiór Th(Mod_F((F ,C, R))) jest r.e.

Z twierdzenia o peªno±ci wynika

Twierdzenie (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 (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 t_n b¦dzie zdaniem, które mówi, »e model ma przynajmniej n elementóe i T = {t_n,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.

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. Σ¹₁- formuªy lub egzystencjalne formuªy II-go rz¦du.

Nietrudo wykaza¢, »e postawienie wi¦kszej ilo±ci kwantykatorów typu ∃_Q daje formuª¦, która jest logicznie równowa»na z

Σ¹₁-formuª¡.

Dla prostoty b¦dziemy te» zakªada¢, »e zajmujemy si¦ teori¡

grafów, czyli modeli z jedn¡ relacj¡ binarn¡.

Twierdzenie

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 "zgadn¡¢" interpretacj¦ P^G predykatu P i nast¦pnie mo»e bada¢ deterministycznie i we wielomianowym czasie, czy powstaª model formuªy ϕ.

Poka»emy, »e zachodzi te» implikacja w drug¡ stron¦, czyli Twierdzenie (Fagin)

Klasa wªasno±ci grafowych wyra»alnych w Σ¹₁-logice jest równa NP.

Dowód jest podobny do dowodu tw. Cooka. Dla MT dziaªaj¡cej w czasie n^k i lewostronnie ograniczonej rozstrzygaj¡cej pewien zbiór grafów skonstruujemy »¡dan¡ formuª¦. Ponownie rozwa»ymy tablic¦ kwadratow¡ rozmiaru n^k. Przypomnijmy, »e w dowodzie wprowadzili±my zbiór zmiennych zdaniowych T_i,j,Y potrójnie indeksowany krokiem obliczenia i, numerem komórki j i jej zawarto±ci¡ Y ∈ Γ. Tutaj wprowadzimy:

1 predykaty T_Y(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 C₀, . . . ,C_q−1 odpowiadaj¡ce za wybór m-tej instrukcji;

3 zapis k-cyfrowych liczb naturalnych w systemie o podstawie n, czyli pozwalaj¡cy na "liczenie" od 0 do n^k−1;

4 predykaty S_j(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}. . . ∃_TYm∃_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 S₁(x, y) jest funkcj¡ nast¦pnika, przykªadowo

∀_x∀_y,zS₁(x, y) ∧ S₁(x, z) ⇒ y = z to jest funkcja cz¦±ciowa(25)

∀_x∀_y,zS₁(y, x) ∧ S₁(z, x) ⇒ y = z która jest ró»nowarto±ciowa(26)

∀_y¬S₁(y, x) denicja zera, ozn.ζ(x)(27)

∀_y¬S1(x, y) denicja n − 1, η(x) (28)

2 Formuªy uniwersalne opisuj¡ce relacje 2j-argumentowe Sj(x, y) deniujemy indukcyjnie:

S_j(x, y) ⇔ ((S₁(x_j,y_j) ∧x₁ =y₁∧ . . . ∧x_j−1=y_j−1)∨

(η(x_j) ∧ ζ(y_j) ∧S_j−1(x1, . . . ,x_j−1,y1, . . . ,y_j−1))

3 Pierwszy wiersz tablicy opisuje konguracj¦ 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ª¦ uniwersaln¡ (dopisz kwantykatory "dla ka»dego"):

(S_k(x⁰,x)∧S_k(y⁰,y)∧S_k(y, y⁰⁰)∧T_x(x⁰,y⁰)∧T_y(x⁰,y)∧T_z(x⁰,y⁰⁰)∧C_c(x⁰))

⇒T_d(x, y)

Trzeba jeszcze zapewni¢ jednoznaczno±¢ wyboru:

(C₀(x) ∨ . . . C_q−1(x)) ∧ (

q−1

_

j=0

¬C_j(x)) Na koniec mo»emy sobie postawi¢ pytanie, czy istnieje charakteryzacja logiczna klasy P?

Tak¡ charakteryzacj¦ podali niezale»nie Imermann, Vardi i

Papadimitriou. 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 wyst¦puj¡. Mo»na zauwa»y¢, »e skªadniki formuªy ϕ opisuj¡ce obliczenia maszyny b¦d¡

uniwersalnymi formuªami hornowskimi. St¡d zachodzi Twierdzenie

Klasa wªasno±ci grafowych wyra»alnych w egzystencjalnej 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 kwantykatorów jest ona alternatyw¡ literaªów, z których co najwy»ej jeden 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¡.