Aksjomaty i prawa logiki klasycznej (TODO)

TODO:

• enumeracja, krótki opis
• podział na grupy: DNE vs LEM (TODO': logika klasyczna jako logika zdań rozstrzygalnych) vs materialna implikacja i równoważność (i potencjalnie pozostałe "słabe" spójniki) vs kontrapozycja vs consequentia mirabilis i Peirce (jako rzeczy wyglądające podobnie do DNE, a w praktyce wyłazące, jak człowiek próbuje użyć LEM)

Logika klasyczna jako logika diabła (TODO)

Dawno dawno temu w odległej galaktyce, a konkretniej w ZSRR, był sobie pewien rusek. Pewnego razu do ruska przyszedł diaboł (a diaboł to, jak wiadomo, coś dużo gorszego niż diabeł) i zaoferował mu taki oto deal: "dam ci miliard dolarów lub jeżeli dasz mi miliard dolarów, to spełnię dowolne twoje życzenie". Rusek trochę skonsternowany, nie bardzo widzi mu się podpisywanie cyrografu krwią. "Nie nie, żadnych cyrografów, ani innych takich kruczków prawnych", zapewnia go diaboł. Rusek myśli sobie tak: "pewnie hajsu nie dostanę, ale przecież nic nie tracę", po czym mówi: "No dobra, bierę". "Świetnie!" - mówi diaboł - "Jeżeli dasz mi miliard dolarów, to spełnie dowolne twoje życzenie". Cóż, rusek był zawiedziony, ale nie zaskoczony - przecież dokładnie tego się spodziewał. Niedługo później diaboł zniknął, a rusek wrócił do pracy w kołchozie. Jako, że był przodownikiem pracy i to na dodatek bardzo oszczędnym, bo nie miał dzieci ani baby, szybko udało mu się odłożyć miliard dolarów i jeszcze kilka rubli na walizkę, coby mieć gdzie trzymać dolary. Wtedy znów pojawił się diaboł. "O, cóż za spotkanie. Trzym hajs i spełnij moje życzenie, tak jak się umawialiśmy" - powiedział rusek i podał diabołowi walizkę. "Wisz co" - odpowiedział mu diaboł - "zmieniłem zdanie. Życzenia nie spełnię, ale za to dam ci miliard dolarów. Łapaj" - i diaboł oddał ruskowi walizkę. Jaki morał płynie z tej bajki? Diaboł to bydle złe i przeokrutne, gdyż w logice, którą posługuje się przy robieniu dealów (względnie podpisywaniu cyrografów) obowiązuje prawo eliminacji podwójnej negacji. Prawo to prezentuje się podobnie jak prawo wyłączonego środka:

Po pierwsze, nie da się go konstruktywnie udowodnić.

Po drugie, jest ono niezaprzeczalne. Po trzecie, jest równoważne prawu wyłączonego środka.

Logika zdań stabilnych

P jest stabilne, gdy ~ ~ P -> P

Logika klasyczna jako logika Boga (TODO)

Zdania określone

Metoda zerojedynkowa (TODO)

Tutaj o rysowaniu tabelek.

Logika klasyczna jako logika kontrapozycji

Zdania kontrapozowalne dziedzinowo (TODO)

Zdania kontrapozowalne przeciwdziedzinowo

Logika klasyczna jako logika cudownych konsekwencji (TODO)

Logika cudownych konsekwencji

Zdania cudowne

Logika Peirce'a

Logika zdań penetrowalnych

Aksjomaty i pojęcie "tabu" (TODO)

Tutaj o tym, co to znaczy, że w logice konstruktywnej LEM i tympodobne są tabu. Drobna klasyfikacja na coś w stylu:

• zdania prawdziwe (P zachodzi)
• zdania fałszywe (~ P zachodzi)
• zdania niezaprzeczalne (~ ~ P zachodzi)
• zdania kontyngentne (P jest fałszywym zdaniem postaci forall x : A, Q x i zachodzi exists x : A, Q x. Inne podejście: tylko w kontekście, w którym zdanie P składa się z nieznanych części, np. P -> Q jest kontyngentne, bo P -> P zachodzi, zaś True -> False nie zachodzi.
• zdania klasycznie prawdziwe (P zachodzi w logice klasycznej)
• zdania tabu (P implikuje jakieś inne tabu, np. LEM)

TODO: być może dać to do podrozdziału o WLEM

Pułapki negacji. O negowaniu słabym i mocnym (TODO)

Poznaliśmy uprzednio pewien spójnik, zapisywany wdzięcznym wygibaskiem ~, a zwany górnolotnie negacją. Powinniśmy się jednak zastanowić: czy spójnik ten jest dla nas zadowalający? Czy pozwala on nam wyrażać nasze przemyślenia w najlepszy możliwy sposób? Jeżeli twoja odpowiedź brzmi "tak", to uroczyście oświadczam, że wcale nie masz racji. Wyobraźmy sobie następującą sytuację: jesteśmy psycho patusem, próbującym pod pozorem podrywu poobrażać przeróżne panienki. Podbijamy do pierwszej z brzegu, która akurat jest normalną dziewczyną, i mówimy: "Hej mała, jesteś gruba i mądra". Nasza oburzona rozmówczyni, jako że jest szczupła, odpowiada nam: "Wcale nie jestem gruba. Spadaj frajerze". Teraz na cel bierzemy kolejną, która siedzi sobie samotnie przy stoliku w Starbuniu, popija kawkę z papierowego kubka i z uśmiechem na ustach próbuje udowodnić w Coqu jakieś bardzo skomplikowane twierdzenie. Podbijamy do niej i mówimy: "Hej mała, jesteś gruba i mądra". Jako, że ona też jest szczupła, oburza się i odpowiada nam tak: "Czekaj, czekaj, Romeo. Załóżmy, że twój tani podryw jest zgodny z prawdą. Gdybym była gruba i mądra, to byłabym w szczególności mądra, bo P i Q implikuje Q. Ale gdybym była mądra, to wiedziałabym, żeby tyle nie żreć, a skoro tak, to bym nie żarła, więc nie byłabym gruba, ale na mocy założenia jestem, więc twój podryw jest sprzeczny. Jeżeli nie umiesz logiki, nie idę z tobą do łóżka." Widzisz różnicę w tych dwóch odpowiedziach? Pierwsza z nich wydaje nam się bardzo naturalna, bo przypomina zaprzeczenia, jakich zwykli ludzie używają w codziennych rozmowach. Druga wydaje się zawoalowana i bardziej przypomina dowód w Coqu niż codzienne rozmowy. Między oboma odpowiedziami jest łatwo zauważalna przepaść. Żeby zrozumieć tę przepaść, wprowadzimy pojęcia silnej i słabej negacji. W powyższym przykładzie silną negacją posłużyła się pierwsza dziewczyna - silną negacją zdania "jesteś gruba i mądra" jest tutaj zdanie "wcale nie jestem gruba". Oczywiście jest też druga możliwość silnego zaprzeczenia temu zdaniu - "nie jestem mądra" - ale z jakichś powodów to zaprzeczenie nie padło. Ciekawe dlaczego? Druga dziewczyna natomiast posłużyła się słabą negacją, odpowiadając "gdybym była gruba i mądra, to... (tutaj długaśne rozumowanie)... więc sprzeczność". Słaba negacja to ta, którą już znamy, czyli Coqowe not. Ma ona charakter hipotetyczny, gdyż jest po prostu implikacją, której konkluzją jest False. W rozumowaniach słownych sprowadza się ona do schematu "gdyby tak było, to wtedy... a zatem sprzeczność". Silna negacja to najbardziej bezpośredni sposób zaprzeczenia danemu zdaniu. W Coqu nie ma żadnego spójnika, który ją wyraża, bo ma ona charakter dość ad hoc - dla każdego zdania musimy sami sobie wymyślić, jak brzmi zdanie, które najsilniej mu przeczy. W rozumowaniach słownych silna negacja sprowadza się zazwyczaj do schematu "nie jest tak". Spróbujmy przetłumaczyć powyższe rozważania na język logiki. Niech P oznacza "gruba", zaś Q - "mądra". Silną negacją zdania P /\ Q jest zdanie ~ P \/ ~ Q ("nie gruba lub nie mądra"), zaś jego słabą negacją jest ~ (P /\ Q), czyli P /\ Q -> False ("jeżeli gruba i mądra, to sprzeczność"). Zauważmy, że o ile słaba negacja jest uniwersalna, tj. słabą negacją P /\ Q zawsze jest ~ (P /\ Q), to silna negacja jest ad hoc w tym sensie, że gdyby P było postaci P1 /\ P2, to wtedy silną negacją P /\ Q nie jest już ~ P \/ ~ Q, a ~ P1 \/ ~ P2 \/ ~ Q - żeby uzyskać silną negację, musimy zanegować P silnie, a nie słabo. Dlaczego silna negacja jest silna, a słaba jest słaba, tzn. dlaczego nazwaliśmy je tak a nie inaczej? Wyjaśnia to poniższe twierdzenie oraz następująca po nim beznadziejna próba udowodnienia analogicznego twierdzenia z implikacją idącą w drugą stronę.

Jak widać, silna negacja koniunkcji pociąga za sobą jej słabą negację. Powód tego jest prosty: jeżeli jeden z koniunktów nie zachodzi, ale założymy, że oba zachodzą, to w szczególności każdy z nich zachodzi osobno i mamy sprzeczność. A czy implikacja w drugą stronę zachodzi?

Jak widać, nie udało nam się udowodnić odwrotnej implikacji i to wcale nie dlatego, że jesteśmy mało zdolni - po prostu konstruktywnie nie da się tego zrobić. Powód tego jest prosty: jeżeli wiemy, że P i Q razem prowadzą do sprzeczności, to wiemy zdecydowanie za mało. Mogą być dwa powody:

• P i Q mogą bez problemu zachodzić osobno, ale być sprzeczne razem
• nawet jeżeli któryś z koniunktów prowadzi do sprzeczności, to nie wiemy, który

Żeby zrozumieć pierwszą możliwość, niech P oznacza "siedzę", a Q - "stoję". Rozważmy zdanie P /\ Q, czyli "siedzę i stoję". Żeby nie było za łatwo załóżmy też, że znajdujesz się po drugiej stronie kosmosu i mnie nie widzisz. Oczywiście nie mogę jednocześnie siedzieć i stać, gdyż czynności te się wykluczają, więc możesz skonkludować, że ~ (P /\ Q). Czy możesz jednak wywnioskować stąd, że ~ P \/ ~ Q, czyli że "nie siedzę lub nie stoję"? Konstruktywnie nie, bo będąc po drugiej stronie kosmosu nie wiesz, której z tych dwóch czynności nie wykonuję. Z drugim przypadkiem jest tak samo, jak z końcówką powyższego przykładu: nawet jeżeli zdania P i Q się wzajemnie nie wykluczają i niesłuszność P /\ Q wynika z tego, że któryś z koniunktów nie zachodzi, to możemy po prostu nie wiedzieć, o który z nich chodzi. Żeby jeszcze wzmocnić nasze zrozumienie, spróbujmy w zaskakujący sposób rozwinąć definicję (słabej) negacji dla koniunkcji:

I jeszcze raz...

Jak (mam nadzieję) widać, słaba negacja koniunkcji nie jest niczym innym niż stwierdzeniem, że oba koniunkty nie mogą zachodzić razem. Jest to więc coś znacznie słabszego, niż stwierdzenie, że któryś z koniunktów nie zachodzi z osobna.

Jak napisano w Piśmie, nie samą koniunkcją żyje człowiek. Podumajmy więc, jak wygląda silna negacja dysjunkcji. Jeżeli chcemy dosadnie powiedzieć, że P \/ Q nie zachodzi, to najprościej powiedzieć: ~ P /\ ~ Q. Słaba negacja dysjunkcji ma zaś rzecz jasna postać ~ (P \/ Q).

Co jednak dość ciekawe, silna negacja nie zawsze jest silniejsza od słabej (ale z pewnością nie może być od niej słabsza - gdyby mogła, to nazywałaby się inaczej). W przypadku dysjunkcji obie negacje są równoważne, co obrazuje poniższe twierdzenie, które głosi, że słaba negacja implikuje silną (a to razem z powyższym daje równoważność):

Wynika to z faktu, że ~ P /\ ~ Q to tak naprawdę para implikacji P -> False i Q -> False, zaś ~ (P \/ Q) to... gdy pomyślimy nad tym odpowiednio mocno... ta sama para implikacji. Jest tak dlatego, że jeżeli P \/ Q implikuje R, to umieć wyprodukować R musimy zarówno z samego P, jak i z samego Q.

Stary podrozdział, do naprawy

Klasyczna logika pierwszego rzędu (TODO)

Paradoks pijoka

Na zakończenie zwróćmy swą uwagę ku kolejnemu paradoksowi, tym razem dotyczącemu logiki klasycznej. Z angielska zwie się on "drinker's paradox", ja zaś ku powszechnej wesołości używał będę nazwy "paradoks pijoka". Zazwyczaj jest on wyrażany mniej więcej tak: w każdym barze jest taki człowiek, że jeżeli on pije, to wszyscy piją. Jak to możliwe? Czy matematyka stwierdza istnienie magicznych ludzi zdolnych popaść swoich barowych towarzyszy w alkoholizm? Oczywiście nie. W celu osiągnięcia oświecenia w tej kwestii prześledźmy dowód tego faktu (jeżeli nie udało ci się go wymyślić, pomyśl jeszcze trochę). Ustalmy najpierw, jak ma się formalne brzmienie twierdzenia do naszej poetyckiej parafrazy dwa akapity wyżej. Początek "w każdym barze" możemy pominąć i sformalizować sytuację w pewnym konkretnym barze. Nie ma to znaczenia dla prawdziwości tego zdania. Sytuację w barze modelujemy za pomocą typu man, które reprezentuje klientów baru, predykatu drinks, interpretowanego tak, że drinks x oznacza, że x pije. Pojawia się też osoba określona tajemniczym mianem random_guy. Jest ona konieczna, gdyż nasza poetycka parafraza czyni jedno założenie implicite: mianowicie, że w barze ktoś jest. Jest ono konieczne, gdyż gdyby w barze nie było nikogo, to w szczególności nie mogłoby tam być nikogo, kto spełnia jakieś dodatkowe warunki. I tak docieramy do sedna sprawy: istnieje osoba, którą będziemy zwać pijokiem (exists drinker : man), taka, że jeżeli ona pije (drinks drinker), to wszyscy piją (forall x : man, drinks x). Dowód jest banalny i opiera się na zasadzie wyłączonego środka, w Coqu zwanej classic. Dzięki niej możemy sprowadzić dowód do analizy dwóch przypadków. Przypadek 1: wszyscy piją. Cóż, skoro wszyscy piją, to wszyscy piją. Pozostaje nam wskazać pijoka: mógłby to być ktokolwiek, ale z konieczności zostaje nim random_guy, gdyż do żadnego innego klienta baru nie możemy się odnieść. Przypadek 2: nieprawda, że wszyscy piją. Parafrazując: istnieje ktoś, kto nie pije. Jest to obserwacja kluczowa. Skoro kolo przyszedł do baru i nie pije, to z automatu jest podejrzany. Uczyńmy go więc, wbrew zdrowemu rozsądkowi, naszym pijokiem. Pozostaje nam udowodnić, że jeżeli pijok pije, to wszyscy piją. Załóżmy więc, że pijok pije. Wiemy jednak skądinąd, że pijok nie pije. Wobec tego mamy sprzeczność i wszyscy piją (a także jedzą naleśniki z betonem serwowane przez gadające ślimaki i robią dużo innych dziwnych rzeczy — wszakże ex falso quodlibet). Gdzież więc leży paradoksalność całego paradoksu? Wynika ona w znacznej mierze ze znaczenia słowa "jeżeli". W mowie potocznej różni się ono znacznie od tzw. implikacji materialnej, w Coqu reprezentowanej (ale tylko przy założeniu reguły wyłączonego środka) przez implikację (->). Określenie "taka osoba, że jeżeli ona pije, to wszyscy piją" przeciętny człowiek interpretuje w kategoriach przyczyny i skutku, a więc przypisuje rzeczonej osobie magiczną zdolność zmuszania wszystkich do picia, tak jakby posiadała zdolność wznoszenia toastów za pomocą telepatii. Jest to błąd, gdyż zamierzonym znaczeniem słowa jeżeli jest tutaj (ze względu na kontekst matematyczny) implikacja materialna. W jednym z powyższych ćwiczeń udowodniłeś, że w logice klasycznej mamy tautologię P -> Q <-> ~ P \/ Q, a więc że implikacja jest prawdziwa gdy jej przesłanka jest fałszywa lub gdy jej konkluzja jest prawdziwa. Do paradoksalności paradoksu swoje cegiełki dokładają też reguły logiki klasycznej (wyłączony środek) oraz logiki konstruktywnej (ex falso quodlibet), których w użyliśmy w dowodzie, a które dla zwykłego człowieka nie muszą być takie oczywiste.

Ćwiczenie (logika klasyczna)

W powyższym dowodzie logiki klasycznej użyłem conajmniej dwukrotnie. Zacytuj wszystkie fragmenty dowodu wykorzystujące logikę klasyczną.

Ćwiczenie (niepusty bar)

Pokaż, że założenie o tym, że w barze jest conajmniej jeden klient, jest konieczne. Co więcej, pokaż że stwierdzenie "w barze jest taki klient, że jeżeli on pije, to wszyscy piją" jest równoważne stwierdzeniu "w barze jest jakiś klient". Które z tych dwóch implikacji wymagają logiki intuicjonistycznej, a które klasycznej?

Double negation shift

TODO SUPER WAŻNE: logika klasyczna to nie tylko rachunek zdań, ale też kwantyfikatory!

Wzięte z https://ncatlab.org/nlab/show/double-negation+shift

Klasyczna logika wyższego rzędu (TODO)

Aksjomat wyboru (TODO)

Być może jest to właściwe miejsce, by wprowadzić aksjomaty wyboru.

Interpretacja obliczeniowa logiki klasycznej, a raczej jej brak (TODO)

Tu opisać, jak aksjomaty mają się do prawa zachowania informacji i zawartości obliczeniowej.

Porównanie logiki konstruktywnej i klasycznej (TODO)

Uniwersum SProp (TODO)

Konkluzja (TODO)

Ściąga

Zadania (TODO)

Wyrzucić zadania mącące (mieszające typy i zdania)

Komenda Require Import pozwala nam zaimportować żądany moduł z biblioteki standardowej Coqa. Dzięki temu będziemy mogli używać zawartych w nim definicji, twierdzeń etc. Classical to moduł, który pozwala przeprowadzać rozumowania w logice klasycznej. Deklaruje on jako aksjomaty niektóre tautologie logiki klasycznej, np. zasadę wyłączonego środka, która tutaj nazywa się classic.