Nadmierne formalizmy

Algebra zbiorów. Relacje, funkcje, iloczyny kartezjańskie... Nieskończoność, liczby kardynalne... Aksjomatyka.
Jakub Gurak
Użytkownik
Użytkownik
Posty: 1404
Rejestracja: 20 lip 2012, o 21:19
Płeć: Mężczyzna
Lokalizacja: Rzeszów
Podziękował: 61 razy
Pomógł: 83 razy

Nadmierne formalizmy

Post autor: Jakub Gurak »

Spróbuję pokazać że nadmierne formalizowanie może odciągnąć oczy od tego co istotne i doprowadzić do błędu. Tak było z jednym zadań na ważniaku. Oto one:
Udowodnij, że dla każdego dobrego porządku \(\displaystyle{ \displaystyle (X,\leq)}\) istnieje funkcja, która niepustym podzbiorom \(\displaystyle{ \displaystyle X}\) przypisuje ich element najmniejszy. Funkcje tę nazywamy \(\displaystyle{ \displaystyle \min: \mathcal{P}(X) \setminus \left\{\emptyset\right\} \rightarrow X}\)
W tym zadaniu nie ma co dowodzić... Możemy bowiem zdefiniować:

\(\displaystyle{ \displaystyle \min (A)=a}\) - element najmniejszy w \(\displaystyle{ \displaystyle A}\) względem dobrego uporządkowania \(\displaystyle{ \displaystyle \leq}\).

Wiemy bowiem, że zawsze w danym podzbiorze zbioru uporządkowanego istnieje co najwyżej jeden element najmniejszy. \(\displaystyle{ \displaystyle (X,\leq)}\) jest dobrym porządkiem, więc w każdym niepustym podzbiorze \(\displaystyle{ \displaystyle X}\) istnieje element najmniejszy. I tyle.

A na ważniaku, robią to tak:
Zdefiniujemy zbiór \(\displaystyle{ \displaystyle \min}\) następująco:

\(\displaystyle{ \displaystyle \min = \{z\in \mathcal{P}(\mathcal{P}(\mathcal{P}(X)\cup X)): \exists_{A\in \mathcal{P}(X)}\exists_{a\in X} [ z=(A,a) \wedge \forall_{b\in A} a\leq b ] \}.}\)

Istnienie zbioru \(\displaystyle{ \displaystyle \min}\) wynika z aksjomatu wyróżniania.
Niewątpliwie. Ale po co tak rozpisywać Nie ma co, w końcu to \(\displaystyle{ 12}\) ostatni wykład... Ja bym poprzestał na tym:

\(\displaystyle{ \min=\left\{ \left( A,a\right)\in \Bigl( P\left( X\right) \setminus \left\{ \emptyset \right\} \Bigr) \times X \biggl| \quad a \hbox{ jest elementem najmniejszym w } A \hbox{ względem } \le \right\}}\)

Ale jak chcą rozpisywać to, ... proszę bardzo, tylko niech poprawnie zrobią to zadanie. To im się do końca nie udało...

Aby to pokazać, może upewnijmy się najpierw że rzeczywiście jest to wybieranie spośród iloczynu kartezjańskiego \(\displaystyle{ \mathcal{P}(X) \times X}\).
Ukryta treść:    
Więc w szczególności \(\displaystyle{ \mathcal{P}(X) \times X \subset \mathcal{P}\left( \mathcal{P}(\mathcal{P}(X) \cup X)\right)}\) Zatem zbiór

\(\displaystyle{ \{z\in \mathcal{P}(\mathcal{P}(\mathcal{P}(X)\cup X)): \exists_{A\in \mathcal{P}(X)}\exists_{a\in X} \quad z=(A,a)\}}\) oznacza nic innego jak iloczyn kartezjański \(\displaystyle{ \mathcal{P}(X) \times X}\)

wobec czego \(\displaystyle{ \displaystyle \min}\) jest relacją \(\displaystyle{ \displaystyle \min \subset \mathcal{P}(X) \times X}\). Nie jest to jednak funkcja. Czas na kontrprzykład:

Rozważmy \(\displaystyle{ \left( \NN, \le\right)}\) gdzie \(\displaystyle{ \le}\) oznacza standardowy porządek na liczbach naturalnych. Jest to klasyczny dobry porządek. Przykładając do definicji zbioru \(\displaystyle{ \displaystyle \min}\):

Jest \(\displaystyle{ \left\{ 3,4,5\right\}\in \mathcal{P}(\NN)}\), jest \(\displaystyle{ 2\in \NN}\), że \(\displaystyle{ 2<3,4,5}\). Oznacza to że \(\displaystyle{ \left( \left\{ 3,4,5\right\},2\right) \in \displaystyle \min}\)

Jest \(\displaystyle{ \left\{ 3,4,5\right\}\in \mathcal{P}(\NN)}\), jest \(\displaystyle{ 1\in \NN}\), że \(\displaystyle{ 1<3,4,5}\). Oznacza to że \(\displaystyle{ \left( \left\{ 3,4,5\right\},1\right) \in \displaystyle \min}\) Wobec czego \(\displaystyle{ \displaystyle \min}\) nie jest funkcją.

Wiadomo, zapomnieli warunku \(\displaystyle{ a\in A}\)...

Ale to nie wszystko. Jest jeszcze problem z pustym podzbiorem...

Zbiorowi pustemu \(\displaystyle{ \left\{ \right\}}\) nie chcemy nic przyporządkowywać( bo w zbiorze pustym \(\displaystyle{ \left\{ \right\}}\) nie ma elementu najmniejszego). Tymczasem ta definicja zbiorowi pustemu przyporządkowuje dowolny element. Weźmy tak samo zbiór liczb naturalnych ze zwykłym porządkiem. Niech \(\displaystyle{ n}\) będzie dowolną liczbą naturalną. Przykładając do definicji zbioru \(\displaystyle{ \displaystyle \min}\):
Jest \(\displaystyle{ \left\{ \right\} \in \mathcal{P}(\NN)}\), jest \(\displaystyle{ n\in \NN}\), że \(\displaystyle{ \bigwedge\limits_{b\in \left\{ \right\}} n \le b}\). To oczywiście prawda, wobec czego \(\displaystyle{ \Bigl( \left\{ \right\},n\Bigr) \in \displaystyle \min}\),
Co wobec dowolności wyboru \(\displaystyle{ n}\) oznacza że \(\displaystyle{ \displaystyle \min}\) przypisuję zbiorowi pustemu dowolną liczbę naturalną, a więc bardzo niedobrze.

Widać więc że pomimo tego rozpisywania, autorzy ważniaka nie zadbali o wszystko co potrzebne...
Ja natomiast nie jestem nazbyt formalny. Dbam jednak o precyzję zawsze gdy zauważę że jest ona niezbędna. I właśnie o to chodzi w matematyce. A nie tyle o to by formalizować.
Ostatnio zmieniony 10 gru 2016, o 18:24 przez Jan Kraszewski, łącznie zmieniany 1 raz.
Powód: Poprawa wiadomości.
Jan Kraszewski
Administrator
Administrator
Posty: 34238
Rejestracja: 20 mar 2006, o 21:54
Płeć: Mężczyzna
Lokalizacja: Wrocław
Podziękował: 3 razy
Pomógł: 5203 razy

Nadmierne formalizmy

Post autor: Jan Kraszewski »

Nie jestem namiętnym czytelnikiem ważniaka, więc nie wiem, w jakim kontekście pojawia się ta notacja. Niewątpliwe jest też, że jego autorzy nie uniknęli wskazanych przez Ciebie niedokładności. Natomiast czasami taka formalizacja jest ważna. Gdy pozostajemy na gruncie Naiwnej Teorii Mnogości (NTM), to nadmiar formalizmu jest wadą, która może utrudniać zrozumienie istoty rzeczy. Natomiast gdy wkraczamy na teren Aksjomatycznej Teorii Mnogości (ATM), to o formalizm musimy dbać, jest on w pewnym sensie niezbędny. Opisany przez Ciebie przykład wydaje się dotyczyć tej drugiej sytuacji - jeżeli tak, to zastrzeżenia mogą budzić wspomniane błędy, ale nie forma zapisu. Oczywiście, można ten formalizm przekazać w mniej lub bardziej strawny sposób, ale to już inna kwestia.

Warto zauważyć, że o ile NTM jest językiem matematyki i każdy matematyk ma z nią styczność, to z ATM kontakt mają raczej nieliczni i ich formalizm nie odstrasza (także dlatego, że wiedzą, po co on jest).

JK
Jakub Gurak
Użytkownik
Użytkownik
Posty: 1404
Rejestracja: 20 lip 2012, o 21:19
Płeć: Mężczyzna
Lokalizacja: Rzeszów
Podziękował: 61 razy
Pomógł: 83 razy

Nadmierne formalizmy

Post autor: Jakub Gurak »

Jan Kraszewski pisze:Niewątpliwe jest też, że jego autorzy nie uniknęli wskazanych przez Ciebie niedokładności.
I oni chyba nie mogą już tego poprawić I w ogóle, materiały z ważniaka zostały zatwierdzone około \(\displaystyle{ 2007}\) roku i zatem nie mogą być już poprawiane, tak Bardziej z ciekawości pytam.
Jan Kraszewski pisze:Gdy pozostajemy na gruncie Naiwnej Teorii Mnogości (NTM), to nadmiar formalizmu jest wadą, która może utrudniać zrozumienie istoty rzeczy. Natomiast gdy wkraczamy na teren Aksjomatycznej Teorii Mnogości (ATM), to
Już nie

Też uważam, że wtedy nadmiar formalizmu jest wadą, która może niewątpliwie utrudniać zrozumienie istoty rzeczy... Chociażby nasz zbiór \(\displaystyle{ \min}\)...

Na razie tyle. Potem może rozwinę myśli.
Jan Kraszewski
Administrator
Administrator
Posty: 34238
Rejestracja: 20 mar 2006, o 21:54
Płeć: Mężczyzna
Lokalizacja: Wrocław
Podziękował: 3 razy
Pomógł: 5203 razy

Nadmierne formalizmy

Post autor: Jan Kraszewski »

Jakub Gurak pisze:I oni chyba nie mogą już tego poprawić I w ogóle, materiały z ważniaka zostały zatwierdzone około \(\displaystyle{ 2007}\) roku i zatem nie mogą być już poprawiane, tak Bardziej z ciekawości pytam.
To chyba pytanie do warszawiaków.
Jakub Gurak pisze:
Jan Kraszewski pisze:Gdy pozostajemy na gruncie Naiwnej Teorii Mnogości (NTM), to nadmiar formalizmu jest wadą, która może utrudniać zrozumienie istoty rzeczy. Natomiast gdy wkraczamy na teren Aksjomatycznej Teorii Mnogości (ATM), to
Już nie
W ATM dokładny formalizm jest niezbędny, przynajmniej na początku, ale można go podać w mniej lub bardziej strawnej formie. Ja np. raz definiuję iloczyn kartezjański w opisany sposób (jako podzbiór stosownego iloczynu kartezjańskiego), a potem używam go, a nie odwołuję się za każdym razem do definicji.

Ale o ile rozpatrywane w kontekście NTM rozważania ważniakowe są zupełnie przestrzelone i nie na miejscu, to rozpatrywane w kontekście ATM są już tylko niezgrabne.

JK
Jakub Gurak
Użytkownik
Użytkownik
Posty: 1404
Rejestracja: 20 lip 2012, o 21:19
Płeć: Mężczyzna
Lokalizacja: Rzeszów
Podziękował: 61 razy
Pomógł: 83 razy

Nadmierne formalizmy

Post autor: Jakub Gurak »

Jan Kraszewski pisze:Ale o ile rozpatrywane w kontekście NTM rozważania ważniakowe są zupełnie przestrzelone i nie na miejscu, to rozpatrywane w kontekście ATM są już tylko niezgrabne.
Tak, rozumiem. Niezgrabne, no i te wskazane błędy ( bo bez nich chyba nie zakładałbym tego tematu).

Może jeszcze myśl dnia: Żaden logik formalny, nawet najwybitniejszy, nie rozwinąłby za bardzo teorii mnogości, bazując wyłącznie na logice i formalnym przekształcaniu napisów. Bez zrozumienia sytuacji mnogościowej zbyt wiele nie zrobi. Aby rozwinąć teorię mnogości w takim stopniu jak chociażby aksjomatyczna teoria mnogości na ważniaku, to niewątpliwie trzeba rozumieć sytuację mnogościową.
krl
Użytkownik
Użytkownik
Posty: 609
Rejestracja: 10 lis 2009, o 22:39
Płeć: Mężczyzna
Lokalizacja: Wrocław
Pomógł: 135 razy

Nadmierne formalizmy

Post autor: krl »

Dodam, że są różne poziomy formalizmu, adekwatne do sytuacji. Poziom dla zwykłych matematyków to NTM. Dla specjalistów z teorii mnogości: czasami ATM. Ale jest jeszcze poziom hardkorowy formalizmu:
tu nie tylko formalnie zapisujemy wszystkie formuły (bez użycia skrótów), ale również stosujemy dowody formalne w ramach aksjomatycznego systemu rachunku predykatów. To jest "formalizm ostateczny": matematyka przestaje być tu czytelna już zupełnie. Choć tego ostatniego rodzaju formalizmu nigdzie się w praktyce nie stosuje, jego istnienie jest ważne dla rozważań metamatematycznych.
Jakub Gurak
Użytkownik
Użytkownik
Posty: 1404
Rejestracja: 20 lip 2012, o 21:19
Płeć: Mężczyzna
Lokalizacja: Rzeszów
Podziękował: 61 razy
Pomógł: 83 razy

Nadmierne formalizmy

Post autor: Jakub Gurak »

krl pisze:Choć tego ostatniego rodzaju formalizmu nigdzie się w praktyce nie stosuje, jego istnienie jest ważne dla rozważań metamatematycznych.
A to ciekawe. Możesz napisać coś więcej
krl
Użytkownik
Użytkownik
Posty: 609
Rejestracja: 10 lis 2009, o 22:39
Płeć: Mężczyzna
Lokalizacja: Wrocław
Pomógł: 135 razy

Nadmierne formalizmy

Post autor: krl »

Chodzi o rozważania w logice matematycznej, na temat matematyki. Np. twierdzenia Goedla, twierdzenie Tarskiego (o niedefiniowalności prawdy). Metamatematyczne rozważania na temat dowodów w matematyce: tu kluczowe jest twierdzenie Godla o pełności klasycznego rachunku predykatów, dzięki któremu wiemy, że definicja dowodu formalnego jest poprawna. Teoria mnogości jest w tym kontekście jedną z wielu teorii matematycznych, pełni ona jednak rolę wyjątkową...
Jakub Gurak
Użytkownik
Użytkownik
Posty: 1404
Rejestracja: 20 lip 2012, o 21:19
Płeć: Mężczyzna
Lokalizacja: Rzeszów
Podziękował: 61 razy
Pomógł: 83 razy

Re: Nadmierne formalizmy

Post autor: Jakub Gurak »

Twierdzenie Gödla mówi, że w rachunku predykatów tautologie są tym samym co twierdzenia. Nie wiem czy dobrze rozumiem pojęcie tautologii rachunku predykatów (bo nie przebrnę przez te wszystkie definicję: modelu, ...). Ale, mówiąc prosto, podobnie jak dla tautologii rachunku zdań, domyślam się, że tautologia rachunku predykatów, to podobnie prawo rachunku predykatów(tylko dochodzą tu jeszcze kwantyfikatory, i w dowolnych zbiorach niepustych, po których przebiegają kwantyfikatory, dla dowolnego rozumienia znaczenia formuł całe zdanie jest prawdziwe, tak ), czy można tak w uproszczeniu powiedzieć, że to jest prawo rachunku predykatów A twierdzenie- wiadomo- to formuła, która ma dowód formalny, jest konsekwencją układu aksjomatów.Tylko co ma do siebie prawo logiczne do pisania żmudnych znaczków? Jedyne co mi przychodzi na myśl, to prawo to jest prawo- zawsze prawdziwe, a dowody formalne chyba też to jest prawda, bo aksjomaty rachunku predykatów, to chyba nie tyko metody formalne, ale one też głoszą pewną prawdziwą treść, więc ich konsekwencje formalne również są prawdziwe. Czyli to jest prawda, i to jest prawda.

Z ciekawości spytam, jak bardzo żmudne są dowody formalne Czy prosty krok semantyczny jest trochę (kilka razy) bardziej żmudny formalnie, czy może o wiele bardziej, i trzeba tu widzieć coś powtarzającego się, nie wiem.

W każdym bądź razie dokładne semantyczne(pod względem znaczenia) dowody podstaw teorii mnogości, bym szacował, że byłyby około 3 razy dłuższe (czyli materiał teorii mnogości na ważniaku byłby 3 razy większy), a syntaktycznie 5 razy wìększy, jeśli nie więcej .

A autorzy ważniaka mają to wszystko wystarczająco formalnie zrobione, tak Po wprowadzeniu teorii mnogości ZFC, piszą, że wszystkie późniejsze dowody bazują na aksjomatyce ZFC, i wygląda, że chyba tak. Głównym(chyba, pierwszym wymienionym ) autorem jest Pan prof. Marek Zaionc, Profesor Podstaw Matematyki. Jeśli tak, to podziwiam.
krl
Użytkownik
Użytkownik
Posty: 609
Rejestracja: 10 lis 2009, o 22:39
Płeć: Mężczyzna
Lokalizacja: Wrocław
Pomógł: 135 razy

Re: Nadmierne formalizmy

Post autor: krl »

1. Zasadniczo, tak.
2. Tak.
3. Tu jest przykład dowodu formalnego: 416086,15.htm
4. To jest kwestia subiektywna. O możliwych poziomach formalizmu pisałem powyżej w tym wątku.
ODPOWIEDZ