ŚFiNiA

wujzboj

Poniewaz wywalenie Tertium to nic innego jak zmiana definicji negacji i w efekcie dopuszczenie, by czesc tresci negowanego elementu odnajdowala sie rowniez w elemencie zanegowanym, to zrozumiale jest, ze kazda teoria korzystajaca z tego dopuszczenia produkuje objekty zdefiniowane w sposob klasycznie sprzeczny.

Zauwaz natomiast, ze kazdy algorytm jest ostatecznie tlumaczony na kroki wykonywane przez hardwerowe bramki logiczne dzialajace calkowicie zerojedynkowo i klasycznie. Programista (albo w ostatecznosci kompilator) przerabia bowiem nieklasycznie zdefiniowane obiekty tak, by przywrocic zerojedynkowy sens negacji. Opis teoretyczny moze byc latwiejszy w nieklasycznej formie; rowniez implementacja moze isc krotsza droga, jesli wychodzi sie od nieklasycznych formulek. Widzialbym to jako cos podobnego do chodzenia po przestrzeni wektorowej od punktu do punktu albo wzdluz wektorow bazy albo wzdluz ich kombinacji liniowych. W ogolnym przypadku uzycie kombinacji liniowych pozwala na dojscie do celu w mniejszej ilosci krokow, choc ortogonalnosc krokow jest utracona. Ortogonalnosc jednak nie jest celem; celem jest dojscie do celu.

mikon · Dołączył: 15 Gru 2005 Posty: 359 Przeczytał: 0 tematów

wujzboj

mikon · Dołączył: 15 Gru 2005 Posty: 359 Przeczytał: 0 tematów

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

Oj Mikołaju, Mikołaju, niemało masz na sumieniu. Niedość, że znęcasz się za pomocą izomorfizmu Curry'ego-Howarda, Coqa, Kripkego (niedługo może i Heytinga), toposów, etc., a nawet systemów modułów (a sam najlepiej wiesz, co to za ziółka), nad zupełnie niewinnym człowiekiem, to w dodatku robisz to tak, żeby go oświecać, ale nie oświecić. Na taką nonszalancję możesz sobie pozwolić rozmawiając z kolegami po fachu, ale nie z laikami, do których należy mówić w sposób uporządkowany i ŚCIŚLE.

Nie ma racji Wuj, twierdząc, że w logice intuicjonistycznej "zmieniono definicję negacji". Trzeba by się zresztą zapytać, jak ta definicja właściwie jego zdaniem brzmi? Takie pytanie jest mimo wszystko zasadne i ja, jako Twoje sumienie, na to pytanie odpowiem (z tym, że - uczciwie mówiąc - nie zdefiniuję już implikacji, co byłoby większym problemem): po pierwsze, trzeba zdefiniować fałsz. Otóż fałszem jest takie F, że zachodzi F->p dla każdego p. A więc fałsz jest zdefiniowany przez "ex falso quodlibet". (łatwo zauważyć, że każde dwie formuły F i F' spełniające tę własność są równoważne, więc jest to niemal poprawna definicja). Natomiast negacja jest zdefiniowana jako skrót: ~p = p->F. Z tego już wynika, że p->~p->F oraz ~p->p->F, co można rozumieć jako zachodzenie zasady niesprzeczności (tutaj wyrażonej bez koniunkcji, co by nie prowadzić dyskusji o definicję koniunkcji): jeśli p i jeśli nie ~p, to fałsz. Moim jednak zdaniem zasada niesprzeczności mówi w istocie tyle, że nie da się wyprowadzić fałszu z samych aksjomatów. I w tym sensie zasada ta znaczy dokładnie to, co Mikołaju nazywasz "użytecznością" logiki. Logika sprzeczna to taka, w której da się wyprowadzić wszystko, czyli w której dowodliwy jest fałsz.

Oczywiście zasada tertium non datur, czyli p v ~p, wcale nie wynika z powyższej definicji negacji ani nie jest z nią sprzeczna. Muszę przyznać, że nie rozumiem zdania o tym, że przy intuicjonistycznym rozumiemiu negacji dopuszczamy, by "czesc tresci negowanego elementu odnajdowala sie rowniez w elemencie zanegowanym". Jeżeli dobrze rozumiem, że to "część treści" zdania p, to takie zdanie q, że p->q zachodzi. Ale jeżeli tak, to w logice klasycznej też może zachodzić (p->q)^(~p->q), choćby dla q będącego prawdą. Tutaj intuicjonizm niczego nie zmienia.

Swoją drogą niniejszy wątek tylko utwierdza mnie w poglądzie o niezwykłej szkodliwości metody "tabelek zero-jedynkowych" dla umysłów polskiej młodzieży.

wujzboj

Dobre wejscie, prosze Sumienia

. Wobec tego :pidu:

na dzien dobry.

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

wujzboj

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

wujzboj

Moze wygodniej pisac jak w C, oznaczajac zaprzeczenie rownosci przez "!=". Rozumiem, ze przez | oznaczasz warunek, jak w prawdopodobienstwie warunkowym.

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

mikon · Dołączył: 15 Gru 2005 Posty: 359 Przeczytał: 0 tematów

wujzboj

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

wujzboj

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

Zbanowany Uczy

Wybaczcie, ale trochę się pogubiłem – gdzie widzicie problem? Istnieje multum charakteryzacji logiki intuicjonistycznej i jej kuzynek (których jest tyle, ile liczb rzeczywistych, czyli alef1 [zakładam tu aksjomat wyboru - równoważny lematowi Kuratowskiego-Zorna; intuicjonista nie zgodzi się z tym oczywiście]).
Przedstawię jedną z moich ulubionych i – jeśli ktoś będzie miał ochotę – poćwiczymy potem dowodzenie.

Ograniczymy się do logiki zdaniowej. A więc, p,q,r…to zmienne zdaniowe, H, F, G…to metaformuły. Strukturą intuicjonistyczną, w skrócie i-strukturą nazywamy parę <W, R> taką, że W jest niepustym zbiorem (dopuszczającym rozmaite interpretacje, np. zbiór sytuacji wiedzy) a R podzbiorem kwadratu kartezjańskiego W, czyli relacją binarną określoną na W i dodatkowo taką, że jest częściowym porządkiem na W, tj. jest zwrotna, przechodnia i antysymetryczna. Trójkę <W,R,f> nazywamy i-modelem wtw <W,R> jest i-strukturą i f jest funkcją przeprowadzającą zbiór wszystkich zmiennych zdaniowych w potęgowy zbiór W, przy czym spełniony jest warunek: Dla każdego w1,w2 należącego do W, f jest R-monotoniczne wzgl. R-dziedziczne (po ludzku, jeśli w1Rw2 i w1 należy do f(p), to w2 należy do f(p)).
Niech teraz M będzie i-modelem, a w elementem W. Definiujemy relację spełniania przez indukcję strukturalną względem złożoności formuły:
w spełnia p przy M wtw w należy do f(p)
w spełnia nie-H przy M wtw dla każdego w’: jeśli wRw’, to w nie spełnia H przy M
w spełnia H&F przy M wtw w spełnia H przy M i w spełnia F przy M
w spełnia H lub F przy M wtw w spełnia H przy M lub w spełnia F przy M
w spełnia jeśli H, to F przy M wtw dla każdego w’: jeśli wRw’ i w’ spełnia H przy M, to w’ spełnia F przy M

M spełnia H wtw każde w z W spełnia H przy M
Struktura <W,R> spełnia H wtw każdy M oparty na niej spełnia H
H jest spełniona simpliciter (czyli po prostu: intuicjonistycznie prawdziwa lub – jeszcze inaczej – jest i-tautologią) wtw jest spełniona w każdej i-strukturze.

Zbiór formuł Q spełnia H wtw każdy M spełniający Q spełnia H
H jest i-dowiedlna z Q wtw H ma dowód (dokładniej, i-dowód) w sensie Hilberta na podstawie Q
Dla każdego Q i H, Q spełnia (ponieważ spełnianie zafiksowaliśmy, nie piszę ‘i-spełnia’) H wtw H jest dowiedlna z Q (tw. o pełności)

Nie widzę żadnych problemów poza paradoksalnością (na pierwszy rzut oka) dwóch twierdzeń:
Twierdzenie Glivenko: Dla każdego Q i H, H jest i-dowiedlna z Q wtw H jest klasycznie dowiedlna z Q
Twierdzenie Goedla: Niech H zawiera tylko negację i koniunkcję. H jest i–tautologią wtw H jest klasyczną tautologią.

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

[quote="Zbanowany Uczy"]Wybaczcie, ale trochę się pogubiłem – gdzie widzicie problem? Istnieje multum charakteryzacji logiki intuicjonistycznej i jej kuzynek (których jest continuum, czyli alef1).
[quote]

Ja żadnego problemu nie widzę, poza tym, że Wuj po omacku szuka drogi w świecie logiki (zamiast pójść drogą najprostszą, czyli przeczytać odpowiedni podręcznik), a Mikołaj go ciągle zwodzi i niewiele brakuje, a zacznie mu wyjaśniać "Special Adjoint Theorem" w przypadku 2-kategoryjnym. Do czego dopuścić nie mogę.

NB prosiłbym o dowód, że continuum równa się alef1.

Zbanowany Uczy

Jasne, definicje. Zagalopowałem się. (już poprawiłem post; wyjasniłem też, mam nadzieję, sprawę alef1)
A co do tw. Glivenko (czy też Gliwenko) to teraz mnie szczęka opadła, bo tak jak byk napisał je na tablicy jeden z moich profesorów. :think:

Ale co mi tam! :pidu:

wujzboj

SumienieMikołaja · Dołączył: 18 Lut 2006 Posty: 19 Przeczytał: 0 tematów

wujzboj

Zbanowany Uczy

Metodologiczna (w sensie metodologii nauk ścisłych) interpretacja i-logiki?
Czemu nie? Przeczytajcie jeszcze raz "moją" ("", bo ja jej nie wymyśliłem :wink: ) charakteryzację, interpretując relację spełniania jako wymuszanie przez owo w rozumiane jako dostępna informacja.
Stąd niektórzy sugerują, że i-logika jest (pewną) logiką akceptowalności, a nie prawdziwości (jak logika klasyczna).

Oczywiście, ponieważ spełniona jest tu monotoniczność operacji konsekwencji (rozszerzając zbiór przesłanek rozszerzamy zbiór konkluzji), jest to dość anachroniczna metodologia (w badaniach naukowych - ba - w życiu regułą jest raczej NIEmonotoniczność); można ją nazwać metodologią pozytywistyczną (za prof. A. Grzegorczykiem).

wujzboj

Ach, ze paradygmat sie zmienia, wiadomo juz co najmniej od czasow Kuhna.

Zbanowany Uczy

Choć oryginalną motywacją intuicjonizmu były pewne paradoksy i kantowska filozofia matematyki. Ale o tym więcej powie ew. mikon (wzgl. jego sumienie :wink: ).