You are currently browsing the monthly archive for Grudzień 2011.

      Poprzednie rozważania naprowadziły nas na trop dowodzenia twierdzeń za pomocą sprytnie pomyślanych regułek przekształcających jedne napisy w inne, wychodząc od rzeczy uznanych za oczywiste, aż osiągnie się to co chcemy dowieść, lub sprytniej wychodząc od zaprzeczenia tego co chcemy dowieść, tymi samymi regułkami do sprzeczności we wszystkich możliwych przypadkach. Zapewne wielu ludzi wpadło na pomysł że skoro metody te sa algorytmiczne, to można je używać nie tylko na papierze, ale i za pomocą maszyny. Jak widzieliśmy juz w latach 50-tych posiadano dostateczne narzędzia i motywację by budować theorem proovers i dowodzić nimi realne twierdzenia ( np te z ‚Principia Mathematica” Russella i Whiteheada).

    W dalszej części wpisu chciałbym się skupić na Coq. Nie oznacza to bynajmniej że uważam go za najciekawszy czy najlepszy proover. Słynny i nadal chyba najdoskonalszy Mizar – dzieło Andrzej Trybulca ( posiada największą bibliotekę gotowych sformalizowanych teorii na świecie), prosty i ciekawy Mace4/Prover9 bardzo efektywnie wynajdujący kontrprzykłady dla podanych twierdzeń, Isabele, HOL, i wiele innych są przykładami bardzo ciekawych narzędzi. Coq wyróżnia się jednak „niewielkimi kosztami wejścia” i wydaje mi się, że stromą krzywą uczenia. W odróżnieniu np. od Mizara który potrafi sprawdzić dowód zapisany w syntetycznym, lecz bliskim naturalnemu, języku, czym przypomina prace z gołym kompilatorem, Coq oferuje pewną dozę interaktywności. Kiedy mamy do dowiedzenia twierdzenie, to po stosownej formalizacji – czyli po zdefiniowaniu stosownych pojęć i zapisaniu twierdzenia w odpowiednim języku Coq oferuje wybór taktyk dowodowych, przekształceń i reguł inferencji pozwalających na dowodzenie do pewnego stopnia wręcz na chybił-trafił. Oczywiście taka bezmyślna taktyka nadaje się do dowodzenia tylko bardzo prostych twierdzeń, z drugiej strony skoro czasami nie wiadomo od czego zacząć….

    Coq składa się z środowiska obliczeniowego Coq który jest narzędziem pracującym w linii komend i przypomina interaktywne środowiska programistyczne znane np. z pythona czy języków funkcyjnych, lub z tekstowych sesji matlaba. W tym trybie pracy możliwe jest zaczytanie wcześniej przygotowanego zestawu skryptów, ich „kompilacja” i uzyskanie odpowiedzi czy skrypty sa poprawne.
Praca w trybie tekstowym z pewnością jest bardzo użyteczną umiejętnością, zwłaszcza dla osób profesjonalnie użytkujących Coq, pozwala bowiem pracować z naprawdę sporymi teoriami o wielkiej liczbie twierdzeń itp. zapisanych w setkach plików. Dla osoby początkującej z pewnością znacznie ciekawszym sa środowiska interaktywne z interfejsem graficznym, wyposażone w menu z podpowiedziami i tym podobne ułatwienia. Środowiska takie nadają się także do prowadzenia dydaktyki – sądząc po sporej ilości kursów opartych na Coq jest to bynajmniej nie banalna część jego zastosowań.
     Wspomnę tu o trzech takich narzędziach – nadmieniając jedynie, że język programowania Coq nazywa się Gallina:

  • ProofWeb  którego autorem jest Cezary Kaliszyk i zespół programistów – działa świetnie i umożliwia zapoznanie się z systemem Coq bez potrzeby instalacji czegokolwiek – całość działa w przeglądarce – proszę sprawdzić! W szczególności polecam – jeśli ktoś chce sprawdzić przykłady które tu zostaną podane do posłużenia się tym środowiskiem. Warto wspomnieć że strona zawiera także kurs logiki oraz przygotowane skrypty z ćwiczeniami – warto spróbować! Uwaga – ProofWeb posiada własną bibliotekę regułek inferencji i taktyk dowodowych – ja zaś posługiwać się będę czystym Coq bez żadnych dodatków. Pomimo że poniżej używam kilku przykładów zaczerpniętych z materiałów ProofWeb, ich dowody sa poprowadzone inaczej – aby byly kompatybilne z „gołym Coq”. Te same przykłady mają swoje dowody w ProofWeb ( proszę poszukać;-) – jednak ich przeprowadzenie w Coq wymaga zaczytania biblioteki ProofWeb z której ja staram się tu nie korzystać.
  • ProofGeneral – to środowisko przygotowane do pracy z Emacsem. Osobiście używałem raz – nie lubię Emacsa. Jednak dla osób lubiących ten system operacyjny – środowisko to może okazać się bardzo produktywne, zwłaszcza, że nie jest ono ograniczone do wspierania jedynie Coq, i pozwala używać kilka rozmaitych systemów stosowanych w informatyce teoretycznej i matematyce jak Isabele, HOL, ACL2 itp.

    Coq wraz z CoqIde można ściągnąć za darmo ze strony http://coq.inria.fr/download . Coq jest systemem opensource, dystrybuowanym na podstawie licencji GNU Lesser General Public Licence Version 2.1 (LGPL). Coq został napisany głównie w Objective Caml. Prace nad jego stworzeniem rozpoczęto w roku 1984, autorami są Thierry Coquand and Gérard Huet którzy zaczęli prace, oraz Christine Paulin. Oczywiście lista autorów jest znacznie dłuższa. Coq powstał w instytucie INRIA we Francji.
     Instalacja pod Linuxem jest prosta i sprowadza się do użycia standardowych narzędzi dostępnych w dystrybucji, np. w wypadku Ubuntu wystarczy użyć: apt-get install coqide, dla Fedory: yum install coqide, i zgodzić się na pociągnięcie zależności. W wypadku Windows musimy ściągnąć stosowny instalator ze strony podanej powyżej i zainstalować program własnoręcznie. Dostępne są także wersję dla Mac OS oraz źródła programu.

    Pominiemy kwestię użycia interfejsu tekstowego, i przejdziemy do użycia CoqIde. Po uruchomieniu środowiska dostajemy okienko z trzema sekcjami:

1. okno w którym wprowadzamy komendy
2. okienko z komunikatami błędów i ostrzeżeniami
3. okienko w którym oglądamy wyniki naszych prac ( niejako standardowe wyjście programu).

    Jak na poniższym obrazku:

    Aby przejść od słów do czynów, wpiszmy pierwsze komendy w okienko komend (1). Proponuję aby poniższe sekwencje wpisać np. w ProfWeb który swoim wyglądem imituje CoqIde:

Na początek prosty przykład definicji typu wyliczeniowego ( czyli zbioru skończonego):

Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
     Po wpisaniu powyższego w pole (1) należy zatwierdzić to co się wprowadziło naciskając strzałkę w dół ( co spowoduje analizę wpisu i przejście do następnej komendy). Można także użyć wygodnej sekwencji ctrl-alt-down ( klawisz strzałki) – co niestety u mnie pod Ubuntu nie działa…
     Po zatwierdzeniu system zwraca nam komunikat który możemy odczytać w oknie (2) :

day is defined
dayrect is defined
dayind is defined
dayrec is defined

    Następnie definiujemy prostą funkcję pobierająca jako argument zmienną o type „day” i zwracającą wynik o tym samym typie:

Definition nextweekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.

     Po zatwierdzeniu system upewnia nas że „next_weekday is defined”
     Spróbujmy wyliczyć nasza funkcję dla kilku argumentów:

Eval simpl in (nextweekday friday).
Eval simpl in (nextweekday (nextweekday saturday)).

Co wyszło? Możemy teraz zapisać pierwsze twierdzenie dotyczące zdefiniowanej funkcji:

Example testnextweekday:
(nextweekday (nextweekday saturday)) = tuesday.

    Po zatwierdzeniu dostaniemy komunikat:

1 subgoal

============================
nextweekday (nextweekday saturday) = tuesday

    jak widać system nie przyjął równości na wiarę i oczekuje od nas uzupełnienia podanej zależności dowodem. Mamy konkluzję do dowiedzenia, i jest ono napisane pod kreską, nad kreska znajdują się zas dane przesłanki – w tym wypadku ich zbiór jest pusty. Jeśli teraz będziemy chcieli bawić się w dalsze definiowanie bez dostarczenia dowodu, system zaprotestuje pouczając nas że znajdujemy się w proof mode. Działania systemu zostały niejako wstrzymane do momentu w którym dowiedziemy naszej tezy. No to dowodzimy:

Proof. <- rozpoczynamy dowód. Nie trzeba tego robić, ale jak ładnie wygląda!
unfold nextweekday._ <- rozpiszmy definicję naszej funkcji. jak widać jawne wyliczenie prowadzi do oczywistej równości…
reflexivity. <- …którą uważamy za prawdziwą na mocy prawa zwrotności relacji równości
Qed. <- ;-) ładny koniec dowodu.

    Kilka słów komentarza. W powyższym „dowodzie” użyliśmy dwu tak zwanych taktyk dowodowych. Pierwsza nosi nazwę unfold, jej składnia to unfold nazwaobiektu_ i polega na wpisaniu w miejsce nazwy obiektu jego definicji. W naszym przypadku takie postępowanie pozwoliło od razu na wyliczenie wartości funkcji nextweekday z definicji. Wynikiem zastosowania tej taktyki była równość ( proszę sprawdzić!) w postaci tuesday = tuesday Wynik ten jest kolejnym twierdzeniem które musimy dowieść! Kolejnym krokiem było zastosowanie taktyki reflexivity czyli powołanie się na własność relacji równości. Ten sam dowód mógłby byc zapisany w nieco mniej wyrafinowany sposób: Proof. simpl. reflexivity. Qed. ( w jednej linii). Tym razem stosujemy taktykę simpl która sprowadza się do uproszenia wyrażeń przez wyliczanie tego co da się wyliczyć wprost.

    Taktyki o których tu mowa, to przykłady reguł inferencji, o jakich była mowa poprzednio, o mniej lub bardziej wymyślnych formach. Taktyki proste, jak te które sprowadzają się do rozpisania definicji funkcji są dosyć oczywiste, należy jednak wiedzieć, że Coq dostarcza taktyk w liczbie około 200 przy czym są wśród nich tak „proste” jak unfold czy simpl , skomplikowane jak induction realizująca indukcję matematyczną (postaram się o przykład w następnym wpisie), praktyczne jak taauto która umie dowieść skomplikowane tautologie logiczne, czy pochodna do niej intuition , są taktyki operujące po stronie przesłanek jak i taktyki operujące na konkluzjach. Można za ich pomocą eliminować implikacje, kwantyfikatory, dodawać dodatkowe założenia i budować lematy. Użytkownik może także samodzielnie budować własne taktyki, nazwać je i stosować kiedy mu to potrzebne. Spis gotowych taktyk wraz z opisem można znaleźć tu: http://coq.inria.fr/doc/tactic-index.html

    Podam teraz przykłady z klasycznego rachunku zdań:
Variables A B C D : Prop.

Theorem example01 : A /\ B -> B /\ A._
Proof. <- mamy dowieść implikacji A /\ B -> B /\ A.
intros. <- rozbijamy implikację na hipotezę H: A /\ B i konkluzję B /\ A.
destruct H. <- destruct to taktyka która sprawdza możliwe przypadki, w naszym przypadku hipoteza H zostaje rozbita na przesłanki H:A i H0:B. Obie przesłanki muszą być spełnione.
split. <-tym razem rozbijamy konkluzję na możliwe przypadki – w naszym wypadku mamy dowieść konkluzję 1. A i 2. B
assumption. <- konkluzja 1. wynika z założenia H.
assumption. <- konkluzja 2. wynika z założenia H0.
Qed. <- dowiedliśmy tezy.

(* komentarz w kodzie Coq tworzymy tak jak tu)
(Kontynuujmy wprowadzanie dalszych taktyk*)

Theorem example04 : A \/ B -> B \/ A._
Proof.
intros.
destruct H.
right.
assumption.
left.
assumption.
Qed.

    Po standardowym początku w którym pozbyliśmy sie implikacji, dokonaliśmy rozbicia na przypadki zostawiając tylko jeden ( z powodu obecności alternatywy). Tym razem pojawiły sie taktyki dotyczące alternatywy left i right które zostawiają z alternatywy odpowiednio lewy i prawy czynnik konkluzji. W każdym przypadku prawdziwość wynika z spostrzeżenia że konkluzja pojawia się w przesłankach.

    W następnym odcinku będą trochę bardziej złożone konstrukcje, a potem, na koniec postaram się uzupełnić wpisy o uwagi na temat Dependent Type Theory i Izomorfizmu Curryego-Howarda.

Reklamy

  

    Oj, jak się napracowałem. Wykonałem chyba z 60 testów dzisiaj i wreszcie osiągnąłem coś co można by nazwać zadowalającym stanem. Wreszcie mam możliwość użycia LaTeX do wzorów na blogu! Cała ta praca jest trochę wynikiem mojej pryncypialności i nonkonformizmu -chciałem mieć odpowiadającego moim gustom bloga. Nie cierpię wąskich szpalt dostosowanych do czytania na komórkach i olbrzymich marginesów z boku. Sa jakieś tam powody by tak robić, ale przecież problem nie polega na tym, że ktoś tak robi – tylko na tym że nagle cały internet się umówił że cokolwiek jest szerokie – nie istnieje. Mógłbym zatem podać tu długa listę blogów i serwisów których liczba co dzień wzrasta, a co do których mogę powiedzieć że twórcy mogą mnie pocałować w d* Jakoś tak bowiem się dzieje że wymyśla się coraz bardziej skomplikowane narzędzia ( xhtml, css, javascript, bóg wie co jeszcze) by na koniec nie dawać użytkownikowi żadnego wyboru i zmuszać go do wąskiej szpalty. Chciałem mieć szeroka i na dodatek ciemną stronę – użyłem więc motywu Nishita  ( bardzo ładny, zaprojektowany ponoć do publikacji zdjęć). Niestety okazało się, że wzory na których zależy mi jeszcze bardziej są wyświetlane zawsze od nowej linijki. Tragedia, bo znaczy to że jak w linii tekstu umieszczę głupi {sin (x) } to on złamie ta linię! Estetyczna porazka! Poprawka – możliwa – a jakże – trzeba wydać 30 dolarów na zakup profesjonalnego bloga na WordPress co pozwala samodzielnie modyfikować css….

    Na szczęście okazało się, że istnieje prosty sposób – motyw Tarski  używany pewnie nie bez przyczyny przez Terrence Tao na swoim znakomitym blogu, także na WordPress. Prosta zmiana tematu pozwala mieć wzory zarówno w linii jak i od nowej linii! Dałem wiec za wygraną i zdecydowałem się iść tą droga, rezygnując zarazem z ambicji publikacji szerokiego tekstu i na ciemnym tle.

 

     Inna kwestia techniczna to jak pisać formuły matematyczne na WordPress – w necie sa instrukcje więc nie ma sensu ich tu powielać. Chciałbym jednak zwrócić uwagę na następująca technikę publikacji ( stosowaną także przez Terrence Tao – uczmy się od najlepszych!). Mianowicie używa się skryptu latex2wp.py który z tekstu pisanego pod LaTeX robi kot pseudo html z tagami dostosowanymi do wordpress.com – w efekcie zyskujemy:

  • LaTeX warto znać a pisząc w nim poznajemy go coraz lepiej.
  • piszemy w naszym ulubionym edytorze
  • wzory wyglądają jak powinny – efekt można obejżeć u siebie przed publikacją na blogu generując na przykład pliki pdf
  • dokumenty mamy u siebie na dysku – żadna awaria nam niestraszna. Niech sobie chmury spadają na ziemię – nasze dzieła są nasze i nie zawahamy się ich użyć w innych wpisach
  • Eksperyment myślowy: a jak napiszemy coś genialnego? Taka ewentualność zawsze trzeba brać pod uwagę – to się nazywa optymizm i to zwiększa szanse na przeżycie w skrajnych sytuacjach np. w górach kiedy zsypie nas lawina!  Takie rzeczy zdarzały się nawet kompletnym idiotom! Albo temat się rozwinie? Powstanie cykl 100 wpisów o niebywałej wartości? Skontaktuje się z nami jakieś wydawnictwo ( zupełnie jak w reklamie telefonów komórkowych sprzed 10 lat gdzie z kwiaciarką kontaktował się wizytujący Kraków amerykański biznesmen)? Może zrobimy z tego książkę? Droga Latex -> cokolwiek jest znacznie prostsza niż HTML -> coś użytecznego… 

    Tak więc polecam – może warto wypróbować – konto na WordPress jest za darmo a posty – jeśli ktoś ma depresję i jest człowiekiem pozbawionym wrodzonego entuzjazmu – mogą pozostać prywatne! Skrypt o którym mowa można pobrać na tej stronie, zaś instrukcja jego używania znajduje się tuż obok. 

    Droga ku genialnym wpoisom wydaje się prostsza!

   

    Systemy dedukcji

    Chciałbym napisać coś o Coq. temat jest jak rzeka, ale nie brak tez materiałów w necie a nawet książek wśród których, co ciekawa, a dla mnie przyznam zaskakujące, pojawiają się polskie nazwiska. Pomyślałem jednak że warto na początku podzielić się trochę historyczną wiedzą, zwłaszcza, że jak jej nie zapiszę to i tak mi z głowy zniknie;-) W zasadzie celem poniższego jest skierowanie czytelnika do przeglądnięcia metody tabel analitycznych oraz pokazania jakiegokolwiek systemu dedukcji naturalnej. Wszystko to w celu zwrócenia uwagi, że systemy automatycznego dowodzenia twierdzeń nie sa cudem ale przemyślnie skonstruowanymi programami, i że jest to dziedzina posiadająca obecnie długa historię sięgająca co najmniej lat 50-tych a może i początków wieku XX. Autor, czyli ja, jest laikiem i amatorem, rad więc przyjmie;-) komentarze i uwagi, zwłaszcza od chcących podzielić się wiedzą, byle nie na temat ortografii;-)

    Początek wieku XX był czasem burzliwego rozwoju logiki. Koniec XIX wieku przyniósł sporo zmian i zamieszania po pracach Fregego i Cantora. Frege dokonał reformy logiki tworząc ją taką jaką znamy obecnie – wprowadził większość znanej nam symboliki, ustalił znaczenie pojęć, podał podstawowe definicje. Cantor tworząc teorię mnogości określił język dla uprawiania matematyki jednak uznanie zostało poprzedzone wielkim zamieszaniem u podstaw samej matematyki – bowiem teoria mnogości wydawała z początku się paradoksalna i niespójna, nie została przyjęta ze zrozumieniem. Można wręcz zasugerować, choć to pewnie kontrowersyjna ocena, że w dużej mierze burzliwy rozwój matematyki w tym przełomowym okresie był próbą wprowadzenia ładu w teorie Fregego i Cantora, okazały się one bowiem tak istotne i wpływowe że zatrzęsły podstawami matematyki. Istotną rolę w rozwoju logiki w tamtych czasach odegrały prace Hilberta nad teorią dowodu, siłą rzeczy zahaczające o logikę i będące próbą formalizacji wnioskowania matematycznego.

    Hilbert starał się wdrożyć potężny program uporządkowania podstaw matematyki w celu przezwyciężenia trudności wynikających z rozlicznych paradoksów odziedziczonych po pracach o których mowa. Okres ten można by podsumować omawiając prace Russella i Witheheada „Principia Mathematica” będącą próbą sprowadzenia matematyki do logiki Fregego i całej matematyki – prąd ten nazywamy logicyzmem ( współcześnie uważa się raczej zgodnie że była to próba nieudana). Można by to dzieło nazwać łabędzim śpiewem logicyzmu, pozostała jednak po niej teoria typów, rozwijana współcześnie w ramach informatyki w zupełnie innym kontekście i z innych powodów. Następne przyszły prace Goedla i Tarskiego niejako zamykające pewien etap, w znaczeniu – ustalające pewien kanon ścisłości i metod opisu w rozwoju logiki. W zasadzie wąsko rozumiany program Hilberta, podobnie jak logicyzm, upadł – prace Goedla przypieczętowały koniec marzeń o absolutnych i obiektywnych podstawach matematyki – jednak z tą opinią nie zgadza siwe zdecydowana większość matematyków;-) Jak było tak było, co wygrało to wygrało, ale wypracowane rozwiązania i metody okazały sie bardzo owocne i przetrwały niejako w nowej roli – stworzono teorię modeli, nowoczesną semantykę, teorię prawdy, ugruntowano pojęcie teorii formalnej.

    Mniej więcej pośrodku tego okresu podjęto próbę formalizacji teorii dowodu i wnioskowania matematycznego. Opisano wówczas tak zwane systemy dedukcji.

    Systemy dedukcji zostały formalnie opisane po praz pierwszy w pracach G.Gentzen  i S.Jaśkowskiego  Warto nadmienić, że jakkolwiek popularność zdobyły prace Gentzen i to one stały się motorem rozwoju tej dziedziny logiki, to wikipedia przyznaje pierwszeństwo otwarcia tematyki badań Jaśkowskiemu. Systemy te, nieco zapomniane i mam wrażenie wyparte z kursów matematyki uniwersyteckiej wydają się co najmniej od lat 60-tych zdobywać na znaczeniu za sprawą rozwoju metod automatycznego dowodzenia twierdzeń. Prace Gentzen i Jaśkowskiego miały jednak motywację czysto teoretyczną i można przypuszczać, że np. Gentzen starał się częściowo być może realizować program Hilberta którego był asystentem.

    Systemy dedukcji w myśl prac Gentzen składają się z dwu elementów (za „Małą Encyklopedią logiki” ): „Każdy system dedukcyjny może być określony jako para (A,R) gdzie A jest zbiorem aksjomatów, zaś R zbiorem reguł dedukcyjnych.”

    Jeśli zbiór aksjomatów jest niepusty, mamy do czynienia z systemem logicystycznym i odpowiada to klasycznym sformułowaniom teorii matematycznych, kiedy zaś zbiór aksjomatów jest zbiorem pustym – mamy do czynienia z systemem dedukcji naturalnej. Co ciekawe systemy dedukcji naturalnej opisano dopiero w latach 30-tych ubiegłego stulecia – wcześniejsze systemy to systemy logicystyczne mające swoje pochodzenie w tradycji logiki i matematyki. Dla porządku, za „Małą Encyklopedią logiki” podam tu przykład dla zestawu reguł dla systemu Naturalnej Dedukcji Klasycznej:

operator: reguła prowadzania: reguła opuszczania:
     
(\land)  \frac{A B} {A \land B}  \frac{A \land B}{A}; \frac{A \land B}{B}
     
(\lor)  \frac{A}{A \lor B};\frac{A}{A \lor B}  \frac{A \lor B, A \vdash C, B \vdash C}{C}
     
(\lnot)  \frac{A \vdash 0 }{ \lnot A}  \frac{A \lnot A}{0};\frac{ \lnot \lnot A }{A}
     
(\to)  \frac{A \vdash B}{A \to B }  \frac{A,A \to B}{B}
     
(\forall)  \frac{B(a)}{(x)B(x)}  \frac{(x)B(x)}{B(a)}
     
(\exists)  \frac{B(a)}{(Ex)B(x)}  \frac{(Ex)B(x),B(a) \vdash A}{A}
     

    oraz reguła dodatkowa: { \frac{0}{A} }

    Rozszyfrujmy powyższe reguły. Każda z nich ma postać „ułamka” w którym nad kreską znajdują się przesłanki, a pod kreską konkluzja. Są to reguły wnioskowania lub inaczej inferencji i należy przez to rozumieć, że jeśli dla przykładu w regule wprowadzania {(\land)} mamy jako przesłanki prawdziwe zdanie A oraz prawdziwe zdanie B, to należy przyjąć że prawdziwe jest także zdanie {"(A \land B)"}. Ciekawa jest reguła (v) w której pojawia się symbol odwróconej litery T. Oznacza on wynikanie – A T C oznacza, że z A logicznie wynika C. Jest to wynikanie logiczne w odróżnieniu od implikacji która jest zdefiniowana jako {p \rightarrow q = \lnot (p \land \lnot q)} bądź za pomocą znanej tabelki z 0 i 1-kami. Kolejny ciekawy szczegół to druga reguła opuszczania {( \lnot )} zwana regułą wyłączonego środka. Jej usunięcie z przytoczonego zestawu prowadzi do innego, nierównoważnego zestawu reguł dedukcji związanego z systemami intuicjonistycznymi – i jest podstawą logiki intuicjonistycznej. Logika ta jest używana w wielu systemach komputerowych dowodów w tym w systemie Coq, o którym będzie ( być może;-) mowa. Reguła opuszczania dla {(\rightarrow)} to oczywiście modus poens czyli reguła odrywania. Reguły {( \forall )} i {( \exists)} dotyczą kwantyfikatorów i pozwalają od zdania kwantyfikowanego przejść do szczególnego przypadku ( „skoro prawdą jest że dla każdego x B(x) to mogę za x wstawić jakąś stała a i opuścić kwantyfikator”, „skoro prawda jest że dla dowolnej stałej B(a), to prawda jest że dla każdego x, B(x)” itp.) Nie ma potrzeby wnikać tutaj dalej w szczegóły. Systemy Gentzen są ciekawe z wielu powodów, teoretycznych związanych z teorią dowodu i praktycznych sa bowiem podstawą automatycznego generowania – a przez to dowodzenia, twierdzeń. Wychodząc od znanych przesłanek, w ramach systemu dedukcyjnego opisanego regułami jak powyżej ( lub innymi) możemy generować kolejne konkluzje będące przesłankami dla następnych konkluzji itp. Oczywiście jeśli zbudujemy ciąg prowadzący od uznanych przesłanek, a zakończony interesującym nas zdaniem – otrzymamy dowód wprost zdania nas interesującego. Jeśli przesłanki są aksjomatami ( co w systemach dedukcji naturalnej nie jest konieczne) – otrzymamy klasyczny dowód wprost zgodnie z definicją twierdzenia w teorii aksjomatycznej.

    Systemy dowodzenia wprost jakkolwiek mają wielkie znaczenie teoretyczne – sa trudne do stosowania w praktyce. Aby dowodzić zadane twierdzenia należałoby kolejno stosować możliwe kombinacje reguł az znajdziemy stosowną i uzyskamy tezę. Oczywiście liczba możliwości rośnie błyskawicznie wraz ze stopniem komplikacji twierdzenia, i metoda staje się niepraktyczna. Z tego a także z wielu innych powodów w badaniach teoretycznych systemów formalnych ogranicza się zwykle liczbę reguł inferencji do modus poens, często przy tym rozbudowując aksjomaty. Warto jednak pamiętać, że rachunek oparty na systemach reguł jak powyżej jest w stanie generować automatycznie twierdzenia wychodząc z zadanych przesłanek. Jest on także bardzo ważnym narzędziem teoretycznym w teorii dowodu zwłaszcza kiedy doda się do niego tak zwaną regułę cięcia ( cut), która pozwala zdziałać cuda, miedzy innymi pozwoliła Gentzen na dowód niesprzeczność arytmetyki Peano bez schematu indukcji, niesprzeczność rachunku kwantyfikatorów i wiele innych. Utorowała także drogę do metody tablic analitycznych która jest kolejną, podstawową techniką mechanicznego dowodzenia twierdzeń. Twórcami metody tablic analitycznych są holenderski logik Beth (1956)  i Fin Hintikka (1955). Nie będę się tu wgłębiał w szczegóły metody, w skrócie odpowiada ona dowodowi niewprost czyli przez zaprzeczenie tezy i doprowadzenie do sprzeczności. W metodzie mechanicznej zaprzeczamy tezie i badamy kolejno wszystkie możliwe implikacje tego działania – tworzy się w ten sposób rodzaj drzewa zawierającego w gałęziach formuły logiczne. Sprzeczności – czyli jednoczesne pojawienie sie na jednej gałęzi p i ~p – ograniczają wzrost drzewa. Jeśli twierdzenie jest prawdziwe, każda z gałęzi zawiera sprzeczność – mówimy że drzewo jest zamknięte. Jeśli twierdzenie jest fałszywe – gałąź niezawierająca sprzeczności daje jednocześnie kontrprzykład – przynajmniej w wypadku klasycznego rachunku zdań. Klasyczny rachunek zdań jest rozstrzygalny, to znaczy dla każdego zdania jesteśmy w stanie w skończonej liczbie kroków podać czy jest prawdziwe. Odpowiada to skończonemu drzewu w ramach metody tablic analitycznych. Dobre przedstawienie metody po polsku zawiera podręcznik Kazimierza Trzęsickiego „Logika i teoria mnogości Ujęcie systematyczno-historyczne” – polecam. W wypadku użycia kwantyfikatorów, a wiadomo że taki przypadek nas interesuje, z wyżej podanych reguł inferencji wynika, że ich eliminacja kwantyfikatora wymaga wprowadzania kolejnych stałych. Liczba tych stałych szybko rośnie, de facto uniemożliwiając skuteczne dowodzenie dowolnych twierdzeń – jak wiemy rachunek logiczny kwantyfikatorów nie jest rozstrzygalny. Współczesny kształt metodzie nadał znany logik Smullayan, jego wpływ był tak wielki że w zasadzie mówi się współcześnie o tablicach jako o jego metodzie. Najpewniej należy przypisać temu, że nie tyle mamy do czynienia z jedną metoda a raczej z ich całą rodziną, i że Smullyan opracował i usystematyzował efektywną i praktyczną metodę dla klasycznego rachunku logiki pierwszego rzędu. Smullyan jest także autorem kilkunastu książek popularyzujących logikę napisanych w całkowicie brawurowy sposób.

    Ciekawym aspektem metody tablic analitycznych jest kolejny polski trop. Otóż jak pisze Melvin Fitting w ‚Introduction” w „Handbook of Tableau Methods” M.D’Agostino, D. M. Gabbay, R. Hahnle and J. Posegga, eds. „Notational simplification was the essential next step in the development of tableaus and, just as with the preceding stage, it was taken independently by two people: Zbigniew Lis and Raymond Smullyan. Lis published his paper [Lis, 1960] in 1960, but in Polish (with Russian and English summaries), in Studia Logica. At that time there was a great gulf fixed between the East and the West in Europe, and Lis’s ideas did not become generally known. They were subsequently rediscovered and extended by Smullyan, culminating in his 1968 book [Smullyan, 1968]. The work of Lis himself only came to general attention in the last few years. […] It is through Smullyan’s 1968 book First-Order Logic [1968] that tableaus became widely known. They also appeared in the 1967 textbook [Jeffrey, 1967], which was directed at beginning logic students. Smullyan’s book was preceded by [Smullyan, 1963; Smullyan, 1965; Smullyan, 1966] in which the still unknown contributions of Lis were rediscovered, deepened, and extended.”

    Metody tablic analitycznych zostały wymyślone od podstaw w celu automatyzacji technik dowodu. Poniżej ciekawy cytat z tego samego artykułu: „In 1957–58, Dag Prawitz, Prawitz, and Neri Voghera developed a tableau-based a system that was implemented on a Facit EDB [Prawitz et al., 1960]. At approximately the same time, the summer of 1958, Hao Wang proposed a family of theorem provers based on the sequent calculus, which he then implemented on an IBM 704 [Wang, 1960]. The first of Wang’s programs, for classical propositional logic, proved all the approximately 220 propositional theorems of Russell and Whitehead’s Principia Mathematica in 3 minutes! This was quite a remarkable achievement for 1958.”

Komentarze ( z buzz):

Marcin Rzeźnicki – Świetny post. Moje gratulacje. Dobrze napisane. Wspomniał bym jeszcze o Heytingu i semantyce Heytinga jako o „dynamicznym”, funkcjonalnym obrazie logiki w celu uzupełnienia przykładu o prawie wyłączonego środka – to może być ciekawe dla „komputerowców”. Polecam książkę Girarda „Proofs and Types” – do ściągnięcia za free z: http://www.paultaylor.eu/stable/Proofs+Types (w tym ujęciu a or not a polegało by na znalezieniu dowodu dla a lub funkcji mapującej dowód a -> 0 co, jak wiemy, nie zawsze jest możliwe). Podobnie z eliminacją podwójnej negacji. a potem pewnie izomorfizm Curryego-Howarda, ale to pewnie masz w zanadrzu na potem. Czekam z niecierpliwością !!8/6

Kazimierz Kurz – @Marcin Rzeźnicki dziękuję, jest mi bardzo miło. Obawiam się jednak że przeceniasz moje możliwości i aż tak kompetentnie tematu nie opiszę – onieśmieliłeś mnie ;-). Chciałem tylko pokazać system dedukcyjny na papierze, i pokazałem jego definicję żeby było jasne że nie od komputerów się zaczęło. O tw. Curryego-Howarda rzeczywiście trzeba będzie wspomnieć, ale jednak celem raczej jest pokazanie samego Coq, a nie „Wprowadzenie do komputerowych metod dowodu – ujęcie historyczne” ;-) bo zwyczajnie nie mam do tego stosownej wiedzy i kwalifikacji, choć chciałbym mieć. Marcin – a może uzupełnisz to co napisałem? Dodaj co uważasz za stosowne – będzie cykl wpisów;-). Mam juz za sobą niedokończone obietnice na temat grupy renormalizacji – tam tez nie powstała najbardziej techniczna część tematu – za co ze wstydem przepraszam – poległem jednak na diagramatyce – aby coś w tej teorii pola porachować trzeba mieć diagramy Feynmanna a to mnie wyraźnie przerosło. Z drugiej strony taki jest ten Web2.0 – jak człowiek się zleniwi a motywacja uleci – cudne plany idą w odstawkę. Tym razem Mój Sprytny Plan ;-) jest taki, że chciałbym napisać takie wpisy -systemy dedukcji (*zrobione, ew do uzupełnienia) -opis narzędzia -Prosty dowód -Nieco skomplikowany dowód Pisząc toto spostrzegłem jak niewiele wiem;-) i jak wiele trzeba by się dowiedzieć by wyjaśniać komuś kto, zakładam, wie jeszcze mniej. BTW. szalenie żałuję, że nie ma tu nigdzie Wlodzimierza Holsztyńskiego – jego uwagi merytoryczne i biograficzne mogłyby być tu znacznie bardziej wartościowe niż sam mój wpis, gdyby zechciał toto skomentować. Jeszce raz dziękuję.
    W następnym wpisie postaram się napisać coś o Coq.

    Jeśli Laplace by się nie mylił, Bóg byłby rachmistrzem, stałby za pulpitem i w swojej księdze buchalteryjnej rozwiązując równania różniczkowe i ustalając warunki początkowe kontrolowałby każde zdarzenie we wszechświecie. Obraz ten ma ponad x lat, ale nadal ciąży na naszym pojmowaniu Boga, jedyne co od tamtego czasu się zmieniło, to stanowisko z jakiego patrzymy na Jego istnienie. Raz zatem widzimy w nim informatyka, innym razem genetyka, za każdym razem chcemy w im widzieć uosobienie naszych nadziei na poznanie świata, panowanie nad przyrodą i na koniec, choć to może najważniejsze zrozumienie egzystencji nas samych – ludzi.

     Modele Boga dla ateistów ( i nie tylko):

1. Magik: Bóg składa w twoją rękę kopertę. Dokonujesz wolnego wyboru. Otwierasz kopertę a tam jest napisane co wybrałeś

2. Oszust ( model sfalsyfikowany przez nierówność Bella – czyli nauka dowiodła, że Bóg nie jest oszustem ;-): szafki jak w skrytkach pocztowych, Bóg zagląda do środka od swojej strony bo ma takie drzwiczki i może określić wartości układu kwantowego. My jako klienci świata z drogiej strony musimy z konieczności patrzyć na szafeczki przez oczy rozumu zasłonięte źle dobranymi i dalekimi od doskonałości okularami. Niestety nie widać przez nie zbyt dokładnie, i albo udaje nam sie dostrzec ze coś sie porusza albo widzimy w którą stronę ale nie wiemy jak szybko.

3. Matematyk w prochowcu: Bóg jako metamatematyk ma w kieszeni zbiór wszystkich zbiorów

4. Supier-Kompiuter: Bóg a umie obliczyć wartości funkcji nieobliczalnych i umie zdefiniować co to prawda posługując się kilkoma znanymi sobie sentencjami.

5. Mnich Filozof: Bóg parzy na nas z góry i się zastanawia po co ta bieganina, ale tak naprawdę mało go to obchodzi, bo jego oczy zwrócone sa ku wieczności i sprawy doczesne niewiele go obchodzą skoro nie ma po co się martwić o wikt i opierunek.

6. Mechanik: Bóg jako mechanik został wymyślony przez Laplace’a kiedy jeszcze się zdawało że światem rządzi mechanika precyzyjna….

7. Posthumanista: Bóg jako tajemnica która leży u źródeł wszystkich dekonstrukcji naszych narracji opisujących świat. Jakby ktoś wiedział co znaczy to zdanie, proszę o informacje…

    Inspiracja: http://www.staff.amu.edu.pl/~zbigonys/model_boga.html

 

Ale spiewać, marzyć, snić, smiać się
Wolnym biec ku tenczy, miec oko żywe
i glos, który dzwięczy
na bakier nosić pilsń i dla estymy bić się do woli
albo składać rymy
Nie dla fortuny, nie dla marnej sławy
pracować, ale dla zabawy i na ksieżyc patrzeć
I się nie prosić, jak ów bluszcz w potrzebie
Lecz mieć szacunek dla samego siebie
Choćby debem ni klonem się było
Iść nie wysoko, ale wlasną siła.

 

Sztuka: tu i tam, Autor, Postać ;-)

   

    Dobra książka to taka która jest zrozumiała, dobrze się czyta, przekaz jest nie tylko chwytliwy ale i rzetelnie zaargumentowany, tematyka aktualna ( nie mylić z opisywaniem zdarzeń bierzących), i ważna. W dzisiejszych czasach bywa to rzadkie zwierzę. Trzeba przyznać, a powody zostana wyjawione bliżej poniżej, że książek wydawanych przez polskich autorów o tych cechach jest naprawdę niewiele. jakos wydaje mi się, że jesteśmy skażeni jednak prowincjonalizmem i to zartówno w dziedzinie literatury pieknej ( no…) jak i literatury polemicznej, o naukowej nie będę się wypowiadał bo takowa w Polsce nie istnieje. Tym ciekawsza wydaje sie pozycja o której piszę: Jan Sowa „Ciesz sie późny wnuku. Kolonializm, Globalizacja i Demokracja Radykalna”.

   Waga ksiązki niekoniecznie musi dotyczyc racji czy prawdy przedstawianych tez. Uznanie dla dzieła niekoniecznie musi oznaczać podzielanie pogladów autora, lub sprzyjanie proponowanym diagnozom. NIemniej jak mówia z mądrym lepiej stracic nieraz jak z głupim zyskać.

    1 Demokratyzacja

    Książka jest o demokrartyzacji. Pozostałe elementy tytułu wskazuja na powiązania z pozostałymi wątkami pracy, i w rzeczy samej nie mylą, autor porusza temat kolonializmu i globalizacji. Co jednak ważne, porusza nie tylko z racji pola zainteresowań, czy innych arbitralnych w gruncie rzeczy powodów ( np. panującej mody), lecz z powodu zasadniczego: podstawowa teza książki jak by ja nie odczytać, zawiera jeden dominujący pierwiastek: teorie proponujące opisujące problemy tego świata muszą dawać perspektywę równie szeroka jak zakres owch problemów, a te sa globalne, i muszą ujmować rzecz w kontekście historycznym a w aspekcie jakim jest demokratyzacja społeczeństw, globalna ekonomia, kontrasty biedy i bigactwa, jest on zasadniczo kolonialny.

    Demokratyzacja rozumiana jest tu jako idea na wpół utopijna, stawiająca człowieka przed problemem dobrych rządów i dobrego ustroju politycznego i głosząca że rozwiązaniem jest współuczestnictwo we władzy szerokich mas społecznych. Autor rozpoczyna analizę od archetypicznej demokracji ateńskiej. Posiadala ona szereg paradoksalnych dla nas cech: była bynajmniej niepowszechna, obejmowała bowiem tylko nieznaczny odsetek obywateli: wolnych obywateli Aten. MIlcząca większość była owej mniejszości podporządkowana, i w tym sensie archetypiczny ustrój ludowy był w istocie dyktaturą elity. Niemniej w jej ramach ideał rządzenia zasadzał się na absolutnej równości pociągniętej tak dalece, że na urzędy wybierano w drodze losowania.

    Podobne koncepcje narażone sa na operacje konsekwencji logicznej: jesli bowiem ideał polityczny greków zakładał, że prawdziwie obywatelem, podmiotem i jednostką danego polis staje się jego obywatel wyłącznie kiedy uczestniczy we władzy i przyjmuje jej brzemię, to tym samym osoba która tego czynić nie mogła, nie uzyskiwała podmiotowości a była jedynie rządzona. A zatem nie w pełni była podmiotem. Podobna operację jak sie okazuje wykonywano w historii wielokroć, i choć nie sposób argumentować z sensem za tezą o liniowym rozwoju społeczeństw ku jakiemuś utopijnemu dobru, faktem jest, że obecne formy rządów i politycznej organizacji także w rozumieniu praktycznym de facto dają przeciętnemu zjadaczowi chleba w społeczeństwach zachodu szerokie uprawnienia współudziału we władzy. przynajmniej w teorii.

    Oczywiście w świecie pełno biedy, a akumulacja kapitału w obszarze północnej pułkuli jest przytłaczająca. Są w świecie kraje w których przeżycie grancz z cucem, co wobec dylematów konsumenta z kultury zachodniej w sklepie z artykułami AGD jest dosyć niekonfortową perspektywą.

    Wygląda tez na to, że społeczeństwa zyjące w demokracji ( w różnym stopniu zdemokratyzowane, i zliberalizowane co nie jest tym samym) żyja dostatniej. A może ci co zyja dostatniej zyją demokratyczniej? Czy to wynik przypadku czy demokratyzacja zyci aw istony sposób jest związana z efektywnościa ekonomiczną? Czy liberalizm gospodarczy i obyczajowy sa z demokracja związane? A z dobrobyrtem? Odpowiedzi wcale nie muszą być tak oczywiste jak sie przyjmuje w płytkiej polskiej dyskusji politycznej.

    Co ciekawe pojawia się także pytanie o możliwość demokratyzacji społeczeństw biednych. Kultura zachodnia zorganizowana jest wokół koncepcji indywidualistycznych, podkreślających wartość aspiracji jednostki i potrzebę jej samorealizacji w warunkach szerokiej wolnosci i realizacji swobód. Na ile jednak jest to związane z demokracją? W wydaniu ateńskim niemal wcale. Stawiamy więc pytanie o relacje miedzy liberalizmem, neoliberalizmem, ekonomią, demokracja i rozwojem krajów zacofanych i biednych wobec wyzwań globalizacji i w kontekście niedawnego i, tak, tak, obecnego kolonializmu.

    2 Solidarność

    Jednym z najciekawszych, choć zarazem dla mnie najbardziej kontrowersyjnych fragmentów ksiązki jest rozdział poświęcony przemianom w Polsce. O ile wydają mi się trafne tezy autora o tym, że upadek komunizmu była bardziej koniecznością dziejowo-ekonomiczna niz zasługa papierza, oraz, że polityka regana wobec ZSRR była bardziej dowodem słabości USA niż dominacji wolności i demokracji, o tyle obraz Solidarności i jej relacji do opisywanych w dosyc ambwiwalenty sposób elit wydaje mi się nadużyciem. Oczywiście nie będę tu polemizował z tezą, że społeczna baza ruchu Solidarności, a więc przede wszytstkim robotnicy, de facto poniosła największe koszty przemian gospodarczych w Polsce po roku 89. To oczywista prawda. Niemniej z obrazu tych czasów jaki zapamiętałem wiem też jak wyglądały puste pułki, oraz to, że ruch ów nie miał az tak konstruktywnego charakteru jak chciałby tego autor.

    Nie chodzi mi tu o stwierdzenie jakoby Solidarność była ruchem destrukcyjnym tylko, bo to nieprawda, ale raczej o to, że mam wrażenie iż Sowa zdecydowanie przecenia celowość działan tego ruchu. Nie jest prawdą, że Solidarność miała jakąs alternatywę dla porzadku społecznego do którego obalenia się przyczyniła. Był to jednak niewątpliwie ruch artykuujący tendencje wolnosciowe i związane z podmiotowoscia obywateli i wtym elemencie zgadzam się z autorem.

    Nie zgadzam się natomiast z teza jakoby przedstawiciele inteligencji, owe niesławne elity, zdradziły ruch Solidarności dla władzy. Wchodzą tu w grę bowiem dwa czynniki które autor pomija: odpowiedzialności i ograniczności czy zaściankowości. Jakie byłoby zdanie Sowy o Michniku, Mazowieckim czy Wałesie, gdyby wobec politycznego zwycięstwa nie wzięli na siebie ciężaru władzy? Czy nie byłaby to wielka nieuczciwość: walczyć z aparatem opresji w imie wolnosci i samostanowienia a w momencie gdy walka owa zakonczona zostaje sukcesem nie podjąc ciężaru dobudowy zdewastowanego kraju i odnowy społeczeństwa?

    Zdecydowanie odmiennie niz Sowa oceniam tez Okrągły Stól. Zjawisko to jest jednym z najbardziej chlubnych punktów w historii polskiej państwowości, rodzajem narodowej zgody nieznanej na tej ziemi, kompromisu bedącego podwaliną nowych ram egzystencji wolnej ojczyzny. Oczywiście, kompromis pozostawia niedosyt, wolę niedosyt od rzeki krwi. Jeśli w Solidarność urzeczywistniła jakieś wartości, a uważam to za bezsprzeczne, to było wśród nich także i wyrzeczenie się przemocy w działaniach i pewien minimalizm, pewna konkretność rządań ( nie mylic z oczekiwaniami). Niemniej podzielam krytyczna opinie na temat kształtu gospodarki w wolnej Polsce. Zaściankowośc polskich elit, ich ograniczoność ma zaś głębokie historyczne tradycje. Społeczeństwo nasze zamkniete jest w kregu własnego samouwielbienia, zaś inteligencja z jej rola niesienia światła w zdrowa materię lawy pokrytej skorupa pełna jest przekonania o dziejowej roli i misji zbawienia narodu. Postawa taka nie sprzyja ani krytycznemu myśleniu o sobie samym ani tym bardziej uważnemu obserwowaniu innych. Tym samym zarzucanie Kuroniowi czy Geremkowi że bezkrytcznie zaimportowali symbolike i mity zaachodniej wolnosci i liberalizmu nie dostrzegając, zę importuja także konsumpcjonizm i implantuja de facto zamordystyczna gospodarke kaptalistczną jest po prostu nieporozumieniem. Wszytskim nam się wydawało, że los robotnika w RFN jest wart implantacji na warunki Polskie, bo nasz robotnik nie miał nawet tyle co ów jak obecnie sie okazuje również wyzyskiwany ( ale z jakim konsumpcjnym wdziekiem…).

    3 Odrobina dziegciu ( Nie taka znowu mała…)

    Książka w istocie przedstawia pewną perspektywę rozwoju społeczności i demokracji. Podstawową teza zdaje się byc przkonanie, że największa słabnością neoliberalizmu i współczesnej liberalno-demokratycznej konstrukcji społeczeństwa jest to, iż w istocie odsuwa na daleki plan wszelkie dywagacje o pożądanym kształcie społecznosci. W tym sensie jest to zrealizowana koncepcja końca historii Fukujamy, oto bowiem nic lepszego juz sie nie da osiągnąc, niz konsumpcyjny raj przerywany co pare lat wyborami które we współczesnym wydaniu coraz bardziej zaczynają przypominać, cuż, zakupy. I tu moge się z Sową zgodzić: nie powinniśmy zamykać oczu na możliwości poprawy warunków zycia naszych i innych ludzi także, i poszukiwac należy lepszych rozwiązań. Autor wielokrotnie zwraca uwagę, że dzisiejsze oczywistości w postaci wolnosci, praw człowieka, równosci płci, niedyskryminacji kilkaset czy nawet kilkadziesiąt lat temu bywały określane jako mżonki. Nie ma w ich istnieniu nic oczywistego. Zostały wywalczone i co więcej nieraz krwawo. Na marginesie, bo nie moge się powstrzymać, nadmienie, że jednym z najbardziej zakłamanych pod tym względem obrazów w dziejach kina jest „Forest Gump”. Nie będę jednak tu tematu rozwijał, może innym razem.

    Logiczną konsekwencją tych działań, a więc walki o wolność osobistą, standardy międznarodowe, prawa człowieka, inkluzywność instutucji przedstawicielskich jest poszerzenie zakresu demokracji, do skali globalnej, Autor zatem proponuje damokratyzację działan międzynarodowych przy użyciu środków technicznych jakimi dysponujemy, o zmiane tam gdzie to realnie mozliwe, rządów z formy przedstawicielskiej na formę reprezentacji. W tej ostatniej wybierany przez społeczność reprezentant ma w ramach udziału we władzy reprezentować zdanie wyborców, pod zagrożeniem natychmiastowego odwołania, nie jest to więc rodzaj posła-przedstawiciela obdazonego polityczną autonomią, a raczej wynajęty reprezentant o ściśle okreslonych przerogatywach.

    Autor wspomina nawet o proppozycji demokratycznej kontroli nad badaniami naukowymi i decydowaniu o przeznaczaniu funduszy w ramach demokratycznych i w pełni uspołecznionych procedur.

    Łyżka dziegciu tkwi w okolicach środka książki, gdzie autor wspomina, w jednym z krajów demokratycznych, prawa kobiet do głosowania zostały uznane dopiero w latach 60-tych. Chodzi o Szwajcarię. Jak się okazuje, co Sowa wielekroć podkreśla w pierwszej części pracy, powszechność i konsekwentcja w demokratycznej organizacji społeczności prowadzi czasami do patologicznej petryfikacji zabobonów. Remedium twki w organizacji demokracji w wiekszości istniejących państwach demokratycznych: co prawda procedury wyborcze sa inkluzywne i demokratyczne, rządy jednak sa juz prowadzone rpzez wbraną w ten sposób elitę, która nie musi sprzyjać w dziłaniu populizmom, czy powszechnym w społeczeństwie zabobonom. Praktyka pokazuje, że po latach narody szczyca się nierzadko tym, co zafundowały im ich elity bez niczyjej zgody i konsultacji społecznych. Sowa to wie, bo o tym pisze. Sam wiem to od niego. A jednak widzi w dalszym poszerzeniu demokracji na bardziej bezpośrednie formy rozwiązanie bolączek świata. Czy gdyby byc konsekwentnym, i przyjąć to za dobra monete, ale byc tez realistą, nie dojdzie się do wniosku, ze jedyna mozliwa współcześnie forma takich rządów będzie nader podobna do konkursu audiotele? Dziwne, żę osoba zdolna napisać tak świetna książkę pozwala sobie na taka niekonsekwencje. W końcu zatem czytelnik zostaje pozostawiony wobec niej bezbronny, a autor zdaje się zapomniał co wcześniej napisał. A może nie?

    Istotna słabością książki, w istocie krytykującej neoliberalizm i demokrację w jej obecnym, niedorozwiniętym zdaniem autora, wydaniu, jest brak odniesień do Poppera. Nie wiem czy Autor nie zdaje sobie sprawy z jego istnienia i głębokości jego głosu w temacie o którym mowa? Rzecz to niepodobna jako że Sowa jest doktorantem Uniwersytetu Jagiellońskiego. Cuż zatem znaczy zdziwienie nad liberalizmem który ogranicza władzę ludu do wybierania rządzących a odsuwa na dalszy plan realizacje bezpośrednich rządów ludu. Autor odkrywa jakby nowa prawdę, która nigdy zakryta nie była, stąd zdaje się wzmiankowane wyżej pęknięcie. Dowodzi to jak sądzę że Sowa celowo pominął pewne niewygodne dla niego publikacje, chciał bowiem uchodzić za odkrywce i demaskatora spraw które stanowią na przkład treść przedmowy Poppera do polskiego wydania z 1999 „Społeczeństwa Otwartego i jego wrogów”. Czy to nie zabawne? Zdemaskować w 2007 roku treści analizowane przez filozofa, bardzo prominentnego, w roku 1943? W dodatku filozofa będącego głównym ideologiem ruchu który się krytykuje – współczesnego liberalizmu.

    Nie wiem czy Sowa ma rację czy nie, ale nie podoba mi się że nie przedyskutował tej słabości i w gruncie rzeczy wielu innych. Książka jest warta przeczytania, ale z naukowościa do jakiej zdaje sie pretenduję, przynajmniej w sensie popularnym nie ma wiele wspólnego. To niestety manifest. Może dzięki temu jednak tak dobrze się czyta?

 

    Sowa Jan – „Ciesz się, późny wnuku!: Kolonializm, globalizacja i demokracja radykalna”
    Karl R. Popper„Społeczeństwo Otwarte i jego wrogowie”

    Z prawej strony znajduje się cień. Nie wiadomo co niesie. Złowrogo otacza postać siedmioletniej dziewczynki. Ubrana w koszulkę na ramiączkach ze wzorkiem przedstawiającym czereśnie, głowę ma zwróconą w strone plamy światła. Tuż obok widzimy ptaka, można pomysleć że to jaskółka, jednak jest znacznie bardziej barwny, ma niebieski kapturek na łebku i jasne pióra. A może to zimorodek? Czy za chwilę odfrunie? W dziobie trzyma czereśnię. Ręce dziewczynki swobodnie spoczywają na prześcieradle, widzimy tylko fragment powyżej łokcia. Ich ułożenie sugeruje niemoc. Upadła? Trudno nie odnieść wrażenia że za chwilę odwróci sie od światła i spojży w mrok. Jej oczy są zamknięte. Czy wtedy je otworzy? Rozchyli usta i coś w końcu powie, wygląda jakby coś chciała powiedzieć. Myślę, że bardzo chciałaby spojżec w światło ale już nie może. Juz za późno. Jest taka delikatna i zwiewna. Wzbudza czułość. Głowa spoczywa we wgłębienu na prześcieladle, widzimy profil, obok nosa, ust i szyi plama krwi.
    Wygląda jakby nadal żyła.

     Gottfried HelnweinTemptation

    

    Pewien człowiek kochał swoja żonę, a i ona go kochała. Byli razem jednak od dosyć dawna, ich związek był już wieloletni i mieli dziecko. Nadal byli dla siebie atrakcyjni, ale czy nie stało się tak, że zbyt wiele zostało już wyjaśnione? Zbyt wiele ustalone? Zbyt wiele dopowiedziane, albo pozostając niedopowiedziane pozostawało także poza obszarem dyskusji? Kochany: „jesteś dla mnie kimś ważnym czy podobają ci się moje włosy?” „Kochana są piękne!” „Nawet na nie nie spojrzałeś…”
    Tak mniej więcej rozpoczyna się ten film i standardowa interpretacja zakłada że reżyser zabiera nas na podróż po krainie konsumpcjonizmu i rozpasania. Ona wzbudzi w nim zazdrość, on nie będzie mógł jej tego darować. Będzie uciekał przed wizją zdrady dokonanej przez żonę w coraz bardziej ryzykowne sytuacje. Czy cokolwiek co zostało pokazane w tym filmie było udziałem jego bohaterów? A może to tylko opowieść pokazująca co im się śniło po kłótni jaka miała miejsce na lekkim haju po paleniu trawki, by zabić zbyt jednostajny spokój kolejnego wieczoru?
    Jakie są przyczyny dramatycznych zdarzeń? Dlaczego kobieta która kocha swojego męża zadaje mu takie cierpienie? Naigrawa się z jego pewności siebie? A może raczej nie mieści się w swoim życiu, w rolach jakie postawiło przed nią bycie małżonką i matką? Jakieś pęknięcie na naturze ludzkiej sprawia, że nie umie zaakceptować układu dni który zdaje się być już na tak długo ustalony? Nie znosi, mierzi ją to coraz bardziej, zaufania jakie pokłada w niej mąż? Żadne z nich, mężczyzna i kobieta, mając po temu okazję nie popełnia zdrady. Ani na moment nie dochodzi do fizycznego zbliżenia między kimkolwiek z głównych bohaterów a żadną z pozostałych postaci dramatu. Co zatem prowokuje zachowanie kobiety? Chęć zmiany? Podkreślenia swojej roli? Niezależności? Nie należę do Ciebie w całości ani ciałem ani duszą, zdaje się mówić. Ale to zdanie nie jest odpowiedzią na czyjekolwiek uzurpatorstwo: nikt bowiem w takiej pozycji poza nią samą jej nie stawia. Czy jesteś tak pewny siebie by sądzić, że nie mogłabym cie zdradzić? – pyta kobieta – jestem tak pewny Ciebie – odpowiada on. Czasem przychodzi ranić tych których kochamy, z racji własnego poczucia niespełnienia. Ale skąd ono się bierze?
    Urażony mąż czuje się wygnany i jak zbieg krąży od miejsca do miejsca, jak Odyseusz przemierza fantastyczne krainy, staje się częścią wydarzeń nad którymi nie panuje, i które każą mu porzucić własne przekonanie o poczuciu bezpieczeństwa, stałości, własnej sile i wartości.
Na koniec wraca do zony, zajętej własnym wnętrzem, swoja relacją do siebie samej, swymi snami, która zdaje się nie zauważać, że w międzyczasie jej samej, jej małżonkowi i ich dziecku grożono śmiercią. Ona wie: to był tylko sen. realne jest tylko to co zaspokaja jej potrzeby. Ani na moment zona bohatera nie wychodzi poza krąg własnych doznać, odczuć, przemyśleń. Bohater filmu kończy swoje perypetie pomniejszony, w strachu i zależny emocjonalnie od tej silnej kobiety. Im dłużej o tym myślę tym bardziej widzę w tym filmie opowieść o samotności i bezsensownych usiłowaniach poszukiwania bliskości poza własnym związkiem, który okazał się nagle fikcją.
    Nie umiem zrozumieć dlaczego Kubrick trzyma się jedności miejsca, czasu i akcji, wszystkie postacie odgrywają swoja rolę, i strzelba widoczna w pierwszym akcie wypala w ostatnim, a jednak brak pointy. Za skromnie na surrealizm, za bogato na kryminał, za taktownie na pornos, za bajecznie na filozofie. Oniryczne obrazy, powolne wystudiowane sceny, niespieszny tryb narracji.
    Zostaje mi wrażenie że współczesny Odys jak go nam przedstawiono w filmie, nie powraca do Itaki by rozprawić się z uzurpatorami i odebrać należna mu cześć, ale ginie gdzieś w połowie drogi, może ma szczęście, przygarnęła go Calypso. A może nie, może to Kirke? Kim jest jego partnerka?
    W centrum handlowym, pełnym błyskotek, odzyskujemy spokój, będzie dobrze. Trzeba tylko się pieprzyć – mówi zjawiskowa kobieta.

    O tym mowa: „Eyes Wide Shut”

    Jakoś mi się te dwa filmy łączą nie wiedzieć czemu: „The night of the Iguana”.


    TWF in MP znaczy This Week’s Finds in Mathematical Physics. Osoby czytające, lub jak to się mówiło dawniej, subskrybujące jedną z grup dyskusyjnych sci.physics.research, sci.math.research, sci.physics, lub sci.math wiedzą o czym mowa. Autor, John Baez, umieszcza co tydzień na grupie listę artykułów, książek lub tematów które zwróciły jego uwage w ostatnich siedmu dniach. Zawartość ma na ogół formę eseju, adresowanego do specjalistów, pasjonatów, ludzi zainteresowanych tematami trzeba przyznać elitarnymi. Można zatem tu znaleźć poglądowy artykuł o teorii kategorii adresowany do praktykujących fizyków, o krzywych eliptycznych lub geometrii algebraicznej i jej związku z teoria kwantowej grawitacji albo komentarz na temat aktualnej pozycji Pioneer, najodleglejszego od Ziemi wytworu rąk ludzkich. Pisane z pasją, chumorem, gawędziarskim tonem. Po angielsku.
    Dlaczego taki wpis na blogu osoby deklarującej, że będzie pisała o czytaniu? Eseje Baez są świetnie pisane. Pełne są zadziwienia i egzaltacji związanego z zastanawiającymi a nawet zaskakującymi powiązaniami zdawałoby się niezwiązanych tematów. Baez z rzadka jedynie analizuje skomplikowane przypadki: skupia się zwykle na wyjaśnianiu skomplikowanych pojęć na prostych przykładach. Jest uczciwy intelektualnie nie udając że posiada więcej wiedzy niż ma w istocie. Nie przedstawia prawd objawionych a raczej droge dojścia do drobnego nieraz stwierdzenia, które rozpatrzone w szerszym kontekście bywa źródłem autentycznego zaskoczenia.
    Nie każdy zrozumie o czym pisze Baez. Ale to mniej ważna kwestia. Szkoda, że w naszej kulturze nie mamy takich standardów dzielenia się wiedzą, że nawet w naukach ścisłych pisanie czegoś dla innych z potrzeby podzielenia się wiedzą jest rzadkością w Polsce. Nie znam przypadku opisywania wyników swojej pracy z taką pasją jak czyni to Baez i z taka otwartością. I z taką odwagą. Odwagą bo każdy może skomentować, zadać pytanie na które trzeba odpowiedzieć czasem: nie wiem. Baez nie pisze wywiadów, on pisze bloga, który rozsyła pocztą do subskrybentów wymienionych grup dyskusyjnych. I robi to od 93 roku…
    Dlaczego ludzie nie dzielą się wiedzą? Odpowiedź, że wiedza to pieniądz jest truizmem który jest na ogół głoszony przez tych którzy nie maja za wiele do zaoferowania. Powiedzenie że jak nie wiadomo o co chodzi to chodzi o pieniądze jest zwykłą głupota powtarzaną z ust do ust. Osoba która komuś przekazuje wiedzę nic nie traci. Na ogół zyskuje możliwość zobaczenia swej wiedzy w innym kontekście, w innych uwarunkowaniach, wobec innych problemów, z innym podejściem w zamiarze. Sądzę że raczej chodzi o brak odwagi, o brak śmiałości skonfrontowania się z realiami. O zamknięty sposób uprawiania działalności naukowej, co w ostatecznym wyniku musi zaowocować jej zapaścią. A może i o to, że ludzie którzy tak postępują w istocie nie lubią tego co robią. Nie znam ani jednego człowieka który nie lubi opowiadać o swojej pasji. Jeśli jakaś osoba zagadnięta o swoją pracę milknie, najpewniej nie jest zbyt szczęśliwym człowiekiem. Zdaje sie że większość ludzi akceptuje taką sytuację, a nawet nazywa taki stan rzeczy dorosłością.
    Baez jest świetny, warto czytać o matematyce: to cześć kultury taka sama jak poezja czy teatr. I potrafi być nie mniej dramatyczna, porywająca i piękna. Z pewnością jest znacznie rzetelniejsza i głębsza intelektualnie niż niejedna ikona kultury wysokiej. I tylko pozornie jest oderwana od świata.
Na koniec taki cytat:

” Tekst dotyczący polityki lub moralności, artykuł krytyczny, a nawet podręcznik wykładający sztukę publicznego przemawiania, byłby – przy wszystkich rzeczach takich samych – znacznie lepszy, gdyby jego autorem była osoba biegła w geometrii”

Bernard Fontenelle, sekretarz Akademii Francuskiej

(koniec XVIII wieku)

Czy podobna zależność nie dotyczy bycia pasjonatem przedmiotu? Zimny profesjonalizm nie załatwi wszystkiego.

John Baez TWF

    Baricco Alessandro – „Jedwab”. Mała forma, powieść poetycka, klejnocik co błyska. Dobrze skrojone, i na temat. O miłości. Jak juz się przeczyta warto zadać sobie pytanie: co wzrusza?

    Pomyśl: spotykasz miłość swojego życia z dala od domu, w obcym kraju, po podróży pełnej niebezpieczeństw i niewiadomych. Osobę obcą tak, że trudno o większą obcość: nie zamienisz z nią ani słowa. Będą listy. Czy kochasz? Czy kochasz to że ktoś cię kocha? Czy w tej miłości znajdujesz pokrewieństwo dusz i bliskość w nieodgadnionej i niemal archetypicznej formie? Czy tylko pożądanie i pragnienie sprostania wyzwaniu uczucia niszczycielskiego, fatalnego i niebezpiecznego? Banał pięknie podany czy głębia uczuć i tajemnica istnienia?
    Jesteś kochany, a osoba która cię kocha, pragnie twojej miłości. Gotowa byłaby stać się kimś innym gdyby można było stać się kimś innym niż się jest. Pragnęła by sprostać twojej miłości i dać ci szczęście za cenę własnej tożsamości. Żyje dla ciebie i pragnie twojego powrotu z tej dalekiej wyprawy. Jak niewłaściwie! Jak niesłusznie! Jak można!
    To bardzo dobra książka. Warto sobie jednak zadać pytanie: co wzrusza? Jak miłość która pragnie trwać ma się do podobno szalenie niezbędnej życiowo asertywności. Jak można podziwiać uczucie zasadzające sie na oddaniu strącającym człowieka w nieszczęście? Czy nie lepiej szanować siebie znacznie mocniej, skoro jest to warunek prawdziwej miłości do innych? A skoro tak, to czy fikcyjna sytuacja opisana w książce jest fikcyjna także w warstwie psychologicznej? Fikcyjne osoby, fikcyjna sytuacja, opisana pomysłowo ale przecież wręcz zabawnie prosta i prozaiczna; proszę pominąć literaturę i sobie narysować diagram, pomijając wszelkie poetyckie dodatki, celne zabiegi autora zmierzające do tego aby ubarwić sytuację, zagmatwać wątki, i przygotować pointę. Wyjdzie, że to powieść o kryzysie wieku średniego w rodzinie niezbyt dojrzałych emocjonalnie ludzi których związek jest od samego początku na granicy rozpadu. A gdzie zachodzi taka sytuacja pojawia sie ta trzecia osoba, to konieczność, jak uczy psychologia, i mamy prosty skok w bok. Co tu romantycznego? Wystarczyłaby prosta terapia grupowa. Byle w odpowiednim czasie. Albo rozwód, przecież trwanie w toksycznym związku jest dowodem patologicznych tendencji.
    Coś tracimy szukając każdego dnia wyjść z sytuacji za pomocą porad z Cosmo… I to coś jest istotą tej książki i reakcji jakie wywołuje.

    Na temat roli Cosmo właśnie w tym kontekście taki cytat:

„Dostrzegam – mówię – że świat stał się tak mechaniczny, że mam obawy, że wkrótce zaczniemy się go wstydzić; świat w dużej skali będzie jak zegar w małej, który jest bardzo regularny i zależy tylko od dokładnego rozmieszczenia kilku części wprowadzających go w ruch. Ale niech mi Pani powie, Madame, czyż nie miała Pani wcześniej wznioślejszej idei wszechświata?”

Bernard Fontenelle, sekretarz Akademii Francuskiej (1686)

   „Jedwab” Baricco Alessandro w Biblionetce http://biblionetka.pl/ks.asp?id=11487

Enter your email address to follow this blog and receive notifications of new posts by email.

Dołącz do 256 obserwujących.

Reklamy
%d blogerów lubi to: