Co ( mi sie wydaje że) wiem o automatycznym dowodzeniu twierdzeń i systemie Coq

   

    Systemy dedukcji

    Chciałbym napisać coś o Coq. temat jest jak rzeka, ale nie brak tez materiałów w necie a nawet książek wśród których, co ciekawa, a dla mnie przyznam zaskakujące, pojawiają się polskie nazwiska. Pomyślałem jednak że warto na początku podzielić się trochę historyczną wiedzą, zwłaszcza, że jak jej nie zapiszę to i tak mi z głowy zniknie;-) W zasadzie celem poniższego jest skierowanie czytelnika do przeglądnięcia metody tabel analitycznych oraz pokazania jakiegokolwiek systemu dedukcji naturalnej. Wszystko to w celu zwrócenia uwagi, że systemy automatycznego dowodzenia twierdzeń nie sa cudem ale przemyślnie skonstruowanymi programami, i że jest to dziedzina posiadająca obecnie długa historię sięgająca co najmniej lat 50-tych a może i początków wieku XX. Autor, czyli ja, jest laikiem i amatorem, rad więc przyjmie;-) komentarze i uwagi, zwłaszcza od chcących podzielić się wiedzą, byle nie na temat ortografii;-)

    Początek wieku XX był czasem burzliwego rozwoju logiki. Koniec XIX wieku przyniósł sporo zmian i zamieszania po pracach Fregego i Cantora. Frege dokonał reformy logiki tworząc ją taką jaką znamy obecnie – wprowadził większość znanej nam symboliki, ustalił znaczenie pojęć, podał podstawowe definicje. Cantor tworząc teorię mnogości określił język dla uprawiania matematyki jednak uznanie zostało poprzedzone wielkim zamieszaniem u podstaw samej matematyki – bowiem teoria mnogości wydawała z początku się paradoksalna i niespójna, nie została przyjęta ze zrozumieniem. Można wręcz zasugerować, choć to pewnie kontrowersyjna ocena, że w dużej mierze burzliwy rozwój matematyki w tym przełomowym okresie był próbą wprowadzenia ładu w teorie Fregego i Cantora, okazały się one bowiem tak istotne i wpływowe że zatrzęsły podstawami matematyki. Istotną rolę w rozwoju logiki w tamtych czasach odegrały prace Hilberta nad teorią dowodu, siłą rzeczy zahaczające o logikę i będące próbą formalizacji wnioskowania matematycznego.

    Hilbert starał się wdrożyć potężny program uporządkowania podstaw matematyki w celu przezwyciężenia trudności wynikających z rozlicznych paradoksów odziedziczonych po pracach o których mowa. Okres ten można by podsumować omawiając prace Russella i Witheheada „Principia Mathematica” będącą próbą sprowadzenia matematyki do logiki Fregego i całej matematyki – prąd ten nazywamy logicyzmem ( współcześnie uważa się raczej zgodnie że była to próba nieudana). Można by to dzieło nazwać łabędzim śpiewem logicyzmu, pozostała jednak po niej teoria typów, rozwijana współcześnie w ramach informatyki w zupełnie innym kontekście i z innych powodów. Następne przyszły prace Goedla i Tarskiego niejako zamykające pewien etap, w znaczeniu – ustalające pewien kanon ścisłości i metod opisu w rozwoju logiki. W zasadzie wąsko rozumiany program Hilberta, podobnie jak logicyzm, upadł – prace Goedla przypieczętowały koniec marzeń o absolutnych i obiektywnych podstawach matematyki – jednak z tą opinią nie zgadza siwe zdecydowana większość matematyków;-) Jak było tak było, co wygrało to wygrało, ale wypracowane rozwiązania i metody okazały sie bardzo owocne i przetrwały niejako w nowej roli – stworzono teorię modeli, nowoczesną semantykę, teorię prawdy, ugruntowano pojęcie teorii formalnej.

    Mniej więcej pośrodku tego okresu podjęto próbę formalizacji teorii dowodu i wnioskowania matematycznego. Opisano wówczas tak zwane systemy dedukcji.

    Systemy dedukcji zostały formalnie opisane po praz pierwszy w pracach G.Gentzen  i S.Jaśkowskiego  Warto nadmienić, że jakkolwiek popularność zdobyły prace Gentzen i to one stały się motorem rozwoju tej dziedziny logiki, to wikipedia przyznaje pierwszeństwo otwarcia tematyki badań Jaśkowskiemu. Systemy te, nieco zapomniane i mam wrażenie wyparte z kursów matematyki uniwersyteckiej wydają się co najmniej od lat 60-tych zdobywać na znaczeniu za sprawą rozwoju metod automatycznego dowodzenia twierdzeń. Prace Gentzen i Jaśkowskiego miały jednak motywację czysto teoretyczną i można przypuszczać, że np. Gentzen starał się częściowo być może realizować program Hilberta którego był asystentem.

    Systemy dedukcji w myśl prac Gentzen składają się z dwu elementów (za „Małą Encyklopedią logiki” ): „Każdy system dedukcyjny może być określony jako para gdzie A jest zbiorem aksjomatów, zaś R zbiorem reguł dedukcyjnych.”

    Jeśli zbiór aksjomatów jest niepusty, mamy do czynienia z systemem logicystycznym i odpowiada to klasycznym sformułowaniom teorii matematycznych, kiedy zaś zbiór aksjomatów jest zbiorem pustym – mamy do czynienia z systemem dedukcji naturalnej. Co ciekawe systemy dedukcji naturalnej opisano dopiero w latach 30-tych ubiegłego stulecia – wcześniejsze systemy to systemy logicystyczne mające swoje pochodzenie w tradycji logiki i matematyki. Dla porządku, za „Małą Encyklopedią logiki” podam tu przykład dla zestawu reguł dla systemu Naturalnej Dedukcji Klasycznej:

operator:	reguła prowadzania:	reguła opuszczania:

    oraz reguła dodatkowa:

    Rozszyfrujmy powyższe reguły. Każda z nich ma postać „ułamka” w którym nad kreską znajdują się przesłanki, a pod kreską konkluzja. Są to reguły wnioskowania lub inaczej inferencji i należy przez to rozumieć, że jeśli dla przykładu w regule wprowadzania mamy jako przesłanki prawdziwe zdanie A oraz prawdziwe zdanie B, to należy przyjąć że prawdziwe jest także zdanie . Ciekawa jest reguła (v) w której pojawia się symbol odwróconej litery T. Oznacza on wynikanie – A T C oznacza, że z A logicznie wynika C. Jest to wynikanie logiczne w odróżnieniu od implikacji która jest zdefiniowana jako bądź za pomocą znanej tabelki z 0 i 1-kami. Kolejny ciekawy szczegół to druga reguła opuszczania zwana regułą wyłączonego środka. Jej usunięcie z przytoczonego zestawu prowadzi do innego, nierównoważnego zestawu reguł dedukcji związanego z systemami intuicjonistycznymi – i jest podstawą logiki intuicjonistycznej. Logika ta jest używana w wielu systemach komputerowych dowodów w tym w systemie Coq, o którym będzie ( być może;-) mowa. Reguła opuszczania dla to oczywiście modus poens czyli reguła odrywania. Reguły i dotyczą kwantyfikatorów i pozwalają od zdania kwantyfikowanego przejść do szczególnego przypadku ( „skoro prawdą jest że dla każdego x B(x) to mogę za x wstawić jakąś stała a i opuścić kwantyfikator”, „skoro prawda jest że dla dowolnej stałej B(a), to prawda jest że dla każdego x, B(x)” itp.) Nie ma potrzeby wnikać tutaj dalej w szczegóły. Systemy Gentzen są ciekawe z wielu powodów, teoretycznych związanych z teorią dowodu i praktycznych sa bowiem podstawą automatycznego generowania – a przez to dowodzenia, twierdzeń. Wychodząc od znanych przesłanek, w ramach systemu dedukcyjnego opisanego regułami jak powyżej ( lub innymi) możemy generować kolejne konkluzje będące przesłankami dla następnych konkluzji itp. Oczywiście jeśli zbudujemy ciąg prowadzący od uznanych przesłanek, a zakończony interesującym nas zdaniem – otrzymamy dowód wprost zdania nas interesującego. Jeśli przesłanki są aksjomatami ( co w systemach dedukcji naturalnej nie jest konieczne) – otrzymamy klasyczny dowód wprost zgodnie z definicją twierdzenia w teorii aksjomatycznej.

    Systemy dowodzenia wprost jakkolwiek mają wielkie znaczenie teoretyczne – sa trudne do stosowania w praktyce. Aby dowodzić zadane twierdzenia należałoby kolejno stosować możliwe kombinacje reguł az znajdziemy stosowną i uzyskamy tezę. Oczywiście liczba możliwości rośnie błyskawicznie wraz ze stopniem komplikacji twierdzenia, i metoda staje się niepraktyczna. Z tego a także z wielu innych powodów w badaniach teoretycznych systemów formalnych ogranicza się zwykle liczbę reguł inferencji do modus poens, często przy tym rozbudowując aksjomaty. Warto jednak pamiętać, że rachunek oparty na systemach reguł jak powyżej jest w stanie generować automatycznie twierdzenia wychodząc z zadanych przesłanek. Jest on także bardzo ważnym narzędziem teoretycznym w teorii dowodu zwłaszcza kiedy doda się do niego tak zwaną regułę cięcia ( cut), która pozwala zdziałać cuda, miedzy innymi pozwoliła Gentzen na dowód niesprzeczność arytmetyki Peano bez schematu indukcji, niesprzeczność rachunku kwantyfikatorów i wiele innych. Utorowała także drogę do metody tablic analitycznych która jest kolejną, podstawową techniką mechanicznego dowodzenia twierdzeń. Twórcami metody tablic analitycznych są holenderski logik Beth (1956)  i Fin Hintikka (1955). Nie będę się tu wgłębiał w szczegóły metody, w skrócie odpowiada ona dowodowi niewprost czyli przez zaprzeczenie tezy i doprowadzenie do sprzeczności. W metodzie mechanicznej zaprzeczamy tezie i badamy kolejno wszystkie możliwe implikacje tego działania – tworzy się w ten sposób rodzaj drzewa zawierającego w gałęziach formuły logiczne. Sprzeczności – czyli jednoczesne pojawienie sie na jednej gałęzi p i ~p – ograniczają wzrost drzewa. Jeśli twierdzenie jest prawdziwe, każda z gałęzi zawiera sprzeczność – mówimy że drzewo jest zamknięte. Jeśli twierdzenie jest fałszywe – gałąź niezawierająca sprzeczności daje jednocześnie kontrprzykład – przynajmniej w wypadku klasycznego rachunku zdań. Klasyczny rachunek zdań jest rozstrzygalny, to znaczy dla każdego zdania jesteśmy w stanie w skończonej liczbie kroków podać czy jest prawdziwe. Odpowiada to skończonemu drzewu w ramach metody tablic analitycznych. Dobre przedstawienie metody po polsku zawiera podręcznik Kazimierza Trzęsickiego „Logika i teoria mnogości Ujęcie systematyczno-historyczne” – polecam. W wypadku użycia kwantyfikatorów, a wiadomo że taki przypadek nas interesuje, z wyżej podanych reguł inferencji wynika, że ich eliminacja kwantyfikatora wymaga wprowadzania kolejnych stałych. Liczba tych stałych szybko rośnie, de facto uniemożliwiając skuteczne dowodzenie dowolnych twierdzeń – jak wiemy rachunek logiczny kwantyfikatorów nie jest rozstrzygalny. Współczesny kształt metodzie nadał znany logik Smullayan, jego wpływ był tak wielki że w zasadzie mówi się współcześnie o tablicach jako o jego metodzie. Najpewniej należy przypisać temu, że nie tyle mamy do czynienia z jedną metoda a raczej z ich całą rodziną, i że Smullyan opracował i usystematyzował efektywną i praktyczną metodę dla klasycznego rachunku logiki pierwszego rzędu. Smullyan jest także autorem kilkunastu książek popularyzujących logikę napisanych w całkowicie brawurowy sposób.

    Ciekawym aspektem metody tablic analitycznych jest kolejny polski trop. Otóż jak pisze Melvin Fitting w ‚Introduction” w „Handbook of Tableau Methods” M.D’Agostino, D. M. Gabbay, R. Hahnle and J. Posegga, eds. „Notational simplification was the essential next step in the development of tableaus and, just as with the preceding stage, it was taken independently by two people: Zbigniew Lis and Raymond Smullyan. Lis published his paper [Lis, 1960] in 1960, but in Polish (with Russian and English summaries), in Studia Logica. At that time there was a great gulf fixed between the East and the West in Europe, and Lis’s ideas did not become generally known. They were subsequently rediscovered and extended by Smullyan, culminating in his 1968 book [Smullyan, 1968]. The work of Lis himself only came to general attention in the last few years. […] It is through Smullyan’s 1968 book First-Order Logic [1968] that tableaus became widely known. They also appeared in the 1967 textbook [Jeffrey, 1967], which was directed at beginning logic students. Smullyan’s book was preceded by [Smullyan, 1963; Smullyan, 1965; Smullyan, 1966] in which the still unknown contributions of Lis were rediscovered, deepened, and extended.”

    Metody tablic analitycznych zostały wymyślone od podstaw w celu automatyzacji technik dowodu. Poniżej ciekawy cytat z tego samego artykułu: „In 1957–58, Dag Prawitz, Prawitz, and Neri Voghera developed a tableau-based a system that was implemented on a Facit EDB [Prawitz et al., 1960]. At approximately the same time, the summer of 1958, Hao Wang proposed a family of theorem provers based on the sequent calculus, which he then implemented on an IBM 704 [Wang, 1960]. The first of Wang’s programs, for classical propositional logic, proved all the approximately 220 propositional theorems of Russell and Whitehead’s Principia Mathematica in 3 minutes! This was quite a remarkable achievement for 1958.”

Komentarze ( z buzz):

Marcin Rzeźnicki – Świetny post. Moje gratulacje. Dobrze napisane. Wspomniał bym jeszcze o Heytingu i semantyce Heytinga jako o „dynamicznym”, funkcjonalnym obrazie logiki w celu uzupełnienia przykładu o prawie wyłączonego środka – to może być ciekawe dla „komputerowców”. Polecam książkę Girarda „Proofs and Types” – do ściągnięcia za free z: http://www.paultaylor.eu/stable/Proofs+Types (w tym ujęciu a or not a polegało by na znalezieniu dowodu dla a lub funkcji mapującej dowód a -> 0 co, jak wiemy, nie zawsze jest możliwe). Podobnie z eliminacją podwójnej negacji. a potem pewnie izomorfizm Curryego-Howarda, ale to pewnie masz w zanadrzu na potem. Czekam z niecierpliwością !!8/6

Kazimierz Kurz – @Marcin Rzeźnicki dziękuję, jest mi bardzo miło. Obawiam się jednak że przeceniasz moje możliwości i aż tak kompetentnie tematu nie opiszę – onieśmieliłeś mnie ;-). Chciałem tylko pokazać system dedukcyjny na papierze, i pokazałem jego definicję żeby było jasne że nie od komputerów się zaczęło. O tw. Curryego-Howarda rzeczywiście trzeba będzie wspomnieć, ale jednak celem raczej jest pokazanie samego Coq, a nie „Wprowadzenie do komputerowych metod dowodu – ujęcie historyczne” ;-) bo zwyczajnie nie mam do tego stosownej wiedzy i kwalifikacji, choć chciałbym mieć. Marcin – a może uzupełnisz to co napisałem? Dodaj co uważasz za stosowne – będzie cykl wpisów;-). Mam juz za sobą niedokończone obietnice na temat grupy renormalizacji – tam tez nie powstała najbardziej techniczna część tematu – za co ze wstydem przepraszam – poległem jednak na diagramatyce – aby coś w tej teorii pola porachować trzeba mieć diagramy Feynmanna a to mnie wyraźnie przerosło. Z drugiej strony taki jest ten Web2.0 – jak człowiek się zleniwi a motywacja uleci – cudne plany idą w odstawkę. Tym razem Mój Sprytny Plan ;-) jest taki, że chciałbym napisać takie wpisy -systemy dedukcji (*zrobione, ew do uzupełnienia) -opis narzędzia -Prosty dowód -Nieco skomplikowany dowód Pisząc toto spostrzegłem jak niewiele wiem;-) i jak wiele trzeba by się dowiedzieć by wyjaśniać komuś kto, zakładam, wie jeszcze mniej. BTW. szalenie żałuję, że nie ma tu nigdzie Wlodzimierza Holsztyńskiego – jego uwagi merytoryczne i biograficzne mogłyby być tu znacznie bardziej wartościowe niż sam mój wpis, gdyby zechciał toto skomentować. Jeszce raz dziękuję.
    W następnym wpisie postaram się napisać coś o Coq.