Metody dowodowe: wst¦p

Metody dowodowe: wst¦p

Jerzy Pogonowski

Zakªad Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka

pogon@amu.edu.pl

MDTiAR

Wymagania

Korzysta¢ b¦dziemy z wiadomo±ci przekazanych na kursach:

Wprowadzenie do logiki, Logika I, Logika II.

Kurs Matematyczne podstawy kognitywistyki nie byª obowi¡zkowy dla studentów obecnego V roku. Potrzebne nam poj¦cia matematyczne b¦d¡ omawiane na bie»¡co.

Konwersatoria 17 prowadzi Jerzy Pogonowski Kolokwium I (na konwersatorium 8)

Konwersatoria 914 prowadzi Szymon Chlebowski Kolokwium II (na konwersatorium 15)

Syllabus jest dost¦pny na stronach ZLiK.

Kurs ko«czy si¦ egzaminem.

1 Preliminaria matematyczne i logiczne oraz uwagi historyczne

2 Ogólne operacje konsekwencji

3 Metoda aksjomatyczna

4 Postacie normalne i preksowe

5 Tablice analityczne Smullyana

6 Rezolucja

7 Dedukcja naturalna

8 Rachunki sekwentów

9 Dual tableaux (diagramy Rasiowej-Sikorskiego)

10 Metody dowodowe: zalety, wady, wzajemne zwi¡zki

11 Wybrane twierdzenia metalogiczne i metody ich dowodzenia

12 Teoria rekursji a metody dowodowe

13 Automatyzacja rozumowa«

14 Rozstrzygalno±¢

15 Dowody matematyczne.

1 Fitting, M. 1996. First-Order Logic and Automated Theorem Proving.

Springer, Berlin.

2 Šawrow, I.A., Maksimowa, Š.L. 2004. Zadania z teorii mnogo±ci, logiki matematycznej i teorii algorytmów. Wydawnictwo Naukowe PWN, Warszawa.

3 Pogorzelski, W.A. 1992. Elementarny sªownik logiki formalnej.

Wydawnictwo Filii Uniwersytetu Warszawskiego, Biaªystok.

4 Stanford Encyclopedia of Philosophy: http://plato.stanford.edu/

(artykuªy po±wi¦cone teorii dowodu oraz automatyzacji rozumowa«:

The development of proof theory, Automated reasoning).

Proponuj¦ tak»e lektur¦ zamieszczonych na stronach ZLiK materiaªów dydaktycznych: Pani Dr Doroty Leszczy«skiej-Jasion, Pana Prof.

Mariusza Urba«skiego oraz Pana prof. Andrzeja Wi±niewskiego.

1 D'Agostino, M., Gabbay, D., Hähnle, R., Posega, J. (Eds.) 1999.

Handbook of Tableaux Methods. Kluwer Academic Publishers, Dordrecht Boston London.

2 Gallier, J. 2003. Logic for Computer Science. Foundations of

Automated Theorem Proving. Dover Publications, Mineola, New York.

3 Kaye, R. 2007. The Mathematics of Logic. A guide to completeness theorems and their applications. Cambridge University Press,

Cambridge.

4 Negri, S., von Plato, J. 2001. Structural Proof Theory. Cambridge University Press, Cambridge.

5 Nerode, A., Shore, R.A. 1997. Logic for Applications. Springer-Verlag, New York.

6 Orªowska, E., Goli«ska-Pilarek, J. 2011. Dual Tableaux: Foundation, Methodology, Case Studies. Springer, Dordrecht Heidelberg London New York.

7 Smullyan, R. 1968. First-Order Logic. Springer, Berlin.

Uciechy szkolne

Podano kilkaset dowodów Twierdzenia Pitagorasa. Znasz co najmniej jeden?

Czy istnieje najwi¦ksza liczba pierwsza?

Szok cywilizacyjny: wielko±ci niewspóªmierne. Czy równanie n² =2m² ma rozwi¡zanie dla wzgl¦dnie pierwszych liczb m, n ∈ N, m > 0?

Czy√ 2

√2 jest liczb¡ wymiern¡ czy niewymiern¡?

Jak obliczy¢√ 2

√2

√2

√2···

?

Czy mo»liwa jest kwadratura koªa?

Szkoªa uczyªa gªownie prostych algorytmów. Pami¦tasz algorytm dzielenia Euklidesa? Urocze uªamki ªa«cuchowe wygoniono ze szkoªy.

Dlaczego ró»niczkowanie jest ªatwiejsze od caªkowania?

Uciechy studenckie

Wykªadnicze okrucie«stwo algorytmu 0 − 1. Có», M¡dra Ksi¦ga nie obiecywaªa, »e wszystkie algorytmy b¦d¡ dziaªa¢ w czasie

wielomianowym.

Okrucie«stwo metody aksjomatycznej: co dobre dla teorii, niekoniecznie jest przyjazne (Czªowiekowi, a nawet Maszynie).

Metody dowodowe popularne wspóªcze±nie: tablice analityczne, rezolucja, dedukcja naturalna, rachunki sekwentów.

Wspóªcze±nie stosowane notacje (znasz) i notacje porzucone (Frege, Le±niewski).

Algorytmiczne po»ytki z diagramów Venna i Carrolla.

Rozwa»my dwa przykªady argumentacji:

Nasza Pani od Biologii i Nietoperze

Milicja, Wrocªaw i ja

Nasza Pani od Biologii i Nietoperze

Nasza Pani od Biologii opowiada o Nietoperzach: Je±li Nietoperze nie maj¡ piór, to: s¡ Ptakami, o ile fruwaj¡. Nasza Pani od Biologii wyci¡ga z kieszeni Nietoperza i stwierdza: Nietoperze nie maj¡ piór.

Nasza Pani od Biologii zagl¡da do podr¦cznika systematyki Zwierz¡t i stwierdza: Ale przecie» Nietoperze nie s¡ Ptakami. Nasza Pani od Biologii konkluduje: A zatem Nietoperze nie fruwaj¡.

p: Nietoperze maj¡ pióra.

q: Nietoperze fruwaj¡.

r: Nietoperze s¡ Ptakami.

Przesªanka: ¬p → (q → r) Przesªanka: ¬p

Przesªanka: ¬r Wniosek: ¬q

Nasza Pani od Biologii i Nietoperze

Drzewo argumentacji (dowodu) ma posta¢ nast¦puj¡c¡:

¬r

¬p → (q → r) ¬p

q → r

¬q

W tej argumentacji posªu»ono si¦ kolejno reguªami:

modus ponens modus tollens.

Argumentacja jest poprawna z logicznego punktu widzenia. Wniosek jest faªszywy, a zatem która± z przesªanek jest faªszywa.

Milicja, Wrocªaw i ja

Czy na podstawie uznania nast¦puj¡cych stwierdze«:

Je±li nie udowodniono podejrzanemu popeªnienia morderstwa, to:

stwierdzono samobójstwo denata lub wykonano sentencj¦ wyroku, o ile udaªo si¦ zatrzyma¢ podejrzanego.

Podejrzanemu nie udowodniono popeªnienia morderstwa.

Nie stwierdzono samobójstwa denata.

Udaªo si¦ zatrzyma¢ podejrzanego.

gotowa jeste± uzna¢ stwierdzenie:

Wykonano sentencj¦ wyroku?

Uwaga: musimy podj¡¢ decyzj¦ dotycz¡c¡ reprezentacji skªadniowej pierwszej przesªanki.

Milicja, Wrocªaw i ja

Zdania proste w tym tek±cie:

p: Udowodniono podejrzanemu popeªnienie morderstwa.

q: Stwierdzono samobójstwo denata.

r: Udaªo si¦ zatrzyma¢ podejrzanego.

s: Wykonano sentencj¦ wyroku.

Przesªanka: ¬p → (q ∨ (r → s)) Przesªanka: ¬p

Przesªanka: ¬q Przesªanka: r Wniosek: s

Milicja, Wrocªaw i ja

Drzewo argumentacji (dowodu):

r

¬q

¬p ¬p → (q ∨ (r → s))

q ∨ (r → s) r → s

s

W tej argumentacji posªu»ono si¦ kolejno reguªami:

modus ponens (reguªa odrywania) opuszczania alternatywy

modus ponens.

Argumentacja jest poprawna z logicznego punktu widzenia.

Ku Wrogiej Sztucznej Inteligencji?

Dowody (w sensie logicznym): dobrze okre±lone obiekty syntaktyczne.

Dowody matematyczne: argumentacje stosowane w matematyce.

Dogmat: ka»dy dowód matematyczny mo»e zosta¢ przeksztaªcony w dowód w sensie logicznym.

Algorytm: czysto mechaniczna procedura, pozwalaj¡ca w sko«czonej liczbie prostych, z góry okre±lonych kroków uzyska¢ wynik (odpowied¹, rozwi¡zanie).

Intuicyjne poj¦cie procedury obliczalnej poddano formalizacji, na wiele sposobów: funkcje rekurencyjne, maszyny Turinga, systemy Posta, algorytmy Markowa, rachunek λ Churcha, itd.

Uzyskano wyniki dotycz¡ce niezupeªno±ci oraz nierozstrzygalno±ci wa»nych teorii matematycznych.

Optymistyczne pocz¡tki

Pocz¡tki logiki: Arystoteles, Stoicy, logicy ‘redniowiecza, Leibniz.

Pocz¡tki logiki matematycznej: De Morgan, Boole, Peano, Frege, Pierce, Schröder, Russell, Le±niewski, Šukasiewicz,. . .

Nurt algebraiczny w logice

Stanowiska lozoczne: logicyzm, formalizm, intuicjonizm Inspiracje matematyczne

Szkoªa Lwowsko-Warszawska Podstawy matematyki i metalogika

4T: teoria dowodu, teoria modeli, teoria rekursji, teoria mnogo±ci Uwaga: bardziej szczegóªowe informacje historyczne podawane b¦d¡

podczas kolejnych wykªadów.

Zªoty wiek XX

David Hilbert (18621943) i jego program Ernst Zermelo (18711953): teoria mnogo±ci

Emil Post (18971954): algebra logiki, systemy Posta Gerhard Gentzen (19091945): dedukcja naturalna, sekwenty Alan Turing (19121954): teoria oblicze«

Jacques Herbrand (19081931): twierdzenie Herbranda, obliczalno±¢

Thoralf Skolem (18871963): teoria mnogo±ci, arytmetyka Kurt Gödel (19061978): niezupeªno±¢ PM, teoria mnogo±ci Luitzen Egbertus Jan Brouwer (18811966): intuicjonizm Alonzo Church (19031995): nierozstrzygalno±¢ KRP Stanisªaw Ja±kowski (19061965): dedukcja naturalna Alfred Tarski (19031983): teoria modeli

Adolf Lindenbaum (19041941): lemat Lindenbauma

Nadchodzi Matrix

Bªogosªawiony Rajmund Lull (Doctor Illuminatus, 12321315): logika w sªu»bie nawracania niewiernych.

Gottfried Wilhelm von Leibniz (16461716): prekursor logiki formalnej.

Od mechanicznych kalkulatorów do elektronicznych maszyn cyfrowych.

Matematyczne reprezentacje oblicze«. Teza Churcha-Turinga.

Automatyczne dowodzenie twierdze«: ile mo»na osi¡gn¡¢?

Marciszewski, W., Murawski, R. 1995. Mechanization of reasoning in a historical perspective. Rodopi, Amsterdam-Atlanta.

Ligonniére, R. 1992. Prehistoria i historia komputerów. Ossolineum, Wrocªaw-Warszawa-Kraków.

Drzewem (o korzeniu x0) nazwiemy ka»dy ukªad hX , R, x0itaki, »e:

1 hX , Ri jest grafem o zbiorze wierzchoªków X i zbiorze kraw¦dzi R ⊆ X × X ;

2 R jest cz¦±ciowym porz¡dkiem w X ;

3 x₀ jest elementem R-najmniejszym w X ;

4 zbiór wszystkich R-poprzedników ka»dego wierzchoªka jest liniowo uporz¡dkowany przez relacj¦ R.

Li±¢mi drzewa D nazywamy wszystkie te jego wierzchoªki, które nie maj¡ R-nast¦pników.

Je±li (x, y) ∈ R jest kraw¦dzi¡ w D, to x nazywamy przodkiem y, a y nazywamy potomkiem x. Je±li (x, y) ∈ R − R² jest kraw¦dzi¡ w D, to x nazywamy bezpo±rednim przodkiem y, a y nazywamy bezpo±rednim potomkiem x.

Ka»dy podzbiór zbioru wierzchoªków drzewa D, który jest

uporz¡dkowany liniowo przez R nazywamy ªa«cuchem w D (czasem:

±cie»k¡ w D). Ka»dy ªa«cuch maksymalny (wzgl¦dem inkluzji) w D nazywamy gaª¦zi¡ w D.

Przez dªugo±¢ ªa«cucha P rozumiemy liczb¦ elementów zbioru P.

Rz¦dem wierzchoªka x nazywamy moc zbioru wszystkich

bezpo±rednich potomków x. Rz¦dem drzewa D jest kres górny rz¦dów wszystkich wierzchoªków drzewa D.

Drzewo D jest sko«czone, je±li zbiór jego wierzchoªków jest sko«czony;

w przeciwnym przypadku jest niesko«czone. Drzewo D jest rz¦du sko«czonego (jest sko«czenie generowane), je±li ka»dy jego wierzchoªek ma rz¡d sko«czony.

Przez indukcj¦ deniujemy poziomy drzewa:

1 poziom zerowy to zbiór jednoelementowy, zªo»ony z korzenia drzewa;

2 poziom k + 1 to zbiór wszystkich bezpo±rednich nast¦pników wierzchoªków poziomu k.

Oswajanie drzew

W dalszym ci¡gu b¦dziemy rozwa»a¢ gªównie drzewa sko«czone lub rz¦du sko«czonego. Bli»ej oswoimy si¦ z drzewami na konwersatorium.

Drzewo dwójkowe to drzewo, w którym ka»dy wierzchoªek ma co najwy»ej dwóch bezpo±rednich potomków. Peªne drzewo dwójkowe to drzewo, w którym ka»dy wierzchoªek ma dokªadnie dwóch

bezpo±rednich potomków.

Przez drzewo znakowane (elementami ze zbioru L) rozumiemy par¦

uporz¡dkowan¡ (D, f ), gdzie D jest drzewem, a f jest funkcj¡ ze zbioru wierzchoªków drzewa D w zbiór L. Zwykle L b¦dzie pewnym zbiorem formuª.

Graczne reprezentacje drzew s¡ rysunkami, na których wierzchoªki (jako± znakowane  punktami, liczbami, formuªami, itd.) poª¡czone s¡ liniami, odpowiadaj¡cymi kraw¦dziom. Przy tym, je±li hX , R, x₀i jest drzewem, to na rysunku zaznaczamy tylko kraw¦dzie nale»¡ce do R − R².

Lemat Königa. Je±li drzewo D = hX , R, x₀i rz¦du sko«czonego jest niesko«czone, to ma gaª¡¹ niesko«czon¡.

Dowód. Przypu±¢my, »e D jest niesko«czone. Zdeniujemy gaª¡¹ niesko«czon¡ {x₀,x₁,x₂, . . .}w D przez indukcj¦ matematyczn¡.

Element x0 (czyli korze« drzewa D) jest pierwszym elementem konstruowanej gaª¦zi. Poniewa» D jest niesko«czone, wi¦c x₀ ma niesko«czenie wiele R-nast¦pników.

Przypu±¢my, »e x0,x1,x2, . . . ,xn−1 zostaªy zdeniowane tak, »e xi nale»y do i-tego poziomu drzewa D oraz x_i ma niesko«czenie wiele

R-nast¦pników. Z zaªo»enia, x_n−1 ma tylko sko«czenie wiele bezpo±rednich R-nast¦pników. Poniewa» xn−1 ma niesko«czenie wiele R-nast¦pników, wi¦c co najmniej jeden z jego bezpo±rednich R-nast¦pników tak»e ma niesko«czenie wiele R-nast¦pników. Wybieramy wi¦c element x_n z n-tego poziomu drzewa D o tej wªa±nie wªasno±ci. Wtedy xn ma niesko«czenie wiele R-nast¦pników. Poniewa» jest tak dla ka»dego n, pokazali±my istnienie niesko«czonej gaª¦zi {x₀,x₁,x₂, . . .}w drzewie D.

Logiczne BHP

Konstrukcje syntaktyczne w j¦zykach systemów logicznych s¡

jednoznaczne. Termy, formuªy, dowody mo»na reprezentowa¢ np. przez stosowne drzewa. Indukcyjne denicje termów i formuª wykorzystywa¢

mo»na w dowodach wielu wªasno±ci, opieraj¡c si¦ na nast¦puj¡cym twierdzeniu o oczywistym dowodzie (zob. np. Fitting 1990, 10):

Twierdzenie. (Zasada Indukcji Strukturalnej). Ka»da formuªa j¦zyka KRZ ma wªasno±¢ Q, o ile:

1 Krok pocz¡tkowy. Ka»da formuªa atomowa ma wªasno±¢ Q;

2 Kroki indukcyjne.

1 Je±li ϕ ma wªasno±¢ Q, to ¬ϕ ma wªasno±¢ Q;

2 Je±li ϕ oraz ψ maj¡ wªasno±¢ Q, to (ϕ ◦ ψ) ma wªasno±¢ Q, gdzie ◦ jest funktorem dwuargumentowym.

Logiczne BHP

W teorii mnogo±ci dowodzi si¦ twierdzenia o deniowaniu przez rekursj¦.

Jego zastosowaniem w przypadku j¦zyków logiki jest twierdzenie (zob. np.

Fitting 1990, 10):

Twierdzenie. (Zasada Rekursji Strukturalnej). Istnieje dokªadnie jedna funkcja f okre±lona na zbiorze F wszystkich formuª j¦zyka KRZ taka, »e:

1 Krok pocz¡tkowy. Warto±¢ f jest podana wyra¹nie dla formuª atomowych.

2 Kroki rekurencyjne.

1 Warto±¢ f dla ¬ψ jest okre±lona w terminach warto±ci f dla ψ;

2 Warto±¢ f dla (ϕ ◦ ψ) jest okre±lona w terminach warto±ci f dla ϕ oraz dla ψ, gdzie ◦ jest funktorem dwuargumentowym.

Mo»emy zatem deniowa¢ m.in. ró»ne funkcje o warto±ciach liczbowych, charakteryzuj¡cych zªo»ono±¢ formuª.

Chyba nie spaliªa± notatek z wykªadów?

W omawianiu wªasno±ci metod dowodowych po»yteczne b¦dzie korzystanie z Lematu Hintikki oraz Twierdzenia o Istnieniu Modelu (najpierw: dla KRZ; pó¹niej: dla KRP); zob. np. Fitting 1990, 5156.

Zakªadamy te», »e intensywne prze»ycia wakacyjne nie wymazaªy z pami¦ci sªuchaczy denicji podstawowych poj¦¢ logicznych (z KRZ oraz KRP).

Zwykle korzysta¢ b¦dziemy jedynie z wybranych funktorów

prawdziwo±ciowych (primary connectives w terminologii podanej w Fitting 1990, 13).

By¢ mo»e sªuchacze mieli ju» styczno±¢ z notacj¡ Smullyana (α-formuªy i β-formuªy). Oswoimy si¦ z ni¡ na konwersatorium.

Nie zakªadamy pryncypialnie, »e podczas caªego cyklu wykªadów zachowamy konsekwencj¦ w oznaczeniach.

Wszystkie funkcje prawdziwo±ciowe 2-argumentowe

p q ⊥ ∧ 9 p 8 q 6 ≡ ∨ ↓ ≡ ¬q ← ¬p → ↑ >

0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1

0 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1

1 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1

1 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1

Pierwsze dwie kolumny podaj¡ wszystkie ukªady warto±ci argumentów, kolejne kolumny podaj¡ warto±¢ dla tego ukªadu argumentów ka»dej z szesnastu dwuargumentowych funkcji prawdziwo±ciowych. Czy widzisz jakie± symetrie w tej tabeli?

Lubimy odró»nia¢: spójnik, funktor oraz funkcj¦ (wszystkie z okre±leniem: prawdziwo±ciowy). Nie jeste±my jednak ortodoksami i przystajemy na uproszczenia w podr¦cznikach.

Funktory pierwszorz¦dne

1arg. 2 arg. ∧ ∨ → ← ↑ ↓ 9 8

1 1 1 1 1 1 0 0 0 0

1 0 0 1 0 1 1 0 1 0

0 1 0 1 1 0 1 0 0 1

0 0 0 0 1 1 1 1 0 0

Poszczególne kolumny tej tabeli odpowiadaj¡: pierwszemu argumentowi, drugiemu argumentowi, koniunkcji, alternatywie, implikacji prostej, implikacji odwrotnej, kresce Sheera, binegacji, zaprzeczeniu implikacji prostej, zaprzeczeniu implikacji odwrotnej.

Funktor ↑ jest (przez informatyków) nazywany NAND, natomiast ↓ nazywany jest (przez informatyków) NOR.

Uwaga na porz¡dek wierszy tej tabeli! Taki podaje Fitting, my lubimy dokªadnie odwrotny porz¡dek.

Notacja Smullyana

Od kilku dekad karier¦ robi notacja zaproponowana przez Raymonda Smullyana, zwana te» jednolit¡ notacj¡ (uniform notation).

Notacja ta motywowana jest wªasno±ciami semantycznymi.

Naszym zdaniem ªatwo j¡ zapami¦ta¢, patrz¡c na diagram Hassego stosownej algebry Lindenbauma-Tarskiego, który narysujemy na konwersatorium.

W±ród funktorów pierwszorz¦dnych oraz ich zaprzecze« wyró»nimy te, które dziaªaj¡ koniunkcyjnie oraz te, które dziaªaj¡ alternatywnie.

Formuªy z tymi pierwszymi funktorami oznacza si¦ symbolem α, te drugie za± symbolem β. Skªadniki takich formuª s¡ oznaczane symbolami, odpowiednio: α₁, α₂ oraz β₁, β₂. Skªadniki te wyznaczane s¡ wedle nast¦puj¡cej konwencji:

Formuªy koniunkcyjne i formuªy alternatywne

α α₁ α₂

ϕ ∧ ψ ϕ ψ

¬(ϕ ∨ ψ) ¬ϕ ¬ψ

¬(ϕ → ψ) ϕ ¬ψ

¬(ϕ ← ψ) ¬ϕ ψ

¬(ϕ ↑ ψ) ϕ ψ

ϕ ↓ ψ ¬ϕ ¬ψ

ϕ 9 ψ ϕ ¬ψ

ϕ 8 ψ ¬ϕ ψ

β β₁ β₂

¬(ϕ ∧ ψ) ¬ϕ ¬ψ

ϕ ∨ ψ ϕ ψ

ϕ → ψ ¬ϕ ψ

ϕ ← ψ ϕ ¬ψ

ϕ ↑ ψ ¬ϕ ¬ψ

¬(ϕ ↓ ψ) ϕ ψ

¬(ϕ 9 ψ) ¬ϕ ψ

¬(ϕ 8 ψ) ϕ ¬ψ

Pó¹niej rozszerzymy jednolit¡ notacj¦ na j¦zyk KRP.

Zasady: Indukcji Strukturalnej oraz Rekursji Strukturalnej zachodz¡

te» w nast¦puj¡cych wersjach:

Zasada Indukcji Strukturalnej

Twierdzenie. (Zasada Indukcji Strukturalnej). Ka»da formuªa j¦zyka KRZ ma wªasno±¢ Q, o ile:

1 Krok pocz¡tkowy. Ka»da formuªa atomowa oraz jej negacja maj¡

wªasno±¢ Q;

2 Kroki indukcyjne.

1 Je±li ϕ ma wªasno±¢ Q, to ¬¬ϕ ma wªasno±¢ Q;

2 Je±li α₁oraz α₂maj¡ wªasno±¢ Q, to α ma wªasno±¢ Q.

3 Je±li β₁oraz β₂maj¡ wªasno±¢ Q, to β ma wªasno±¢ Q.

Dowód (Fitting 1990, 2122). Zaªó»my, »e Q jest wªasno±ci¡ speªniaj¡c¡

warunki twierdzenia. Powiemy, »e formuªa ψ jest dobra, je±li ψ oraz ¬ψ maj¡ wªasno±¢ Q. Je±li poka»emy, »e ka»da formuªa jest dobra, to wyniknie z tego, »e ka»da formuªa ma wªasno±¢ Q.

Dowód Zasady Indukcji Strukturalnej

Je±li ψ jest atomowa, to jest dobra (na mocy kroku pocz¡tkowego).

Zaªó»my, »e ψ jest dobra. Wtedy ψ, ¬ψ maj¡ wªasno±¢ Q. Na mocy kroku indukcyjnego 1, ¬¬ψ ma wªasno±¢ Q. A zatem ¬ψ jest dobra.

Zaªó»my, »e ϕ oraz ψ s¡ dobre. Je±li (ϕ ◦ ψ) jest α-formuª¡, to

¬(ϕ ◦ ψ) jest β-formuª¡, a je±li (ϕ ◦ ψ) jest β-formuª¡, to ¬(ϕ ◦ ψ) jest jest α-formuª¡. W ka»dym z tych przypadków,

{α₁, β₁} ⊆ {ϕ, ¬ϕ}. Poniewa» ϕ oraz ¬ϕ s¡ dobre, wi¦c obie maj¡

wªasno±¢ Q (czyli α₁ i β₁ maj¡ wªasno±¢ Q).

Podobnie, {α2, β₂} ⊆ {ψ, ¬ψ}, a wi¦c α2, β2 maj¡ wªasno±¢ Q.

Na mocy ostatnich dwóch kroków indukcyjnych, α i β maj¡ wªasno±¢

Q.

Na mocy pierwotnej wersji Zasady Indukcji Strukturalnej, ka»da formuªa jest dobra, czyli ka»da formuªa ma wªasno±¢ Q.

Zasada Rekursji Strukturalnej

Twierdzenie. (Zasada Rekursji Strukturalnej). Istnieje dokªadnie jedna funkcja f okre±lona na zbiorze F wszystkich formuª j¦zyka KRZ taka, »e:

1 Krok pocz¡tkowy. Warto±¢ f jest podana wyra¹nie dla formuª atomowych oraz ich negacji.

2 Kroki rekurencyjne.

1 Warto±¢ f dla ¬¬ψ jest okre±lona w terminach warto±ci f dla ψ;

2 Warto±¢ f dla α jest okre±lona w terminach warto±ci f dla α₁oraz dla α₂.

3 Warto±¢ f dla β jest okre±lona w terminach warto±ci f dla β₁ oraz dla β₂.

Twierdzenie to mo»na wykorzysta¢ do deniowania stopnia zªo»ono±ci formuª, zapisywanych w jednolitej notacji.

Stopnie i rangi formuª j¦zyka KRZ

Funkcja stopnia dg zdeniowana jest indukcyjnie:

Stopie« formuª atomowych (zmiennych oraz ⊥ i >) jest równy 0.

dg(¬ψ) = dg(ψ) + 1

dg((ϕ ◦ ψ)) = dg(ϕ) + dg(ψ) + 1, gdzie ◦ jest funktorem dwuargumentowym.

Funkcja rangi rk zdeniowana jest indukcyjnie:

rk(p) = rk(¬p) = 0 dla zmiennych zdaniowych p.

rk(⊥) = rk(>) = 0.

rk(¬¬ψ) = rk(ψ) + 1 rk(α) = rk(α1) +rk(α2) +1 rk(β) = rk(β1) +rk(β2) +1