Matematyka.pl

Już od co najmniej kilku miesięcy zastanawia mnie ta sprawa( z przerwami, nie cały czas). W końcu zapytam: co jest motywem tej formalizacji logiki i teorii mnogości Nie chodzi o pytanie nurtujące wielu niematematyków- po co dowodzić rzeczy oczywiste( dla mnie jest to zrozumiałe, przyjmujemy pewien układ aksjomatów, wtedy rozpatrywane twierdzenie musi być konsekwencją formalną aksjomatów, intuicyjna oczywistość (pod względem znaczenia )nie ma tu nic do rzeczy), gdy się zamknie układ aksjomatów, to niestety resztę twierdzeń trzeba dowieść (nawet tych " oczywistych"), ale o chodzi o motywy, z powodu, którego niektórzy matematycy decydują się na ten trud. No bo jak zauważył foundofmath dowód tego, że dla dowolnych zbiorów \(\displaystyle{ X,Y}\) mamy \(\displaystyle{ X \cap Y=Y \cap X,}\) zajął mu 52 formuły, i sam się też zastanawiał jak zrobić dowody bardziej doniosłych twierdzeń teorii mnogości. Czy jest zatem głębsza przyczyna tego trudu Nie wystarczy tak jak Euklides przedstawić dokładne, staranne rozwiązanie. Dowody formalne służą temu aby je sprawdzał komputer, i potwierdził poprawność rozumowania( no tak, wtedy jest poprawnie, co więcej komputer jest znakomity(w przeciwieństwie do człowieka) do takiej żmudnej roboty). Przeczytałem, w pewnym artykule, że dowody formalne służą do tego aby mając założenia (przesłanki), dojść do pewnych wniosków, w przeciwnym wypadku błąd może wiele kosztować. Oczywiście chcemy uniknąć błędów w dowodach (ale ponoć teoria mnogości ZFC może być sprzeczna- niewykluczone to jest, tego nie wiemy ), ale czy gdzieś ta formalną pewność otrzymywania pewnych wniosków z danych założeń ma praktyczne zastosowanie Jak tak to gdzie?

Co stoi za tą formalizacją

Formalizacja teorii polega na tym, żeby podać jej składnię, aksjomaty i reguły dowodzenia. Dodatkowo można podać jej semantykę. Nie oczekuje się, że po formalizacji matematyk będzie wszystko (łącznie z dowodami) wyrażał w terminach formalnych, ale zakłada się, że w razie potrzeby taka formalizacja części lub całości danej teorii będzie możliwa do przeprowadzenia.

Pierwszym historycznie systemem formalnym (lub o dużym stopniu formalizacji) był system sylogizmów (niemodalnych) Arystotelesa. Ten system (przedstawiony przez Arystotelesa w Organonie w IV wieku p.n.e.) posiadał wyraźnie określoną składnię i wymienione aksjomaty (zdaje się, że były to cztery sylogizmy). Przy użyciu tych aksjomatów oraz kilku reguł dowodzenia, których Arystoteles nie wymienił explicite i to jest wada jego systemu, wyprowadza on wszystkie tezy swojego systemu. Ponadto dla każdego zdania systemu, który nie jest tezą, podał kontrprzykład przy użyciu rozważań semantycznych. W jego systemie nie ma jednak wyraźnego określenia semantyki, co jest kolejną wada ze współczesnego punktu widzenia. Nie jest to aż tak rażące, bo od Arystotelesa pochodzi klasyczna definicja prawdy, która potem została rozwinięta przez Tarskiego i zawiera w sobie zaczyn pomysłu, który przerodzi się w teorię modeli. W XX wieku Jan Łukasiewicz dokonał pełnej formalizacji (we współczesnym znaczeniu tego terminu) systemu sylogizmów Arystotelesa. W każdym razie dokonania Arystotelesa są przykładem eleganckiego, matematycznego cacka i dzięki nim Arystoteles już zawsze będzie postrzegany jako jeden z największych (największy?) logików formalnych (obok Fregego, Tarskiego, Gödla) oraz twórca tej dziedziny. Dzieło Euklidesa (powstałe znacznie później, bo Euklides się urodził mniej więcej w tym czasie, gdy Arystoteles zmarł) w sensie logicznym nie zawiera nic nowego poza tym, co Arystoteles już wiedział i co sam wprowadził.
Współcześnie formalizacja jest związana z programem Hilberta. Zacytuję fragment książki Haskella Curry'ego na temat poglądów Hilberta:


Jego podstawowe stanowisko wyraża się tym, że pozaskończone pojęcia matematyczne są pewnymi idealnymi konstrukcjami ludzkiego umysłu. Hilbert przyznaje, że istnieją pewne "finitarne", intuicyjne rozumowania, których pewność jest absolutna i a priori; pojęcia pozaskończone, które poza nie wykraczają, uważa on za umysłowe twory, które pozostają w podobnym stosunku do skończonych, intuicyjnych procesów jak liczby rzeczywiste do liczb urojonych. Możemy tworzyć te idealne twory dowolnie z jednym wszakże ograniczeniem, a mianowicie, że nie będziemy przy tym popadali w sprzeczność. Hilbert proponował, żeby udowodnić niesprzeczność matematyki poprzez analizę języka, w którym matematyka się wyraża. Ten język należy sformułować w sposób na tyle zupełny i precyzyjny, żeby rozumowania w tym języku mogły być postrzegane jako przekształcenia oparte na ściśle określonych regułach – regułach, które byłyby mechaniczne w tym sensie, że prawidłowość ich zastosowania mogłaby zostać sprawdzona poprzez inspekcję symboli jako prostych obiektów fizycznych, bez jakiegokolwiek odwołania się do tego, co te symbole mogą lub czego nie mogą oznaczać. Te sformalizowane rozumowania miały być przedmiotem nowej dziedziny matematycznych dociekań, którą nazwał metamatematyką. W metamatematyce miały być dopuszczalne tylko skończone, absolutnie niepodważalne metody rozumowania. Jego program miał doprowadzić do ustanowienia niesprzeczności całej matematyki przy użyciu tych środków. Jego realizacja miała dzięki temu zagwarantować absolutną pewność matematyki już na zawsze.


Hilbertowi zależało na badaniu matematycznych teorii przy użyciu metod samej matematyki (ale tylko tych finitarnych i pewnych) oraz na tym by poprawność matematycznych teorii można było sprawdzać poprzez stwierdzenie zgodności przekształceń ciągów symboli z góry zadanym zbiorem reguł. Korzyści z tego rodzaju postępowania są matematycznie owocne, co zresztą wyraża się w olbrzymim postępie logiki i metamatematyki (weź dowolną książkę na ten temat i przekonaj się sam, ile ciekawych twierdzeń można w ten sposób uzyskać). Po formalizacji można teorie matematyczne badać pod względem ich niesprzeczności (consistency) i zupełności (completness) oraz (o ile określi się ich semantykę) pod kątem ich poprawności (soundness) i pełności (semantical completness). Sam program Hilberta (niesprzeczność całej matematyki) nie zostanie nigdy ukończony z powodu drugiego twierdzenia Gödla (chyba, że wyrzucimy z matematyki arytmetykę Peano pierwszego rzędu i wszystkie systemy formalne, które ją zawierają hehehekhekkkkkrrrwwwwww... ).

Dobra, dzięki, ale pytałem też o praktyczne zastosowanie tych systemów formalnych. Ponoć jest coś takiego( gdzie jest potrzeba otrzymywania pewnych wniosków), ale nie wiem co dokładnie.

Jakub Gurak pisze:(...) No bo jak zauważył foundofmath dowód tego, że dla dowolnych zbiorów \(\displaystyle{ X,Y}\) mamy \(\displaystyle{ X \cap Y=Y \cap X,}\) zajął mu 52 formuły, i sam się też zastanawiał jak zrobić dowody bardziej doniosłych twierdzeń teorii mnogości. (...)

Przy czym tyle było w wersji swobodnego dobierania sobie tautologii krz, przy korzystaniu z ustalonych na wstępie 8 tautologii krz (stanowiących podzbiór skończonej aksjomatyki zbioru wszystkich tautologii krz) - ok. 460 formuł (przy tych samych regułach dowodzenia, tych samych tautologiach zawierających kwantyfikatory i tych samych aksjomatach specyficznych teorii).

Ale ręcznie tego chyba nie pisałeś( to program Ci to zrobił).

A widzisz w tym dowodzie kierunek zmierzania do celu (w końcu te dowody formalne skądś się biorą- chyba to nie jest zupełny przypadek).

Ręcznie, nie korzystałem z żadnych programów w dowodzie tego twierdzenia.

Kierunek jest następujący - przeprowadzasz standardowe rozumowanie (w aksjomatycznej teorii mnogości), uzmysławiasz sobie z jakich praw logicznych korzystałeś (rachunek predykatów), pedantycznie uściślasz swoje rozumowanie semantyczne w oparciu o te prawa, zapisujesz tezę w danym języku i starasz się połączyć poszczególne ogniwa rozumowania semantycznego przy użyciu obranych reguł wnioskowania syntaktycznego (dla odpowiedniego naboru formuł języka teorii). Oczywiście pożądana jest biegłość we wnioskowaniu syntaktycznym w logice (teoretycznie rzecz biorąc nie jest nieodzowna, jednak żeby nie liczyć specjalnie ani na łut szczęścia ani na maniakalny upór, to bez tego ani rusz).

Nie jestem ekspertem, ale zainteresowałem się niedawno programem Coq służącym między innymi do komputerowej weryfikacji dowodów twierdzeń matematycznych. Z tego co można wyczytać we wstępie darmowej elektronicznej książki Software Foundations poświęconej programowi Coq, znajduje on wiele praktycznych zastosowań poza samą matematyką teoretyczną. Cytat:

Coq has been a critical enabler for a huge variety of work across computer science and mathematics:

• As a platform for modeling programming languages, it has become a standard tool for researchers who need to describe and reason about complex language definitions. It has been used, for example, to check the security of the JavaCard platform, obtaining the highest level of common criteria certification, and for formal specifications of the x86 and LLVM instruction sets and programming languages such as C.
• As an environment for developing formally certified software and hardware, Coq has been used, for example, to build CompCert, a fully-verified optimizing compiler for C, and CertiKos, a fully verified hypervisor, for proving the correctness of subtle algorithms involving floating point numbers, and as the basis for CertiCrypt, an environment for reasoning about the security of cryptographic algorithms. It is also being used to build verified implementations of the open-source RISC-V processor.
• As a realistic environment for functional programming with dependent types, it has inspired numerous innovations. For example, the Ynot system embeds "relational Hoare reasoning" (an extension of the Hoare Logic we will see later in this course) in Coq.
• As a proof assistant for higher-order logic, it has been used to validate a number of important results in mathematics. For example, its ability to include complex computations inside proofs made it possible to develop the first formally verified proof of the 4-color theorem. This proof had previously been controversial among mathematicians because part of it included checking a large number of configurations using a program. In the Coq formalization, everything is checked, including the correctness of the computational part. More recently, an even more massive effort led to a Coq formalization of the Feit-Thompson Theorem — the first major step in the classification of finite simple groups.

Moje rozumienie tego co umożliwia ten program wygląda mniej więcej tak, że pozwala on za pomocą metod matematycznych (logicznych) weryfikować poprawność algorytmów rzeczywistych programów komputerowych.

Skoro wykazano, że aksjomat wyboru jest niezależny od pozostałych aksjomatów teorii mnogości, a teoria klas NBG jest rozszerzeniem teorii mnogości ZFC, i teoria klas jest teorią skończenie aksjomatyzowalną (tzn. można ją ująć w skończony układ aksjomatów), to aby wykazać niesprzeczność teorii klas NBG, wystarczy wykazać, że pierwszy aksjomat, dajmy na to aksjomat zbioru pustego, jest niezależny od pozostałych aksjomatów (których jest skończona ilość, więc można zrobić to ręcznie, tzn. pojedyńczo ), dalej pokazać, że kolejny aksjomat jest niezależny od pozostałych (oczywiście nie musimy już sprawdzać niezależności tego aksjomatu z pierwszym),...; dzięki czemu możemy dodawać takie aksjomaty do pozostałych; rachunek predykatów jest teorią niesprzeczną, więc ponieważ pierwszy aksjomat, aksjomat zbioru pustego, jest niezależny od pozostałych aksjomatów, to możemy go dodać do aksjomatów rachunku predykatów, podobnie możemy dodać drugi aksjomat, itd. ..., i tak do ostatniego, i otrzymać niesprzeczność teorii mnogości NBG, a więc otrzymamy niesprzeczność całej (w zasadzie) matematyki.

Ma to sens
(Jestem logik )

Nie, to nie ma sensu. Trzeba wyjaśnić, że w praktyce "niezależność od aksjmatów ZF(C)" oznacza relatywną niezależność, tzn. niezależność przy założeniu, że ZF(C) jest niesprzeczna. I tak np. "pewnik wyboru AC jest niezależny od ZF" znaczy dokładniej:

"jeśli ZF jest niesprzeczna, to nie można w niej udowodnić ani AC ani negacji AC".

Podobnie z niezależnością hipotezy continuum CH od ZFC (Goedel-Cohen, forcing itd.).

Tego typu niezależność nie może być użyta do dowodu niesprzeczności matematyki.

Niesprzeczność ZF może być zapisana jako zdanie w języku ZF: \(\displaystyle{ Con(ZF)}\). Podobnie dla rozszerzeń ZF. I teraz w ZFC można udowodnić, że następujące zdania sa równoważne:
\(\displaystyle{ Con(ZF), Con(ZFC), Con(ZFC+CH), Con(ZFC+\neg CH)}\). Ogólniej metoda forcingu prowadzi do wzbogaceń ZFC o mocy niesprzecznościowej równej ZFC. Natomiast wzbogacenia ZFC o aksjomaty o istnieniu dużych liczb kardynalnych mają moc niesprzecznościową większą niż ZFC. Tzn. w tych wzbogaceniach można udowodnić, że ZFC jest niesprzeczna.