Teoria operacji łącznej, przemiennej i idempotentnej (Cz.0)

Wstęp

Operacje rozpatrywane w niniejszej nocie występują w logice, w teorii mnogości, w algebrach Boole'a, i ogólniej w kratach Birkhoffa, a te ostatnie występują z kolei w wielu działach matematyki.

"Teoria" - słowo rozpoczynające tytuł niniejszej noty - brzmi dumnie i szumnie, ale formalna teoria operacji [;\Upsilon;] opisanych w tytule jest tylko malutką i bardzo skromną "teorią". Na ogół traktuje się ją jako coś oczywistego. I słusznie. Moim celem jest jednak więcej niż pedantyczny opis i formalny dowód pewnych (raczej oczywistych) własności, konieczny dla dalszego działania w logice od podstaw. Przy okazji, na łatwym materiale, można będzie zaobserwować styl matematycznej logiki, ważny zarówno w matematyce jak i w informatyce. Zobaczymy, że w przypadku teorii operacji [;\Upsilon;], o własnościach podanych w tytule artykułu, jednomiany - mimo gęstwy nawiasów i innych komplikacji - są w istocie (z dokładnością do pewnej równoważności [;\equiv;]) we wzajemnie jednoznacznej odpowiedniości ze skończonymi, niepustymi zbiorami zmiennych.

Chodzi o teorię jednomianów. Rozpadają się one na pewne równoważne klasy. Pokażemy, że każda klasa zawiera dokładnie jeden jednomian kanoniczny. Istnienie w matematyce jednoznacznych reprezentantów kanonicznych (gdy rzeczywiście istnieją) jest silnym narzędziem, upraszczającym teorię, wygodnym przy dowodach twierdzeń.

NOTACJA

Żeby uniezależnić się od przyzwyczajeń, będę używał dwóch dosyć rzadko stosowanych symboli, przede wszystkim [;\Upsilon;] (grecka duża litera upsilon), ale także  [;\equiv;]  (równoważność). Należą one do naszej formalnej teorii. Ponadto będę używał ciągu symboli  [;x'\ x''\ x'''\ \ldots;] , nazywanych zmiennymi. Są one uporządkowane właśnie tak. Dla wygody, mając na myśli jedną z tych zmiennych będę pisał na przykład [;x;] lub [;y;] lub [;z;], itd., ale te ostatnie symbole (bez prima) już nie należą do samej teorii. Cały czas, gdy się widzi taki nieformalny symbol, to należy wyobrażać sobie jeden z symboli [;x'\ x''\ \ldots;] . Na koniec, teoria posiada również dwa dodatkowe znaki, mianowicie okrągłe nawiasy [;(\ );].

Oprócz znaków teorii będziemy także stosować pewien znak metateoretyczny  [;\vdash;].

Wybiegając nieco naprzód, wspomnę już teraz, że nie tylko dla wygody, ale także z metamatematycznej konieczności, będziemy używać dużych liter [;A\ B\ \ldots\ J;], być może z primami, dla oznaczenia jednomianów takich jak

            [;\left(\left(x'''\Upsilon x'\right)\Upsilon x'''''\right);]

i podobnych, co ściśle opiszę poniżej, w następnym paragrafie. Czasem, dla poprawienia czytelności (z punktu widzenia człowieka), będę wstawiał odstępy wewnątrz jednomianu, na przykład tak:

            [;\left(\left(x'''\,\Upsilon x'\,\right)\ \Upsilon\ x'''''\right);]

Jednak dla prostoty umówmy się, że tych odstępów w jednomianach nie ma, że to tylko takie złudzenie optyczne (nie jesteśmy robotami, trochę bujać musimy).

Podobnie będę używał dużych liter [;K\ L\ \ldots\ Z;] dla oznaczenia zdań teorii, czyli wyrażeń typu

            [;(\left(\left(x'''\,\Upsilon x'\,\right)\ \Upsilon\ x'''''\right)\ \equiv\ (\left(\left(x'''''\,\Upsilon x'\,\right)\ \Upsilon\ x'''\right);]

Ścisły opis podam w drugim paragrafie poniżej, po paragrafie opisującym jednomiany.

Poprawnie zapisane jednomiany

Poprawnie zapisane jednomiany lub po prostu jednomiany definiujemy następująco:

1. Zmienna jest jednomianem (na przykład [;x'''';] jest jednomianem).
   
2. Jeżeli struny znaków  [;A;]  i  [;B;]  są jednomianami, to także struna:
   
               [;(A\Upsilon B);]
   jest jednomianem.


3. Wszystkie jednomiany są otrzymane przez (skończone) iterowanie powyższych dwóch reguł - innych jednomianów nie ma.

Na przykład, co nietrudno sprawdzić, jednomianem jest następująca struna:

            [;\left(x'\Upsilon \left(x''\Upsilon\left( x'''\Upsilon x''''\right)\right)\right);]

Jednomiany jednoznacznie rozkładają się na mniejsze, aż po zmienne (informatycy powiedzieliby, że jednomiany jednoznacznie się parsują): jeżeli [;C;] jest jednomianem, to albo [;C;] jest jedną ze zmiennych, albo istnieją (jednoznacznie wyznaczone) jednomiany [;A\ B;] takie, że [;C;] jest struną  [;(A\Upsilon B);]. Zachodzi przy tym jednoznaczność: jeżeli także [;D\ E;] są jednomianami takimi, że struna  [;(D\Upsilon E);]  jest jednomianem [;C;], to struna [;D;] jest identyczna (znak po znaku) ze struną [;A;], oraz struna [;E;] jest identyczna ze struną [;B;].

Poprawnie zapisane zdania

Poprawnie zapisanym zdaniem lub po prostu zdaniem nazywamy struny postaci

            [;A\equiv B;]

gdzie [;A\ B;] są dwoma dowolnymi jednomianami (niekoniecznie różnymi). Innych zdań nie ma (w naszej teorii).

Na przykład zdaniem jest struna

            [;x'\ \equiv\ (((x'\Upsilon(x'\Upsilon x'))\Upsilon x');]

(Należy udawać, że odstępów wokół znaku równoważności nie ma, jako że w teoretycznym zapisie ich nie ma - dałem je dla zwiększenia czytelności). Wolno też, dla lepszej czytelności, zdania zawrzeć w nawiasach:

            [;(A\equiv B);]

na przykład:

            [;(x'\ \equiv\ (((x'\Upsilon(x'\Upsilon x'))\Upsilon x'));]

Teoria operacji łącznej, przemiennej i idempotentnej operacji [;\Upsilon;]

Poprzednie paragrafy były etapami wstępnymi metateorii naszej teorii. Celem metateorii jest wydzielenie (zdefiniowanie) twierdzeń ze zbioru wszystkich zdań. Czyni się to definiując dowód. Sam dowód twierdzenia należy do teorii. Natomiast objaśnienie dowodu już do metateorii, co wkrótce zobaczymy. Celem samej teorii jest odpowiedź na pytanie typu: czy dane zdanie [;K;] jest twierdzeniem? W przypadku teorii złożonych takie pytania mogą być bardzo trudne, a nawet nierozstrzygalne. W przypadku prostych teorii, jak ta rozwijana tutaj, metateoria jest w stanie nie tylko twierdzenia wydzielić spośród zdań w sensie teoretycznym (niekonstruktywnym, niealgorytmicznym), ale wręcz potrafi zbiór wszystkich twierdzeń określić konkretnie (algorytmicznie). Chociaż takie teorie są uważane na ogół za nieciekawe, to sam akt wykazania, że teoria jest nieciekawa, może być bardzo ciekawy.

Gdy chcemy powiedzieć, że zdanie [;K;] jest twierdzeniem, to krótko zapisujemy to metateoretycznie tak:

            [;\vdash\,K;]

gdzie po lewej stronie znaku [;\vdash;] nie ma niczego (żadnego zdania). Podobnie zapisujemy twierdzenia relatywne. Na przykład, gdy chcemy powiedzieć, że zdanie [;M;] wywodzi się ze zdań [;K\ L;], to zapisujemy to metateoretycznie jako:

            [;K\ L\ \vdash\ M;]

(tym razem odstęp po lewej pomiędzy [;K;] oraz [;L;] jest pożądany, by było widać, że mamy dwa zdania; w przyszłości moglibyśmy używać oznaczeń wieloliterowych, i wtedy odstęp pozwalałby nam widzieć, gdzie się kończy jedna nazwa i zaczyna druga - mówimy o oznaczeniach metateoretycznych, a nie wewnątrz jednomianów).

Definiuje się to wszystko (twierdzenia i dowody) za pomocą reguł dowodzenia, w tym aksjomatów, które formułuje się dla specyficznych zdań. Dla większej ekspresywności korzysta się jednak z całych schematów, gdzie zamiast zmiennych występują metasymbole dowolnych jednomianów i zdań. Każde podstawienie za symbol zdania lub jednomianu konkretnego zdania lub odpowiednio jednomianu daje wtedy konkretną regułę, czyli każdy schemat reprezentuje nieskończenie wiele reguł.

UWAGA o:  gdy podstawiamy strunę zdania (odpowiednio - jednomianu) za metasymbol w regule, to czynimy to dla wszystkich wystąpień tego symbolu w regule, podstawiając przy tym za każdym razem tę samą strunę.

A teraz do rzeczy - nasza teoria jest określona przez następujące 7 schematów reguł (w tym 4 schematów aksjomatów), w których [;A\ B\ C;] są dowolnymi jednomianami:

1. [;\vdash\ A\ \equiv\ A;]


2. [;(A\ \equiv\ B)\ \vdash\ (B\ \equiv\ A);]


3. [;(A\equiv B)\ \ (B\equiv C)\quad \vdash\quad (A\equiv\ C);]


4. [;\vdash\ (A\Upsilon A)\ \equiv\ A;]


5. [;\vdash\ (A\Upsilon B)\ \equiv\ (B\Upsilon A);]


6. [;\vdash\ ((A\Upsilon B)\Upsilon C)\ \equiv\ (A\Upsilon(B\Upsilon C));]


7. [;(A\equiv B)\ \vdash\ ((A\Upsilon C)\, \equiv\, (B\Upsilon C));]

Widzimy, że reguły 1,4,5 oraz 6 są aksjomatami (ściślej mówiąc, chodzi o schematy). Ostatnia reguła 7, wspólnie z regułą 5, mówi nam, że operacja [;\Upsilon;] indukuje operację na klasach jednomianów - więcej o tym potem.

Dowodem konkretnego zdania [;Z;] w naszej teorii nazywamy skończony ciąg zdań, z których każde jest albo aksjomatem albo jest otrzymane z jednej z reguł dowodzenia, przy czym ostatnie zdanie ciągu jest zdaniem [;Z;]. Zdania, dla których istnieje dowód, nazywamy twierdzeniami. Często dowodzi się nie pojedyncze twierdzenia, lecz całe schematy twierdzeń - za pomocą schematów dowodów. W schematach twierdzeń i dowodów zamiast zmiennych występują symbole oznaczające jednomiany (czyli zmienne jednomianowe).

W teorii podaje się tylko gołe dowody (czyli ciągi), podczas gdy w metateorii te dowody objaśnia się, podając explicite numery schematów reguł, z których się korzysta, oraz rodzaj podstawień - chociaż czytelnik w zasadzie może sam wszystko znaleźć (może nawet sobie napisać program komputerowy), to objaśnienia ogromnie ułatwiają przeczytanie dowodu ze zrozumieniem, i ułatwiają sprawdzenie poprawności. W praktyce, teksty matematyczne zawsze są trochę metateoretyczne (mimo, że niekompletne), jako że dowody są objaśniane.

Przykłady dowodów i schematów dowodów

Udowodnijmy zdanie:

            [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x'\,\Upsilon\,x''));]

Niech symbol [;A;] oznacza jednomian  [;(x'\Upsilon x'');].  Wtedy powyższe zdanie jest postaci:

            [;(A\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,A);]

a więc podpada pod schemat aksjomatu 5. Czyli nasz dowod ma jeden krok - z miejsca możemy napisać, że rozpatrywane zdanie jest aksjomatem:

            [;\vdash\ ((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x'\,\Upsilon\,x''));]

Uffff, nie taki straszny wilk jak go malują :-) No to rozpatrzmy z kolei zdanie:

            [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x'));]

Jego goły dowód wygląda nastepująco (dla wygody kolejne zdania w dowodzie ponumerujemy):

1. [;(x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x');]


2. [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ ((x''\,\Upsilon\,x')\,\Upsilon\,x''');]


3. [;((x''\,\Upsilon\,x')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x'));]


4. [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x'));]

Ostatnie zdanie było naszym celem, czyli zakończyliśmy dowód żądanego twierdzenia. A teraz objaśnienia (przywołuję w nich zdania z powyższego dowodu w postaci "tw.2" dla

            [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ ((x''\,\Upsilon\,x')\,\Upsilon\,x''');],

itp.):

1. [;\vdash\ ((x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x'));]   -   schemat aksjomatyczny 5.


2. [;(x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x')\ \vdash\ ((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ ((x''\,\Upsilon\,x')\,\Upsilon\,x''');]   -   schemat reguł 7.


3. [;\vdash\ (((x''\,\Upsilon\,x')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x')));]   -   schemat aksjomatyczny 5.


4. [;\vdash\ (((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x')));]   -   schemat reguł 3.

W podobny sposób możemy dowieść schemat twierdzeń:

            [;((A\,\Upsilon\,B)\,\Upsilon\,C)\ \equiv\ (C\,\Upsilon\,(B\,\Upsilon\,A));]

Oto goły dowód:

1. [;(A\,\Upsilon\,B)\ \equiv\ (B\,\Upsilon\,A);]


2. [;((A\,\Upsilon\,B)\,\Upsilon\,C)\ \equiv\ ((B\,\Upsilon\,A)\,\Upsilon\,C);]


3. [;((B\,\Upsilon\,A)\,\Upsilon\,C)\ \equiv\ (C\,\Upsilon\,(B\,\Upsilon\,A));]


4. [;((A\,\Upsilon\,B)\,\Upsilon\,C)\ \equiv\ (C\,\Upsilon\,(B\,\Upsilon\,A));]

Objaśnienia tego dowodu wyglądają podobnie jak w przypadku objaśnień dowodu konkretnego twierdzenia.