szukanie zaawansowane
 [ Posty: 6 ] 
Autor Wiadomość
Mężczyzna Offline
PostNapisane: 29 mar 2019, o 21:42 
Użytkownik

Posty: 503
Lokalizacja: Rzeszów
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 X,Y mamy 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ą :?:
Uniwersytet Wrocławski Instytut Matematyczny - rekrutacja 2019
Góra
Mężczyzna Offline
PostNapisane: 30 mar 2019, o 12:08 
Użytkownik

Posty: 360
Lokalizacja: Warszawa
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... ).
Góra
Mężczyzna Offline
PostNapisane: 30 mar 2019, o 22:16 
Użytkownik

Posty: 503
Lokalizacja: Rzeszów
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.
Góra
Mężczyzna Offline
PostNapisane: 8 kwi 2019, o 01:10 
Użytkownik

Posty: 62
Jakub Gurak napisał(a):
(...) No bo jak zauważył foundofmath dowód tego, że dla dowolnych zbiorów X,Y mamy 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).
Góra
Mężczyzna Offline
PostNapisane: 8 kwi 2019, o 22:32 
Użytkownik

Posty: 503
Lokalizacja: Rzeszów
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).
Góra
Mężczyzna Offline
PostNapisane: 9 kwi 2019, o 01:19 
Użytkownik

Posty: 62
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).
Góra
Utwórz nowy temat Odpowiedz w temacie  [ Posty: 6 ] 


 Zobacz podobne tematy
 Tytuł tematu   Autor   Odpowiedzi 
 uwagi do teorii informacji Shannona  artbyte  2
 Dlaczego logiki nie naucza się w szkole średniej?  iksinski  2
 Jak uczyc sie teorii?  moniac91  1
 Elementy logiki w szkole  Anonymous  42
 Jak samodzielnie uczyć się teorii mnogości?  realpetr  1
 
Atom [Regulamin Forum] [Instrukcja LaTeX-a] [Poradnik] [F.A.Q.] [Reklama] [Kontakt]
Copyright (C) Karpatka.pl