🚀 go-pugleaf

On Jul 20, 9:51 am, Maciej Woźniak <mlwozniak_no_sp...@wp.pl> wrote:
> Użytkownik "Wlodzimierz Holsztynski (Wlod)" <sennaj...@gmail.com> napisał w
>
> >Wierzę w to, bo to w sensie staroświeckim,
> >prehilbertowskim, udowodniłem. Dopóki danego
> >kawałka metateorii nie sformalizujemy, to lepiej
> >dowodzić nie można.
>
> Ja też w to wierzę. A jak sformalizujemy, to,
> zauważ, dowód będzie lepszy (a co to znaczy?),
> ale podstaw do wierzenia nie da żadnych. Bo
> formalnie implikacji (udowodniłem p, więc p)
> nie ma.
> Na czym zatem będzie polegała wyższość dowodu
> formalnego nad tym, co teraz jest? Każdy, kto
> będzie chciał, zaneguje to twierdzenie i tak,
> i tak.

Najpierw miejmy na oku dokładnie to o czym mowimy
(nie przeczę Ci, a tylko chcę jasności w rozmowie):

1. Pokazałem/ twierdziłem, że coś jest skomponowaną
regułą, oraz że skomponowane reguły od twierdzeń
teorii prowadzą do twierdzen teorii (rachunku zdań);
i w tym sensie są pożyteczne.

2. Pokazałem to bez żadnej ramy formalnej dla takich
meta-twierdzeń. Pokazałem to w sensie staroświeckim:
90% matematyków zgodzi się bez wahania, że dałem
dowód (w staroświeckim sensie).

3. Alonzo Church przy takich okazjach z góry powiedziałby
niedowiarkom: jeżeli nie wierzysz w moje meta-twierdzenie
o skomponowaniu X |--> Z to przy każdej okazji, gdy ja
je stosuję, to Ty rób moje kroki  X |-> Y oraz Y |-> Z,  czyli
traktuj moje meta-twierdzenie jak makro, za które należy
podstawić kroki z dowodu.

4. Człowiek mechanicznie, albo komputer, może sprawdzić
statystycznie, że meta-twierdzenie zadziałało sto razy na sto,
albo 9999 na 10000, a w tym jednym przypadku był robak,
i po usunięciu robaka dostało się 10000 razy na 10000,
czyli że wygląda to bardzo prawdopodobnie.

5. Stworzenie ramy formalnej, obejmującej dane meta-pojęcie
skomponowania |-->,  oraz dowodów kom,pozycji, samego
meta-twierdzenia ani jego użyteczności dla teorii rachunku
zdań nie zmieniłoby ani na jotę, ani nawet dowodu -
byłyby takie same, i znaczyłyby to samo. (Zakładam, że
formalizacji celem było "zalegalizowanie" |-->. Inne
formalizacje mogą mieć inne cele, niekoniecznie zbieżne
z moim).

Z punktu widzenia rozwijania teorii rachunku zdan nic
się istotnie nie zmieniło.

6. Formalizacja kawałka meta-teorii stworzyłoby nowy
kawałek matematyki. Wtedy poprawność mojego meta-
twierdzenia, które stałoby się twierdzeniem nowej
teorii byłaby w zasadzie czymś pewnym (w o wiele-
wiele-wiele wyższym stopniu niż poprzednia pewność),
ale to jest pewność czegoś innego niż przedtem.
Przedtem chodziło o pewność stosowania go do
'rachunku zdań, a teraz o pewność, że mamy dowód
formalny w nowej teorii. Dorobienie formalizacji
kawałka meta-teorii jest cenne, redukuje wieloznaczność
i "staroświeckość", ale w sensie dosłownym to wpływu na
teorię oryginalną nie ma. Realcja badanego met-twierdzenia
do oryginalnej teorii pozostaje oczywiście taka sama.
Co najwyżej nasze samopoczucie się może zmienić.

To tak jak z opinią o związki pewnej własności
samochodu z jego bezpieczeństwem. możemy
taką opinię wyciągnąć z kapelusza, bez uzasadniania
i wyprowadzania tej opinii z meta-teorii samochodu,
lub możemy opinię uzasadnić teoretycznie. W drugim
wypadku poczujemy się lepiej. Ale opinia jest
opinią, i działa tak samo dobrze z uzasadnieniem jak
i ze zgadnięcia. Albo: na oko powiem, że ten okręt
wystaje nad wodą 8 metrów. Ktoś inny zastosuje
wiedzę i Talesa, i policzy, że statek wystaje 8m
ponad wodą. Obie opinie mówią to samo o statku.

> >Tak czy inaczej, logika tu nie ma jeszcze
> >nic do rzeczy. My dopiero logikę budujemy,
> >a raczej jej mały kawałek. Budujemy ją
> >jak mechaniczną zabawkę. Jak inżynierzy.
>
> My, inżynierzy, nie budujemy bez logiki.

Ja mówiłem o dziale naukowym, zwanym
"Logika matematyczna". Ty natomiast mówisz
o logice w sensie: łebski facet, ostry, rozsądny,
i nie w ciemię bity.

> >Trybiki mają pasować, itd.
>
> To nie mozna budować z samej stali. Pewna
> ilość gumy musi zostać. I smar będzie
> niezbędny.

Jest ogromna, zasadnicza różnica w ilości
tego smaru. W przypadku matematyki
formalnej dziwne rzeczy mogą się dziać
dopiero przy napisach, więc i przy przedziałach
czasu potrzebnych na ich parsowanie, tak długich,
że przestają działać zwykłe prawa fizyki.

> Czysty formalizm nie ma prawa praktycznie
> działać. Mówię to jako inżynier od
> informacyjnych konstrukcji trybikowych.

Czyli nie masz tytułu, żeby o tym
mowić :-)

To był tylko żarcik wskazujący na zabawność
Twojego stwierdzenia.

A tak serio, to "praktycznie" formalizm działa
na całego. Do moich "obiekcji einsteinowskich"
chyba jeszcze daleko, choć klasyfikacja
skończonych grup prostych (o wiele mniej
twierdzenia Perelmana, bo jednak otrzymał
je pojedynczy człowiek) może niepokoić.

Przy ogromnie długich dowodach
błędy staną się prawem statystycznym,
a nie czymś co zawsze można tak czy siak
naprawić. Przy tak długich dowodach trudno
będzi mówić o ich stalości w czasie, bo
dowody są czymś materialnym, z materii
(muszą jakoś by gdzieś zapisane), więc
ulegają zniszczeniu (papier butwieje, pamięc
komputerowa nawala, ...). Poza tym jak potwierdzić
dowód, gdy każde jego przeczytanie zajmuje
dłużej niż ludzkie życie?

Moje obiekcje związane są z kontaktem
skończoności (my) z nieskończonością.

Pozdrawiam,

    Włodek