🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: alt.pl.matematyka
Article #9729

Re: Letnie zniechęcenie z Robakksem.

#9729
From: Mateusz Grotek
Date: Wed, 15 Jul 2009 21:53
130 lines
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-mail
References: <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