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.