You are currently browsing the category archive for the ‘metamatematyka’ category.

ModusPoens

W poprzednim wpisie przedstawiłem dosyć oczywisty fakt dotyczący zasady indukcji na grafie o jednej składowej spójnej. W obecnym, przejdziemy do nieco innej tematyki, wszakże wpis poprzedni nie był całkiem oderwany od dzisiejszego tematu. Mam nadzieję posługiwać się nim w przyszłości, był wiec to rodzaj przygotowania artyleryjskiego przed bitwą. Amunicji użyliśmy niewiele, a kaliber nie był zbyt wielki. Zobaczymy co dalej.

Na początek kilka słów o motywacji. W poprzednich kilku wpisach drapałem po wierzchu temat reprezentacji dowodów matematycznych jako grafu i próbowałem zdefiniować dla takich struktur grupy homologii tak by cechy dowodu ( konkretnie sprzeczność) miały jakieś homologiczne odzwierciedlenie. Niestety analizując temat dokładniej, dochodzę do wniosku ( o czym napiszę w kolejnych wpisach) że homologia nie wypali. Jest tak dlatego, ze struktura „triangulacji dowodów” jak ją nazwałem – nie jest struktura simplicjalną. Znalazłem błąd w swoim rozumowaniu, są kontrprzykłady, i trzeba stwierdzić, że tego typu podejście wygląda na skazane na daleko idące kłopoty ( co nie znaczy że homologia i logika nie dadzą się pożenić. Jestem przekonany że istnieje tu głęboki związek, np. przekonuje mnie do tego koincydencja faktu że istnieje tylko jeden rodzaj nieorientowalności rozmaitości i jeden rodzaj sprzeczności logicznej. )

Czas więc na kolejne podejście, bo sam pomysł „triangulacji dowodu” wydaje się nadal żywotny, kopie i kto wie, może coś sie z tego urodzi.

Zamierzamy pracować z dowodem matematycznym. Poniżej przedstawię ścisłą definicję tego co będę rozumiał pod tym pojęciem. Będzie ona oczywiście całkowicie klasyczna, zostanie jednak wypowiedziana w pewnej specyficznej terminologii. Aby ją wprowadzić musimy określić pewien obraz czym jest zbiór wyrażeń których ozywamy podczas dowodzenia twierdzenia matematycznego. Po pierwsze dowody powstają w ramach sformalizowanego rozumowania. Każdy dowód powstaje w ramach określonej teorii ta zaś posiada zwykle aksjomaty, operuje pewnego rodzaju obiektami pierwotnymi ( „rzeczy” o których mówi teoria, a których cechy definiują aksjomaty) oraz intensywnie czerpie z logiki określonego rodzaju ( np. logiki pierwszego rzędu FOL). Aksjomaty są relacjami które nakładamy na obiekty będące przedmiotem naszego rozumowania dowodowego, i zwykle w dowodzie nie używamy ich wszystkich, a tylko pewien podzbiór. Sytuacja ta ma prozaiczny powód – większość użytecznych teorii matematycznych posiada nieskończenie wiele aksjomatów. Jako przykład może posłużyć aksjomat indukcji, a używając prawidłowej terminologii: schemat aksjomatów indukcji. Jest to wyrażenie ( lub zdanie, wszakże w zapisie stosowanym zwykle, jest to zdanie wypowiedziane w logice wyższego rzędu niż FOL) które stwierdza, że „dla każdego zdania {T(n)} dotyczącego liczby naturalnej {n}, jeśli prawdziwe jest zdanie {T(0)} oraz {T(n) \Rightarrow T(n+1)} to prawdziwe jest {T(n)}„. Proszę zwrócić uwagę, ze schemat ów – rozwija sie na nieskończenie wiele aksjomatów, po jednym dla każdego zdania T o ile posiada ono cechy wymienione w owym schemacie aksjomatu. Oznacza to, że teoria korzystająca z owego schematu aksjomatów, w istocie posiada przeliczalną ilość aksjomatów. Rzecz jest znana i omówiona w każdym podręczniku podstaw matematyki.

W jaki sposób z schematu aksjomatów dostajemy konkretny aksjomat? Jakie jeszcze mogą lub są schematy aksjomatów?

Sprawa zwykle nie jest szczególnie drążona, wszakże stosowanie schematów aksjomatów jest powszechne. Dlaczego? W języku FOL nie jesteśmy w stanie wypowiedzieć treści kwantyfikowanej po zdaniach. Teoria matematyczna posługująca się językiem logiki pierwszego rzędu zawiera wyłącznie kwantyfikacje po obiektach, to jest po „rzeczach”. Np. w ramach teorii mnogości wypowiadamy zdania o zbiorach i elementach, ale nie o „twierdzeniach na temat zbiorów”. Tymczasem użycie tak prostej reguły jak

\displaystyle \phi \Rightarrow (\psi \Rightarrow \phi )

wymaga byśmy za {\phi} i {\psi} mogli podstawić dowolne zdania. Zwykle zapisuje się ów schemat aksjomatów systemu Hilberta, za pomocą zmiennych {\phi} i {\psi}, rozumiejąc przez to, że mamy do czynienia z nieskończenie wieloma aksjomatami, a {\phi} i {\psi} reprezentują każde możliwe zdanie. Stąd zapis takiego schematu zawiera zwykle kwantyfikator ogólny „dla każdego zdania {\phi} teorii T” {\phi \Rightarrow(\psi \Rightarrow \phi )} i można by wyobrażać sobie że mamy tu w istocie nieskończoną listę aksjomatów, po jednym dla każdego możliwego podstawienia zmiennych. W realnym rozumowaniu istnieje potrzeba użycia stosownej reguły dedukcji, pozwalającej zrealizować owo podstawienie, zasygnalizować je czytelnikowi dowodu. Zwykle ma ono postać zapisu „{\phi = q}” gdzie {q} jest juz zdaniem teorii, dotyczącym „rzeczy” i zapisanym w języku FOL.Jednak wyrażenie „{\phi=q}” nie jest prawidłowym wyrażeniem języka FOL. jest sztuczką syntaktyczną, zapisem mnemotechnicznym, odwołaniem sie do „indeksu w bazie danych aksjomatów” umyślnie oznaczonej „{\phi \Rightarrow(\psi \Rightarrow \phi )}” po to by z owej listy, wyfiltrować stosowny aksjomat dotyczący zdania „{q}„. Regułą taka, opisująca „podstawienie, oznaczmy ją chwilowo {P}, mogłaby mieć postać

\displaystyle P("\phi=q", "\phi\Rightarrow\phi") = " q \Rightarrow(\psi \Rightarrow q )"

Odczytalibyśmy ją jako „w schemacie „{\phi \Rightarrow(\psi \Rightarrow \phi )}” podstaw za {\phi} zdanie „{q}„. Zauważmy że sam symbol równości „{=}” użyty w nawiasach, nie oznacza że owo {\phi} staje się równe „{q}” na stałe a tylko mamy na myśli pewną konkretną realizację, selekcję, ze zbioru opisanego schematem aksjomatów. W terminologii informatycznej powiedzielibyśmy że zasięg leksykalny owego znaku „=” ograniczony jest wyłącznie do zapisu powyżej. Co więcej. wynik takiej operacji podstawienia nie jest zdaniem, a zaledwie kolejnym schematem który może zawierać, i zawiera w naszym przykładzie inne zmienne! Dopiero sekwencja podstawień eliminująca ze schematu wszystkie występujące w nim zmienne, daje w wyniku określone jednoznacznie przez użyte podstawienia, zdanie używanego w ramach teorii języka. Oczywiście jest wiele symbolik opisujących powyższą operację podstawienia. Wydaje mi sie jednak że zaproponowana jest w miarę wygodna i przejrzysta. Co więcej – wyrażenie „{\phi = q}” – choć nie jest zdaniem teorii ( a nawet nie jest zdaniem), będzie wprost występowało na liście wyrażeń używanych w dowodzie, podobnie jak schematy aksjomatów. Ale o tym poniżej.

Kolejnym obiektem który jest używany w procesie dowodowym sa tautologie. Przywołuje sie je czasami wprost – stwierdzając, że pewne zdanie jest prawdziwe niezależnie od prawdziwości występujących w nim zdań, a czasami jako schemat aksjomatów, z zmienną, jak opisano powyżej ( bo też i tautologie są nieprzebranym zbiorem „potencjalnych aksjomatów” zaś ich użycie w taki czy inny sposób jest zwykle kwestią estetyki i optymalizacji środków dowodowych). Ponieważ u podstaw prawdziwości tautologii leży sama logika, a w jej ramach najprostsza metoda sprawdzania prawdziwości – tabela wartościowania prawdy i fałszu, stwierdza sie zwykle że tautologie logiczne są konsekwencją zbioru pustego. Czyli że ich prawdziwość nie wymaga czynienia żadnych specyficznych założeń. Można by rzec, że posiadamy pewną regułę dedukcyjną T, od słowa tautologia, która pozwala nam wprowadzić do dowodu dowolne wyrażenie będące tautologią, a to poprzez wskazanie, ze jest owo wyrażenie konsekwencją zbioru pustego. Zapis wyglądałby następująco:

\displaystyle T(\emptyset ,t) \Rightarrow t

gdzie {\emptyset} to zbiór pusty zaś {t} to tautologia.

Widzimy że w takim zapisie, ze zbioru tautologii wybraliśmy zdanie {t}. Zapis ten jest w pewnym sensie patologiczny, gdyż reguła dedukcyjna dotycząca tautologii {T}, zawiera po obu stronach wyrażenia to samo zdanie {t}. Dlatego zapis ten, choć formalnie prawdziwy i zgodny z resztą terminologii ( o czym poniżej) nie będzie używany dalej zaś osiągniemy to kosztem dodania do naszego zapisu wszystkich tautologii jako dodatkowego, wyróżnionego zbioru tautologii o tym samym statusie co schematy aksjomatów. Nie musi być to od razu zbiór wszystkich tautologii używanej logiki. Wystarczy by zbiór ten zawierał te tautologie które są użyte w dowodzie który będziemy analizować.

Rozważyliśmy zatem trzy zbiory – zbiór aksjomatów A, zbiór tautologii T, oraz zbiór „indeksów”, wyrażeń postaci „{\phi=q}” oraz symbol {\emptyset}, które będę dalej nazywał zbiorem filtrów. Tutaj drobny komentarz, sygnalizujący rzecz nad którą sie zastanawiam, jednak nie umiem jej rozstrzygnąć. Zgodnie z teorią mnogości, zbiór pusty jest częścią każdego zbioru, tym samym należy też do zbiorów {T} i {A}. Być może rozsądniej byłoby rozważyć specjalny symbol na określenie tego rodzaju elementu którego konsekwencją sa tautologie, ale który sam nie jest konsekwencją żadnego rozumowania. Warto dodatkowo pamiętać, że w sensie ogólnym konsekwencją sprzecznego zbioru zdań ( np. teorii o sprzecznych aksjomatach) jest dowolne zdanie, a więc zbiór pełny zdań, a nie zbiór pusty.

Zacznijmy od formalnego przedstawienia opisanego powyżej budulca.

Mamy dany:

 

  • zbiór schematów aksjomatów {A},
  • zbiór tautologii {T},
  • zbiór filtrów {F}, który zawiera wyrażenia postaci „zmienna = zdanie”, oraz zbiór pusty {\emptyset}
  • zbiór L poprawnych syntaktycznie wyrażeń teorii

 

Definicja Zbioru Selektorów: Zbiór selektorów {S} to zbiór zawierający aksjomaty, tautologie i filtry.

Zbiór {Z = A \cup T} nazwiemy zbiorem zdań pierwotnych teorii. Element należący do zbioru selektorów {S} nazwiemy selektorem.

Chcielibyśmy nad zbiorem selektorów i zdań logiki bazowej zbudować mechanizmy umożliwiające rozumowanie dedukcyjne. Należy w tym celu zdefiniować reguły dedukcji, które w niezawodny sposób prowadzą od aksjomatów do poprawnych syntaktycznie wniosków. Pojawia się tu jednak pewien problem. Reguła dedukcji {R}, to funkcja, o 2 argumentach, która odwzorowuje zbiór selektorów {S} i zbiór zdań pierwotnych {Z} teorii, w zbiór poprawnych wyrażeń pewnego rodzaju. Nie są to jednak zdania, a jak widzieliśmy wyżej, schematy zdań, lub listy zdań, w zależności od przyjętego podejścia. Mamy zatem następującą definicję:

Reguły dedukcji: Regułą dedukcji jest to funkcja 2 argumentowa taka że, jeśli {x \in L}, {y \in S} to istnieje takie ( jednoznacznie wyznaczone) {z \in L} że

\displaystyle R(x,y) = z

Wyrażenie {x} nazywamy przesłanką, wyrażenie {y} nazwiemy selektorem, wyrażenie {z} to wniosek.

Ponieważ „nowe” zdania w teorii powstają wyłącznie w wyniku realizacji pewnej reguły dedukcji, a w powyższym wyrażeniu symbol „{=}” oznacza zwykłą równość, możemy każde wystąpienie zdania z zastąpić równoważnym wyrażeniem {R(x,y)}. Tym samym pojecie „zbiór zdań logiki bazowej” staje się czysto mnemotechnicznym wybiegiem, zaś każde zdanie teorii to po prostu odpowiednio zagnieżdżony ciąg reguł dedukcyjnych operujących na selektorach ( w pierwszym argumencie) oraz aksjomatach i tautologiach ( w drugim). Tym samym możemy stwierdzić, że zbiór zdań {L} jest zbyt duży dla naszych rozważań, zaś w tym co nastąpi będziemy rozważali wyłącznie wyniki iteracji reguł dedukcji na zbiorze {A \cup T}.

Zamiarem moim jest zbudowanie graficznej reprezentacji takich struktur, co ma też i taką zaletę, że choć wypowiadam wszystkie zdania poniżej w języku aksjomatów, dowodów itp. te same narzędzia powinny nadać sie do analiz systemów matematycznych gdzie zachodzi iteracja funkcji 2 argumentowych.

Podkreślmy w tym miejscu, że istotne cechy reguł dedukcyjnych:

 

  • reguły dedukcyjne są operacjami czysto syntaktycznymi
  • reguła dedukcyjna jest funkcją.
  • Zachodzą relacje jednoznaczności:
  • ( {R(a,b) =c} i {R(a,d) = c ) \Rightarrow b=d}
  • ( {R(a,b) =c} i {R(d,b) = c ) \Rightarrow a=d}
  • ( {R(a,b) =c} i {R(a,b) = d ) \Rightarrow c =d}
  • wynik działania reguły dedukcyjnej jest prawidłowym zdaniem języka L. Wolę jednak określić tą cechę w innych sposób. Zachodzi cecha przeniesienia typu zmiennej. Reguła dedukcyjna „przy użyciu selektora” przenosi typ z przesłanki na wniosek. Własność ta jest spełniona dla wszelkich reguł postaci modus ponens ( modus tollens itp.), zachodzi też dla wielu reguł rachunku sekwentów.

 

Uwaga – ostatnia cecha to pewnego rodzaju nadużycie. Niestety ściśle rzecz biorąc nie jest spełniona dla reguł polegających na podstawianiu czy też „filtrowaniu” jak wolałbym ten proces nazwać. W takim bowiem przypadku jako pierwszy argument występuje schemat aksjomatów, czyli lista zdań, zaś na etapie wyeliminowania wszystkich zmiennych, ostatni selektor wybiera z niej jedno zdanie, które zostaje zwrócone jako wniosek. Nie jest wykluczone, że jest to ślad czegoś ważniejszego, np. że reguły dedukcyjne powinny być odwzorowaniami zwracającymi nie tyle zdania, co całe listy zdań, zaś teoria powinna posiadać kanoniczne odwzorowanie pomiędzy jednoelementową listą zawierającą zdanie bez zmiennych a zbiorem zdań ( czyli pomiędzy jednoelementową listą i jej elementem) . Definicja taka dodałaby do teorii miłej symetrii, i miałaby sens, bowiem w wypadku podstawiania za jedną zmienną w schemacie w którym występuje ich kilka, wynik podstawienia nadal jest schematem a nie zdaniem.

W ogólności w teorii może występować więcej niż jedna reguła dedukcji, co będziemy sygnalizować przez ich ponumerowanie. Tym samym będziemy mówili o k-tej regule dedukcji {R_k}. Typowym przykładem może być tu system Hilberta gdzie mamy dwie reguły dedukcji: modus ponens i regułę podstawiania za zmienną. Istnieją systemy rachunków zdań gdzie reguł jest więcej ( lub mniej). W dalszych rozważaniach modus ponens ( zapisywana jako „mp”) i reguła podstawiania będą traktowane przeze mnie jako modelowy przykład takich reguł.

Zdefiniujmy co mamy na myśli operując pojeciem dowodu:

Definicja Dowodu: Dowód P twierdzenia t, to ciąg zdań {a_1,a_2 \cdots a_N =t}, o tej własności że dla każdego zdania {a_i} zachodzi jeden z elementów alternatywy:

  • {a_i \in A}, {a_i} jest schematem aksjomatu
  • {a_i \in T}, {a_i} jest tautologią,
  • {a_i \in F}, {a_i} jest elementem zbioru filtrów
  • ogólniej moglibyśmy napisać że {a_i \in S} – jest selektorem lub
  • istnieje liczba {p} oraz {j,k<i} takie że {a_i = R_p(a_j,a_k)} gdzie {R_p} to {p}-ta reguła dedukcji.
  • {a_N = t} nie jest filtrem.

wyrażenie t jest zdaniem ( bo nie jest filtrem) i nazywamy je tezą dowodu.

W ramach takiej definicji w dowodzie zostają zapisane jawnie wszystkie wyrażenia użyte w krokach dowodowych ( a nie tylko te które są zdaniami). Przez długość N dowodu P, rozumiemy ilość selektorów, czyli po prostu wyrażeń, które sie na niego składają.

Z powyższej definicji wynika, że dla każdego dowodu P, mamy ciąg wyrażeń będący jego reprezentacją. Każdemu wyrażeniu {a_i} w dowodzie P przyporządkujmy liczbę naturalną { \#(P,a_i)} – numer miejsca na którym wyrażenie to występuje w dowodzie P. Każdy dowód to skończony ciąg wyrażeń, więc { \#(P,a_i)} jest dobrze zdefiniowane i przybiera wartości od 1 ( dla pierwszego wyrażenia dowodu) aż po { \#(P,t) =N} gdzie {t} to teza dowodu zaś {N} to jego długość.

Dla wygody, kiedy dowód jest ustalony, opuścimy symbol P w powyższym zapisie, czyli będziemy używać wyrażeń postaci { \#(a_i) = n}. Jeśli zdanie q nie występuje w dowodzie, napiszemy \#(q) = 0 . Czasami pewnie opuścimy nawiasy pisząc sam symbol \#a_i =n

W dalszym ciągu będę używał słowa „zdania” w znaczeniu – schematy aksjomatów, tautologie lub zdania właściwe logiki bazowej teorii. Tym samym nie będziemy pedantycznie analizować zagadnień sygnalizowanych w pt. 4 cech reguł dedukcji. Proszę pamiętać jednak że zdanie może oznaczać zarówno poprawne twierdzenie teorii jak i cały schemat zdań ( a więc wyrażenie zawierające zmienne).

Dowód składa się z wyrażeń, ale nowe zdania pojawiają sie w dowodzie wyłącznie jako wynik działania reguł dedukcyjnych. Jeśli w wyniku działania {R_k(q_i,q_j) = q_s} to wykonaniu reguły dedukcyjnej {R_k} przypiszemy taki sam numer jak zdaniu {q_s}. Mamy zatem {\#(P, R_k(q_i,q_j)=q_s) = \#(P,q_s)} i definicja numeru miejsca w dowodzie {\#} zostaje rozszerzona na realizacje ( wystąpienia) reguł dedukcyjnych. O ile w wypadku wyrażeń numeracja jest ciągła, od 1 do N o tyle numeracja wystąpień reguł dedukcyjnych może zawierać luki. Prawdziwe jest jednak poniższe, oczywiste stwierdzenie:

Stwierdzenie: dla danego dowodu P, numeracja użycia reguł dedukcyjnych jest cięgiem ściśle monotonicznym.

Jest to wniosek z faktu, że numeracja zdań w dowodzie jest ściśle monotoniczna, zaś reguły dedukcyjne otrzymują te same numery co zdania, z pominięciem wyrażeń ze zbioru filtrów oraz bezpośredniego użycia aksjomatów i tautologii.

Wydaje sie że wyposażeni w takie narzędzia możemy wypisać podstawowe pojecie jakim będziemy sie zajmować w dalszym ciągu wpisów:

Definicja Triangulacji dowodu:

Triangulacja dowodu P to odwzorowanie {\mathcal{F}} dowodu P w graf skierowany G. Każde wystąpienie reguły dedukcyjnej {R(p,q)=s} jest odwzorowane na trójkąt skierowany {(pqs) = (pq) \cup (qs) \cup (ps)}

W odwzorowaniu tym każdemu zdaniu dowodu {a_i} przypisany jest wierzchołek grafu G. Różnym zdaniom przypisujemy rożne wierzchołki, tym samym zdaniom przypisujemy te same wierzchołki.

Będziemy zajmowali sie własnościami grafów które sa obrazami dowodów w odwzorowaniu {\mathcal{F}}. W następnym wpisie podam przykłady triangulacji, oraz zastanowimy się na jakie sposoby łączą się trójkąty w owej triangulacji.

 

Reklamy

MathTextOntology-pasek

Rozważmy abstrakcyjny graf G. Nieformalnie abstrakcyjny graf matematyczny to obiekt złożony ze zbioru wierzchołków oraz zbioru krawędzi łączących wierzchołki. Wierzchołki połączone wspólną krawędzią nazwiemy sąsiadującymi.

W zastosowaniach zwykle wierzchołki posiadają jakieś konkretne cechy ( i zwykle mają etykietki ), zaś fakt łączenia wierzchołków krawędzią, zwykle ma jakąś interpretację. W ramach rozlicznych interpretacji, możemy mówić o posiadaniu przez wierzchołek określonej własności X. X będziemy tu traktowali jako predykat o dziedzinie w zbiorze wierzchołków, a wartościach w zbiorze {T,F} reprezentującym prawdę i fałsz. Tym samym jeśli wybierzemy pewien wierzchołek v grafu G, to możemy zapytać jaka jest wartość X(v), oraz powiemy że v ma własność X jeśli X(v) = T lub krócej będziemy pisać że X(v).

Przy takiej dosyć prostej terminologii, możemy sformułować w miarę oczywistą zasadę indukcji na grafie.

    Zasada indukcji na grafie.

Dany jest graf nieskierowany G, z jedna składową spójną. Załóżmy że zachodzą następujące własności:

  1. dla każdego wierzchołka v grafu G z tego że X(v) wynika, że X zachodzi dla każdego wierzchołka sąsiadującego z v.
  2. dla pewnego wierzchołka a zachodzi własność X

    Teza: X jest prawdziwe dla wszystkich wierzchołków grafu G.

Dowód ( niewprost):

Załóżmy że spełnione jest założenie (2), to znaczy istnieje wierzchołek a dla którego zachodzi X, oraz spełniona jest zasada (1), że z faktu że X zachodzi dla pewnego wierzchołka wynika ze zachodzi dla wszystkich połączonych z nim wierzchołków.  Mimo to twierdzimy że twierdzenie nie jest prawdziwe, to znaczy że  istnieje pewien wierzchołek d dla którego X nie jest prawdziwe.

Załóżmy że istnieje pewien wierzchołek s sąsiadujący z d dla którego X(s). Wówczas z (1) wynika że d ma cechę X podczas gdy w poprzednik kroku założyliśmy że d nie posiada cechy X. Sprzeczność. Wynika z tego że żaden wierzchołek sąsiadujący z d nie może posiadać cechy X.

Wierzchołki sąsiadujące z nimi także itp, itd.

Oznaczmy przez U zbiór wierzchołków które nie posiadają cechy X. Zbiór U jest niepusty bo zawiera co najmniej wierzchołek d, a także  wierzchołki sąsiadujące z d, wierzchołki sąsiadujące z tymi wierzchołkami itd. Innymi słowy zbiór U to składowa spójna grafu zawierająca d.

Jednak z założenia graf jest grafem spójnym, posiada więc jedna składową spójna.

W takim razie A należy do U.

Ale dla A zachodzi X.
Sprzeczność.
Co prawda zasada wydaje się w miarę oczywista, ale nie znalazłem jej w google ;-)

Po drugie, oczywista to ona pewnie jest dla grafów skończonych, ale z dowodu wydaje się wynikać, ze dla nieskończonych także, co więcej, prosty dowód nie narzuca jakichś ograniczeń na moce zbiorów wierzchołków…

Pinky: Móżdżku, co będziemy robić dzisiaj wieczorem?

Mózg: Dokładnie to samo, zawsze, Pinky, zdobędziemy władze nad światem!

woda.jpg

W poprzednim wpisie opisałem sposób wyliczania odczepionej grupy homologii dla prostego ( ale już nie trywialnego) przykładu dowodu sprzecznego. Przypomnijmy że dla grup kompleksów łańcuchowych tego obiektu geometrycznego tworzymy ciąg grup homologii {H_n} za pomocą schematu pomocniczego:

\displaystyle 0 \overset{\partial_3}{\longrightarrow} C_{2} \overset{\partial_2}{\longrightarrow} C_{1} \overset{\partial_1}{\longrightarrow} C_{0} \overset{\partial_0 = 0 }{\longrightarrow} 0

n-ta grupa homologii to grupa ilorazowa:

\displaystyle H_n = ker(\partial_n)/img(\partial_{n+1})

W przypadku grupy odczepionej {H_a} postąpiliśmy nieco inaczej. Zdefiniowałem mianowicie dodatkowe mapowanie {\partial_a} który przyporządkowywał wierzchołkom grafu obiekty geometryczne ( dla wierzchołka {a} taki obiekt geometryczny oznaczałem{|a|} ) wraz z informacja o ich wewnętrznej strukturze. W naszym przypadku, a stale mówimy o obiektach geometrycznych będących odwzorowaniem obiektów logicznych – ciagów dowodowych w systemie formalnym z regułą modus ponens -mapowanie {\partial_a} miało następującą własność:

\displaystyle \partial_a(\neg q) = - \partial_a(q)

gdzie {q} w poyższym wyrażeniu jest zdaniem logicznym. W następnym kroku definiowałem odszczepioną grupę homologii {H_a} jako:

\displaystyle H_n = ker(\partial_a)/img(\partial_{1})

Przyglądnijmy się bliżej mapowaniu {\partial_a}.

Obecny wpis zacznijmy może od tego że przypomnę miejsce odwzorowania {\partial_a} w diagramie grup kompleksów łańcuchowych:

HomologiaOdczepiona

Widzimy wyraźnie że zdefiniowałem nowy kompleks łańcuchowy {C_a} który jest dziedziną odwzorowania {\partial_a}. Zbiór ten jest obrazem grupy cykli krawędziowych {C_1} pod działaniem odwzorowania {\partial_1} Jego elementami nie są jednak wierzchołki, a obiekty posiadające wewnętrzną strukturę. Z jednej strony bowiem spełniają one zależności wynikające z faktu bycia brzegiem grupy cykli krawędziowych {C_1}, czyli w wypadku tych obiektów, ich struktura niesie dodatkową informację o fakcie że są one spięte w pętle simpleksów reprezentujących reguły modus ponens. I faktycznie, jak czytelnik może pamięta, pisałem że: { img (\partial_1) = <b-a,c-b,c-a> } oraz, że dodatkowo {x+y-z=0} gdzie {x,y,z} reprezentowały wierzchołki złożone w krawędzie simpleksu reprezentującego {MP(a,b)=c}. Innymi słowy działanie mapowania {\partial_1} jest identyczne jak w wypadku normalnej definicji grup homologii. Operator {\partial_a} działa na grupie cykli wierzchołków. Formalnie rzecz biorąc, grupa ta to {C_0} i na diagramie grupa taka znajduje sie w „ciągu głównym” grup łańcuchów. W naszym jednak przypadku mapowanie {\partial_a} działa na tym zbiorze wyciągając z niego dodatkową informację, stąd właściwym jest odróżnienie go od zwykłego zbioru {C_0} który zawiera przecież tylko wierzchołki. Co więcej, obrazem {\partial_a} w działaniu na zbiór {C_a} nie jest bynajmniej 0, pomimo iż tak właśnie narysowałem na diagramie powyżej. Czytelnik wybaczy to oszustwo, w istocie w miejscu 0 powinna znajdować sie grupa ( powiedzmy) {C_{0a}} która zawiera punkty geometryczne wierzchołków uzupełnione o informację o ich strukturze wewnętrznej. Nie jest to jednak grupa łańcuchowa równoważna {C_0} gdyż w obiekcie tym nie leży żaden obraz {\partial_1}. Jest tak, gdyż działanie operatora {\partial_a} skutecznie usuwa z tej struktury informacje o spięciu w krawędzie. Przyznam że spędziłem jakiś czas usiłując „włożyć” grupę {C_a} pomiędzy {C_1} i {C_0} ale nie widzę za bardzo takiej możliwości ( chyba ze kosztem znacznego skomplikowania). Prawdziwy diagram grup łańcuchowych powinien wiec wyglądać tak:

HomologiaOdczepionaPoprawnie

Przyglądnijmy sie teraz działaniu odwzorowania {\partial_a}. Odwzorowanie to przypisuje elementowi grupy łańcuchów 0-wymiarowych, element w grupie abelowej {C_0a}. W grupie tej różnym elementom {C_a} przypisywane są różne elementy, poza sytuacją kiedy elementy {C_a} związane sa relacją:

\displaystyle p = \neg q

dla pewnych zdań {p} i {q}. Widać wyraźnie ze tego typu odwzorowanie uwzględnia dodatkową informację o negacji zdań logicznych.

Być może czytelnikowi umknęła jeszcze jedna subtelność, którą chciałbym tu wyciągnąć na światło dzienne. Mianowicie w pierwszym dowodzie mieliśmy następująca sytuację: w grafie złożonym z zdań {a="a",b="a\rightarrow a",c="a"} zdania {a} i {c} zostały potraktowane jako różne. Właściwie to jest to błąd. Zdania te to w istocie jedno i to samo zdanie, którego obrazem w grupie {C_a} jest jeden element. Gdyby było inaczej, w grupie tej istniałby nietrywialny cykl (postaci {a-b} gdzie a i b byłyby dwoma obrazami tego samego zdania {q} ) i grupa homologiczna odczepiona dla dowodu niesprzecznego byłaby nietrywialna, czego wolelibyśmy uniknąć. Takie „sklejenie” zdań w obrazie {\partial_a} pozwala uniknąć nietrywialnych pętli występujących z powodu powtarzania sie zdań w dowodzie. Jednocześnie zdania zanegowane przekształcane są na rożne ( przeciwne!) elementy grupy {C_a} co pozwala nam nietrywialnie reprezentować sprzeczność dowodu.

Możemy podsumować. Odwzorowanie {\partial_a} działa w następujący sposób:

  • jego dziedziną jest zbiór  {C_a} wierzchołków grafu reprezentującego dowód
  • jego obrazem jest grupa przemienna {C_{0a}} łańcuchów 0-wymiarowych z uwzględnieniem struktury wewnętrznej zdań z poprzedniego punktu
  • na obecnym etapie uwzględniamy wyłącznie negację. Obrazami zdań {p} i {\neg p} są elementy wzajemnie odwrotne grupy {C_a} tak, że {\partial_{a} (p) + \partial_{a} (\neg p) =0}.
  • obrazami wierzchołków {p}  i {q = "p"}  w których mamy zdania syntaktycznie tożsamych jest ten sam element {|p|}  grupy  {C_a}

Grupa homologii jest {H_a} zdefiniowana jako grupa ilorazowa jądra przekształcenia {\partial_a} przez obraz {\partial_1} operatora brzegów jednowymiarowych na zbiorze krawędzi {C_1}. Właściwie to całe zagadnienie tym samym sprowadza sie do zdefiniowania {H_a} i do pojęcia grup homologii odnosi sie w zapewne dosyć odległy, a a na pewno nie jakiś szczególnie nietrywialny sposób. Z drugiej strony starałem sie złapań jakieś intuicje związane z pojęciem sprzeczności, i chyba całkiem nieźle sie to udało, biorąc pod uwagę, że w ramach przedstawionych rozważań jest w miarę oczywiste że skończone zbiory sprzeczne będą miały nietrywialne ( i skończone!) grupy {H_a} zaś zbiory niesprzeczne – grupy trywialne.

Dlaczego jest to interesujący fakt sam w sobie? Otóż od dłuższego czasu zastanawiało mnie, dlaczego sprzeczności logiczne, mają tak prostą postać syntaktyczną. Proszę porównać najprostszy ze znanych paradoksów w teorii zbiorów, paradoks Russella z aksjomatyką tej teorii ( na przykład w wersji naiwnej, albo ZFC). W każdym wypadku paradoks jest prostszy niż sama teoria! A paradoks kłamcy? Czy nie jest tak, że „każdy głupi go zrozumie”? A rozwiązanie? ło, doktoraty można robić… Tarski całą teorię modeli na tym zbudował. Mamy zatem paradoksy, a ich reprezentantami wydają się być niewielkie, a czasami nawet znaczeniowo, koncepcyjnie proste, zbiory zdań. Tymczasem okazuje sie że przy zastosowaniu odczepionej grupy topologii, sprzeczność ma odpowiednik w prostej postaci takiej grupy! Kontekst geometryczny nie jest tu całkiem od rzeczy. Widać że relatywnie proste rozumowanie ( dowód sprzeczny jaki podałem jako przykład odpowiada paradoksowi kłamcy) ma nietrywialna reprezentację geometryczną, w postaci simpleksu w którym grupa odczepiona jest nietrywialna. Dlaczego zatem paradoksy są tak proste? Chciałoby się odwrócić całe rozumowanie: „Bo struktury geometryczne proste są same w sobie”. Czy istnieją „skomplikowane paradoksu”? Oczywiście istnieją takie które wymagają wielu zdań by je zapisać, i zapewne odwzorują się w skomplikowaną strukturę geometryczną. Ale z tego co napisałem/zdefiniowałem wydaje się że nadal nie będziemy mieli w takich paradoksach niczego istotnie innego niż w tych prostych. Zapewne będą im odpowiadały bardziej złożone grupy odczepione, ale należy przypuszczać że nadal będą to sumy proste grup {Z_2}( po jednej grupie dla każdej pary zdań sprzecznych, lub wy wypadku paradoksów typu „koło kłamców” grupy cykliczne rozmiaru n, co będziemy zapewne analizować w jednym z przyszłych wpisów) a ta występuje już w bardzo prostym przypadku rozumowania sprzecznego. I to jest coś co wydaje mi się ciekawe…

A co dalej? Kolejne działania powinny polegać na analizie struktur coraz bardziej złożonych, a na koniec nieskończonych zbiorów zdań związanych relacją konsekwencji syntaktycznej modus ponens.I zapewne będę o tym jeszcze pisał.

Wymieńmy możliwe uogólnienia:

  • moglibyśmy analizować bardziej złożoną strukturę wewnętrzną zdań w wierzchołkach. W miejsce operatora {\partial_a} można by wprowadzić inny, który byłby czuły na występowanie alternatywy, koniunkcji lub jeszcze bardziej złożonych struktur. Pewne przekształcenia syntaktyczne mają całkiem ładną strukturę wewnętrzną, powiedzmy prawa de Morgana odznaczają sie sporą dozą (syntaktycznej) symetrii, co pozwalałoby odwzorowywać wierzchołki w grupy o niebanalnej strukturze. Marzy mi sie coś w rodzaju teorii Galois dla logiki, budowanej w języku algebry homologicznej…
  • można sobie wyobrazić cały ciąg grup odczepionych, który gubiłby informację o geometrii triangulacji dowodu ( właściwie nie jest ona jak na razie szczególnie ciekawa…) ale wyciągałby na światło dzienne, informacje o wewnętrznej strukturze zdań. Być może to jest najbardziej obiecujące uogólnienie/droga rozwoju tego pomysłu?
  • od strony teorii homologii, pomysł wydaje sie być dosyć oryginalny ( ale nie wiem czy interesujący). Operacje odczepienia można bowiem wykonać nie tylko dla wierzchołków! Możliwe jest przecież obdarzenie krawędzi simpleksów, ich elementów 2-wymiarowych i w ogólności n-wymiarowych, w jakąś dodatkową strukturę. Na każdym etapie n, można „coś odczepić” definiując odpowiednie operatory {\partial^n_a} analizujące strukturę symetrii takich obiektów w relacji do ich „umieszczenia” w całym kompleksie, która jest zadana przez klasyczny operator {\partial_n}. To czego nie widać ( i co nieco rozczarowuje) to fakt, iż nie bardzo mam pomysł jak powiązać ( i czy w ogóle istnieje takie powiązanie!) grupy odczepione na różnym poziomie n. A priori, w strukturze abstrakcyjnej można oczywiście budować tu jakieś abstrakcyjne obiekty, mnie wszakże interesowałoby podanie jakiegoś modelu takiego zjawiska. Modelu – czyli struktury która by niosła ciekawą informację w grupach odczepionych a jednocześnie pozwalała je definiować dla kilku poziomów struktur….

I to na tyle dziś.

Pinky: Móżdżku, co będziemy robić dzisiaj wieczorem?

Mózg: Dokładnie to samo, zawsze, Pinky: zdobędziemy władze nad światem!

W poprzednim wpisie pokazałem jak wyliczać grupy homologii na (trywialnym) przykładzie pojedynczego simpleksu. W tym wpisie pokaże jak, modyfikując mechanizmy teorii homologii, uwzględnić kwestie logiczne którym poświęciłem już kilka wpisów. Aby uniknąć odwoływania się do innych wpisów, poniżej krótkie przypomnienie zagadnień logicznych o jakich będzie mowa.

Mamy zadany system formalny, czyli zbiór zdań logicznych złożony z zdań wyróżnionych, zwanych aksjomatami,oraz pewnego zestawu reguł przekształcania napisów zwanych regułami inferencji, dedukcji lub wnioskowania. Reguły wnioskowania akceptują pewną formę zdań ( w sensie czysto graficznym, syntaktycznym, jako napisy) i pozwalają na podstawie takich argumentów, uznać że do systemu wolno nam dopisać kolejne, określone w swojej formie syntaktycznej przez „mechanikę reguły wnioskowania”, zdanie. Modelowym przykładem reguły wnioskowania jest znana z poprzednich wpisów reguła modus ponens. Symbolicznie będę tą regułę zapisywał w formie {MP(P,Q) =S} co jest oczywiście równoważne zapisowi {MP(a \rightarrow b,a) = b}. Regułę tą rozumiemy czysto syntaktycznie, jako napis.

Dowodem zdania {S} w systemie logicznym zawierającym aksjomaty i regułę dedukcyjną modus ponens jest uporządkowany ciąg zdań {a_{0},a_{1},a_{2} \cdots ,a_{n}} gdzie {a_{n} = S}, zaś zdania numerowane od {1, \cdots n-1} to aksjomaty, tautologie lub wcześniej dowiedzione zdania. Ponieważ wcześniej dowiedzione twierdzenia mają dowody ( a więc ciągi zdań…), możemy przyjąć ( zastępując każde zdanie w powyższym ciągu jego dowodem) że zdania {a_{1}, \cdots a_{(n-1)}} to aksjomaty lub tautologie. Dla każdego podciągu uporządkowanego {a_{0} \cdots , a_{k},a_{(k+1)}} istnieje reguła wnioskowania ( inferencji, dedukcji), która pozwala wyprowadzić zdanie {a_{(k+1)}} z zdań {a_{0},\cdots , a_{k}}. Jest to klasyczna definicja dowodu, czytelnik spotkał sie z nią zapewne wielokrotnie. W tym co nastąpi będę wiele razy pisał o graficznym przedstawieniu dowodu, o dowodach sprzecznych itp. W każdym takim wypadku pisząc dowód mam na myśli ciąg uporządkowany zdań jak powyżej, i jest całkowicie obojętne jakie twierdzenie zostaje odwiedzone. W istocie dyskusja dotyczy więc pewnego skończonego zbioru konsekwencji syntaktycznych zadanego zbioru aksjomatów. I tak należy rozumieć obiekt który poniżej nazywam dowodem.

Załóżmy że mamy zdania {a,b,c} o budowie syntaktycznej wiążącej te zdania reguła modus poens ( proszę zwrócić uwagę na kolejność!) {MP(b,a) =c}. Zdaniom tym przyporządkujemy graf, w postaci jak na rysunku poniżej:

MOdusPoens-general

Prosiłbym by czytelnik zwrócił uwagę, że graf jest skierowany, porządek ten zaś wynika z uporządkowania zdań w regule modus ponens. Przyjęliśmy mianowicie konwencję w której pierwsze zdanie to implikacja, drugie to przesłanka, a trzecie to następnik implikacji. Na grafie zaś reprezentujemy to odwracając kolejność implikacji i przesłanki. W poprzednim wpisie, dla takiego ogólnego obiektu wyliczyliśmy, w celach edukacyjnych, grupy homologii.

Tak jak poprzednio przy tak zdefiniowanej reprezentacji graficznej reguły modus ponens możemy kolejne użycia jej w dowodzie przypisać kolejnym trójkątom a w wyniku otrzymamy graf złożony z uporządkowanych trójkątów posklejanych wierzchołkami w miejscach gdzie powtarzają sie w dowodzie przypisane im zdania. Graf ten w swoich wierzchołkach zawiera zdania, zaś jego krawędzie to związek pomiędzy wierzchołkami polegający na tym że wystąpiły one w jednej regule modus ponens. W tym miejscu następuje pewien poważny przeskok koncepcyjny. Dotychczas rozważaliśmy grafy, teraz dołączmy do naszego postępowania także to co znajduje sie pomiędzy nimi. Będziemy uważać, rysunek powyżej przedstawia nie tyle graf z wierzchołkami i krawędziami co element powierzchni – czyli 2 wymiarowy simpleks i konsekwentnie, graf reprezentujący dowód stanie się „zlepkiem” takich simpleksów, czyli kompleksem simplicjalnym.

Podkreślmy że w zbiorze tym simpleks występuje tylko tam, gdzie 3 zdania będące jego wierzchołkami są użyte w pewnej regule modus ponens. Nie ma żadnej możliwości uzupełnienia krawędzi ( np. do postaci simpleksów 3 wymiarowych czyli czworościanów posiadających pewną objętość) tam gdzie reguła modus ponens nie występuje.

W tak otrzymanej strukturze geometrycznej, będziemy rozważać grupy homologii. Dodamy jednak do owej struktury dodatkowa informację o negacji pełnych zdań ( a więc o zdaniach postaci {A= \neg p} dla pewnego zdania {p}. Jakiekolwiek występowanie negacji w innej formie syntaktycznej nie będzie nas interesować, toteż jej użycie np. w koniunkcji, wewnątrz nawiasów itp jest dla nas całkowicie pomijalne. Przypomnijmy dodatkowo że dowód jest sprzeczny, kiedy na liście jego zdań występuje zarówno zdanie {A} jak i {\neg A}.

Formalizacje odwzorowania zbioru dowodu w grupy homologii rozpoczniemy od pokazania obliczeń na przykładzie najprostszych dowodów. Pierwszy z nich ma postać:

\displaystyle a_{0}. a \rightarrow a

\displaystyle a_{1}. a

\displaystyle a_{2}. MP(a_{0},a_{1} ) = a

Mamy zatem do czynienia z prostym simpleksem ( trójkątem skierowanym ) jak na rysunku poniżej:

AiA

gdzie zdanie b jest równe zdaniu a_0 z dowodu powyżej.  W odróżnieniu jednak od obliczeń które pokazaliśmy w poprzednim wpisie, tym razem w trójkącie tym dwa wierzchołki, a i c, są identyczne w tym sensie że zawierają to samo zdanie a.

Moglibyśmy teraz wyliczać ciąg grup kompleksów łańcuchowych tego obiektu, wg. znanych i nie bardzo złożonych zasad rachunków algebry homologii. Rozpoczęlibyśmy zatem od zbudowania ciągu grup abelowych kompleksów łańcuchowych, w następującej postaci:

\displaystyle 0 \overset{\partial_3}{\longrightarrow} C_{2} \overset{\partial_2}{\longrightarrow} C_{1} \overset{\partial_1}{\longrightarrow} C_{0} \overset{\partial_0 = 0 }{\longrightarrow} 0

Postąpimy jednak nieco inaczej. Obliczenia jak powyższe dają taki sam wynik, jak dla trywialnego przykładu pokazanego wcześniej i nie będziemy tutaj powtarzać tych obliczeń. Natomiast wprowadzimy pewien dodatkowy kompleks łańcuchowy {C_a} oraz odpowiadające mu odwzorowanie {\partial_a}. Grupa {C_a} będzie zawierała wierzchołki wraz z informacją o strukturze związanej z negacją zdań logicznych, zaś odpowiadający jej operator brzegu będzie działała na grupie łańcuchów 0-wymiarowych, a jego działanie będzie zależeć od wewnętrznej struktury związanej z wierzchołkami. Ciąg grup kompleksów łańcuchowych będzie zatem wyglądał tak:

HomologiaOdczepiona

Jak widać „rozdwoiliśmy końcówkę” ciągu grup łańcuchowych, możemy ją nazwać „odczepem” i mówić o „odczepionej” grupie homologii {H_a}. Aby określić działanie operatora {\partial_a} opiszemy jego działanie na generatorach grupy wierzchołków {C_0} zaś jego działanie na elementach pełnej grupy, które są, przypomnijmy, formalnymi sumami elementów zbioru wierzchołków, otrzymamy przez standardowe liniowe rozszerzenie.

Operator {\partial_a} definiujemy za pomocą następującej relacji:

\displaystyle \partial_a ( u) = |u| = u = - \partial_a( \neg u)

I to wszystko.

Zauważmy że działanie operatora {\partial_a} pozostawia działanie innych operatorów brzegu całkowicie niezmienionym. Nie wpływa zatem na wyliczanie żadnych grup homologii, poza swoją własną, oznaczmy ja {H_a}.

Przypatrzmy sę teraz jak wygląda {H_a}. mamy zależność:

\displaystyle H_a = ker( \partial_e ) / img (\partial_1)

Obrazem operatora brzegów {\partial_1} na zbiorze krawędzi, jest oczywiście grupa złożona ze wszystkich wierzchołków, w naszym wypadku {<a,b>}. Czym jest zbiór {ker(\partial_a)}? Jeśli zbiór wierzchołków zawiera wyłącznie różne wierzchołki, to nie istnieje pomiędzy nimi żadna relacja związana z operatorem {\partial_a}. Jest tak, gdyż operator ten przekształca każdy wierzchołek „z orientacją” na tożsamy mu wierzchołek „geometryczny”. Załóżmy że mamy zbiór N takich „wierzchołków z orientacją”. Nawet jeśli niektóre z „wierzchołków z orientacją” zawierają negacje, jeśli są to parami różne zdania, wynik nadal zawiera N wierzchołków, niektóre z nich co najwyżej mają znak minus.

Tak właśnie wygląda sytuacja dla simpleksu przedstawionego na rysunku powyżej. Wyliczmy bowiem jak zostaną przekształcone jego wierzchołki pod wpływem operatora {img (\partial_a)}:

\displaystyle \partial_a(a) = |a| = a

\displaystyle \partial_a(b) = |b| = b

\displaystyle \partial_a(c) = |c| = c

Jak widać zaczęlismy od 3 wierzchołków i na trzech wierzchołkach kończymy. W efekcie grupa homologii {H_a}jest równa:

\displaystyle H_a = 0 / <a,b,c> = 0

A co z pozostałymi grupami homologii? W przykładzie jaki tu rozważamy występuje istotna różnica w stosunku do przykładu trywialnego. A mianowicie zdanie {a = c}, czyli rozważany przez nas trójkąt ma sklejone dwa wierzchołki. Mamy zatem w trójkącie krawędzie {x,y,z} jednak krawędź {z} zaczyna i kończy sie w tym samym punkcie:

\displaystyle \partial_1(x) = b-a

\displaystyle \partial_1(y) = a-b

\displaystyle \partial_1(z) = a-a = 0

Oznacza to iż

\displaystyle Z_1 = ker(\partial_1) = <z,x+y>

Pierwszy generator jadra wynika bezpośrednio z rachunku {\partial(z) =0} zaś ostać drugiego generatora wynika oczywiście z faktu, że w sklejonym trójkącie, dwie pozostałe krawędzie, {x,y} tworzą samodzielny cykl. Tymczasem obraz brzegu trójkąta, to oczywiście suma jego krawędzi tak jak poprzednio:

\displaystyle B_1 = img(\partial_2) = <x+y-z>

Tym samym grupa homologii {H_1} jest równa:

\displaystyle H_1 = ker(\partial_1) / img(\partial_2) = <z,x+y> / <x+y-z> = Z

Grupa {H_0} która mierzy ilość spójnych składowych, jest izomorficzna z {Z} ( mamy tylko jedną składową i jest taka sama jak w poprzednim wypadku ( i dotyczy to wszystkich pozostałych grup).

Podsumujmy – sklejenie wierzchołka {a=c} doprowadziło do zmian w głównym ciągu grup homologii. Sklejenie to spowodowało powstanie dodatkowych jednowymiarowych pętli, zmieniając grupę {H_1}. Jednocześnie grupa odczepiona, jak ją nazwaliśmy, dla teorii niesprzecznej jest grupą trywialną równą grupie złożonej z jednego, tożsamościowego równego 0 elementu addytywnego.

Sytuacja wygląda zupełnie inaczej gdy rozważmy następujący dowód ( sprzeczny):

\displaystyle a_{0}. a \rightarrow \neg a

\displaystyle a_{1}. a

\displaystyle a_{2}. MP(a_{0},a_{1} ) = \neg a

Co odpowiada grafowi jak na rysunku poniżej

AinotA

Podkreślmy że nie ma w tym wypadku mowy o sklejeniu wierzchołków ( na wcześniejszych rysunkach oznaczanych {a} i {c}) gdyż tkwią w nich inne zdania, mianowicie zdania {a} i {\neg a} odpowiednio. Tu obecny pomysł istotnie rożni sie od opisów z kilku poprzednich wpisów. Wynika z tego że mamy do czynienia geometrycznie z przypadkiem trywialnym, odpowiadającym w sensie grup homologii dokładnie obliczeniom z pierwszego przykładu, opisanym w poprzednim wpisie. Zobaczmy jednak jak wygląda odczepiona grupa homologii {H_a}. Sprawdźmy jakie jest działanie operatora {\partial_a} na zbiorze wierzchołków:

\displaystyle \partial(a) = |a| =a

\displaystyle \partial(b) = |b| = b

\displaystyle \partial(c) = - \partial(a) = -|a|

Widzimy wyraźnie, że w zbiorze tym istnieje relacja która sprawia, że pewna suma generatorów {<a,b,c>} jest równa zeru, mianowicie {a+c = 0}. Czyli {Z_a=ker(\partial_a ) = <a+c>}. Natomiast obraz {B_0= img(\partial_1)} czyli zbiór brzegów, ma standardowe generatory {<b-a,c-b,c-a>} wraz z relacją, że wierzchołki te są spięte w cykl brzegu trójkąta. Grupa ilorazowa:

\displaystyle Z_a / B_0 = <a+c> / <b-a,c-b> = Z / 2Z = \{ 0,1 \}

Wyjaśnijmy. W mianowniku mamy tylko 2 a nie trzy generatory, gdyż relacja „spinająca trójkąt” pozwala wyeliminować jeden z generatorów związanych z wierzchołkami. Mamy zatem grupę ilorazową grup o jednym generatorze wolnym ( w liczniku) i 2 generatorach ( w mianowniku). Grupa w liczniku jest izomorficzna z zbiorem liczb naturalnych, zaś w mianowniku z suma prosta 2 takich grup. Iloraz jest grupą skończoną, złożoną z 2 elementów, 0,1, izomorficzną do grupy Z mod 2. Innymi słowy jest to grupa cykliczna, skończona o 2 elementach.

Mamy zatem następująca sytuację – dla przypadku teorii sprzecznej, odczepiona grupa homologii jest nietrywialną grupą skończoną, zaś pozostałe grupy homologii pozostają bez zmian.

Powyżej mieliśmy do czynienia z sytuacją wystąpienia jednej pary zdań sprzecznych. Wystąpienie większej liczby takich par, zwiększa wymiary grupy odczepionej – zyska ona nowe generatory. Jednocześnie będziemy oczekiwać, że nadal pozostanie ona grupą skończoną ( co wynika z faktu że ilość generatorów w jądrze operatora brzegu wynika z ilości par zdań sprzecznych, zaś w mianowniku z ilości cykli związanych z krawędziami. Analizowany graf ma w pewnym sensie minimalną liczbę krawędzi, i w bardziej skomplikowanych grafach liczba cykli złożonych z krawędzi będzie tylko większa )

I to by było na tyle w temacie grup homologii. Podane przykłady łatwo uogólniają sie na bardziej złożone teorie logiczne/kompleksy łańcuchów. W dalszych wpisach z tego cyklu będziemy z pewnością analizowali rozmaite konsekwencje przytoczonych definicji. W tym miejscu chciałbym sie jednak zastanowić nad ogólną sytuacją i możliwymi uogólnieniami.

Po pierwsze, pokazany ciąg homologii z doczepioną homologią odczepioną wygląda nieco sztucznie, ma jednak tą zaletę że w zerowym stopniu modyfikuje pozostałe grupy homologii.

Po drugie operator {\partial_a} został zdefiniowany w sposób uwzględniający własności negacji – jej zachowanie – na przykład zasada wyłączonego środka – przypomina oczywiście działanie grupy alternującej. Stąd propozycja definicji {\partial_a} podana powyżej. Nic jednak nie stoi na przeszkodzie, by zamiast obiektów logicznych rozpatrywać ogólne sympleksy, zaś zamiast zdań i ich negacji w każdym wierzchołku umieszczać obiekt z jakąś bogatą strykturą wewnętrzną, reprezentowaną przez grupę ( skończoną lub nie?). Odczepiona grupa homologii mierzy „zgodność” wierzchołków która, w odróżnieniu od własności mierzonych przez pozostałe grupy homologii, nie jest związana z własnościami geometrycznymi a jednocześnie nie jest lokalna. Wyobraźmy sobie sieć spinów, gdzie każdy z wierzchołków zawiera element grupy spinorowej. Grupa odczepiona może wówczas mierzyć własności związane z nierozróżnialnością cząstek umieszczonych w takim „krysztale spinowym”. Nie spotkałem sie z taką konstrukcją nigdzie, a nie wydaje sie być ona całkowicie pozbawiona zabawnych cech, czy może nawet praktycznych właściwości ( opis kryształu z pełną delokalizacją cząstek w określonej liczbie rozróżnialnych stanów spinowych). Widać, że uogólnienie w tym kierunku jest zarówno możliwe jak i niebanalne!

Po trzecie, dla przypadku logiki, konstrukcja homologii odczepionej, przedstawiona powyżej, wydaje się być dosyć przejrzysta. Kolejnym krokiem ( obok analizy homologicznych konsekwencji przedstawionych pomysłów) jest analiza teorii kohomologii. Kohomologia to teoria zajmująca sie odwzorowaniami liniowymi nad grupami homologii, albo alternatywnie, teoria analizująca związki odwrotne w stosunku do homologii. W wypadku homologii mieliśmy grypy łańcuchowe {C_k,C_a} analizowaliśmy które z cykli sa identyczne z dokładnością do brzegów obiektów o jeden większego wymiaru. W wypadku kohomologii sprawdzamy brzegami jakich obszarów większego wymiaru, są zadane cykle. nie posiadam obecnie wiedzy by napisać na ten temat cokolwiek sensownego, dlatego chętnie sformułuję przypuszczenie, że w kontekście logiki oznacza to analizowanie następującego zagadnienia. Brzegiem jakiego kompleksu symplicjalnego ( będącego geometrycznym modelem jakiegoś logicznego systemu formalnego, w tym kontekście – zwykle będzie to kompleks nieskończony! ) może być dowód sprzeczny?

ModusPoens2

Pinky: Móżdżku, co będziemy robić dzisiaj wieczorem?

Mózg: Dokładnie to samo, zawsze, Pinky, zdobędziemy władze nad światem!

Mam wrażenie że udało mi się wreszcie sformalizować intuicje związane z odwzorowaniem zbioru zdań dowodu w systemie formalnym ( ogólniej – zbioru zdań konsekwencji syntaktycznych zadanego zbioru zdań) w zbiór grup homologii. Ostateczna wersja dosyć istotnie odbiega od pomysłów poprzednich, jest bardziej elegancka jak sądzę, pozwala na ciekawe uogólnienia ( także w sensie teorii homologii) i ma pewien potencjał rozwojowy ( teorie kohomologii, o których na razie zbyt mało wiem by rozważać coś więcej). Formalizacja którą opisze poniżej, odbywa się w pewien konserwatywny, czy minimalny sposób, i polega na rozszerzeniu ciągu grup kompleksów łańcuchowych o dodatkowy element związany z odwzorowaniem wierzchołków w grupę alternującą. Aby jednak uniknąć opisywania abstrakcyjnego nonsensu, całość zostanie przedstawiona na przykładach obliczeń, które dosyć łatwo uogólnić.

Tradycją tego bloga, i moją ambicją, było dotychczas aby tekstu tu prezentowane mogły być czytane przez osoby z minimalnym przygotowaniem, toteż starałem się podawać cały potrzebny materiał, tak przystępnie jak tylko byłem w stanie. I tym razem postąpimy podobnie, zaczniemy od wprowadzenia pojęcia homologii, a w kolejnym wpisie odniesiemy ją do logiki.

Przypomnijmy że cała idea sprowadza się do tego że jeśli mamy zdania {a,b,c} o budowie syntaktycznej wiążącej te zdania reguła modus ponens ( proszę zwrócić uwagę na kolejność!) {MP(b,a) =c}, to zdaniom tym przyporządkujemy graf, w postaci jak na rysunku poniżej:

MOdusPoens-general

I dla takiego prostego obiektu będziemy starali sie, w celu edukacyjnym i by przygotować się do bardziej ambitnych wyzwań,  skonstruować grupy homologii.

Po pierwsze wyjaśnijmy co jest ta rysunku! Na rysunku powyżej, mamy obiekt płaski, trójkąt {X}. Jest to element powierzchni obdarzony orientacją zadaną przez kierunek obiegu jego krawędzi. Krawędzie te oznaczymy {x,y,z}. Krawędzie te łączą wierzchołki, na rysunku oznaczone {a,b,c}. Wypisane obiekty mają następujące wymiary: trójkąt jest obiektem 2 wymiarowym, krawędzie skierowane sa 1-dno wymiarowe, zaś wierzchołki to obiekty 0-wymiarowe. Brak na rysunku obiektów o wymiarach większych niż 2 i mniejszych niż 0 oczywiście. Obiekty te nie są bynajmniej niezależne, ale połączone sa w dosyć szczególny sposób. Na przykład każda krawędź ma dwa wierzchołki, zaś fakt iż złożenie krawędzie jest tak szczególne że tworzą pętlę – brzeg trójkąta – wynika że wierzchołek będący końcem jednej z krawędzi jest początkiem następnej i sytuacja ta powtarza sie tworząc cykl wierzchołków, w którym każdy z nich pojawia sie dwa razy – raz jako początek a raz jako koniec pewnej krawędzi.

Wyjściem dla budowania teorii homologii, która stara sie uchwycić właśnie takie wzajemne relacje pomiędzy elementami składowymi obiektu geometrycznego ( ogólniej topologicznego) jest zdefiniowanie dla każdego wymiaru części składowych, formalnego odwzorowania w grupę przemienną. Na przykład rozważmy sumę krawędzi {x+y}. Sumę ta będziemy traktować czysto formalnie, niemniej warto spostrzec, że chcąc być konsekwentny musimy uznać iż spełniona jest własność: {x+y=z} lub inaczej: {x+y-z=0} gdyż położenie wzajemne krawędzi jest takie ze tworzą one pętlę. Ponieważ suma jest czysto formalna, nic nie zabrania nam rozważać obiektów bardziej wymyślnych, na przykład {3x-4y+5z}. Konsekwentne postępowanie wymaga jednak by przyjąć że {mx+my-mz = m(x+y-z) =0} bo taka kombinacja zawsze oznacza ( moglibyśmy starać się to zinterpretować) m-krotne obejście pętli brzegu trójkąta. Całkiem identyczne obiekty, sumy formalne, możemy rozważać w wypadku wierzchołków czy wnętrza trójkąta i innych, więcej wymiarowych obiektów gdyby takowe występowały.

Grupę abelową obiektów o wymiarze {n} oznaczamy {C_n} i nazywamy n-tą grupą łańcuchową kompleksu X ( który w naszym przypadku jest szczególnie prosty, jest bowiem pojedynczym sympleksem). I tak grupa krawędzi, a więc 1-sza grupa łańcuchowa naszego trójkąta, jest generowana przez 3 elementy {<x,y,z>}. Nie jest to jednak grupa wolna ( a więc nie wszystkie elementy te są niezależne!). Z faktu istnienia relacji {x+y-z = 0} wynika że istnieje pomiędzy generatorami grupy związek, zaś sama grupa ma co najwyżej 2 niezależne elementy ( i tu już mamy pełną dowolność, mogą być to dowolne dwa boki trójkąta, np. {x,y} lub ich dowolna kombinacja liniowa). Jak widać niektóre związki pomiędzy elementami grupy łańcuchowej {C_1} ( krawędzi) w naszym przypadku były interesujące, czyli grupy takie mają czasami wewnętrzną strukturę! Istnieją także związki pomiędzy grupami o różnych {n}!

Weźmy grupę jaka jest związana z wnętrzem ( powierzchnią) trójkąta. Mamy tylko jeden trójkąt, cała grupa {C_2} jest zatem dosyć uboga, zawiera bowiem tylko jeden element {<X>}. Wszystko co możemy z takim elementem nawyczyniać, sprowadza sie do dodawania ( bądź odejmowania) go pewną liczbę razy, np. elementami grupy sa wyrażenia: {X+X, 34X, -7X} Brak jest też jakichkolwiek związków ograniczających ten element, jest więc to grupa wolna abelowa o jednym elemencie, czyli grupa izomorficzna ze zbiorem liczb całkowitych {Z}. Jednak brzeg tej figury, czyli zbiór jej skierowanych krawędzi, jak widzieliśmy ma niebanalną strukturę! Zdefiniujmy operator, oznaczany symbolem {\partial_2}, który działając na 2 wymiarowy trójkąt {X} przyporządkuje mu element grupy łańcuchowej wymiaru 1-mniejszej, a więc element z {C_1}, który będzie reprezentował brzeg figury {X}. Oczywiście wyliczenie wygląda następująco:

\displaystyle \partial_2 (X) = x+y-z

Całkiem podobnie możemy postąpić w wypadku krawędzi. Krawędzie są skierowane, zdefiniujmy więc podobne odwzorowanie do obiektów o wymiarze 1- mniej, w tym wypadku do grupy wierzchołków, które owo skierowanie będzie brało pod uwagę. Naturalne jest przyjęcie że operator {\partial_1} który każdej krawędzi przyporządkuje element grupy łańcuchowej wierzchołków będzie działał w sposób następujący:

\displaystyle \partial_1 (x) = b-a

\displaystyle \partial_1(y) = c-b

\displaystyle \partial_1(z) = c-a

Aby sprawdzić że się nie pomyliliśmy, policzmy ile wynosi {\partial_1 (x+y-z)} Mamy:

\displaystyle \partial_1 (x+y -z ) = \partial_1(x) + \partial_1 (y) - \partial_1 (z) = b-a +c -b -c +a = 0

co zgadza sie z obserwacją, że krawędzie trójkąta domykają się w pętlę.

A co z brzegiem wierzchołka? Czy możliwe jest zdefiniowanie operacji {\partial_0} ? Ile wynosi na przykład {\partial_0 (a)} ? Arbitralnie przyjmiemy że wynik to 0 w każdym wypadku.

Mamy zatem następująca sytuację.

\displaystyle 0 \overset{\partial_3}{\longrightarrow} C_{2} \overset{\partial_2}{\longrightarrow} C_{1} \overset{\partial_1}{\longrightarrow} C_{0} \overset{\partial_0 = 0 }{\longrightarrow} 0

Zera na początku i na końcu pokazanego ciągu grup i wzajemnych odwzorowań oznaczają że w trójkącie nie ma obiektów o wymiarze mniejszym niż 0 i większym niż 2.

Widzieliśmy powyżej, że operator {\partial_1(x+y-z) = 0}. Zbiór elementów grupy {C_1} których obrazem w grupie {C_0} przy przekształceniu {\partial_1} jest 0, określa się nazwą jądra ( kernel) operatora. Oczywiście suma czy różnica takich elementów także daje zero, co oznacza, jest to zresztą ogólna właściwość algebraiczna, że elementy jądra tworzą podgrupę. Zbiór ten w naszym przypadku złożony jest z jednego elementu, reprezentującego kompleks łańcuchowy odpowiadający brzegowi trójkąta. Symbolicznie zapisujemy to w następujący sposób:

\displaystyle Z_1 = ker (\partial_1 )

Zwróćmy uwagę, ze brzeg ów, jest z kolei obrazem całego trójkąta (X) przy odwzorowaniu {\partial_2} (M proszę zwrócić uwagę na indeks przy literze {B}):

\displaystyle B_1 = img (\partial_2)

I tym razem mamy do czynienia z podgrupą, gdyż suma formalna brzegów figur, jest brzegiem figury będącej ich sumą. Operator brzegu przypisuje figurom płaskim ich brzegi, a brzegi takie są zawsze łańcuchami cyklicznymi, czyli zamkniętymi pętlami. Nic więc dziwnego, że elementy grupy {B_1} leżą w grupie {Z_1} ( bo każdy cykl w przekształceniu {\partial_1} jest mapowany na 0). W naszym wypadku grupy te są wręcz równe, wynika to jednak z faktu że rozważamy wyjątkowo prosty przykład. Gdyby zamiast trójkąta rozważać figurę która zawiera „dziurę” w swoim wnętrzu, istniałyby także cykle krawędzi, które nie są brzegami żadnej powierzchni ( nie mają żadnego „wypełnienia” ). W takim wypadku grupa {B_1} byłaby podgrupą właściwą, zaś grupa {Z_1} cykli krawędziowych zawiewałaby obok elementów będących brzegami rozmaitych pól płaskich na jakie dzielilibyśmy taką figurę, także elementy będące cyklami pomimo iż nie otaczają „niczego”. Pierwszą grupą homologii {H_1} nazywamy grupę ilorazową grup {Z_1/ B_1}. Analogicznie n-tą grupą homologii jest grupa ilorazowa grup {Z_n/ B_n}:

\displaystyle H_n = Z_n/ B_n = ker(\partial_{n} ) / img(\partial_{(n+1)})

.

Wyliczmy zatem grupy homologii dla naszych grup łańcuchowych {C_k}. Dla k=2 jądro jest puste, gdyż żadna kombinacja 2-wymiarowych elementów ( a mamy tylko jeden: X ), nie sumuje sie do zamkniętej powłoki. Oczywiście nie ma także żadnych 3-wymiarowych obiektów… Zatem:

\displaystyle H_2 = ker( \partial_2 ) / img (\partial_3 ) = 0 / 0 =0

widać zatem że wszystkie grupy homologii {H_n} dla {n \geq 2} są równe 0.

\displaystyle H_1 = ker (\partial_1 ) / img (\partial_2 ) = <x+y-z> / <x+y-z> = 0

Zwróćmy tu uwagę, że w powyższym równaniu 0 po prawej stronie oznacza trywialną grupę złożona z jednego elementu – identyczności w grupie abelowej – a więc 0.

Teraz wyliczmy grupę homologii dla n=0. Ponieważ arbitralnie przyjęliśmy, że {\partial_0 = 0} to jądrem tego odwzorowania jest cała grupa wierzchołków, a wiec jądro to trójelementowa grupa wolna o 3 generatorach {<a,b,c>}. Przypomnijmy że powyżej wyliczyliśmy jakie sa elementy produkowane z krawędzi przez odwzorowanie {\partial_1} ( na przykład {\partial_{1}(x) = b-a} ). Obraz ten produkuje 3 elementy, które jednak, jak już wspominaliśmy nie są niezależne, bowiem wierzchołki owe spinają się w pętle brzegu trójkąta. Mieliśmy relację {x+y-z = 0} ( którą formalnie powinniśmy zapisać za pomocą symboli wierzchołków {a,b,c}, gdyż rozumiemy ja jako relację w zbiorze {C_0} a nie {C_1} którego elementami są {x,y,z}). Tym samym w zbiorze {<b-a,c-b,c-a>} tylko dwa elementy są niezależne, a trzeci można wyeliminować. Zatem grupa brzegów {img( \partial_1)} jest grupą wolną o generatorach {<b-a,c-b>} zaś trzeci element {c-a} jest od nich zależny ( łatwo sprawdzić że jest ich sumą!). Mamy:

\displaystyle H_0 = ker( \partial_0) / img (\partial_1) = <a,b,c>/<b-a,b-c>

Zauważmy że możliwe jest przejście od {<a,b,c>} do {<a,b-a,c-b>} bo polega ono na zamianie generatorów {a,b,c} przez ich liniowe i niezależne kombinacje co jest operacją dopuszczalną ( gdyż nie zmienia struktury grupy, stare generatory są liniowymi kombinacjami nowych i nie zmieniliśmy liczby generatorów niezależnych). Mamy zatem:

\displaystyle H_0= <a,b-a,c-b>/<b-a,c-b> = <a> = Z

Wynik nie jest zaskakujący, zwłaszcza że grupa {H_0} ma geometryczną interpretację: mierzy ilość składowych spójnych figury, w naszym wypadku trójkąta, który oczywiście ma tylko jedną składową spójną. Pozostałe grupy homologii, w naszym wypadku trywialne, także dają się geometrycznie interpretować. Mierzą one mianowicie ilość dziur o stosownych wymiarach. I tak np. grupa {H_1} mierzy ilość „pustych oczek” czyli dziur w figurze otoczonych jednowymiarowymi łańcuchami cyklicznymi które nie są wypełnione ( nie są brzegiem żadnej figury płaskiej pełnej). Z kolei {H_2} mierzy ilość cykli 2-wymiarowych które otaczają 2 wymiarowe otwory ( coś jak wnętrze walca, rurki, lunety), które nie są brzegiem żadnej figury posiadającej objętość ( wyplenionej).

Zauważmy że branie grupy ilorazowej we wzorze na grupę homologii właśnie taki ma cel – eliminuje z pełnej grupy cykli na n-tym poziomie te cykle, które są brzegami figur wymiaru n+1. Stąd homologia mierzy wzajemne położenia (homo-gogie) składowych o rożnych wymiarach w figurze geometrycznej. Teoria homologii została zapoczątkowana przez Poincare w trakcie jego prac nad topologia, obecnie zaś została znacząco uogólniona i rozszczepiona na wiele dziedzin o wspólnych korzeniach, od czysto geometrycznej klasycznej teorii homologii, przez rozmaite uogólnienia jak teoria (ko)homologii Cecha, aż do obiektów całkowicie abstrakcyjnych jak homologia kombinatoryczna i algebra homologiczna. Cechą wspólną wszystkich tych teorii pozostaje występowanie ciągu grup jak na diagramie grup kompleksów łańcuchowych wraz z przekształceniem \partial o stosownie ( do czego wrócimy) zdefiniowanych, nieraz aksjomatycznie, własnościach. Jeśli kogoś ciekawią zagadnienia topologii algebraicznej której teoria homologii jest twardym rdzeniem, polecam ten ciąg wykładów autorstwa N.J.Wildbergera. Forma wykładów jest bardzo elementarna, zaś przykłady obliczane w sposób bardzo szczegółowy, można skoczyć od razu w okolice wykładu 30-tego gdzie znajdują się zagadnienia związane z teorią homologii właśnie.

To już wszystko w tym wpisie. Przygotowałem sobie aparat za pomocą którego w kolejnym będę w stanie opisać jak zmodyfikować ciąg grup łańcuchowych {C_k} tak by zawierał informacje o zdaniach logicznych które w naszym wypadku będą leżały w wierzchołkach figury. Zapraszam.

Pinky: Móżdżku, co będziemy robić dzisiaj wieczorem?

Mózg: Dokładnie to samo, zawsze, Pinky: zdobędziemy władze nad światem!

ModusPoens2

W poprzednich odcinkach opisałem pomysł odwzorowania zbioru zdań dowodu w systemie formalnym, na strukturę topologiczną typu zbioru simplicjalnego ( czyli zbioru złożonego z „porządnie” posklejanych simpleksów). Ponieważ spostrzegłem wiele niejasności i sam nie mam pewności czy konstrukcja ta jest sensowna, postanowiłem że zacznę od nowa, od najprostszych przypadków. Wpis ten ma pokazać na kilku obrazkach istotę konstrukcji dla pewnych elementarnych i bardzo krótkich dowodów. Będę się przy tym starał opisać całą konstrukcję raz jeszcze ( a więc z konieczności będę się powtarzał) wszakże obecnie wyrobiłem sobie nieco inny obraz całej sytuacji i mam nadzieję że będzie on bardziej czytelny niż poprzednie wpisy.

Zacznijmy od tego czym system formalny i dowód w ramach takiego systemu. System formalny to zbiór zdań logicznych złożony z zdań wyróżnionych, zwanych aksjomatami,oraz pewnego zestawu reguł przekształcania napisów zwanych regułami inferencji, dedukcji lub wnioskowania. Reguły wnioskowania akceptują pewną formę zdań ( w sensie czysto graficznym, syntaktycznym, jako napisy) i pozwalają na podstawie takich argumentów, uznać że do systemu wolno nam dopisać kolejne, określone w swojej formie syntaktycznej przez „mechanikę reguły wnioskowania”, zdanie. Modelowym przykładem reguły wnioskowania jest reguła modus ponens, mająca postać: jeśli w zbiorze zdań występuje zdanie { P= ''A \rightarrow B'' }, oraz zdanie {Q=''A''} to możemy dopisać zdanie {S=''B''}. Symbolicznie będę tą regułę zapisywał w formie {MP(P,Q) =S} co jest oczywiście równoważne zapisowi {MP(A \rightarrow B,A) = B}. Powiedzmy tutaj jasno że modus ponens jest regułą syntaktyczną zaś zdania w cudzysłowach,a wiec faktyczna postać syntaktyczna zdań, jest kluczowa dla jej zastosowania. Nie ma sensu używanie reguły {MP(P,Q) = S} dla „abstrakcyjnych” zdań {P,Q,S}. Jeśli poprawnie zastosowano regułę modus ponens, zdania {P,Q,S} miały określona ( i wypisaną jawnie powyżej) postać syntaktyczną ( to znaczy istniały takie zdania {A,B} że {P=''A=B''}, {Q=''A''} … itp. cudzysłowu używam w tym kontekście po to by jednoznacznie określić co jest zdaniem o które nam chodzi – mianowicie na przykład wyrażenie {P=''A \rightarrow B''} oznacza że istnieją zdania {A i B} takie że zdanie {P} ma postać jak w cudzysłowie. )

Dowodem zdania {S} w systemie logicznym zawierającym aksjomaty i regułę dedukcyjną modus ponens jest uporządkowany ciąg zdań { \{ a_{0},a_{1},a_{2} \cdots ,a_{n} \} } gdzie {a_{n} = S}, zaś zdania numerowane od {1, \cdots n-1} to aksjomaty, tautologie lub wcześniej dowiedzione zdania. Ponieważ wcześniej dowiedzione twierdzenia mają dowody ( a więc ciągi zdań…), możemy przyjąć ( zastępując każde zdanie w powyższym ciągu jego dowodem) że zdania {a_{1}, \cdots a_{(n-1)}} to aksjomaty lub tautologie. Dla każdego podciągu uporządkowanego { \{ a_{0} \cdots , a_{k},a_{(k+1)} \} } istnieje reguła wnioskowania ( inferencji, dedukcji), która pozwala wyprowadzić zdanie {a_{(k+1)}} z zdań {a_{0},\cdots , a_{k}}. Jest to klasyczna definicja dowodu, czytelnik spotkał sie z nią zapewne wielokrotnie.

Pewnej uwagi wymaga kwestia uporządkowania zdań w dowodzie. Co do zasady aksjomat lub zdanie uprzednio dowiedzione może się pojawiać na liście w dowolnym miejscu i dowolną ilość razy. Nowe zdania ( takie których nie ma na liście ) pojawiają się wyłącznie dzięki stosowaniu reguł dedukcji, w naszym przypadku – wyłącznie modus ponens. Jednocześnie, jak wspomnieliśmy aksjomaty, są zdaniami. Jest to konwencja różna od zwyczajowo stosowanej, mianowicie zwykle rozważa sie schematy aksjomatów. Oznacza to że np. wyrażenie ( założone jako aksjomat na przykład w systemie logiki Hilberta)

\displaystyle \phi \Rightarrow ( \psi \Rightarrow \phi )

nie reprezentuje zdania logicznego ale cały zbiór zdań, powstałych przez zastąpienie występujących w nim zmiennych {\phi,\psi} przez wszelkie możliwe i poprawne składniowo kombinacje zdań elementarnych ( które oznaczamy {P,Q,S...}) uzyskane przez zastosowanie spójników logicznych ( alternatywa, koniunkcja, implikacja, negacja itp.). Tym samym zbiór aksjomatów jest oczywiście zbiorem nieskończonym, przeliczalnym, zaś jego numeracja może odpowiadać pewnej arbitralnej ale określonej konwencji na przykład zdefiniowanej za pomocą złożoności składniowej zdania itp. Nie jest to w tej chwili kwestia istotna, głównie z tego powodu, że standardowy dowód to skończony ciąg zdań, a zatem i zawiera skończoną liczbę „realizacji” schematu aksjomatu i każde z tych zdań może mieć przypisany kolejny numer ( a nawet możemy przypisać różne numery tym samym zdaniom, np. ten sam aksjomat może być zdaniem 2, 10 i 12 na liście). Zauważmy, że choć w dalszym ciągu wywodu będę używał pojęcia dowodu, jak zdefiniowane powyżej, nie ma tu potrzeby by ograniczać się do dowodów konkretnych i określonych twierdzeń. Możemy powiedzieć, ze badamy po prostu uporządkowane ze względu na regułę modus ponens ciągi zdań z wyróżnionym, skończonym podciągiem startowym zwanym zbiorem aksjomatów i tego typu ogólność będziemy stale utrzymywali.

Załóżmy że mamy zdania {P,Q,S} o budowie syntaktycznej jak wypisana powyżej. Zdaniom tym przyporządkujemy graf, w postaci jak na rysunku poniżej:

ModusPoens

Prosiłbym by czytelnik zwrócił uwagę, że graf jest skierowany, porządek ten zaś wynika z uporządkowania zdań w regule modus ponens. Przyjęliśmy mianowicie konwencję w której pierwsze zdanie to implikacja, drugie to przesłanka, a trzecie to następnik implikacji. Konwencja ta nie jest całkowicie arbitralna i choć właściwie nigdzie nie będziemy w dalszym ciągu się na nią powoływać ponad fakt, że została określona i będziemy konsekwentnie jej używać, to ma ona dalece idące konsekwencje koncepcyjne. Nie przemyślałem tego faktu dostatecznie głęboko, wszakże konwencja wynikająca z korespondencji Currego-Howarda każe odnieść modus ponens do pojęcia „aplikacji funkcji” i można w tym kontekście przyjąć że nasza konwencja oznacza iż podajemy wpierw funkcję ( której odpowiada implikacja) a następnie jej argument czyli przesłankę implikacji, zaś w wyniku otrzymujemy następnik implikacji. Tymczasem w grafie postępujemy odwrotnie i odwracamy kolejność strzałek tak by pierwsza była przesłanka ( argument funkcji) który zgodnie ze strzałkami trafia pod działanie funkcji ( implikacja) i w wyniku dostajemy następnik implikacji. Owo odwrócenie kolejności ma znaczenie dla dalszych rozważań – stawiając przesłankę i następnik po „przeciwnych stronach” obiektu który zostanie dalej zdefiniowany a zwany jest plakietką ( proszę czytelnika o cierpliwość, kolejny przykład wyjaśni co mam tu na myśli).

Przy tak zdefiniowanej reprezentacji graficznej reguły modus ponens możemy kolejne użycia jej w dowodzie przypisać kolejnym trójkątom a w wyniku otrzymamy graf złożony z zorientowanych trójkątów posklejanych wierzchołkami. Graf ten w swoich wierzchołkach zawiera zdania, zaś jego krawędzie to związek pomiędzy wierzchołkami polegający na tym że wystąpiły one w jednej regule modus ponens. W tym miejscu następuje pewien poważny przeskok koncepcyjny. Dotychczas rozważaliśmy grafy, teraz dołączmy do naszego postępowania także to co znajduje się pomiędzy ich krawędziami. Będziemy uważać, że rysunek powyżej przedstawia nie tyle graf z wierzchołkami i krawędziami co element powierzchni – czyli 2 wymiarowy simpleks i konsekwentnie, graf reprezentujący dowód stanie się „zlepkiem” takich simpleksów, czyli kompleksem simplicjalnym ( bo z konstrukcji złączenie następuje wyłącznie w wierzchołkach lub wzdłuż krawędzi – o tym za chwilę).

Podkreślmy że w zbiorze tym simpleks występuje tylko tam, gdzie 3 zdania będące jego wierzchołkami są użyte w pewnej regule modus ponens. Nie ma żadnej możliwości uzupełnienia krawędzi ( np. do postaci simplesków 3 wymiarowych czyli czworościanów posiadających pewną objętość) tam gdzie reguła modus ponenes nie występuje. Operacje wstawiania i usuwania krawędzi, są istotne dla dalszych uogólnień, na razie jednak nie jestem w stanie podać ich spójnej definicji.

Typową sytuacją w zbiorze o jakim piszemy jest wspólny wierzchołek pomiędzy dwoma regułami modus ponens, to jest następująca sytuacja: istnieją zdania {A,B,C,D,E} takie że {MP(A,B) =C} oraz {MP(C,D)=E}. Jak widać mamy tu dwa simpleksy {(B,A,C)} oraz {(D,C,E)} ( zwracam uwagę na zmienioną kolejność wierzchołków w geometrycznej reprezentacji w stosunku do kolejności w regule modus ponens!) które mają wspólny wierzchołek.

Inna możliwa sytuacja to wspólna krawędź:

\displaystyle MP(A,B)=C

\displaystyle MP(B,C)=D

W tym przypadku mamy simpleksy {(B,A,C)} oraz {(C,B,D)} posiadające wspólna krawędź {(B,C)} czyli wspólny simpleks jednowymiarowy. Przykład takich zdań to: {A=''(s \rightarrow q) \rightarrow s''}, {B=''s \rightarrow q''}, {C=''s''}, {D=''q''}. Proszę sprawdzić że relacja powyżej jest spełniona.

Ciekawym pytaniem jest czy możliwe jest zbudowanie czworościanu, czyli simpleksu 3-wymairowego, o właściwej strukturze syntaktycznej zdań tak by każda ściana reprezentowała modus ponens i czworościan był właściwie zorientowany ( na zewnątrz, regułą lewej dłoni). Innymi słowy czy możliwa jest następująca konstrukcja:

\displaystyle MP(A,B)=C

\displaystyle MP(B,C)=D

\displaystyle MP(A,B)=D

\displaystyle MP(C,A)=D

dla różnych zdań {A,B,C,D}. Podkreślmy że ostatni warunek jest tu istotny. Polecam czytelnikowi jako ćwiczenie z zabawy tautologiami próbę zbudowania takiego obiektu. Zwrócę tu dodatkowo uwagę, że choć jak przypuszczam w ogólności nie jest to możliwe ( regułą modus ponens nie jest tranzytywna, własność tranzytywności ma natomiast sama implikacja), to być może stosowna konstrukcja jest możliwa przy dodatkowym założeniu o prawdziwości występujących w niej zdań np. że prawdziwe jest zdanie „B i C” itp…

Przy przyjętych założeniach, powstały graf wyraża wyłącznie strukturę wynikła ze stosowania reguły modus ponens. Odwzorowanie powyższe, pomiędzy dowodem a kompleksem symplicjalnym całkowicie pomija wewnętrzną strukturę zdań. Nic więc dziwnego że właściwie niewiele z niego wynika. Chciałbym dodać do obrazu powyżej informację na temat sprzeczności w dowodzie.

Przypomnijmy że dowód jest sprzeczny, kiedy na liście jego zdań występuje zarówno zdanie {A} jak i {\neg A}. Oczywiście w praktyce szukamy dowodów niesprzecznych, nic jednak nie stoi na przeszkodzie by analizować i sprzeczne. Co więcej, we wszystkich rozważaniach rozpatrujemy jedynie konsekwencje syntaktyczne, tak więc nie mówimy np. o wartościowaniu zdań, nie analizujemy które z nich są prawdziwe itp. Nie ma więc przeszkód by analizować uporządkowane ciągi zdań zawierające także i wyrażenia {A} i {\neg A}. Przy takich założeniach ciąg zdań, który nazywamy dowodem nie jest ciągiem sprzecznym tak długo jak długo nie występuje w nim para zdań sprzecznych! O ile w logice czy teorii modeli zwykle stosuje sie natychmiastowe uogólnienie polegające na dołożeniu do danego zbioru zdań, wszystkich ich konsekwencji syntaktycznych lub semantycznych, i o sprzeczności mówi sie w kontekście takie, nieskończonego obiektu, o tyle tu podkreślmy wyraźnie rozmawiamy wyłącznie o skończonych zbiorach zdań. Tym samym zbiór zdań, wśród którego konsekwencji występują sprzeczności, będzie przez nas rozważany jako zbiór niesprzeczny tak długo, jak długo owe zdania sprzeczne nie zostaną jawnie wyprowadzone ( dołączone do zbioru, doklejone kompleksu simpleksów) regułą modus ponens.

Rozważmy bardzo prostą zabawkową teorie o następujących aksjomatach:

\displaystyle a_{0}. A \rightarrow A

\displaystyle a_{1}. A

Bezpośrednie zastosowanie {MP(a_{0},a_{1} )} dale w wyniku zdanie A. Przedstawimy tą sytuację za pomocą następującego grafu.

MP-A-A

Tak jak na pierwszym rysunku, relacja modus poens między zdaniami jest przedstawiona za pomocą ciągłych, skierowanych linii, zaś kierunek przepływa od przesłanki przez implikację do następnika implikacji. Tym razem jednak każde kolejne zdanie, poprzednio reprezentowane jako punktowy wierzchołek, zostało pokazane jako odcinek obdarzony kierunkiem. Można uznać że w naszym odwzorowaniu każdemu wierzchołkowi przyporządkowaliśmy uporządkowaną parę punktów. Nadal moglibyśmy odwoływać sie do obiektu na rysunku powyżej jako do simpleksu ( dokonując dodatkowych odwzorowań wierzchołków w grupę alternującą itp. wierze że taka konstrukcja jest możliwa, zapewne gdyby ja wykonać teoria zyskałaby na ścisłości ) wszakże dla prostoty przedstawienia konsekwencji takiego rozszerzenia będę obiekty jak na rysunku powyżej nazywał plakietkami.

Po pierwsze linie ciągłe nadal reprezentują regułę modus ponens i ich orientacja jest nadal ustalona w taki sam sposób jak wcześniej. Zwróćmy uwagę że zdanie {A} występuje na rysunku dwukrotnie – raz jako przesłanka a raz jako następnik. jest to jednak to samo zdanie, możemy zatem ‚skleić” naszą plakietkę. Przymnijmy że mówimy tu o „geometrycznej” czy „topologicznej” reprezentacji, a więc o powierzchni. Otrzymamy w wyniku figurę topologicznią izomorficzną z powierzchnią boczną walca. Zauważmy że cały efekt uzyskaliśmy dzięki stosownej orientacji zdania {A} w wierzchołku w którym występuje on jako następnik implikacji ( wniosek).

Jako kolejny przykład rozważmy następującą, inną, teorię:

\displaystyle b_0. A \rightarrow \neg A

\displaystyle b_1. A

Bezpośrednie zastosowanie {MP(b_{0},b_{1} )} daje oczywiście zdanie {\neg A}. Oczywiście „teoria” którą się tu bawimy jest jawnie sprzeczna ( i faktycznie regułą modus ponens produkuje nam sprzeczność syntaktyczną po jednokrotnym jej zastosowaniu). Tym razem reprezentacja graficzna ma następująca postać:

MP-A-notA

Proszę zwrócić uwagę na odwróconą kolejność wierzchołków reprezentujących zdanie {\neg A}, oraz na to że kierunki strzałek reprezentujących przepływ w regule wnioskowania są identyczne jak na obrazku dla trywialnej teorii niesprzecznej. Otrzymany obiekt zawiera, podobnie jak poprzedni graf, dwukrotnie to samo zdanie {A} tyle że „inaczej podłączone”. Przy takiej reprezentacji, sklejenie którego musimy dokonać ( biały punkt do białego, czarny do czarnego) daje nam klasyczną reprezentacje wstęgi Mobiusa czyli powierzchni nieorientowalnej.

Co więcej, możemy przyjąć, że krawędzie  plakietki indukują na niej orientację, przy czym orientacja wynika owa z faktu, ze w regule modus ponens przesłanka i implikacja są zdaniami dowiedzionymi ( bo występują w zbiorze zdań z numerami wcześniejszymi niż następnik implikacji ). Tym samym załóżmy że plakietki możemy zorientować zgodnie z kierunkami „większości strzałek” reguły modus ponens.

Cały pomysł jaki chciałbym przeanalizować opiera sie na konstatacji że moja intuicja podpowiada mi że w przedstawionej reprezentacji, dowodom syntaktycznie sprzecznym, odpowiadają powierzchnie nieorientowalne, zaś dowodom niesprzecznym – orientowalne.

Zauważmy że „sklejenie” plakietek które pokazano na rysunku, zachodzi wzdłuż krawędzie przerywanych reprezentujących zdania ( a nie wzdłuż krawędzi reprezentujących reguły modus ponens). Jeśli teoria jest sprzeczna to wśród zdań które generuje sa zdania {A} i {\neg A}. Oznacza to że istnieją dwie krawędzie o przeciwnych orientacjach, które zostaną sklejone. Każda z nich jest jednocześnie jedną z krawędzi plakietki reprezentującej odpowiedni modus ponens. Zauważmy, że choć w teorii mogą istnieć izolowane plakietki ( bo możemy wypisać niezwiązaną z innymi regułę modus ponens), to jednak fakt że teoria jest sprzeczna oznacza że co najmniej jedna plakietka ( co najmniej ta na rysunku powyżej) jest sklejona. Istnieje tym samym droga zamknięta przechodząca po plakietkach od krawędzi {A} do {\neg A}. Wzdłuż tej drogi niemożliwe jest określenie orientacji plakietek ( orientacja ta nie musi mieć nic wspólnego z orientacjami indukowanymi z reguły modus ponens. Być może ma – ale bynajmniej tego nie twierdzę, wymaga to analizy).

Odwrotnie, niech pewna składowa spójna powierzchni sklejonych plakietek będzie nieorientowalna. Istnieje wówczas droga zamknięta, oraz krawędź zdaniowa przez którą przechodzi ona po plakietkach ( bo plakietki są sklejone wyłącznie wzdłuż krawędzi zdaniowych), wzdłuż której nie można określić orientacji. Jednocześnie orientacje lokalne wzdłuż krzywej raz indukują na owej krawędzi zdaniowej orientację typu {A} a raz ( „z drugiej strony”) {\neg A} – czyli teoria jest sprzeczna.

W dalszej części chciałbym zająć się kwestią definicji odwzorowań charakterystycznych dla teorii homologii – są to odwzorowania i-tej ściany {d_i} simpleksu ( ang. face map ) i odwzorowania degeneracji {s_i} ( ang. degeneration map). Pierwsze z ich mapuje simpleks na ścianę przeciwległą do i-tego wierzchołka, drugie zaś mapuje simpleks n wymiarowy na zdegenerowany o (n+1) wymiarach, poprzez powtórzenie i-tego wierzchołka. Zagadnienia te nie sa oczywiste gdyż dopisanie lub eliminacja wierzchołków odpowiada eliminacji lub dopisywaniu zdań do reguł modus ponens.

MathTextOntology-pasek

 

 

     W tym wpisie opiszę na prostym przykładzie ;-) w jaki sposób wygenerować własny parser za pomocą antlr. Po zainstalowaniu i skonfigurowaniu zgodnie z instrukcją na stronie ( różne tam systemowe aliasy żeby wszystko się uruchamiało ze ścieżek bezszmerowo), uzyskujmy trzy elementy w systemie: zainstalowany program antlr o którym za chwilę napiszę więcej, program grun – a właściwie spreparowany alias systemowy pewnego złożonego polecenia pozwalający na uruchamianie kodu generowanego przez antlr ( o czym za chwilę) oraz oczywiście zainstalowaliśmy stosowną wersję java, jak napisano w instrukcji instalacji. Jak ktoś chce wykonać własnoręcznie to co opisałem poniżej, musi mieć zainstalowane wszystkie trzy komponenty. Nie będę opisywał tych szczegółów bo są dobrze ujęte na stronie antlr, a ponadto dla prostej nauki można użyć AntlrWorks który nie wymaga żadnych szczególnych konfiguracji i dostarcza „wszystko w jednym” i to dla rozmaitych systemów operacyjnych, a na dodatek obok tego co opisałem poniżej, sprawdza poprawności, koloruje i wyświetla diagramy składniowe dla podanej gramatyki.

    Przejdźmy do samego antlr. Wpis omawia antlr w wersji 4, czyli antlr4. W stosunku do antlr3 są spore różnice, in plus, więc kwestie antlr3 zostawmy na boku, zaznaczając tylko, że jak ktoś czyta gdziekolwiek artykuł o antlr powinien zadać sobie jako pierwsze pytanie o jakiej wersji mowa bo różnice sa spore.

    Antlr jest narzędziem które na wejściu przyjmuje definicję gramatyki języka i na jej podstawie generuje kod programu który potrafi ten język analizować. Nie będę wnikał tu zbyt głęboko w temat, ale właściwie mamy tu do czynienia z definicją gramatyki w postaci BNF zapisaną w specyficzny dla antlr sposób. Pominę także detale związane z poprawnością gramatyki i ograniczeniami jakie niesie antlr – szczegóły sa do odnalezienia w dokumentacji – antlr pozwala na gramatyki wprost lewo rekurencyjne – jak w przykłądzie poniżej, ale nie pozwala na gramatyki niejawnie lewo rekurencyjne ( generacja kodu kończy sie błędem).
Jako przykład niech posłuży nam gramatyka wyrażeń numerycznych obejmujących liczby naturalne oraz ich dodawanie, odejmowanie, mnożenie i dzielenie, oraz nawiasy. Definicja takiej gramatyki ma postać pliku .g4 który wygląda następująco ( numery na początku wierszy nie są częścią pliku):

———————-Expr.g4—————–
(1) grammar Expr;
(2) progr: (expr NEWLINE)*
(3) ;
(4) expr: expr (‚*’|’/’) expr
(5)          | expr (‚+’|’-‚) expr
(6)          | INT
(7)          | ‚(‚ expr ‚)’
(8)          | expr NEWLINE
(9) ;
(10) NEWLINE : [\n]+ ;
(11) INT : [0-9]+ ;
—————————————

    Opiszmy jaki jest cel użycia takiej gramatyki i co z nią potrafi zrobić antlr, a przy okazji wyjaśnimy znaczenie poszczególnych linii pliku. Gramatyka pokazana powyżej nazywa sie Expr, co definiuje linia (1) pliku. Opisuje ona reguły interpretacji pewnego rodzaju tekstu – czyli zespołów znaków tekstowych. Wyrażenia te, jeśli są prawidłowo zbudowane, powinny dać sie zinterpretować w kontekście tej gramatyki, dla siebie powiedzielibyśmy że jako wyrażenia arytmetyczne, a dla programu – jako zgodne z gramatyką ciągi znaków. Wyrażenie takie to progr który jest pewną liczbą wyrażeń expr zakończonych znakami NEWLINE ( linie (2)-(3) pliku). Wyrażenie expr zdefiniowane w liniach (4)-(9) składa sie z wyrażeń typu expr NEWLINE – ( mamy tu jawnie lewą rekurencję)   lub   „nawias” expr „nawias” lub INT lub expr  ( „+” lub „-„ ) expr itp. Kreski pionowe na początku linii (5) i następnych oznaczają alternatywy. Na końcu w liniach (10) i (11) zdefiniowano co znaczy NEWLINE i INT w składni przypominającej wyrażenia regularne. Przykłady bardziej – niekiedy znacznie bardziej – złożonych gramatyk można znaleźć na tej stronie. Polecam zwłaszcza zerknięcie na gramatykę jakiegoś języka programowania jak choćby java czy python, oraz gramatykę opisująca plik csv.

    Program komputerowy analizujący wyrażenie zgodne z powyższą gramatyką, na przykład „(5*(3+4) -12)/(2+3*(6-3))”, powinien prawidłowo rozpoznać elementy wyrażenia, takie jak „(3+4)”, określić ich „znaczenie” i poprawność. Nazwijmy taki program analizatorem. Proces tworzenia analizatora który będzie dokonywał interpretacji takich wyrażeń ma wiele uniwersalnych cech, niezależnych od szczegółów gramatyki zdefiniowanej powyżej. Elementy te powtarzają się zarówno przy budowie analizatorów dla wyrażeń jak „(3+4)” jak i w przypadku analizatorów języka naturalnego, języka SQL, analizatorów sprawdzających konstrukcje języka C++ lub pliki xml. Twórcy antlr stworzyli narzędzie które w oparciu o definicję gramatyki, buduje szkielet programu, w jednym z kilku dostępnych języków, który programista może zmodyfikować dostosowując je w trakcie pracy do własnych potrzeb. Antlr jest zatem programem który generuje programy ( a raczej programem który generuje źródła innych programów). Tego rodzaj programów nazywa sie generatorami kodu, a w tym konkretnie przypadku mamy do czynienia z programem generującym analizatory ( sa oczywiście inne generatory, programy mogą generować szkielety stron www, szkielety GUI, szkielety baz danych i inne. Właściwie każdy IDE który posiada pewnego rodzaju wbudowaną „automatyzację” tworzenia kodu – na przykład dopisuje szkielety klas języka itp. jest tego rodzaju generatorem. Całkiem spora część kodu jest tym samym generowana). Program wygenerowany przez antlr ( domyślnie w java), nasz analizator, składa sie z dwu podstawowych elementów logicznych. Pierwszy z nich nazywa się lekserem. Lekser to program który dzięki wbudowanej gramatyce, takiej jak ta powyżej, jest w stanie prawidłowo rozpoznać elementy języka, zwane tokenami. Tokeny w naszym przykładzie to: złożone wyrażenia progr i expr, symbole operacji logicznych „+,-,*,/”, wyrażenie INT – reprezentowane w prostym tutaj przykładzie jako dowolnej długości ciąg znaków 0,1,2…9 = [0-9]+, oraz wyrażenie NEWLINE, obejmujące znaki nowej linii [\n]+ w dowolnej ilości. Lekser przegląda zatem strumień znaków jaki program analizuje i wykrzykuje z radością – „o! expr! „, „o! progr!”, „o! nawias!”.

     Lekser rozpoznaje ciągi znaków i przekazuje je do kolejnego elementu analizatora – parsera. Parser otrzymuje od leksera, z powodów nazwijmy to technicznych, numer pozycji w wyrażeniu gdzie zaczyna i kończy się dany element języka. Wtedy parser sprawdza czy spełnione sa reguły gramatyki. Prosta gramatyka jaką tu omawiam, nie ma zbyt wielu skomplikowanych aspektów, ale jednym z śladów złożoności z jaką musi poradzić sobie parser jest kwestia poprawnego otwarcia i domknięcia nawiasów. Parser zatem dokona sprawdzenia czy zgodnie z regułami gramatyki zapisanymi w linii o numerze (7) każdy nawias który został otwarty został także prawidłowo zamknięty, czy każdy operator „+” zawiera dwa wyrażenia expr z swojej prawej i lewej strony itp. Parser mówi „nawias mówisz? a gdzie drugi?”.

    Podsumujmy – lekser rozpoznaje, parser sprawdza.

    Jak używać antlr? Zapisujemy definicje gramatyki w pliku o nazwie zgodnej z nazwą gramatyki – w naszym przypadku będzie to plik Expr.g4. Najlepiej całą operację przeprowadzić w stworzonym uprzednio katalogu, gdyż antrl wygeneruje kilka plików z kodem i katalog zapełni się plikami. Następnie generujemy pareser/lexer poleceniem
>antlr4 Expr.g4

Wykonanie tego polecania powoduje że w katalogu w którym je wykonaliśmy pojawi się sporo plików z kodem java.
Kompilujemy owe kody ( w katalogu gdzie to wszystko jest):
>javac *.java

    I już. Powstał nam prosty parser, który potrafi rozpoznać i sprawdzić poprawność wyrażeń arytmetycznych na liczbach naturalnych. Oczywiście od takiej prostej generacji do użytecznych działań daleka droga, ewentualny rozwój aplikacji ( prostego kalkulatora ?) wymagałby od nas grzebania po kodzie jaki wygenerował antlr i dostosowywania tego kodu do naszych potrzeb. W szczególności musielibyśmy napisać kod który zinterpretuje wyrażenia które rozpoznał lekser i sprawdził parser ( ale jeśli ktoś poda nam złe wyrażenie, np. nie domknie nawiasu – obsługę błędów już mamy!). Interpretacja oznacza w ostatnim zdaniu przejście od tego, że program rozumie iż (3+4) to prawidłowe wyrażenie w którym 3 i 4 to elementy INT, + to operator „+” zaś „(” i „)” to nawiasy, do użycia w miejsce + operatora dodawania zaś w miejsce 3 i 4 liczb integer. Antlr bowiem parsuje, czyli przetwarza, pliki tekstowe, i wszystko co sprawdza to znaki w takich plikach, po prostu napisy.

    Sprawdźmy jak to działa. stworzyłem plik tekstowy example.txt o następującej zawartości:

———–example.txt—————–
((2+7*(13-10/7)/8)*12 -3*(5+7))/5
((2+7*(13-10/7)/8)/12 -3*(5+7))/6
———————————————

i za pomocą polecenia:
>grun Expr prog -gui example.txt

wygenerowałem następujący obrazek:

antlr4_parse_tree

    Jak widać w ostatnim poleceniu wskazałem jawnie że wierzchołek parsowania ma postać dyrektywy progr z gramatyki ( jak się wskaże co innego drzewo wygląda inaczej – i jest błędne dla podanego przykładu – co jak rozumiem oznacza, że przykład nie spełnia założenia, czyli że jest czym innym niż elementem, progr. ), czego kod wygenerowany z antlr sam nie rozpozna.

    Antlr generuje kod w java który zawiera lekser i parser. Programy te nie tylko wykonują to co opisaliśmy powyżej – to rola leksera i parsera – ale także reprezentują dostarczony strumień znaków w postaci drzewa jakie widzimy ma obrazku powyżej – jest to tak zwane drzewo parsowania. W drzewie tym, reguły złożone gramatyki, takie jak progr i expr reprezentowane są jako korzenie drzewa, zaś tokeny proste, jak NEWLINE, INT i nawiasy – są liśćmi. Obok leksera i parsera antlr generuje także kod walkera i listenera. Walker potrafi przeglądać drzewo – od lewej do prawej, i generować zdarzenia których oczekuje lekser i potrafi je zinterpretować. Na przykład walker trafiając na wyrażenie „3+4” wygeneruje zdarzenia „wchodzę w wyrażenie „+”, końcowy liść – „3”, końcowy liść „4”, wychodzę z wyrażenia”. Listener może zinterpretować te sygnały i wykonać operację arytmetyczną na koniec wypisując „wynik: 7”, ale może także zamienić nasze wyrażenie do postaci: „wyrażenie to: trzy plus cztery”. Oba te zachowania, i wiele innych, są możliwe, relatywnie łatwe do wykonania, wymagają jednak modyfikacji kodu czego nie będę tu pokazywał – odsyłam do strony antlr. Warto wszakże zwrócić uwagę, że choć z ludzkiego punktu widzenia pierwszy rodzaj działania to wyliczanie, czyli ewaluacja, a drugi to „tłumaczenie na język pisany”, to w sensie koncepcyjnym nie ma tu właściwie żadnej różnicy – zamieniamy symbole jednego rodzaju na symbole innego rodzaju. W taki sam sposób właściwie działa kompilator, translator i interpreter i koloryzator składni.  Antlr jest używany także przy analizie składni zapytań w wyszukiwarkach np. Twitter.

 

Jeśli słomiany zapał mi nie opadnie – wpis będzie miał kontynuację..

 

 

 

    Znane każdemu rodzicowi sa ciągi pytań „A dlaczego?”. Dlaczego Niebo Jest Niebieskie? Bo rozpraszania przebiega w taki sposób że czerwone promieniowanie rozprasza się mało, a niebieskie dużo. A dlaczego czerwone mało a niebieskie dużo? Bo taka jest charakterystyka związana z prawem Rayleigha. A dlaczego taka charakterystyka? Bo rozpraszanie zależy od odwrotności długości fali w 4-tej potędze. A dlaczego od 4-je potęgi? Bo takie jest rozwiązanie stacjonarne równania rozpraszania dla dużych długości fali. A dlaczego … I tak dalej i tak dalej.

    Wiadomo ze można taką zabawę ciągnąć bez końca. W wypadku wiedzy fizycznej, realnej wiedzy o realnym świecie, ciąg takich pytań nie ma końca. Jak jest w wypadku matematyki?

    Kiedyś pisałem, niezbyt jasno, o przypadkowej matematyce . Ostatnio zaś w necie natrafiłem na ciekawe pytanie jakoś tam związane z tym tematem. Oto Gil Kalai, matematyk z Izraela pracujący także w Stanach Zjednoczonych, i prowadzący bardzo fajnego bloga, zadał pytanie „Dlaczego jest możliwe uprawianie matematyki?”, po czym dodatkowo zwrócił uwagę na komentarz Timothy Gowersa, laureata medalu Fieldsa, na to pytanie. Wydaje sie że obaj panowie starają sie nadać temu pytaniu nieco bardziej techniczny, niż czysto filozoficzny, czy metamatematyczny charakter.

     Odpowiedź Gowersa jest o tyle ciekawa, że przywołuje pojęcia teorii złożoności obliczeniowej i probabilistyki. Gowers stwierdza, że jeśli wszystkim twierdzeniom matematycznym przypisać liczbę, zdefiniowaną jako „długość dowodu”, i potraktować ją jako zmienną losową, to „efektywna możliwość uprawiania matematyki” odpowiada ciekawej własności tej zmiennej. Otóż zmienna owa może przyjmować w zasadzie dowolnie wielkie wartości, wiemy że mogą istnieć twierdzenia posiadające proste, krótkie dowody, ale oczywiście istnieją także twierdzenia matematyczne, posiadające dowody bardzo długie, właściwie to dowolnie długie. Co prawda pojęcie nieskończenie długiego dowodu nie ma za bardzo sensu, jednak całkiem uzasadnione jest przyjąć że wartość zmiennej „długość dowodu” należy do przedziału od zera do nieskończoności. Mimo to – i tu dochodzimy do niebanalnej własności owej zmiennej – matematyka się rozwija przy użyciu relatywnie krótkich dowodów – zatem Gowers spekuluje że wartość spodziewana owej zmiennej „długości dowodu” jest niewielka. Długość dowodu może być bardzo mała lub bardzo duża, ale większość dowodów zdaje się być zdumiewająco krótka. Oczywiście sa to spekulacje, czego autor nie zapomina nadmienić.

     Wróćmy do kwestii „przypadkowej matematyki”. Rozumowanie Gowersa przypomniało mi to że o tym temacie kiedyś myślałem. I rzeczywiście także i tu, może warto do tematu podejść nieco bardziej rzeczowo. Będziemy starali sie rozumować przez analogię. Przypuśćmy że rozważamy inne pytanie. Mam liczbę, powiedzmy 3. Dodam do niej liczbę 2 – uzyskam 5. Pomnożę przez 8 – uzyskam 40. Mogę potęgować, dodawać, mnożyć. Wreszcie na koniec mogę wszystkie te operacje zapisać jako program komputerowy, albo sporych rozmiarów, wzór. Uzyskam przepis pozwalający wyliczać wynik wszystkich tych działań, nie tylko dla owej jednej liczby, ale dla innych liczb także, mówiąc krótko – stworzę pewną procedurę obliczeniową definiującą funkcję. Funkcja owa, złożona z elementarnych działań ( takich jak dodawania, mnożenie itp) może być bardzo wymyślna. mimo to w pewnych bardzo ogólnych warunkach będzie obliczalna. Wielkim osiągnięciem matematyki początków XX wieku było określenie owych warunków a zwłaszcza pokazanie, że funkcje obliczalne w ogóle wszystkich funkcji sa relatywnie niewielkim zbiorem. Budując analogię do rzeczy które chcę tu rozważać, możemy stwierdzić, że cokolwiek zrobimy z kilkoma elementarnymi działaniami, w skończonej ilości kroków, uzyskana w ten sposób operacja będzie funkcją obliczalną.

    Niemniej istnieją funkcje nieobliczalne, to znaczy takie których nie da się w ten sposób zapisać, ani nawet obliczyć. Czytelnikowi zainteresowanemu tym tematem polecam doskonałą monografię Murawskiego, w tym miejscu zwrócę zaś uwagę, że mamy tu do czynienia z fenomenem wielkiej wagi oraz posiadającym kilka ciekawych cech:

  1. nieobliczalność jest pewnego rodzaju fenomenem obiektywnym. Do tematu wrócimy poniżej.
  2. nieobliczalność nie polega na tym, że nie potrafimy obliczyć wartości funkcji f(x) nieobliczalnej dla pewnego jej argumentu x. To da sie zrobić dla każdego ustalonego argumentu, oczywiście pomijając kwestie techniczne typu rozmiarów pamięci czy wielkości uzyskanych liczb. Natomiast nie jest możliwe podanie „wzoru” czy tez „procedury” – dokładniej algorytmu – który pozwalałby na obliczenie wartości takiej funkcji dla wszystkich możliwych argumentów. Inaczej – nie istnieje pojedyncza procedura obliczeniowa – jedna dla wszystkich elementów dziedziny funkcji nieobliczalnej – która da jej wartość w tych punktach.
  3. w zasadzie brak odpowiedzi na pytanie czym charakteryzuje sie nieobliczalność w wypadku „realnie występujących zjawisk fizycznych”. Na pytanie „czy istnieją zjawiska fizyczne opisywane funkcjami nieobliczalnymi” nie znamy odpowiedzi. Z jednej strony obliczalność zdefiniowana jest dla liczb naturalnych ( ew. całkowitych) zaś fizyka używa liczb wymiernych. Jest to niezbyt istotna, ale jednak zawsze przeszkoda. Z drugiej strony wydaje się że nieobliczalność mogłaby manifestować się na dwa sposoby – albo jako bardzo szybki, nadeksponencjalny wzrost ( i przykładem takiego zjawiska jest np. Busy Beaver function), albo jako losowość.

 

    W tym miejscu przejdę do innego nieco zagadnienia. Jak wiadomo dla każdego systemu formalnego, mamy dwa możliwe sposoby opisu – syntaktyczny i semantyczny. Oba systemy wuymagają określenia symboli języka, relacji i funkcji wraz z ich arością, aksjomatów pozalogicznych i logicznych wraz z regułami inferencji ( jeśli tego nie określimy pozostaniemy w klasie systemów dedukcji). W systemie syntaktycznym możmy zapisywać twierdzenia i szukać ich dowodów, przy czym dowód jest ciągiem zdań zaczynającym sie od aksjomatów, a kończącym się twierdzeniem którego dowodzimy. W ciągu zdań o którym mowa albo zdania kolejne są aksjomatami, albo sa wynikiem użycia reguł inferencji do zdań poprzednich. Uzyskany w ten sposób zbiór twierdzeń, nazywamy konsekwencją syntaktyczną zbioru aksjomatów. Konsekwencja syntaktyczna to odpowiednik „rachunku”, „kalkulacji”.

     W obrazie semantycznym mamy pewien zbiór A zdań, zwykle aksjomatów, podobnie jak wyżej pozalogiczncyh i logicznych. Zdania te sa odnoszone do pewnego modelu – zbioru obiektów które spełniają zadania z wybranego zbioru A. Zwykle modeli – a więc „zbiorów przedmiotów spełniających zdania ze zbioru A” jest więcej niż jeden. Jeśli pewne inne zdania, zapisane w tym samym języku co zdania ze zbioru A są także prawdziwe w każdym z modeli zbioru A – wówczas mówimy że zdania te są konsekwencją semantyczną zdań ze zbioru A. Konsekwencja syntaktyczna to współprawdziwość, czy może lepiej „współspełnianie” gdyż omijając kwestię prawdziwości i ograniczając sie do spełnienia ( w sensie wartościowania logicznego), unikamy niebanalnych rozważań o tym czym jest prawda itp.

     Czy kwestia istnienia matematyki, możliwości jej uprawiania, nie przypomina tezy o obliczalności pewnych operacji? Tak jak zestawiając ze sobą działania elementarne uzyskiwaliśmy funkcje obliczalne, tak budując twierdzenia lub zbiory zdań współspełnialnych – budujemy teorie oparte o pewne elementarne operacje logiczne. Składamy rzeczy z jednakowych i wcześniej przygotowanych klocków. Możemy użyć ich jak nam sie podoba, możemy dokładać je z lewej, z góry i z prawej, ale klocki pozostają niezmienne, a możliwości łączenia pozostają ustalone z góry.

 

    W tym miejscu należy wspomnieć o kwestii niezależności i niedowiedlności. Oto jednym z ważnych faktów jest zjawisko niezależności logicznej. Okazuje sie że dla dostatecznie złożonych systemów, o ile pracujemy w logice pierwszego rzędu, istnieje wiele modeli. Fenomen ten oznacza, że nawet budując systemy fromalne, bradzo precyzyjnie i ścisle, nie określamy jednoznacznie obiektów które opisują wybrane przez nas aksjomaty.  Jest więcej „rodzajów liczb naturalnych” a dokładniej struktór spełniających aksjomatyke liczb naturalnych – niż tylko jeden znany nam przykład szkolny. W niektórych z modeli pewne zdania sa spełnione w innych nie. Przypomnijmy że konsekwencją semantyczna zbioru zdań są jedynie te zdania które są współprawdziwe z tym zbiorem, dla wszystkich modeli spełniających aksjomaty. Zdania te są zatem niezależne od zbioru aksjomatów – semantycznie nie są zdaniami współprawdziwymi. Ponieważ jednak istnieją modele w których możliwa jest współprawdziwość z aksjomatami ( choć w innych modelach nasze zdania sa nieprawdziwe a więc niespełnione) to stajemy przed kwestią wyboru. Wybór jest takiego rodzaju – albo możemy przyjąć że owe niezależne zdania należą do zbioru aksjomatów ( i tym samym poszerzyć ów zbiór, zaś zawęzić zbiór modeli), albo możemy osąd o zdaniach niezależnych zawiesić i badać teorie z większą ilością modeli, ewentualnie dodając że pewne „fakty” zależą od zawieszonego rozstrzygnięcia co do prawdziwości owych zdań. Zwykle w praktyce posiłkujemy sie kryterium efektywności – wybieramy ewentualności prowadzące do ciekawszej, efektywniejszej, bardziej estetycznej matematyki. Nie jest to jedak cała historia. Zdania prawdziwe we wszystkich modelach, będące sematyczną konsekwencją aksjomatów, mogą być niedowiedlne w ramach przyjętych metod syntaktycznych. Fenomen ten objawia się w fakcie że z punktu widzenia metod logiki 1-szego rzędu, dowody pewnych twierdzeń muszą przebiegać „inaczej” dla każdej liczby n która spełnia warunki takich twierdzeń. Każda liczba może być „przypadkiem szczególnym” zaś ogólne rozumowanie dowodzące twierdzenia we wszystkich takich przypadkach możliwe jest dopiero w logice wyższego rzędu lub w mocniejszej teorii ( np. w teorii mnogości)

     Pytając „dlaczego?” dostatecznie długo, w fizyce, nie uzyskujemy ostatecznej odpowiedzi. W matematyce jest inaczej. W końcu ostateczną odpowiedzią zawsze jest aksjomat. „Dlaczego to twierdzenie jest prawdziwe? Bo tak wynika logicznie z aksjomatów.” Zauważmy że w przypadku opisanym powyżej mamy do czynienia z niezależnością od zadanego zbioru aksjomatów. Tym samym fenomen niezależności logicznej jest fenomenem relatywnym. Obiektywnym faktem jest fakt istnienie zdań niezależnych – dla każdego skończonego zbioru aksjomatów ( a nawet dla zbiorów nieskończonych, przeliczalnych, pewnych określonych własnościach) istnieją zdania niezależne. Zdania których prawdziwość w modelach nie jest jednakowo określona. Sama niezależność konkretnego zdania nie wydaje sie jednak być obiektywnym faktem. Zmieniając układ aksjomatów ( w ramach zbiotu zdań pozostających swoimi konsekwencjami semantycznymi), uzyskamy inne zdania niezależne i inne „moce teorii”. Zdania wcześniej niezależne moga stać sie dowodliwe ( jeśli któryś z „nowych aksjomatów” był wcześnij zdaniem współprawdziwym lecz niedowiednlnym). Wreszcie rozszerzenie zbioru aksjomatów o zdania niezależne ( a więc niewspółprawdziwe) prowadzi do innych – mocniejszych teorii. Jest to zupełnie inna sytuacja niż w wypadku fenomenu nieobliczalności. Jak nadmieniłem w punkcie 1 powyżej – fenomen obliczalności funkcji ma znaczenie obiektywne. Być może jest tak, gdyż elementarne operacje jakie wykonujemy na funkcjach – tak zostały zdefiniowane funkcje obliczalne – są określone w sposób obiektywny i ustalony. Dysponujemy tu operacjami arytetycznymi, ograniczonym kwantyfikatorem i efektywnym minimum, oraz operacją składania funkcji ( rekurencja). Nie mamy tu wolności wyboru. Nie umiemy jako „bazy funkcji elementarnych” wybrać operacji nieobliczalnych co być może pozwoliłoby zapisywać złożone funkcje nieobliczalne jako „złożenie” prostszych klocków.

     W tym miejscu mogę wreszcie zadać pytanie o „przypadkową matematykę” w nieco bardziej techniczny sposób. Pytanie to mogłoby brzmieć mniej więcej tak: czy istnieją fakty matematyczne których prawdziwość nie zależy od przyjętego zbioru aksjomatów, pomimo że są spełnione w każdym z modeli? Na przykład – logika 2-giego rzędu pozwala na usunięcie problemów niezależności zdań dla arytmetyki Peano (PA). Fenomen ten polega na tym, iż w logice 2-giego rzędu istnieje tylko jeden model liczb naturalnych, nie ma modeli niestandardowych. Każde twierdzenie takiej teorii albo jest spełnione albo nie. Płacimy za to pewną cenę, teoria taka ma w zasadzie patologiczne własności ( np. niektóre dowody stają sie nieskończenie długie). Jednak przypuśćmy że w takiej teorii występuje pewna własność liczb, powiedzmy „twierdzenie X”, które stwierdza że liczba X o pewnej własności istnieje. Można sobie wyobrazić sytuację w której owa liczba istnieje także w każdym z modeli PA w logice 1-szego rzędu. I że brak jest dowodu tego faktu, bowiem dowód taki wymaga narzędzi dostępnych jedynie w logice 2-giego rzędu, powiedzmy indukcji pozaskończonej ( takie przykłady istnieją). Możemy wówczas stwierdzić, że choć istnienie liczby X nie ma wyjaśnienia na gruncie PA, to przecież nie jest przypadkiem. Jest to „prawdziwa” własność liczb naturalnych, wszakże niezależna od aksjomatów PA w teorii 1-szego rzędu.

     Pytam więc o istnienie takich cech obiektów teorii które są niezależne od aksjomatów – obiektywnie – a więc w dowolnym rzędzie logiki i w dowolnej aksjomatyzacji. Cech których istnienie jest całkowicie przypadkowe, i nie wynika z niczego co jawnie założyliśmy. Być może odwołując sie do kwestii obiektywności obliczalności funkcji, można by napisać że owa „przypadkowa cecha” nie tyle jest przypadkowa, co raczej wynika z pewnych określonych i niemożliwych do zmiany cech naszych rozumowań, tak jak nieobliczalność, nierelatywnych do wygodnych konwencji, lecz związanych z samą naturą języka i konsekwencji logicznej. Byłyby to zdania, twierdzenia czy własności, których istnienie byłoby konsekwencją np. skończoności zapisu elementów języka, związane z elementarnymi koncepcjami logicznymi jak kwantyfikacja czy negacja. Cechy czy własności takie byłyby obecne we wszystkich modelach jednak nie znajdywałyby syntaktycznego dowodu. Istnienie takich własności jest łatwe do przeoczenia, głównie dlatego że praktyka matematyczna, to przede wszystkim nieformalna praktyka syntaktyczna. Wydaje sie że praktykujący matematyk częściej buduje sobie określony model badanych pojęć a następnie szuka dowodu spostrzeżonych cech, niż szuka zdań wspólprawdziwych w jednym z wielu modeli

 

 

    O sztuce definiowania.

    „Gdy Platon podał definicję „Człowiek jest to istota żywa, dwunożna, nieopierzona” i tą definicją chełpił się i zdobył poklask, Diogenes oskubał koguta i zaniósł do szkoły na wykład Platona, mówiąc „Oto jest człowiek Platona”. Odtąd do tej definicji dodawano słowa: „o szerokich pazurach””. ( W oryginale Πλατων = Platon, πλατωνυχοζ- „o szerokich pazurach” )

„Żywoty i poglądy słynnych filozofów” Diogenes Laertios. O Diogenesie z Synopy, str. 331. PWN Wydanie 3. Warszawa 1982

Przekład: Irena Krońska, Kazimierz leśniak, Witold Olszewski przy współpracy Bogdana Kupisa. Opracowanie przekładu, przypisy ( jak ten powyżej w nawiasie wyjaśniający znaczenie greckiej gry słów) i skorowidz – Irena Krońska.

 

    Wygląda na to że Platonowi jako pierwszemu, za sprawą Diogenesa z Synppy, przydażyło się odkryć modele niestandardowe.

    Pozwolę sobie zacytować fragment z książki „Współczesne teorie Prawdy” Zbigniewa Tworaka ( Ksiązka świetna – autorem jest wykładowca Uniwersytetu Adama Mickiewicza w Poznaniu. Polecam – proszę się nie zrażać ewentualnym poglądem na moją osobę czy poglądy – Tworak prezentuje bardzo normalne, zdrowe matematycznie podejście do poruszanego tematu, a ja cytuję złośliwie nieadekwatny dla książki fragment „filozoficzny” ). Cytat jednak , aby uczynic go zrozumiałym, poprzedze krótkim przypomnieniem tematyki związanej z Semantyczną teorią Prawdy Tarskeigo. Chodzi o kilka uwag na temat hierarchii języków.

    Jak wiadomo Sematyczna Koncepcja Prawdy, definiuje pojęcie prawdy nawiązując  do korespondencyjnej teorii prawdy w sposób następujący:

( T ) Zdanie „A” jest prawdziwe wtedy i tylko wtedy gdy A

przy czym „A” ( z cudzysłowem) to zdanie wypowiedziane w języku przedmiotowym ( powiedzmy w teorii mnogości, czy arytmetyce Peano),  zaś kryterium T sformowane jest w metajęzyku czyli języku nadrzędnym tego języka, i jego elementem jest zdanie A wyrażajace korespondującą treść. Od Tarskiego pochodzi podstawowy przykład użycia tej hierarchii:  „Zdanie „śnieg jest biały” jest prawdziwe wtedy i tylko wtedy gdy śnieg jest biały.” Należy przy tym rozumieć że prawdziwość zdania śnieg jest biały w metajęzyku odnosimy do konstrukcji teoretycznej związanej z metajęzykiem ( nie chodzi tu o jakiekolwiek empiryczne stwierdzanie czy śnieg jest biały, a jedynie o prawdziwość tego zdania w metajęzyku). Mówi się w tym kontekście że prawda została tym samym zrelatywizowana do poziomu języka. Aby analizować własności logiczne  metajęzyka należałoby w tym miejscu dokonać jego formalizacji, a pytanie o prawdziwość zdań metajęzyka J_{n} wymaga w tym miejscu odwołanie się do meta-meta języka J_{(n+1)}. Działanie takie ma na celu wyeliminowanie z języka paradoksu kłamcy – zdania samozwrotne jak na przykład zdanie „Ja kłamię” zostają z języka wyeliminowane jako mieszające poziomy języka i metajęzyka. Wyeliminowanie antynomii kłamcy sprawia że teorie aksjomatyczne o aksjomatach niesprzecznych powinny poprawnie formułować twierdzenia prawdziwe ( zbiór konsekwencji zbioru zdań prawdziwych zawiera wyłącznie zdania prawdziwe). W szczególności zdania prawdziwe języka J_{n} dają się zinterpretować ( są prawdziwe) w metajęzyku języka J_{(n+1)} , jednak predykat prawdy metajęzyka J_{(n+1)} jest istotnie szerszy niż to co można o prawdzie powiedzieć w języku przedmiotowym ( który może być metajęzykiem dla teorii o języku niższego rzędu), w którym jak wiadomo z prac tarskeigo – predykatu prawdy zdefiniować się nie da. Oztatnie zdanie oznacza że kryterium (T) jest nieprzekładalne z metajęzyka, w którym jest wypowiedziane, do języka o którego prawdziwości zdań mówi.

    Stosując taką konstrukcję uzyskujemy pewien zadowalający z punktu widzenia matematyki efekt. Możemy jednak zapytać o jej ścisłe uzasadnienie, to znaczy o teorię hierarchii języków i metajęzyków. Dalej następuje cytat z książki Tworaka ( strona 56).
 

    „Weźmy zdania:

(40) Jakiekolwiek zdanie prawdziwe na jakimś poziomie m hierarchii języków Tarskiego jest tez prawdziwe na każdym n> m. Nie istnieje stopień najwyższy w hierarchii języków Tarskiego.

    Można się nimi posłużyć, opisując teorię Tarskiego. Za pomoca pierwszego stwierdzamy że hierarchia języków (H) ma charakter kumulatywny. Za pomocą drugiego stwierdzamy że nie istnieje górna granica owej hierarchii. Ponieważ dotyczą one każdego poziomu hierarchii języków (H), więc stopień ich jest większy od dowolnego n \in \omega co powoduje że nie są one zdaniami żadnego z języków owej hierarchii. Sugeruje to, że sa one pozbawione sensu. W efekcie niemożliwe staje się sformułowanie ogólnej teorii hierarchii języków. Teoria taka musiałaby być sformułowana w jezyku, który byłby metajęzykiem dla każdego języka z hierarchii (H), co jest jednak niemożliwe, ponieważ jest ona teorią ogólna. Argument ten mozna by nazwać paradoksem hierarchii języków.
    Uwaga 30. Nawiązując do antynomii kłamcy, rozważmy  zdanie:

(41) Niniejsze zdanie nie jest prawdziwe na żadnym poziomie hierarchii języków Tarskiego

    i zapytajmy czy jest ono prawdziwe. Otrzymamy sprzeczność gdyż z każdej odpowiedzi wynika jej negacja.[…]

    Ale przecież opisując ów paradoks, używam pewnego – jak się wydaje – uniwersalnego lub ostatniego (meta)języka, który – przypuszczalnie da sie sformalizować.  […] A zatem[…] hierarchia języków nie jest domknięta. Dokładniej język w którym opisujemy hierarchię (H) nie może być jej elementem. W praktyce współczesnej logiki w roli „ostatniego” (meta)języka występuje zwykle jakiś język naturalny, do którego – pod groźba sprzeczności – nie stosuje sie rozwiązania Tarskiego, tzn. nie jest on elementem hierarchii (H).
    Ostatecznie uzyskujemy uzasadnienie że (1) opis języka naturalnego oparty na hierarchii (H) jest nieadekwatny, oraz (2) istnieją nieuniknione ograniczenia formalizacji. W zwięzły sposób ujmuje to J.Woleński:

    „[A]by cokolwiek [tj. jakikolwiek język] mogło być sformalizowane, coś innego [tj. pewien język] musi pozostać niesformalizowane ((Woleński „Matematyka a epistemologia” 1993 s. 32)”

    Pełniejszy cytat z Woleńskiego to:

    „Analiza statusu teori typów logicznych czy schematu hierarchii języków skłania do umiaru w naszych pretensjach poznawczych, oraz dostarcza intuicyjnych argumentów na rzecz tezy o nieuniknionych ograniczeniach formalizcji: aby cokolwiek mogło być sformalizowane, coś innego musi pozostać niesformlizowane. Z tego wynika, że formalizacja dfowolnego segmentu ciągu (8) [języków i metajzyków] zakłada istnienie jakiegoś języka niesformalizowanego, oraz że ogólny opis tego fenomenu nie da sie inaczej wyrażić jak tylko nieformalnie, co wcale  nie znaczy, że nieprecyzyjnie lub sprzecznie. ” ( Woleński „Matematyka a epistemologia” 1993 s. 31-32 )

    U źródeł Semantycznej Teorii Tarskiego stoi dwojaka motywacja. Po pierwsze, dzięki rozbiciu języków formalnych na język i metajęzyk, wyeliminowano z teorii formalnych antynomię kłamcy. Zdania samozwrotne nie są uważane za zdania poprawne. Po drugie wypowiedziano pewien predykat, podano konstrkcję, której celem jest formalizacja pojęcia prawdy. Konstrukcja ta odwołuje się do mechanizmów językowych, Tarski bardzo wyraźnie dawał do zrozumienia, że jego teoria nie wymusza zajęcia stanowiska w kwestii sporu jak „ostatecznie” określa się prawdziwość zdania w metajęzyku „śnieg pada” –  czy wyglądając za okno, czy – szukając odpowiedzi w Biblii. W szczególności Tarski pisał w pracy „Z badań metodologicznych nad definiowalnościa prawdy”, Przegląd filozoficzny 1944  ( cytat za J. Woleński Epistemologia, który cytuje tu ta pracę na podstawie przedruku z wydania dzieł Tarskeigo,  str. 340):

    „Możemy […] przyjać semantyczną koncepcję prawdy nie porzucajac własnego stanowiska epistemologicznego, jakiekolwiek by ono było; możemy pozostać naiwnymi realistami, krytycznymi realistami lub metafizykami – kimkolwiek bylismy wcześniej”

    Wydaje się zatem że Tarski stał na stanowisku istotnie różnym niż naiwna teoria korespondencyjna prawdy Arystotelesa, który jako kryterium prawdy widział zdanie: „pogląd jest prawdziwy gdy rzeczy istotnie mają sie tak jak ów pogląd stwierdza” co w języku potocznym brzmi niemal identycznie jak w (T). STP Tarskiego odnosi sie do semnatyki języka, zaś jej odniesienie do zjawisk empirycznych jest tylko jedną z mozliwych interpretacji, bynajmniej nie najbardziej owocną czy ciekawą.  Warto w tym miejscu zastanowić się jednak nad nastepującym paradoksem sformułowanym przez Kripkego. Został on opisany w ksiażce Tworaka w następujacy sposób. Bohaterami naszej historyjki sa dziennikarzyna Jones i wybitny polityk Nixon. Załóżmy że Jones w jednym ze swoich artykułów napisał:

(J) „Wiekszość wypowiedzi Nixona o aferze Watergate jest fałszywych.

I że jest to jedyna wypowiedź Joensa o aferze Watergate jaką uczynił zanim nieznani sprawcy zastrzelili go z broni palnej. Nixon zaś, wypowiedział następujacą kwestię:

(N) „Wszystkie wypowiedzi Joensa o aferze Watergate są prawdziwe”

    Wydaje się zasadne by nie dopatrywać się samozwrotności w żadnym ze zdań (J) czy (N). Każde z tych zdań wypowiada inna osoba i dotyczą one wypowiedzi innej osoby. Wydaje sie że samozwrotność tutaj jest jest cechą całego systemu zdań. Jak zastosować kryterium Tarskiego o niemieszaniu języka i metajęzyka? Paradoks ten jest wzorowany na ogólniejszym paradoksie zdefiniowanym dla n zdań, każde z nich stwierdza że następne jest fałszywe, zaś n-te stwierdza żę pierwsze mówi prawdę. Paradoks ten nosi nazwę paradoksu „Koła kłamców”.

    Zauważmy jednak że nie tylko fakt „kolistości w zespole” jest tu ciekawy, nie dlatego przytoczyłem zdania (J) i (N). Problem jest znacznie ciekawszy. Każda próba rozstrzygnięcia czy system (J) i (N) jest paradoksalny czy nie, musi odwołać się do ustaleń ile X zdań wypowiedział Nixon na temat afery Watergate. W zależności od relacji liczowych zdań prawdziwych do liczby X, zdanie (J) jest prawdziwe lub nie, a tym samym zostaje ustalona prawdziwość zdania (N). Dla pewnych sytuacji nie powstaje tu żadna antynomia! Z sytuacją antynomii mamy do czynienia tylko w wypadku kiedy „wśród wypowiedzi Nixona dotyczących afery Watergate różnych od (N) albo (1) zdań fałszywych jest tyle samo co zdań prawdziwych, albo (2) liczba zdań fałszywych jest o jeden wieksza. Wówczas zarówno (J), jak i (N) są antynimialne[…]” (z ksiązki Tworaka, analiza za Krajewski „W obronie zdań samozwrotnych” Przegląd filozoficzny 2. 1992). Jest to argument za tym, że samozwrotność z antynomiami nie ma w istocie aż tak wiele wspólnego jak się powszechnei uważa….

 

Ksiązki cytowane w tekście:

Zbigniew Tworak „Współczesne teorie prawdy” Wydawnictwo Naukowe UAM, Poznań 2009

Jan Woleński „Epistemologia. Poznanie, prawda, wiedza, realizm” Wydawnictwo Naukowe PWN, Warszawa 2007

Jan Woleński „Matematyka a epistemologia” Wydawnictwo Naukowe PWN, Warszawa 1993

 

 

   

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

Dołącz do 256 obserwujących.

%d blogerów lubi to: