🚀 go-pugleaf

Wlodzimierz Holsztynski pisze:
> Duże litery są meta-symbolami zdań, co znaczy
> że mamy do czynienia ze schematami, a konkretne
> reguły i aksjomaty uzyskujemy przez podstawienia
> zdań pod symbole A B ...  (w ramach danej reguły
> podstawiamy za dany symbol wszędzie to samo zdanie;
> dla różnych symboli można podstawiać różne zdania
> lub te same - i tak dobrze, i tak, byle konsekwentnie).
> 
> Oto reguły dowodzenia (w tym aksjomaty):
> 
> Odrywanie:
> =========
> 
>         A  ((~A) \/ B)  |->  B
> 
> Równoważność:
> ============
> 
> związek z implikacją:
> 
>     (A <=> B)  |->  ((~A) \/ B)
>     (A <=> B)  |->  ((~B) \/ A)
> 
>      ((~A) \/ B)  ((~B) \/ A)  |->  (A <=> B)
> 
> zwrotność -
> 
>     |-> (A <=> A)
> 
> przemienność:
> 
>     |->  ((A <=> B) <=> (B <=> A))
> 
> przechodniość:
> 
>    (A <=> B)  (B <=> C)  |->  (A <=> C)
> 
> *********
> 
> Udowodnijmy skomponowaną regułę dowodzenia:
> 
>     A  (A <=> B)  |-->  B
> 
> Dowód:
> 
>     (A <=> B)  |->  ((~A) \/ B)
> 
>     A  ((~A) \/ B)  |->  B
> 
> Koniec dowodu.
> 
> ***
> 
> Udowodnijmy skomponowaną regułę dowodzenia:
> 
>     (A <=> B)  |-->  (B <=> A)
> 
> Dowód 1:
> 
>     |->  ((A <=> B) <=> (B <=> A))
> 
>     ((A <=> B) <=> (B <=> A))  |->  ((~ (A <=> B)) \/ (B <=> A))
> 
>     (A <=> B)  ((~ (A <=> B)) \/ (B <=> A))   |-  (B <=> A)
> 
> Wolno nam w dowodach stosować już udowodnione
> reguły skomponowane. Zatem:
> 
> Reguła:
> 
>     (A <=> B)  |-->  (B <=> A)
> 
> Dowód 2:
> 
>     |->  ((A <=> B) <=> (B <=> A))
> 
>     (A <=> B)  ((A <=> B) <=> (B <=> A))  |-->  (B <=> A)
> 
> Koniec dowodu.
> 
> *********
> 
> Pozdrawiam,
> 
>     Włodek
Hej. Mam następujące aksjomaty:
p->~p->q
(~p->p)->p
(p-q)->(q->r)->p->r
Wydaje mi się, że dają logikę klasyczną. Ale dość trudno nimi operować. 
Zostawiam to jako zagadkę dla ciekawskich. Oczywiście łatwo napisać 
odpowiedni program. Ale właśnie chodzi tu o to, żeby zrobić to bez 
programu, ręcznie. Powiedzcie, jeśli uda wam się wyprowadzić następujące 
stwierdzenia:
p->q->p
(p->q->r)->(p->q)->p->r
Powodzenia. Według mnie dość trudno zacząć. Ciekawe, czy ktoś poradzi 
sobie z tym łatwo. Jeśli tak, to niech da znać, ale nie podaje dowodów. 
Też chcę mieć trochę przyjemności. :-D

On Jul 19, 7:32 pm, Mateusz Grotek <unodue...@poczta.onet.pl> wrote:
>
> Hej. Mam następujące aksjomaty:
> p->~p->q
> (~p->p)->p
> (p-q)->(q->r)->p->r

No tak, zacytowales cala moja wypowiedz,
zeby w ogole do niej nie odniesc sie.

Tego typu aksjomaty badal Jan Lukasiewicz.
Jegio celem miedzy uinnymi byla ekonomia
definicjui, nawet rekordy prostoty. Byl mistrzem
w takich rzeczach (i w ogole).

Moj cel wylozylem. Chodzi o klaropwny dowod
metqatwierdzenia o tym, ze twierdzenia
rachuhnku zdan i tautologie to to samo.
Pod tym katwem specjalnie dobieram dosyc
rozbudowana konstrukcje (a nie ekonomiczna)
 - dopasowuje ja do dowodu, by dowod uczynic latwym

Gdy to uczynie, to dam podstawe do
konstrukcji rownowaznych, ale juz
ekonomicznych konstrukcji. Dowody
poprawnosci tych nowych bedzie mozna sprowaedzac
do mojej.

Cweiczenia, ktore proponujesz w ogole
nie nakleza do tego watku. Mozesz otworzyc
watek pod roznymi tytulami, zaleznie od Twojego
celu.Gdy chiodzi Ci wylacznie o Ten jeden system, to
napisz w tytule cos jak:

 specjalne aksjomaty implikacji.

Gdy chcesz dyskutowac o roznych systemach,
to w tytule moze byc na przyklad:

    rozne aksjomatyki rachunku zdan

> Wydaje mi się, [...]

Hm, pisanie tu jest beznadziejne.
Wiecej przeszkadzaczy niz wspolgrajacych
lub chocby troche zaciekawionych tym co
jesrt napisane.

Szkoda, bo tak ladnie mi pomogles z programem
Mariusza. A tu taki klops.

Pozdrawiam,

    Wlodek

Wlodzimierz Holsztynski (Wlod) pisze:
> On Jul 19, 7:32 pm, Mateusz Grotek <unodue...@poczta.onet.pl> wrote:
>> Hej. Mam następujące aksjomaty:
>> p->~p->q
>> (~p->p)->p
>> (p-q)->(q->r)->p->r
> 
> No tak, zacytowales cala moja wypowiedz,
> zeby w ogole do niej nie odniesc sie.
> 

Racja. Przepraszam.

> Tego typu aksjomaty badal Jan Lukasiewicz.
> Jegio celem miedzy uinnymi byla ekonomia
> definicjui, nawet rekordy prostoty. Byl mistrzem
> w takich rzeczach (i w ogole).
> 
> Moj cel wylozylem. Chodzi o klaropwny dowod
> metqatwierdzenia o tym, ze twierdzenia
> rachuhnku zdan i tautologie to to samo.
> Pod tym katwem specjalnie dobieram dosyc
> rozbudowana konstrukcje (a nie ekonomiczna)
>  - dopasowuje ja do dowodu, by dowod uczynic latwym
> 
> Gdy to uczynie, to dam podstawe do
> konstrukcji rownowaznych, ale juz
> ekonomicznych konstrukcji. Dowody
> poprawnosci tych nowych bedzie mozna sprowaedzac
> do mojej.
> 
> Cweiczenia, ktore proponujesz w ogole
> nie nakleza do tego watku. Mozesz otworzyc
> watek pod roznymi tytulami, zaleznie od Twojego
> celu.Gdy chiodzi Ci wylacznie o Ten jeden system, to
> napisz w tytule cos jak:
> 
>  specjalne aksjomaty implikacji.
> 

Sądziłem, że jako, że problem związany z tematem wątku, którym jest 
rachunek zdań pozwolę sobie dorzucić to tutaj. Uważam, że ćwiczenie jest 
ciekawe. Nie chciałem zakładać innego wątku. Jedynym moim błędem było 
to, że zacytowałem całą twoją wypowiedź. Ale jeżeli uważasz, że wątek 
jest zamknięty na tematy z nim związane to trudno. :-(

> Gdy chcesz dyskutowac o roznych systemach,
> to w tytule moze byc na przyklad:
> 
>     rozne aksjomatyki rachunku zdan
> 
>> Wydaje mi się, [...]
> 
> Hm, pisanie tu jest beznadziejne.
> Wiecej przeszkadzaczy niz wspolgrajacych
> lub chocby troche zaciekawionych tym co
> jesrt napisane.

Po pierwsze dziękuję za określenie mnie przeszkadzaczem. Po drugie 
czytam ten wątek i nawet jestem zainteresowany, aczkolwiek nie mam nic 
do dodania na razie. Po trzecie chciałem tylko doradzić coś odnośnie 
Woźniaka, gdyż już dwukrotnie złapałem się na rozmowie z nim i wciąż 
występuje ten sam problem, a rozmowa wygląda tak samo. Ja coś wyjaśniam, 
męczę się a na końcu Woźniak stwierdza że to nie ważne/to jest inaczej 
bez podawania argumentów. Po prostu chciałem cię od tego uchrnonić.
> 
> Szkoda, bo tak ladnie mi pomogles z programem
> Mariusza. A tu taki klops.
>
Nie wiem jaka szkoda. Czyżbyś ocenił mnie na podstawie tego jednego 
postu? A jeśli chcesz mnie ocenić, to może po pierwsze przeczytaj inne 
moje posty. Po drugie mógłbyś docenić fakt, że chciałem podać ciekawe 
zadanie związane z tematem twoich postów. Nie sądzę, że jestem 
przeszkadzaczem, a tym bardziej nie świadczą o tym moje posty. Zgadza 
się, cytuję posty innych, przepraszam jeżeli zdarzyło mi się 
niepotrzebnie zacytować twój. Nie zrobiłem tego złośliwie. Poza tym 
wysłałem ten post dość późno i byłem zmęczony, tym bardziej że chciałem 
odpowiedzieć na inny twój post na innej grupie.  Rozumiem, że na 
usenecie jest dużo trolli, ale to nie powód by przeszkadzaczem określić 
każdego, kto po prostu zacytuje zbyt dużo i byćmoże wyśle posta nie do 
tego wątku do którego chciałeś. Chyba, że przez przeszkadzacza określasz 
osobę, która wysyła do ciebie rady w sprawie innych osób. Po pierwsze 
nikogo nie obraziłem. Po drugie jeśli nie zgadzasz się z moją opinią to 
twoja wola. Natomiast jeśli chciałeś uczynić ten wątek wątkiem tylko dla 
ciebie, to mogłeś wyraźnie zaznaczyć to w temacie, lub pierwszym poście. 
  Wiem, że łatwo szafować stwierdzeniami o byciu trollem itp. Ja 
podjąłem próbę porozumienia się z Woźniakiem, czego dowodem są moje 
wypowiedzi. Ty od razu nazwałeś mnie "przeszkadzaczem". Kończę tego 
posta. Przepraszam, że nie utworzyłem nowego wątku dla tego jednego 
posta, ale chciałem odpowiedzieć na twojego w tym samym wątku. 
Pozdrawiam i miłego pisania o rachunku zdań.



> Pozdrawiam,
> 
>     Wlodek

> Hej. Mam nast�puj�ce aksjomaty:
> p->~p->q
> (~p->p)->p
> (p-q)->(q->r)->p->r
> Wydaje mi si�, �e daj� logik� klasyczn�.

To wyprowadź z nich pV~p.

Mateusz Grotek napisał(a):

> Po pierwsze dzi�kuj� za okre�lenie mnie przeszkadzaczem. Po drugie
> czytam ten w�tek i nawet jestem zainteresowany, aczkolwiek nie mam nic
> do dodania na razie. Po trzecie chcia�em tylko doradzi� co� odno�nie
> Wo�niaka, gdy� ju� dwukrotnie z�apa�em si� na rozmowie z nim i wci��
> wyst�puje ten sam problem, a rozmowa wygl�da tak samo. Ja co� wyja�niam,
> m�cz� si� a na ko�cu Wo�niak stwierdza �e to nie wa�ne/to jest inaczej
> bez podawania argument�w. Po prostu chcia�em ci� od tego uchrnoni�.

Kiepsko z pamięcią. Napisałeś A - bez argumentów. Ja napisałem B,
również bez argumentów. Zmusiłem Cię jednak do przyznania, że A
nie jest prawdą. Więc się obraziłeś, nabluzgałeś i splonkowałeś.

Swoją szosą, co miałem wg Ciebie zrobić z tym nie-prawdziwym A?
Uznać za prawdę i przyjąć do wiadomości? Zignorować? Nie wiem.

A WH zna mnie też. Choć już pewnie zapomniał, że kiedyś również mu
pomogłem.

Wlodzimierz Holsztynski napisał(a):


> Udowodnijmy skomponowaną regułę dowodzenia:
>
>     A  (A <=> B)  |-->  B
>
> Dowód:
>
>     (A <=> B)  |->  ((~A) \/ B)
>
>     A  ((~A) \/ B)  |->  B
>
> Koniec dowodu.

No dobrze, dowód jest oczywiście nie do podważenia, tylko czy z
dowodu, że to jest reguła
dowodzenia na pewno wynika, że to jest reguła dowodzenia? Podobno
zgodnie z najnowszymi
osiągnięciami logiki - wcale nie.

On Jul 20, 1:05 am, Maciej Wozniak <mlwozn...@wp.pl> wrote:
> Wlodzimierz Holsztynski napisał(a):
>
> > Udowodnijmy skomponowaną regułę dowodzenia:
>
> >     A  (A <=> B)  |-->  B
>
> > Dowód:
>
> >     (A <=> B)  |->  ((~A) \/ B)
>
> >     A  ((~A) \/ B)  |->  B
>
> > Koniec dowodu.
>
>  czy z dowodu, że to jest reguła
> dowodzenia na pewno wynika,
> że to jest reguła dowodzenia?

To jest "skomponowana reguła dowodzenia".
Użyłem terminów "reguła dowodzenia"
oraz "skomponowana reguła dowodzenia",
by łatwo było to zapamiętać i nawiązać do
matematyki. Można bylo stosować
nazwy "produkcja" oraz "złożona produkcja".
Jakie te nazwy są takie są, nie ma znaczenia,
poza psychologicznym komfortem.

Ważne, że skomponowane reguły dowodzenia
(zlożone produkcje) prowadzą od twierdzeń
do twierdzeń. To wszystko.

Co do "nie do podważenia", to się uśmiecham.
Faktycznie, ten dowód jest krótki, prosty, super
finitystyczny. Jednak to nie jest dowód formalny.
Nie mamy dla niego formalnej ramy. Polegamy
na naszej inteligencji, zdolności, intuicji. Moglibyśmy
też nauczyć komputer lub kogoś bezmyślnego, ale
niezawodnego, żeby stosował skomponowane
reguły, jak powyższa, i z pewnością w ramach
naszego ograniczonego świata materialnego
ta skomponowana reguła działałaby bez zarzutu.
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.

> Podobno
> zgodnie z najnowszymi
> osiągnięciami logiki - wcale nie.

Znowu się uśmiecham. Elementarny
rachunek zdań niemjest teorią matematyczną.
To jest tylko lingo (teoria w sensie
matematyki lingwistycznej). Mamy tu nawet do
czynienia z obiektami materialnymi
(znaczki), a nie matematycznymi. Tak jest, gdy
tę teorię rozwijamy zanim rozwiniemy
matematykę (marginesowo możemy się
w meta matmą podpierać, jak przy twierdzeniu
o nawiasach, ale to są opcjonalne
rzeczy, bo nawet twierdzenie o nawiasach można
traktować w ramach prymitywnego lingo).

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.
Trybiki mają pasować, itd.

Zupełnie mnie nie martwi, co logika
"myśli" o podobnych sytuacjach (które
Ci się kojarzą - w tym sensie podobne).

Pozdrawiam,

    Włodek

On Mon, 20 Jul 2009 08:26:13 +0200, Mateusz Grotek
<unoduetre@poczta.onet.pl> wrote:
 
>
>Po pierwsze dziękuję za określenie mnie przeszkadzaczem. Po drugie 
>czytam ten wątek i nawet jestem zainteresowany, aczkolwiek nie mam nic 
>do dodania na razie. Po trzecie chciałem tylko doradzić coś odnośnie 
>Woźniaka, gdyż już dwukrotnie złapałem się na rozmowie z nim i wciąż 
>występuje ten sam problem, a rozmowa wygląda tak samo. Ja coś wyjaśniam, 
>męczę się a na końcu Woźniak stwierdza że to nie ważne/to jest inaczej 
>bez podawania argumentów. Po prostu chciałem cię od tego uchrnonić.
>> 
>> Szkoda, bo tak ladnie mi pomogles z programem
>> Mariusza. A tu taki klops.
>>
>Nie wiem jaka szkoda. Czyżbyś ocenił mnie na podstawie tego jednego 
>postu? A jeśli chcesz mnie ocenić, to może po pierwsze przeczytaj inne 
>moje posty.   

Zdaje sie ze jestes dosyc nowy na grupie. To jest standarowe
zachowanie Pana H. Wsyscy mu przeszkadzaja albo sa "trolle" albo nie
na poziomie. Dlatego tez polowa ma go w KF a druga polowa olewa.

A.L.

Użytkownik "Wlodzimierz Holsztynski (Wlod)" <sennajawa@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.


>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.

>Trybiki mają pasować, itd.

To nie mozna budować z samej stali. Pewna
ilość gumy musi zostać. I smar będzie
niezbędny.
Czysty formalizm nie ma prawa praktycznie
działać. Mówię to jako inżynier od
informacyjnych konstrukcji trybikowych. 

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

"Wlodzimierz Holsztynski (Wlod)" <sennajawa@gmail.com>
news:1d40e3e4-f355-45da-8ac1-d87ae2c0a4e4@f18g2000prf.googlegroups.com...
> On Jul 20, 9:51 am, Maciej Woźniak <mlwozniak_no_sp...@wp.pl> wrote:

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


> [...]
> Moje obiekcje związane są z kontaktem
> skończoności (my) z nieskończonością.
>
> Pozdrawiam,
>
>    Włodek


Jeśli w Twojej teorii
ja/oo = my/oo = 0
to nie masz kontaktu z rzeczywistością, bo ZERO
nie ma możliwości odbierać danych z fizycznego Świata.
Krezus 

Proponuję skończyć te pseudofilozoficzne dywagacje nie mające żadnych
podstaw i wrócic do matematyki...

Na ogół w dowodach formalnych podaje
się nie tylko kolejne kroki, ale przy nich także
odnośniki do reguł (i aksjomatów) i poprzednich
twierdzeń, które dany krok uzasadniają (co
wydatnie przyspiesza sprawdzanie dowodu).

Nie czynię tego, gdy podaję bardzo krótkie dowody,
a przy tych nie chcę widoku odnośnikami zaśmiecać.

On Jul 19, 3:31 pm, Wlodzimierz Holsztynski <sennaj...@gmail.com>
wrote:

> Oto reguły dowodzenia (w tym aksjomaty):
>
> Odrywanie:
> =========
>
>         A  ((~A) \/ B)  |->  B
>
> Równoważność:
> ============
>
> związek z implikacją:
>
>     (A <=> B)  |->  ((~A) \/ B)
>     (A <=> B)  |->  ((~B) \/ A)
>
>      ((~A) \/ B)  ((~B) \/ A)  |->  (A <=> B)
>
> zwrotność -
>
>     |-> (A <=> A)
>
> przemienność:
>
>     |->  ((A <=> B) <=> (B <=> A))
>
> przechodniość:
>
>    (A <=> B)  (B <=> C)  |->  (A <=> C)
>
> *********
>  [...]
>
> Udowodnijmy skomponowaną regułę dowodzenia:
>
>     (A <=> B)  |-->  (B <=> A)
>
> Reguła:
>
>     (A <=> B)  |-->  (B <=> A)
>
> Dowód 2:


Korzystamy z wcześniej udowodnionej
reguły skomponowanej:

        A  (A <=> B)  |-->  B

>     |->  ((A <=> B) <=> (B <=> A))
>
>     (A <=> B)  ((A <=> B) <=> (B <=> A))  |-->  (B <=> A)
>
> Koniec dowodu.


Jest to bardzo szczególny przypadek
ogólniejszego meta-twierdzenia; dowod
jest ten sam co wyżej, tyle, że mamy  SX
oraz  SY  zamiast  (A <=> B) oraz (B <=> A):

  Jeżeli  |--> SX <=> SY  to  SX |--> SY

Dowód:

    |--> SX <=> SY

    SX  (SX <=> SY)  |-->  SY

Koniec dowodu.
******************

Pozdrawiam,

    Wlodek

PS. Nastawiłem się, żeby całość intensywnie skończyć
w kilka dni, ale pierepałki z trzymaniem się tematu
w wątkach jakoś odebrały mi rozpęd, nawet w pewnym
momencie machnąłem ręką, bo do końca wciąż
zostalo co najmniej 2/3 dystansu. Nawet zacząłem
inny projekt z tego wszystkiego. Jednak staram się,
choćby i bez animuszu, kontynuować, nie ukatrupić
tej serii. Na pewno zajmie to teraz dłużej.

kopia na pl.sci.filozofia
"Mateusz Grotek" <unoduetre@poczta.onet.pl>
news:h45bdm$s4u$1@news.onet.pl...
> "Krezus" <Krezus@gmail.com>
> news:h45af5$mnp$1@achot.icm.edu.pl...
>> "Wlodzimierz Holsztynski (Wlod)" <sennajawa@gmail.com>
>> news:1d40e3e4-f355-45da-8ac1-d87ae2c0a4e4@f18g2000prf.googlegroups.com...
>>> On Jul 20, 9:51 am, Maciej Woźniak <mlwozniak_no_sp...@wp.pl> wrote:


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


>>> [...]
>>> Moje obiekcje związane są z kontaktem
>>> skończoności (my) z nieskończonością.
>>>
>>> Pozdrawiam,
>>>
>>>    Włodek


>> Jeśli w Twojej teorii
>> ja/oo = my/oo = 0
>> to nie masz kontaktu z rzeczywistością, bo ZERO
>> nie ma możliwości odbierać danych z fizycznego Świata.
>> Krezus


> Proponuję skończyć te pseudofilozoficzne dywagacje nie mające żadnych
> podstaw i wrócic do matematyki...


Twoja wypowiedź Mateusz nie ma związku z matematyką
lecz jest wyłącznie nieudolną próbą manipulacji na informacji:
1. Wycięcie adresata
2. Wycięcie meritum
3. Pieniactwo: "pseudofilozoficzne dywagacje"
Zapamiętaj:
Matematyka JEST tylko JEDNA
Jeśli ktoś zakłada sobie, że
ja/oo = 1/oo = 0
my/oo = n/oo = 0
to
sam sobie odbiera prawo bycia wiarygodnym.
Konsekwencją założenia, że
JEDEN z NIESKOŃCZONOŚCI
ma wartość ZERO
jest samozaprzeczenie własnej tożsamości.
ZERO aby być ZEREM nie może ani przyjmować informacji
ani jej przetwarzać - bo wówczas przestaje być ZEREM.


PS.
Jeśli nie masz nic do powiedzenia w temacie 1/oo --> to MILCZ.
Postmodernistyczny bełkot samozaprzeczeń to nie na tej grupie.
Takie teksty zawierające wyłącznie pieniactwo jak zaprezentowałeś
Mateuszu Grotek, to możesz wysyłać na pl.sci.matematyka
(moderowana), a nie tu gdzie żyją wirtualni ludzie rozumiejący
co piszą, jak piszą i dlaczego piszą.
pozdrawiam urlopowo,
Edward Robak* z Nowej Huty
~>°<~
miłośnik mądrości 

Użytkownik "Wlodzimierz Holsztynski (Wlod)" <sennajawa@gmail.com> napisał w


>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.

Tak.

>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).

W staroświeckim sensie, aż do conajmniej
Łobaczewskiego, dowody były po to, żeby ustalić
co jest prawdą, a co nie. Czy to jest Twoim celem?
Chcesz, żebym uwierzył - tak to odbieram.

Pytam, bo oficjalnie matematyka się wypiera takiego
podejścia.


>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.

Czy Euklidesowi przyszłoby do głowy, że nie ma
implikacji pomiędzy dowodem twierdzenia Pitagorasa
i twierdzeniem Pitagorasa? Nie sądzę.
Formalizacja zmienia pewne sprawy.

>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ść),

W staroświeckim podejściu twierdzenie wynika z dowodu.
A w formalnym nie; więc skąd ten wyższy stopień
pewności?


>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ść",

Po staroświecku z dowodu mamy stosowalną
praktycznie regułę. Po formalnemu - twoja teoria
z tym twierdzeniem jest równie dobra, jak teoria
z twierdzeniem przeciwnym, którą też da się zrobić.
Bo się da - zgadzamy się?
A z eliminacją wieloznaczności też nie należy
przesadzać. Trochę wieloznaczności musi zostać,
daje to konstrukcji elastyczność.

> ale w sensie dosłownym to wpływu na
> teorię oryginalną nie ma.

Obaj nie jesteśmy w stanie przeprowadzić
jednoznacznego porównania. Niemniej, na
aksjomat Dunsa Szkota nie wpadł ani Arystoteles,
ani Euklides, ani Archimedes. A to nie jest
skomplikowany aksjomat.
Czy na pewno dla tych 3 był on równie oczywisty,
jak dla Ciebie?

>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.

Mnie tam dziwi zasada, że z dowodu twierdzenia
nie wynika twierdzenie - już teraz.

>A tak serio, to "praktycznie" formalizm działa
>na całego.

Większość ludzi stosujących matematykę
w praktyce - po staroświecku o formaliźmie
nie ma zielonego pojęcia. I po staroświecku
uznaje udowodnione matematyczne twierdzenia
za prawdę. W praktyce to staroświeckie
podejście długo i świetnie się sprawdza. 

On Jul 22, 1:16 pm, Maciej Woźniak <mlwozniak_no_sp...@wp.pl> wrote:

> Użytkownik "Wlodzimierz Holsztynski (Wlod)" <sennaj...@gmail.com> napisał w
>
> W staroświeckim sensie, aż do conajmniej
> Łobaczewskiego, dowody były po to, żeby ustalić
> co jest prawdą, a co nie. Czy to jest Twoim celem?
> Chcesz, żebym uwierzył - tak to odbieram.

"Prawda" zdefiniowana formalnie obchodzi mnie.
Obchodzi mnie tak samo, jak formalnie zdefiniowany
"farfocel". Prawda w mętnym sensie, w kontekście
matematyki ani mnie ziębi ani grzeje.

> Pytam, bo oficjalnie matematyka się wypiera takiego
> podejścia.

Nie wypowiadałbym się w imieniu "oficjalnej matematyki".
Sam mogę co najwyżej w imieniu matematyki.

> >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.
>
> Czy Euklidesowi przyszłoby do głowy, że nie ma
> implikacji pomiędzy dowodem twierdzenia Pitagorasa
> i twierdzeniem Pitagorasa? Nie sądzę.
> Formalizacja zmienia pewne sprawy.

Masz jakieś swoje kwestie, które są mi obce.

W każdym razie dowód nie zmienia sensu
twierdzenia jako wyrażenie czegoś. Dowód
jedynie pokazuje, że to wyrażenie jest twierdzeniem.
(Nie ma w tym żadnej "filozofii").

> >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ść),
>
> W staroświeckim podejściu twierdzenie wynika z dowodu.
> A w formalnym nie; więc skąd ten wyższy stopień
> pewności?

Nasza wiedza o tym, że wyrażenie jest twierdzeniem,
czyli o tym, że dowód istnieje, wynika z kopii takiego
czy innego poprawnego dowodu.

> >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ść",
>
> Po staroświecku z dowodu mamy stosowalną
> praktycznie regułę. Po formalnemu - twoja teoria
> z tym twierdzeniem jest równie dobra, jak teoria
> z twierdzeniem przeciwnym, którą też da się zrobić.
> Bo się da - zgadzamy się?
> A z eliminacją wieloznaczności też nie należy
> przesadzać. Trochę wieloznaczności musi zostać,
> daje to konstrukcji elastyczność.

W danym przypadku nie ma sensu mówić
o twierdzeniu przeciwnym. Mamy super finitystyczną
sytuację. Żadne formalizacje nie zmienią tego, że
skomponowana reguła zastępuje wypisywanie
powiedzmy ciągu trzech danych reguł. To jest
tak pewne jak tylko może być, bo trywialnie
skończone. Mam wrażenie, że bujasz w obłokach,
bez ogniskowania się na danej sytuacji, która
nie dostarcza Ci pożywki.

> > ale w sensie dosłownym to wpływu na
> > teorię oryginalną nie ma.
>
> Obaj nie jesteśmy w stanie przeprowadzić
> jednoznacznego porównania. Niemniej, na
> aksjomat Dunsa Szkota nie wpadł ani Arystoteles,
> ani Euklides, ani Archimedes. A to nie jest
> skomplikowany aksjomat.

Mieszać takie nico jak Arystoteles z ludźmi
na poziomie Euklidesa i Archimedesa
ukatrupia dyskusję. Tak czy śmak, to już
nie na temat. Pakować historię do niniejszego
skromnego wątku, by coś uzasadniać, jest
ogromną przesadą.

Mówienie o "niewpadanie" na trywialności (a wszystkie
tautologie logiczne są trywialne) przez Panów E i A jest
obraźliwe względem matematyki.

> Mnie tam dziwi zasada, że z dowodu twierdzenia
> nie wynika twierdzenie - już teraz.

Nie wiem o czym mówisz. Z dowodu zdania A
wynika, że zdanie A jest twierdzeniem.

> >A tak serio, to "praktycznie" formalizm działa
> >na całego.
>
> Większość ludzi stosujących matematykę
> w praktyce - po staroświecku o formaliźmie
> nie ma zielonego pojęcia.

To niczego nie zmienia.

> I po staroświecku
> uznaje udowodnione matematyczne twierdzenia
> za prawdę. W praktyce to staroświeckie
> podejście długo i świetnie się sprawdza.

Było nieźle, co może i powinno imponować.
Z formalizmem jest bez porównania lepiej
w wielu wymiarach i na kilku poziomach.
Postęp i rozwój nastąpił ogromny. Przecież
nawet informatyka czerpie z formalizmu.
Aż szkoda język strzępić po próżnicy.
To tak jakbyś Bill Gatesowi mówił, że on
nie ma pieniędzy. W każdym razie to jest
już zupełnie inny wątek.

Ten posumuję: pokazałem (prosto), że
w dowodach formalnych pewne ciągi
dwóch lub trzech zastosowań refguł |->
można zastępować odpowiednią jedną
regułą skomponowaną |-->, co jest praktyczne.
Mój dowód jest bardzo bardzo pewny,
jest pewniejszy o śmierci i podatków; a kto
mi nie wierzy, niech mechanicznie zastępuje
każde występowanie |--> przez zastąpiony
ciąg reguł |-> (2 lub 3 lub ile dana
skomponowana reguła.

Naprawdę niewiele w tym miejsca na
kontrowersje.

Dodam, że teoretycznie możnaby dowody
przeprowadzać bez żadnych skrótów.
W praktyce tak by je to wydłużyło, że
niemożliwym byłoby je prześledzić.
I w tym momencie jest miejsce na refleksję
filozoficzną. Ale już nie w tym wątku :-)

Pozdrawiam,

    Włodek

"Wlodzimierz Holsztynski (Wlod)" <sennajawa@gmail.com>
news:8c7980ef-d2d9-4467-9cd1-16bd9fb90ab8@p36g2000prn.googlegroups.com...
> On Jul 22, 1:16 pm, Maciej Woźniak <mlwozniak_no_sp...@wp.pl> wrote:

>> W staroświeckim sensie, aż do conajmniej
>> Łobaczewskiego, dowody były po to, żeby ustalić
>> co jest prawdą, a co nie. Czy to jest Twoim celem?
>> Chcesz, żebym uwierzył - tak to odbieram.


> "Prawda" zdefiniowana formalnie obchodzi mnie.
> Obchodzi mnie tak samo, jak formalnie zdefiniowany
> "farfocel". Prawda w mętnym sensie, w kontekście
> matematyki ani mnie ziębi ani grzeje.
>
> Pozdrawiam,
>
>     Włodek


Prawda w każdym sensie to relacja pomiędzy nazwą, a rzeczą nazywaną.
Nie kpij więc z prawd matematycznych, bo gdybyś nie podał prawdy:
co dla Ciebie znaczą nazwy pisma obrazkowego
 |-->    |->    <=>
to nie małyby te nazwy żadnego sensu jako nowomowa nazw oderwanych
od rzeczy nazywanych. Byłyby więc czystym bełkotem szaleńca.
pozdrawiam urlopowo,
Edward Robak* z Nowej Huty
~>°<~
miłośnik mądrości 

Użytkownik "Wlodzimierz Holsztynski (Wlod)" <sennajawa@gmail.com> napisał w


>"Prawda" zdefiniowana formalnie obchodzi mnie.
>Obchodzi mnie tak samo, jak formalnie zdefiniowany
>"farfocel". Prawda w mętnym sensie, w kontekście
>matematyki ani mnie ziębi ani grzeje.

Więc co jest celem Twojego staroświeckiego,
metateoretycznego dowodzenia? Czy chcesz
mi przekazać przy jego pomocy jakąś informację?
Jaka to informacja?
Czy to jest informacja "twierdzenia RZ są
tautologiami", czy informacja ""twierdzenia
RZ są tautologiami" jest twierdzeniem mojej
teorii"? Bo to drugie jest dość trywialną
informacją, jak to tautologia. Natomiast
to pierwsze, to by było ciekawe.

>W danym przypadku nie ma sensu mówić
>o twierdzeniu przeciwnym. Mamy super finitystyczną
>sytuację. Żadne formalizacje nie zmienią tego, że
>skomponowana reguła zastępuje wypisywanie
>powiedzmy ciągu trzech danych reguł.

Miałem na myśli to, co dopiero zamierzasz
udowodnić, to, ze twierdzenia są tautologiami.

A poza tym, 200 lat temu z taką samą pewnością
mówiono, że żadne formalizacje nie zmienią faktu,
że (tu V aksjomatu Euklidesa).
To, co uważasz za niemożliwe, nie jest nawet
formalnie trudne; natomiast intuicyjnie jest
idiotyczne, co pewnie jeszcze przez jakiś
czas nas przed takim formalizmem uchroni,
amen.


>Mówienie o "niewpadanie" na trywialności (a wszystkie
>tautologie logiczne są trywialne) przez Panów E i A jest
>obraźliwe względem matematyki.

Dla Ciebie jest to tautologia, bo Ty masz
aksjomat Dunsa Szkota. A oni go nie mieli.
Więc nie widzę powodów, żeby twierdzić,
że nie wpadając na to, nie wpadli na
tautologię.


>> Mnie tam dziwi zasada, że z dowodu twierdzenia
>> nie wynika twierdzenie - już teraz.

>Nie wiem o czym mówisz. Z dowodu zdania A
>wynika, że zdanie A jest twierdzeniem.

Mówię o tym, że z dowodu A nie wynika, że
A. Np. z dowodu twierdzenia Pitagorasa
nie wynika, że suma kwadratów przyprostokątnych..

>Było nieźle, co może i powinno imponować.
>Z formalizmem jest bez porównania lepiej
>w wielu wymiarach i na kilku poziomach.

Tylko z dowodu na twierdzenie Pitagorasa
nie wynika już, że suma kwadratów
przyprostokątnych...
A praktyka nie potrzebuje informacji, co
jest twierdzeniem której teorii.
Natomiast informacji, jaka  jest suma
kwadratów przyprostokątnych - potrzebuje.