System Hilberta

1 System Hilberta

2 Rezolucja

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 6 n z_i jest aksjomatem lub dla pewnych j, k 6 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 2, drugie 3, 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.

Obecnie zajmieny si¦ twierdzeniami rachunku logicznego dotycz¡cymi dowolnej teorii i dowolnej formuªy.

Denicja

Niech T b¦dzie dowolnym zbiorem formuª zwanym teori¡.

Dowodem zaªo»eniowym formuªy ϕ w teorii T nazywamy ka»dy dowód, który wykorzystuje elementy T jako dodatkowe aksjomaty.

Fakt, »e ϕ ma taki dowód b¦dziemy zapisywa¢ symbolicznie:

T ` ϕ.

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 ϕ ⇒ ψ.

Najpierw proste zadanie.

Zadanie Wyka», »e A ⇒ A ma dowód w systemie Hilberta.

Zauwa»my,»e A ⇒ (A ⇒ A) ⇒ A) powstaje z aksjomatu 1 przez podstawienie A ⇒ A za B, A ⇒ (A ⇒ A) przez podstawienie A za B. Natomiast

(A ⇒ (A ⇒ A) ⇒ A)) ⇒ ((A ⇒ (A ⇒ A)) ⇒ (A ⇒ A)) jest instancj¡ aksjomatu 2. Stosuj¡c dwa razy MP otrzymujemy dowód A ⇒ A.

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.

W systemach hilbertowskich poszukiwanie dowodu jest bardzo trudne, gdy» nie ma prostych zale»no±ci mi¦dzy formuª¡ a jej dowodem. Metoda rezolucji, zaproponowana przez J.A. Robinsona w 1965 roku, umo»liwia sprawne poszukiwanie dowodu. W

przypadku rachunku zda« bazuje ona na postaci normalnej koniunkcyjnej dla formuª. Jest te» ona podstaw¡ programowania logicznego. Wykorzystuje si¦ j¡ te» w aparatach wnioskowania systemów ekspertowych.

Przypomnijmy, »e formuªa jest w postaci normalnej

koniunkcyjnej, PNK, gdy jest koniunkcj¡ alternatyw literaªów.

Twierdzenie

Dla ka»dej formuªy rachunku zda« istnieje równowa»na formuªa w PNK.

Algorytm przeksztaªacania formuªy do równowa»nej w PNK polega na wykonaniu nast¦puj¡cych operacji, które zachowuj¡ logiczn¡

równowa»no±¢.

1 Usu« wszystkie operatory logiczne z wyj¡tkiem negacji, koniunkcji i alternatywy, korzystaj¡c ze znanych

równowa»no±ci.

2 Przenie± wszystkie negacje do ±rodka korzystaj¡c z praw de Morgana:

¬(A ∨ B) ≡ ¬A ∧ ¬B

¬(A ∧ B) ≡ ¬A ∨ ¬B

3 Usu« wielokrotne zaprzeczenia korzystaj¡c z równowa»no±ci

¬¬A ≡ A.

4 Stosuj wielokrotnie prawa rozdzielczo±ci

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ B) A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ B) w celu usuni¦cia koniunkcji z alternatyw.

Przykªad przebiegu algorytmu

(¬p → ¬q) → (p → q) ≡ ¬(¬p → ¬q) ∨ (p → q)

≡ ¬(¬¬p ∨ ¬q) ∨ (¬p ∨ q)

≡ (¬¬¬p ∧ ¬¬q) ∨ (¬p ∨ q)

≡ (¬p ∧ q) ∨ (¬p ∨ q)

≡ (¬p ∨ ¬p ∨ q) ∧ (q ∨ ¬p ∨ q)

Denicja

Klauzul¡ nazywamy zbiór literaªów, rozumiany jako alternatywa tych literaªów. Formuª¡ w postaci klauzulowej nazywamy zbiór klauzul, rozumiany jako koniunkcja tych klauzul.

Przykªad Formuªa (¬p → ¬q) → (p → q) jest równowa»na nast¦puj¡cej formule w postaci klauzulowej: {{¬p, q}, {q, ¬p}}.

B¦dziemy te» stosowa¢ uproszczon¡ notacj¦, w której ta formuªa ma zapis {pq, qp}.

Denicja

Niech S, S⁰ b¦d¡ zbiorami klauzul. Zapis S ≈ S⁰ oznacza, »e S jest speªnialny wtw, gdy S⁰ jest speªnialny.

Denicja

Klauzul¡ nazywamy zbiór literaªów, rozumiany jako alternatywa tych literaªów. Formuª¡ w postaci klauzulowej nazywamy zbiór klauzul, rozumiany jako koniunkcja tych klauzul.

Przykªad Formuªa (¬p → ¬q) → (p → q) jest równowa»na nast¦puj¡cej formule w postaci klauzulowej: {{¬p, q}, {q, ¬p}}.

B¦dziemy te» stosowa¢ uproszczon¡ notacj¦, w której ta formuªa ma zapis {pq, qp}.

Denicja

Niech S, S⁰ b¦d¡ zbiorami klauzul. Zapis S ≈ S⁰ oznacza, »e S jest speªnialny wtw, gdy S⁰ jest speªnialny.

Metoda rezolucji pozwala rozstrzygn¡¢, czy formuªa w postaci klauzulowej jest speªnialna, przez zast¦powanie zbioru klauzul S zbiorem S⁰ takim, »e S ≈ S⁰.

Odt¡d C oznacza klauzul¦, a l literaª. Wtedy l⁻ jest literaªem równowa»nym z ¬l (czyli l⁻ =p o ile l = ¬p).

Zauwa»my, »e nie zakªadamy, »e C ma by¢ niepusty! Symbolem  oznaczamy pust¡ klauzul¦, a ∅ pusty zbiór klauzul. Wtedy

zakªadamy,»e

1 Pusty zbiór klauzul ∅ jest formuª¡ prawdziw¡.

2 Pusta klauzula  jest niespeªnialna.

Dowody podanych zda« s¡ proste, cho¢ maªo zrozumiaªe dla nie-matematyka. Przykªadowo klauzula  nie zawiera »adnego literaªu, wi¦c przy »adnym warto±ciowaniu jej literaª nie jest speªniony.

Przykªad W systemie Hilberta byªa tylko jedna reguªa wnioskowania: reguªa odrywania:

MP A ⇒ B, A B

Wykorzystuj¡c postaci klauzulowe formuª mo»emy j¡ zapisa¢

nast¦puj¡co:

MP {AB, A}

{B}

zakªadaj¡c oczywi±cie, »e A, B s¡ zmiennymi. Tym niemiej przykªad ten obja±nia dokªadnie o co chodzi w regule rezolucji: o wyszukanie dwóch klauzul zawieraj¡cych par¦ literaªow komplementarnych i zast¡pienie ich now¡ klauzul¡. Metoda ta powinna zachowywa¢

speªnialno±¢!

Zauwa»my jednak, »e (A ⇒ B) ∧ A 6 ≡B, gdy» zmienna B jest speªnialna przy dwóch warto±ciowaniach zmiennych A, B, a formuªa (A ⇒ B) ∧ A tylko przy takim, które zarówno A jak i B przypisuje prawd¦.

W Prologu stosuje si¦ tzw. SLD rezolucj¦, której przykªadem jest reguªa:

MP {AB, B}

{A}

Reguªa rezolucji Niech C₁ i C₂ b¦d¡ klauzulami takimi, »e l ∈ C₁,l⁻ ∈C₂. Mówimy wtedy, »e klauzule te koliduj¡ ze sob¡, gdy» zawieraj¡ par¦ literaªów komplementarnych. Rezolwent¡

klauzul C₁,C₂ nazywamy klauzul¦ C postaci:

R(C1,C2) = (C1\ {l}) ∪ (C2\ {l⁻}).

Klauzule C₁,C₂ nazywamy macierzystymi dla C.

Twierdzenie

Rezolwenta C klauzul C1,C2 jest speªnialna wtw, gdy koniunkcja klauzul C₁,C₂ jest speªnialna.

Dowód Je±li koniunkcja klauzul C1,C2 jest speªnialna przy pewnym warto±ciowaniu v zmiennych w nich wyst¦puj¡cych, a l, l⁻ jest par¡

literaªów usuwanych przy tworzeniu rezolwenty C, to na pewno W C1 lub w C2 wyst¦puje literaª k ró»ny od nich, który ma warto±¢

logiczn¡ 1 przy warto±ciowaniu v. Poniewa» k wyst¦puje w C otrzymujemy, »e v(C) = 1. Odwrotnie, je±li v(C) = 1, a np.

wszystkie literaªy z (C2\ {l⁻})maj¡ przypisany faªsz, to

rozszerzaj¡c v kªad¡c v(l⁻) =1 otrzymujemy warto±ciowanie, przy którym C₁,C₂ s¡ speªnialne.

Opis algorytmu rezolucji Wej±cie: Zbór klauzul S.

Wyj±cie: S jest speªnialny lub nie.

W czasie dziaªania algorytmu wyznacza si¦ ci¡g S_i zbiorów literaªów przez prost¡ iteracj¦, kontroluj¡c, czy ci¡g si¦ stabilizuje. Niech S0=S. Zaªó»my, »e wyznaczyli±my Si. Wybieramy z Si par¦

klauzul koliduj¡cych C₁,C₂, króre jeszcze nie byªy analizowane.

Tworzymy ich rezolwent¦ C i deniujemy S_i+1 =S_i∪ {C}. Je±li C = , to ko«czymy algorytm stwierdzaj¡c, »e S nie jest

speªnialny. Je±li nie ma ju» w S_i par klauzul koliduj¡cych, które nie byªy analizowane, to ko«czymy algorytm stwierdzaj¡c, »e S jest speªnialny.

Przykªady

1 Algorytm rezolucji implementuje si¦ (równie» zapisuje) na ró»ne sposoby. Najpro±ciej mo»na tworzy¢ kolejne zbiory klauzul zgodnie z reguª¡ rezolucji. Wtedy stosuje si¦ ró»ne notacje. My b¦dziemy u»ywa¢ wprowadzonej notacji.

Udowodnimy t¡ metod¡, »e formuªa

(p ⇒ q) ⇒ ((p ∨ r) ⇒ (q ∨ r)) jest tautologi¡, czyli jej negacja nie jest speªnialna. Najpierw wyznaczymy jej PNK:

¬((p ⇒ q) ⇒ ((p ∨ r) ⇒ (q ∨ r))) ≡ (p ⇒ q) ∧ ¬((p ∨ r) ⇒ (q ∨ r)) (¬p ∨ q) ∧ (p ∨ r) ∧ ¬(q ∨ r) ≡ (¬p ∨ q) ∧ (p ∨ r) ∧ ¬(q) ∧ ¬(r) Czyli wej±ciem dla algorytmu jest nast¦puj¡cy zbiór klauzul:

{(1)pq, (2)pr, (3)q, (4)r}, a kolejne zbiory klauzul to:

1 {pq, pr, q, r, (5)p} , dodali±my rezolwent¦ (2), (4);

2 {pq, pr, q, r, p, (6)q} dodali±my rezolwent¦ (1), (5);

3 {pq, pr, q, r, p, q, } rezolwenta (3), (6) jest pusta.

1 W Mini-Prologu program jest zbiorem (koniunkcj¡) klauzul hornowskich, w których dokªadnie jeden literaª jest zmienn¡.

Tzw. klauzula celu nie mo»e zawiera¢ takiego literaªu, jest wi¦c równowa»na negacji koniunkcji zmiennych. Przykªadowo:

niech {pq, qr, p} b¦dzie programem. Fakt, »e r jest konsekwencj¡ logiczn¡ tego programu jest równowa»ny niespeªnialno±ci zbioru {(1)pq, (2)qr, (3)p, (4)r}. Faktycznie, bior¡c rezolwent¦ (4), (2) otrzymamy q, a jej rezolwenta z (1) to p i otrzymamy klauzul¦ pust¡ tworz¡c rezolwent¦ z (3).

Czyli mamy od razu, »e

Wniosek (Poprawno±¢ metody rezolucji)

Je±li na podstawie algorytmu rezolucji zostanie wyprowadzona klauzula pusta, to wej±ciowy zbiór klauzul jest niespeªnialny.

Trudniej udowodni¢

Twierdzenie (Peªno±¢ metody rezolucji)

Je±li wej±ciowy zbiór klauzul jest niespeªnialny, to za pomoc¡

metody rezolucji mo»na wyprowadzi¢ klauzul¦ niespeªnialn¡.