Article View: alt.pl.matematyka
Article #9729Re: Letnie zniechęcenie z Robakksem.
From: Mateusz Grotek
Date: Wed, 15 Jul 2009 21:53
Date: Wed, 15 Jul 2009 21:53
130 lines
6574 bytes
6574 bytes
Robakks pisze: > z alt.pl.matematyka > "Mateusz Grotek" <unoduetre@poczta.onet.pl> > news:h3k77e$d69$1@news.onet.pl... > >> Hejka. Postanowiłem założyć nowy wątek, bo tamten dotyczył troszkę >> czegoś innego. Czyli co, chcesz stworzyć translację teorii mnogości na >> geometrię? Pomysł ciekawy, ale pojawi się problem. Geometria w >> aksjomatyce Tarskiego w logice 1 rzędu jest rozstrzygalna, a poza tym >> nie potrafi kwantyfikować po zbiorach/predykatach punktów/linii etc. Ale >> możemy użyć jakiejś innej aksjomatyki. Na przykład aksjomatyki Hilberta, >> którą można zapisać w logice 1 lub 2 rzędu, lub nawet aksjomatyki >> Tarskiego w logice 2 rzędu lub 1 rzędu wzbogaconej o jakąs postać teorii >> mnogości. >> >> Garść informacji: >> >> http://www.math.umbc.edu/~campbell/Math306Spr02/notes/ - notatki z >> wykładu, na dole są podane różne aksjomatyki. Jest użyty język >> naturalny, więc nie będziesz mieć problemu ich zrozumieniem, o ile >> znasz angielski. Należy przy tym zaznaczyć, że aksjomatyka Euklidesa nie >> jest pełna, gdyż używa on pojęć których nie definiuje do wyprowadzenia >> niektórych twierdzeń. Ale w końcu to było w roku 300 p.n.e. Niestety >> jest tam też kilka niejasności :-( >> >> Tu informacje o rozstrzygalności: >> http://math.berkeley.edu/~scanlon/papers/dedfg1.pdf >> >> Tutaj 3 aksjomatyki opisane: >> http://en.wikipedia.org/wiki/Hilbert%27s_axioms >> http://en.wikipedia.org/wiki/Tarski%27s_axioms >> http://en.wikipedia.org/wiki/Birkhoff%27s_axioms >> >> Tutaj cała książka Hilberta w której wprowadził swoją aksjomatykę: >> ftp://ftp.pg.psnc.pl/pub/1/7/3/8/17384/17384-pdf.pdf >> >> A tutaj aksjomatyka Hilberta w języku polskim: >> http://pl.wikipedia.org/wiki/Aksjomatyka_Hilberta >> >> To na wypadek gdybyś nie znał angielskiego. Jest ona sformułowana w >> języku naturalnym, więc nie powinieneś mieć problemu z jej zrozumieniem. >> Jednakże jeśli porównasz strony: >> http://en.wikipedia.org/wiki/Hilbert%27s_axioms >> i >> http://pl.wikipedia.org/wiki/Aksjomatyka_Hilberta >> to zauważysz że jak to zazwyczaj bywa polska strona jest do bani, bo >> błędnie podaje aksjomat ciągłości, gdyż używa pojęcia liczby naturalnej, >> którego w geometrii NIE MA. >> >> Informacje o aksjomatyce Tarskiego i jej rozwinięciach: >> http://www.math.ucla.edu/~asl/bsl/0502/0502-002.ps >> >> Szczerze mówiąc ja bym tu użył aksjomatyki Tarskiego wzbogaconej o >> mereologię. To mogłoby być dość ciekawe. Podejrzewam, że dostaniemy >> system zawierający arytmetykę :-) Więc nie powinno być problemu z >> formalizacją ZFC wewnątrz niego. >> >> Nadal jesteś zainteresowany zabawą z geometrią? To może być ciekawa >> rozrywka... Jeśli tak, to możemy coś wymyslić :-D > > Piszesz "używa pojęcia liczby naturalnej, którego w geometrii NIE MA." > Czym wobec tego wyskalowana jest oś liczbowa w geometrii > jeśli NIE MA w geometrii pojęcia liczby naturalnej ? :-) Liczby naturalne to dowolne obiekty spełniające aksjomaty arytmetyki. Chodzi tu o to, że aby mówić o liczbach naturalnych musimy znaleźć jakieś obiekty spełniające ich aksjomaty, a także odwzorować operacje arytmetyki na operacje geometryczne. Nie wystarczy tylko wybrać odpowiednich punktów, bo arytmetyka zawiera także operacje dodawania i mnożenia. Dlatego dla geometrii bez żadnej teorii mnogości pojawiają się problemy. Weźmy aksjomaty arytmetyki z poniższej strony: http://www.ltn.lv/~podnieks/gt3.html Przepisałem je w innej notacji: P12) ALL x. ~0=x+1 Dla każdego x nieprawda że zero jest równe następnikowi jakiejś liczby. P22) ALL x. ALL y. x+1=y+1 => x=y Dla dowolnych x,y x+1=y+1 implikuje x=y P32) ALL x. x+0=x P42) ALL x. ALL y. x+(y+1)=(x+y)+1 P52) ALL x. x*0=0 P62) ALL x. ALL y. x*(y+1)=(x*y)+x A to jest schemat aksjomatów indukcji. Podpada pod niego nieskończenie wiele aksjomatów, gdyż jest to schemat dla dowolnej formuły języka arytmetyki B(_) P72) ( B(0) & ALL x. (B(x)=>B(x+1)) ) => ALL x. B(x) B(_) - dowolna formuła języka arytmetyki, gdzie _ to jej wybrany parametr. B(0) i dla każdego x B(x) implikuje B(x+1) implikuje dla każdego x B(x) A więc, żeby mieć liczby musimy jakoś odwzorować mnożenie i indukcję. To się nie uda dla geometrii bez jakiejś teorii mnogości, gdyż jest ona rozstrzygalna, a arytmetyka nie jest. Rozstrzygalność polega na tym, że istnieje algorytm pozwalający stwierdzić, czy dane zdanie jest twierdzeniem danej teorii, czy nie. Inaczej mówiąc można napisać program na komputerze, który byćmoże po bardzo długim, aczkolwiek skończonym czasie odpowie na pytanie, czy dane twierdzenie jest dowodliwe, czy raczej jego zaprzeczenie. A więc nie można włożyć teorii nierozstrzygalnej do rozstrzygalnej, gdyż wtedy ta pierwsza byłaby rozstrzygalna na gruncie drugiej. Ale jeśli dołozymy jakąś formę teorii mnogości/typów itp. to prawdopodobnie wzmocnimy wystarczająco teorię. Proste wyjaśnienie powyższego: Nawet jeśli wybierzesz pewne punkty na osi jako liczby naturalne nie będziesz mógł zdefiniować operacji na nich. Geometria, bez mozliwości mówienia o zbiorach punktów a tylko o samych punktach nie pozwoli na zdefiniowanie wszystkich operacji na liczbach naturalnych. Aczkolwiek jeśli dopuści się mówienie o zbiorach punktów, prawdopodobnie (zgaduję) będzie możliwe zdefiniowanie tych operacji, a tym samym liczb naturalnych. > Edward Robak* z Nowej Huty > ~>°<~ > miłośnik mądrości > - - > kopia na pl.sci.filozofia
Technical Details
Message-ID:
<h3lj65$vg9$1@news.onet.pl>Path:
mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!newsfeed.gazeta.pl!news.onet.pl!not-for-mailReferences:
<h3k77e$d69$1@news.onet.pl> <h3ld69$rof$1@inews.gazeta.pl>Show Full Headers
Complete Article Headers
Path: mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!newsfeed.gazeta.pl!news.onet.pl!not-for-mail From: Mateusz Grotek <unoduetre@poczta.onet.pl> Newsgroups: alt.pl.matematyka Subject: Re: Letnie zniechęcenie z Robakksem. Date: Wed, 15 Jul 2009 23:53:25 +0200 Organization: http://onet.pl Lines: 130 Message-ID: <h3lj65$vg9$1@news.onet.pl> References: <h3k77e$d69$1@news.onet.pl> <h3ld69$rof$1@inews.gazeta.pl> NNTP-Posting-Host: smrw-91-193-87-5.smrw.lodz.pl Mime-Version: 1.0 X-Trace: news.onet.pl 1247694853 32265 91.193.87.5 (15 Jul 2009 21:54:13 GMT) X-Complaints-To: niusy@onet.pl NNTP-Posting-Date: Wed, 15 Jul 2009 21:54:13 +0000 (UTC) User-Agent: Thunderbird 2.0.0.19 (X11/20081227) In-Reply-To: <h3ld69$rof$1@inews.gazeta.pl> X-Enigmail-Version: 0.95.7 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit