AnalyticTableaux

     Wpis poniższy jest powieleniem mojej wypowiedzi na blogu Niedowiary w blogach Polityki. Powtarza on rozmaite moje wypowiedzi zamieszczane tu i ówdzie, także i tematy poruszane już także na tym blogu. Ponieważ komentarz – będący odpowiedzią na wpis jednego z czytelników bloga Niedowiary był długi a jego napisanie wymagało odrobiny zastanowienia – pomyślałem że umieszczę go także i tutaj, dla potomnych oczywiście.

     Jeden z adwersarzy – umieścił w swoim komentarzu do następująca opinię dotycząca matematyki: ” Aksjomatów się z definicji nie dowodzi”. Jest to na tyle popularna opinia, wyrażana tu i ówdzie, że warto się nad nią przez chwilę zatrzymać.

     Dlaczego ktoś twierdzi że “aksjomatów się nie dowodzi” skoro na przykład korespondencja Gaussa z Bolyai ojcem poświęcona jest kwestii dowiedzenia V aksjomatu Euklidesa? Skoro “się nie dowodzi” dlaczego do czasu prac Bolyayi, Łobaczewskiego i Gaussa całe tabuny matematyków starały sie go dowieść? I dziś ludzie starają sie “dowodzić” że jakiś aksjomat, szczególnie bogatych teorii jest zależny lub nie od innych. Jest to absolutnie fundamentalna kwestia w wypadku każdej teorii. Chcąc zatem odczytać opinię o aksjomatach w sposób pozytywny ( warto spróbować dla samego przedstawienia poglądu ;-) musimy uznać że nie chodzi tu o praktykę uprawiania matematyki. Praktyka matematyki jest taka, że próby dowiedzenia aksjomatów, udowodnienia ich zależności lub niezależności od pozostałych, są powszechne by wymienić tylko dwa szczególnie ważne i szalenie w swych wynikach owocne przypadki. Pierwszy to właśnie powszechne próby dowodzenia V aksjomatu Euklidesa zakończone odkryciem geometrii nieeuklidesowych. Owe geometrie miały być w pierwszym zamyśle kontrprzykładem w dowodzie! Drugi przykład, to wieloletnie starania, zakończone dowodem Cohena i wynalezieniem ważnej metody forcingu, by dowieść że pewnik wyboru jest niezależny – a więc nie da sie dowieść – od aksjomatów ZF Teorii Mnogości, oraz by dowieść że hipoteza kontinuum także jest od nich niezależna, a zatem może być przyjęta za kolejny aksjomat . Zatem w opinii „Aksjomatów sie nie dowodzi” nie chodzi o to, że się nie dowodzi. Jak najbardziej matematycy czynią wiele wysiłków by niektóre aksjomaty udowodnić, zwykle na podstawie pozostałych aksjomatów rozważanej teorii, wykazując tym samym że teoria dopuszcza mniejszą w sensie liczby pewników – aksjomatyzację. Zatem w opinii tej chodzi o coś zupełnie innego.

     Nie chodzi o to co robią matematycy, bo ci aksjomaty starają się dowieść, lub dowieść że się ich nie da dowieść, ale o tzw. zasady. Sporo ludzi zapewne wyobraża sobie że praktyka matematyki czy w ogóle nauk ścisłych, wygląda tak: Matematyk siada i na kartce pisze 5-7 aksjomatów, których nie będzie dowoził, a następnie tworzy z nich teorię. Nie wiem czy tak postępują matematycy, wszakże taka praktyka jest możliwa, dlaczego nie? Służą do takich zabaw całe systemy matematyki symbolicznej, jak Coq, a są nawet i takie które na podstawie podanych aksjomatów starają się generować, czysto kombinatorycznie, twierdzenia ( znany i kontrowersyjny matematyk Doron Zeilberger na swojej stronie ma kilka generatorów twierdzeń napisanych w mathematica czy maple. Polecam jego książkę “A = B”, dostępną za darmo, poświęconą po części takim zagadnieniom.). Zatem działanie takie jest możliwe, przynajmniej co do zasady. I tu dochodzimy do fundamentalnego rozróżnienia. Mamy bowiem do czynienia z pomieszaniem terminologii, czy pojęć, wynikającym zapewne z faktu że w szkole nie uczą już teraz logiki jako takiej.

     Systemy rozumowania dzielą się na nieformalne i formalne. Systemy formalne to takie które posługują się językiem formalnym w którym ściśle określone są wszystkie symbole, gramatyka itp. Systemy nieformalne to wszystkie te dla których językiem ich rozwijania jest mowa potoczna. Oczywiście matematyka jest systemem nieformalnym. W przeszłości do wyjątkowej rzadkości należały książki jak te wydawane przez panią Helenę Rasiową, w których przebieg wykładu zbliża się ( ale nie jest!) do stanu systemu formalnego. Helenra Rasiowa wydała kilka książek w których dokonała daleko idącej formalizacji wykładu podstaw matematyki. Oczywiście takie podejście do matematyki w ogóle ( powiedzmy do tw. Fermata, do tw. Poincare dowiedzionego przez Perelmana ) jest szalenie trudne, właściwie niemożliwe, najpewniej bezsensowne. W przeszłości takimi metodami badano podstawy matematyki, a celem tych prac było raczej wyeliminowanie kłopotów niż koncepcja rekonstrukcji matematyki. Wykład uniwersytecki jakiegokolwiek przedmiotu matematyki ( teorii liczb, geometrii różniczkowej itp. normalnych działów matematyki) bardzo rzadko odbywa sie w ramach jakiegoś systemu formalnego. Matematyka tak przedstawiania jest trudna w odbiorze, a nawet można by rzec że jest martwa, bo i formalizacja teorii matematycznych jest wykonywana na ogół w wypadku teorii już ugruntowanych i znanych. Niemniej warto zwrócić uwagę, że podejście formalne zdało się złapać drugi oddech, a przynajmniej nabrać ciała, przez wykorzystanie komputerowych systemów dowodów. Zwrócę tu uwagę na dwa “produkty”. Jednym z nich jest system MIZAR autorstwa Andrzeja Trybulca. Mam wrażenie, że jest to zdecydowanie największy wynalazek Polskiej matematyki 2-giej połowy XX wieku, chyba całkowicie zapoznany w kraju, a szkoda, skoro daje niezwykłe możliwości rozwoju. System ten posiada obecnie najbardziej rozbudowaną bibliotekę twierdzeń matematycznych na świecie, w której całkowicie formalnie sprawdzono logiczną poprawność 49000 twierdzeń zapisując je w aksjomatyzacji Teorii Mnogości. Składnia systemu odpowiada niemal że językowi naturalnemu. Proszę sobie wyobrazić jakie meta-analizy są możliwe w oparciu o taką bazę danych! I nikt tego nie robi… Mizar ma oczywiście swoje wady, a najbardziej ważącą jest fakt że ma zamknięte źródła, i nie jest aktywnie rozwijany w sposób odpowiadający współczesnym standardom. Jego rozwój przebiega tak, jakby zespół ludzi pracujący w tym projekcie tkwił w latach 80-tych. Niestety charakterystyczną cechą projektu jest bardzo niska dynamika zmian, brak użycia narzędzi do współpracy w internecie ( jak repozytoria kodu), braki w takiej konfiguracji systemu i standardu języka by ułatwiała ona ciągłą transformacje tzw. artykułów Mizara i produkowanie wyników wtórnych ( nie tylko dopisywanie nowych dowodów) jak rozmaite analizy systemu dowodów samego w sobie. Rzecz tą nie byłoby chyba aż tak trudno zmienić….
Innym ciekawym przykładem jest Univalent Foundations które idzie w kierunku odwrotnym. Za pomocą COQ zapisano w języku formalnym pewną aksjomatyzację podstaw matematyki, a na tej podstawie stworzono (napisano?) książkę opisującą zawartość tego systemu. Być może tka będzie wyglądała przyszłość jakiegoś fragmentu matematyki: http://homotopytypetheory.org/

     Wróćmy do tematu wpisu. System formalny wymaga określenia języka. Język zawiera stałe ( jak znak równości, kwantyfikator ogólny itp.), symbole zmiennych ( które wiąże kwantyfikator np.) , atomowe symbole na oznaczanie relacji ( np. relacja “jest elementem” w teorii zbiorów itp.) oraz jakieś określenie własności tych symboli. Aby budować system formalny zwykle na dzień dobry zakładamy że obowiązują nas prawa logiki klasycznej, dla klasycznej matematyki zwykle pierwszego rzędu. Same symbole to za mało by sie dobrze bawić, dlatego dodajemy do naszego systemu także reguły wnioskowania, bowiem nie każda “operacja” na zadanych symbolach jest równoprawna. Reguł wnioskowania, tak zwanych reguł inferencji, może być bardzo dużo, co znacząco może komplikować system. Elementarnym wymogiem wydaje się być by owe reguły prowadziły od zdań prawdziwych do zdań prawdziwych co oczywiście sie dowodzi, ale dlaczegóż ktoś nie miałby badać systemów sprzecznych? Można jak kto chce.

     Systemy określa sie tu dwojako. Jeśli system logiczny nie posiada aksjomatów, ale ma pewien zbiór reguł inferencji, mówimy o systemie dedukcyjnym. Systemy takie badali jako pierwsi Jaśkowski i Gentzen. Jeśli jako reguły inferencji ( nadal bez aksjomatów!) weźmiemy zasadniczo znane reguły logiki ( przykłady we wpisie na tym blogu ) to system taki nazwiemy systemem dedukcji naturalnej. Trudno sie takie obiekty bada bo jest wiele metod przekształcania napisów, wiele metod inferencji, co sprawia że drzewa dowodowe mają sporo stopni swobody. Dlatego kiedy formalizujemy w celu badania istniejących teorii, zwykle bierzemy jedną regułę inferencji – tylko modus poens, choć nader często w pierwszych kokach wprowadza sie kolejne reguły, ale już nie jako zadane obiekty początkowe, ale wnioski z istniejących. Dowody konstruuje się w takich strukturach przez podanie ciągu przekształceń od innych udowodnionych twierdzeń, do takiego którego dowodu szukamy gdzie po drodze wolno nam używać tylko założonych reguł inferencji lub strategii dowodowych dowiedzionych za ich użyciem. Zapis takiego “przejścia” od jednych napisów do innych – nazywamy dowodem. Okazuje się, że tak długo jak mamy do czynienia z samą logiką klasyczną ( bez predykatów i dodatkowych aksjomatów), cały system jest rozstrzygalny i zupełny – to znaczy każde twierdzenie ma dowód, a wykonuje sie go na rozmaite sposoby, np. metoda tabelek 0-1-kowych. Dodanie do niego predykatów ( kwantyfikacja!) czyni system nierozstrzygalnym, jest on jednak nadal zupełny. Zupełność oznacza że każde zdanie w nim wyrażone jest albo prawdziwe albo fałszywe, zaś jeśli jest prawdziwe we wszystkich strukturach spełniających aksjomaty, to można go dowieść, i odwrotnie, posiadanie dowodu gwarantuje prawdziwość. Do tej struktury dołączamy następne prawa określające jak pojęcia które opisujemy mają sie do siebie. I właśnie określenie owych własności symboli, obiektów czy stałych to aksjomaty. Te dodatkowe aksjomaty dotyczą relacji pozalogicznych. Powtórzmy jeszcze raz – dodajemy aksjomaty dotyczące obiektów zdefiniowanych poza logiką ( liczb, zbiorów, obiektów grupy, obiektów geometrycznych). Wychodzimy poza logikę. I wówczas życie staje się ciekawe, i nie sposób powiedzieć jakie własności będzie miał cały system. Czy będzie niesprzeczny? Czy każde twierdzenie które ma dowód będzie prawdziwe we wszystkich strukturach spełniających aksjomaty? Czy każde prawdziwe twierdzenie będzie miało dowód? Na te pytania nie ma odpowiedzi, dlatego że struktura która rozważamy jest zbyt ogólna. W ogólności można w ten sposób dostać systemy formalne zupełne i niezupełne. Stąd trzeba wiedzieć więcej by na pytania odpowiedzieć. Odpowiedź zawarta jest w tw. Goedla o niezupełności.

     Po pierwsze trzeba wiedzieć o jakich aksjomatach sie mówi. nie jest to obojętne – bowiem ta sama intuicyjnie rozumiana “teoria w ogóle” jak powiedzmy “liczby naturalne”, “teoria zbiorów”, “teoria wielomianów” itp. może mieć wiele nierównoważnych aksjomatyzacji, każda spełniająca pewien zbiór naszych oczekiwań czy wyobrażeń o własnościach jakie powinna spełniać owa “teoria w ogóle”. Okazuje się że np dodanie pewnych aksjomatów takich jak opisują ciało rzeczywiste ( np. takich ) daje w wyniku teorię zupełną. Geometria Euklidesa także jest teorią zupełną. Istnieją formalizację arytmetyki liczb naturalnych które mają tą własność. Warto zwrócić uwagę na fakt, że znaczenie aksjomatyzacji Peano ( inne niż historyczne ) leży w tym że wydaje nam się iż opisuje ona nasze wyobrażenie o własnościach liczb naturalnych. No ale akurat tak jest że aksjomatyzacja Peano nie ma własności zupełności ( o czym mówi tw. Goedla). W tym kontekście ( nieco sarkastycznie i z przekąsem) kwestia że tak jest i że stanowi to dla nas zaskoczenie więcej mówi o naszych wyobrażeniach niż o samej arytmetyce. No ale nie powoduje to znaczących problemów, gdyż niesprzeczności i zupełności aksjomatyki Peano można dowieść i to na dwa sposoby ( indukcją pozaskończoną Gentzen, lub w ramach aksjomatyki teorii mnogości ZFC). Widać zatem że *istnieją* dowody poprawności czy prawdziwości aksjomatów, tyle że prawdziwość aksjomatów jednej teorii dowodzi sie wyrażając je w języku innej teorii. Dlaczego tak jest?

     Pojęcie prawdy mówi o własności która nie jest precyzyjnie zdefiniowana. Na temat definicji prawdy toczą sie nadal aktywne dyskusje. Istnieje wiele możliwych formalizacji tego pojęcia, wszakże w matematyce zapewne najszerzej przyjmowana jest znana koncepcja Tarskiego ( która wymaga relatywizacji prawdy do metajęzyka opisującego język formalny). Jest to niedoskonała koncepcja, ale przyjęta i działająca, o ile nie mnożymy bytów ponad potrzebę. Stwierdzenie prawdziwości danego twierdzenia w danej teorii, wymaga w jej ramach rozważenie wszystkich struktur spełniających aksjomaty tej teorii ( np. aksjomaty teorii grup spełnia każda grupa, która tym samym jest modelem teorii grup), i sprawdzenie czy twierdzenie które sprawdzamy, jest prawdziwe w każdej, z nich. Oczywiście to beznadziejne zadanie. W praktyce nikt tak nie postępuje! Konstrukcja ta służy wyłącznie definicji prawdy – prawdziwe twierdzenie to takie które zachodzi we wszystkich modelach teorii. Tymczasem matematycy w praktyce zawodowej posługują sie dowodem. A dowód – to jak pisaliśmy wyżej to manipulacja napisami. Skąd wiadomo że taka manipulacja daje nam uzasadnienia dla prawdziwości twierdzeń? Ano z twierdzenia Goedla o pełności logiki, które stwierdza że jeśli reguły inferencji ( a w praktyce tylko modus poens) zachowują własność prawdziwości ( czyli od zdań prawdziwych prowadzą do zdań prawdziwych) to mamy równoważność obu pojęć: _to co daje sie dowieść jest prawdziwe a to co prawdziwe daje sie dowieść. Logika ma taką cudowną własność! Niezwykłe. A na dodatek skoro tego typu działanie jest manipulacją napisami, te zaś posługują się skończoną ilością symboli, trafiamy do prawdziwego raju! Co prawda interpretacje owych symboli są rozmaite, ten sam X oznacza raz zbiór, a to znowu liczbę, wszakże w każdym przypadku mamy skończoną liczbę symboli, a co za tym idzie kombinatorycznych kombinacji. Tym samym, niejeden wpadnie na ten pomysł, matematyka może być całkowicie skomputeryzowana, liczby mogą być reprezentowane jako byty dyskretne, byle zapewnić arbitralnie wybraną dokładność. Cała wiedza matematyczna może zatem być reprezentowana komputerowo, i wreszcie wszystko jest skończone, ładne i da sie zamknąć w pudełeczku. A ponieważ nikt nie używa w dowodzie więcej niż powiedzmy miliona różnych symboli oraz liczb większych niż powiedzmy liczba Avogadro ( rzędu 10^23 ) właściwie można by sie ograniczyć do zbiorów skończonych, choć oczywiście niech będzie że absurdalnie wielkich – by zmieścić w nich całą matematykę. Subtelnie podkreślmy że nie mówimy tu o eliminacji pojęcia nieskończoności z matematyki jako takiej, niech tam sobie matematycy na nieskończonościach rachują, proponujemy jedynie użycie skończonej liczby symboli do owych rachunków Przecież nikt nie rachuje na nieskończenie wielu symbolach naraz, prawda? I w tym miejscu następuje wielkie zdziwienie, a jego powodem bynajmniej nie jest tw. Geodla ale twierdzenie Trachtenbrota które stwierdza, że aby logika była zupełna, nie może być strukturą finitystyczną. Ludzkim językiem idzie to tak: jeśli rozważymy logikę klasyczną realizowaną wyłącznie na strukturach skończonych, jaki opisałem w kilku ostatnich zdaniach to taki system nie jest zupełny. Czyli rozumowanie logiczne wymaga nieskończoności. Przy takich założeniach, logika jest zupełna i jeśli prawdziwe sa zdania które do niej dodaliśmy jako aksjomaty ( Geometrii Euklidesa, Arytmetyki Peano, Ciałą Rzeczywistego, Teorii Zbiorów itp.) to to co dowiedzione jest prawdziwe we wszystkich modelach. Niestety – jak wiadomo z tw. Geodla – to co prawdziwe we wszystkich modelach – nie zawsze jest dowodowe a łyżką cudnej przyprawy która czyni smak matematyki ciekawy jest arytmetyka Peano, która “psuje teorie” jeśli sa one na tyle “wygadane” by ja wyrazić w swoim języku. No ale jak ktoś chce mieć całkiem banalną matematykę bez owej przyprawy – proszę bardzo – wystarczy używać słabszych aksjomatyk dla liczb naturalnych – i będzie miał wszystko dowodliwe. Tyle że to trochę tak jak jeść potrawy bez soli. Co jest najważniejszym wnioskiem z powyższego? Ano że tak jak dowód prawdziwości twierdzenia wykonuje sie w oparciu o aksjomaty, tak prawdziwość aksjomatów dowodzi sie w oparciu o teorie które pozwalają owe aksjomaty wyrazić w swoim języku. Czyli prawdziwość – twierdzeń czy aksjomatów jest relatywna. Relatywna do uniwersum w którym dane pojęcia rozważamy. A uniwersum owo nie może być finitystyczne jeśli chcemy dowodzić twierdzeń by mówić o ich prawdziwości…

    A “Prawda W Ogóle”? Chętnie o niej pogadam – niechże tylko ktoś wyjaśni o czym mówi…