Saturday, February 26, 2011
Thursday, December 2, 2010
Teoria operacji łącznej, przemiennej i idempotentnej (Cz.3)
Niniejsza Część 3 jest kontynuacją poprzednich - oto linki:
Część 0 Część 1 Część 2
Teoria operacji [;\Upsilon;] jest tak prosta, że nie zawiera teorii mnogości (ani nawet pełnej logiki). Mimo to teoria ta pozwala rozważać kwestie skończoności. Jest tak dlatego, że zawiera nieskończony ciąg zmiennych:
[;x'\ x''\ \x'''\ \ldots;]
gdzie każda następna zmienna jest cięższa od poprzedniej (ma więcej primów, co można stwierdzić fizycznie). Gdyby na przykład w pewnym jednomianie występowało nieskończenie wiele zmiennych, to żadna nie byłaby wśród nich najcięższa. Za chwilę zobaczymy, że tak jednak nie jest, czyli liczba zmiennych występujących w jednomianie jest skończona:
TWIERDZENIE 0 Wśród zmiennych występujących w dowolnym jednomianie [;A;] istnieje zmienna najcięższa.
DOWÓD Jeżeli jednomian [;A;] jest zmienną, powiedzmy zmienną [;x;], to w [;A;] występuje dokładnie jedna zmienna (właśnie [;x;]), i jest ona najcięższa (nie ma konkurencji).
Pozostał przypadek jednomianu [;A;] postaci [;(B\Upsilon C);]. Wtedy (indukcja) mają one swoje najcięższe zmienne, odpowiednio [;x;] w [;B;] oraz [;y;] w [;C;]. Niech [;z;] będzie tą z nich, która nie jest lżejsza od pozostałej. Zatem [;z;] występuje w [;A;] - t.zn. w [;(B\Upsilon C);], przy czym jest cięższe od każdej innej zmiennej, występującej w [;A;].
W świetle powyższego wyniku wolno nam sformułować następujące, jednoznaczne pojęcie (będzie poprawne):
DEFINICJA 0 Ciężarem jednomianu nazywamy jego najcięższą zmienną.
UWAGA 0 Jednomiany równoważne mają tę samą wagę; patrz Część 2, Twierdzenie 1.
Na przykład ciężarem zmiennej jest ona sama.
Jednomiany zostały zdefiniowane w Części 0. Jednomiany standardowe definiujemy następująco:
Widzimy, że jednomiany standardowe są albo zmiennymi albo kończą się na pojedynczą zmienną, stanowiącą jeden z dwóch głównych członów jednomianu. Z tego powodu jednomian
[;(x'\,\Upsilon\,(x''\Upsilon x'''));]
nie jest standardowy. Podobnie nie jest standardowy jednomian
[;((x'\Upsilon x''')\,\Upsilon\,x'');]
Tym razem dlatego, że zmienna na zakończeniu struny nie jest najcięższa. Natomiast standardowym jest jednomian:
[;(((x'' \Upsilon x''''')\,\Upsilon\,x'''''')\,\Upsilon\,x''''''''');]
Ogólnie, w jednomianach standardowych, od lewej do prawej, każda następna zmienna jest cięższa od poprzedniej; więc w standardowym jednomianie żadna zmienna nie występuje dwa razy.
TWIERDZENIE 1 Niech [;A\ B;] będą dwoma dowolnymi jednomianami standardowymi. Wtedy następujące warunki są równoważne:
DOWÓD Implikacja [;1.\Rightarrow 2.;] zachodzi na mocy aksjomatu 1.; patrz Część 0.
Implikacja [;2.\Rightarrow 3.;] zachodzi na mocy Twierdzenia 1 z Części 1.
Udowodnię implikację [;3.\Rightarrow 1.;] Gdy [;A;] jest zmienną, to [;B;], będąc standartdowe i mając te same zmienne, jest tę samą zmienną, czyli jednommiany [;A\ B;] są identyczne.
Zastosujmy teraz indukcję po ciężarze [;A;]. Gdy jest najlżejsze, czyli jest zmienną [;x';], to implikacja zachodzi. I ogólnie, gdy [;A;] jest zmienną. Gdy nie jest zmienną, to jest postaci [;C\Uspilon x;], gdzie [;x;] jest zmienną, [;C;] jest jednomianem standardowym, oraz [;x;] jest cięższe od każdej zmiennej występującej w [;C;]. Ale [;B;] ma te same zmienne, więc też jest postaci [;D\Uspilon x;], gdzie [;D;] jest jednomianem standardowym, oraz [;x;] jest cięższe od każdej zmiennej występującej w [;D;]. Ponieważ w jednomianach [;A\ B;] występują dokładnie te same zmienne, to także w jednomianach [;C\ D;] występują dokładnie te same zmienne (te co w [;A;], tylko bez [;x;]). Zatem na mocy indukcji jednomiany [;C\ D;] są identyczne. Zatem jednomiany [;A\ B;] są identyczne.
Już pora:
TWIERDZENIE 2 Dla dowolnego jednomianu istnieje dokładnie jeden równoważny mu jednomian standardowy.
DOWÓD Niech [;A;] będzie dowolnym jednomianem. Mamy pokazać istnienie i jedyność jednomianu standardowego [;B;], takiego że
[;A\ \equiv\ B;]
Jedyność wynika z Twierdzenia 1, powyżej. Skupmy się więc na istnieniu.
Gdy [;A;] jest zmienną, powiedzmy [;x;], to samo [;A;] jest standardowe, czyli standardowe [;B;] istnieje, jest samym [;A;].
W pozostałym przypadku, gdy [;A;] nie jest zmienną, to [;A;] jest równoważne pewnemu jednomianowi [;(C\Upsilon x);], gdzie [;x;] jest najcięższą zmienną, występującą w [;A;], oraz [;C;] jest jednomianem, w którym [;x;] nie występuje; patrz Część 2, Twierdzenie 2. Czyli mamy
[;(C\,\Upsilon\,x)\ \equiv\ A;]
Przy tym jednomian [;C;] jest lżejszy od [;A;]. Istnieje więc (indukcja) jednomian standardowy [;D;], równoważny z [;C;]. Zatem:
[;(D\,\Upsilon\,x)\ \equiv\ A;]
Więc jednomian standardowy [;(D\,\Upsilon\,x);] jest pożądanym jednomianem [;B;].
Widzimy, że klasy równoważności jednomianów są we wzajemnie jednoznacznej odpowiedniości z niepustymi podzbiorami ciągu zmiennych
[;x'\ x''\ \x'''\ \ldots;]
Można uważać teorię operacji [;\Upsilon;] za teorię zbiorów skończonych. Może ona jednak także sł¨żyć za odskocznię do wielu bogatszych teorii, jak logika, arytmetyka, algebra, itd.
Skończoność
Teoria operacji [;\Upsilon;] jest tak prosta, że nie zawiera teorii mnogości (ani nawet pełnej logiki). Mimo to teoria ta pozwala rozważać kwestie skończoności. Jest tak dlatego, że zawiera nieskończony ciąg zmiennych:
[;x'\ x''\ \x'''\ \ldots;]
gdzie każda następna zmienna jest cięższa od poprzedniej (ma więcej primów, co można stwierdzić fizycznie). Gdyby na przykład w pewnym jednomianie występowało nieskończenie wiele zmiennych, to żadna nie byłaby wśród nich najcięższa. Za chwilę zobaczymy, że tak jednak nie jest, czyli liczba zmiennych występujących w jednomianie jest skończona:
TWIERDZENIE 0 Wśród zmiennych występujących w dowolnym jednomianie [;A;] istnieje zmienna najcięższa.
DOWÓD Jeżeli jednomian [;A;] jest zmienną, powiedzmy zmienną [;x;], to w [;A;] występuje dokładnie jedna zmienna (właśnie [;x;]), i jest ona najcięższa (nie ma konkurencji).
Pozostał przypadek jednomianu [;A;] postaci [;(B\Upsilon C);]. Wtedy (indukcja) mają one swoje najcięższe zmienne, odpowiednio [;x;] w [;B;] oraz [;y;] w [;C;]. Niech [;z;] będzie tą z nich, która nie jest lżejsza od pozostałej. Zatem [;z;] występuje w [;A;] - t.zn. w [;(B\Upsilon C);], przy czym jest cięższe od każdej innej zmiennej, występującej w [;A;].
KONIEC DOWODU
W świetle powyższego wyniku wolno nam sformułować następujące, jednoznaczne pojęcie (będzie poprawne):
DEFINICJA 0 Ciężarem jednomianu nazywamy jego najcięższą zmienną.
UWAGA 0 Jednomiany równoważne mają tę samą wagę; patrz Część 2, Twierdzenie 1.
Na przykład ciężarem zmiennej jest ona sama.
Jednomiany standardowe
Jednomiany zostały zdefiniowane w Części 0. Jednomiany standardowe definiujemy następująco:
- Zmienna jest jednomianem standardowym
- Jeżeli [;A;] jest jednomianem standardowym oraz [;x;] jest zmienną cięższą od każdej zmiennej występującej w [;A;], to jednomian [;(A\Upsilon x);] jest standardowy.
- Wszystkie jednomiany standardowe otrzymane są przez stosowanie powyższych dwóch metod (ich skończonych iteracji) - innych jednomianów standardowych nie ma.
Widzimy, że jednomiany standardowe są albo zmiennymi albo kończą się na pojedynczą zmienną, stanowiącą jeden z dwóch głównych członów jednomianu. Z tego powodu jednomian
[;(x'\,\Upsilon\,(x''\Upsilon x'''));]
nie jest standardowy. Podobnie nie jest standardowy jednomian
[;((x'\Upsilon x''')\,\Upsilon\,x'');]
Tym razem dlatego, że zmienna na zakończeniu struny nie jest najcięższa. Natomiast standardowym jest jednomian:
[;(((x'' \Upsilon x''''')\,\Upsilon\,x'''''')\,\Upsilon\,x''''''''');]
Ogólnie, w jednomianach standardowych, od lewej do prawej, każda następna zmienna jest cięższa od poprzedniej; więc w standardowym jednomianie żadna zmienna nie występuje dwa razy.
TWIERDZENIE 1 Niech [;A\ B;] będą dwoma dowolnymi jednomianami standardowymi. Wtedy następujące warunki są równoważne:
- Jednomiany [;A\ B;] są identyczne (jako struny, znak po znaku);
- [;\vdash\ A\,\equiv\,B;]
- W jednomianach [;A\ B;] występują dokładnie te same zmienne.
DOWÓD Implikacja [;1.\Rightarrow 2.;] zachodzi na mocy aksjomatu 1.; patrz Część 0.
Implikacja [;2.\Rightarrow 3.;] zachodzi na mocy Twierdzenia 1 z Części 1.
Udowodnię implikację [;3.\Rightarrow 1.;] Gdy [;A;] jest zmienną, to [;B;], będąc standartdowe i mając te same zmienne, jest tę samą zmienną, czyli jednommiany [;A\ B;] są identyczne.
Zastosujmy teraz indukcję po ciężarze [;A;]. Gdy jest najlżejsze, czyli jest zmienną [;x';], to implikacja zachodzi. I ogólnie, gdy [;A;] jest zmienną. Gdy nie jest zmienną, to jest postaci [;C\Uspilon x;], gdzie [;x;] jest zmienną, [;C;] jest jednomianem standardowym, oraz [;x;] jest cięższe od każdej zmiennej występującej w [;C;]. Ale [;B;] ma te same zmienne, więc też jest postaci [;D\Uspilon x;], gdzie [;D;] jest jednomianem standardowym, oraz [;x;] jest cięższe od każdej zmiennej występującej w [;D;]. Ponieważ w jednomianach [;A\ B;] występują dokładnie te same zmienne, to także w jednomianach [;C\ D;] występują dokładnie te same zmienne (te co w [;A;], tylko bez [;x;]). Zatem na mocy indukcji jednomiany [;C\ D;] są identyczne. Zatem jednomiany [;A\ B;] są identyczne.
KONIEC DOWODU
Twierdzenie podstawowe
Już pora:
TWIERDZENIE 2 Dla dowolnego jednomianu istnieje dokładnie jeden równoważny mu jednomian standardowy.
DOWÓD Niech [;A;] będzie dowolnym jednomianem. Mamy pokazać istnienie i jedyność jednomianu standardowego [;B;], takiego że
[;A\ \equiv\ B;]
Jedyność wynika z Twierdzenia 1, powyżej. Skupmy się więc na istnieniu.
Gdy [;A;] jest zmienną, powiedzmy [;x;], to samo [;A;] jest standardowe, czyli standardowe [;B;] istnieje, jest samym [;A;].
W pozostałym przypadku, gdy [;A;] nie jest zmienną, to [;A;] jest równoważne pewnemu jednomianowi [;(C\Upsilon x);], gdzie [;x;] jest najcięższą zmienną, występującą w [;A;], oraz [;C;] jest jednomianem, w którym [;x;] nie występuje; patrz Część 2, Twierdzenie 2. Czyli mamy
[;(C\,\Upsilon\,x)\ \equiv\ A;]
Przy tym jednomian [;C;] jest lżejszy od [;A;]. Istnieje więc (indukcja) jednomian standardowy [;D;], równoważny z [;C;]. Zatem:
[;(D\,\Upsilon\,x)\ \equiv\ A;]
Więc jednomian standardowy [;(D\,\Upsilon\,x);] jest pożądanym jednomianem [;B;].
KONIEC DOWODU
Widzimy, że klasy równoważności jednomianów są we wzajemnie jednoznacznej odpowiedniości z niepustymi podzbiorami ciągu zmiennych
[;x'\ x''\ \x'''\ \ldots;]
Można uważać teorię operacji [;\Upsilon;] za teorię zbiorów skończonych. Może ona jednak także sł¨żyć za odskocznię do wielu bogatszych teorii, jak logika, arytmetyka, algebra, itd.
Monday, November 29, 2010
Teoria operacji łącznej, przemiennej i idempotentnej (Cz.2)
Niniejsza nota jest kontynuacją dwóch poprzednich:
Część 0 oraz Część 1
Ze zbioru wszystkich jednomianów (patrz Część 0) wydzielimy tak zwane standardowe, tak by w każdej klasie jednomianów równoważnych znajdował się dokładnie jeden standardowy. Dzięki temu będziemy znali strukturę jednomianów kompletnie, z dokładnością do równoważności.
Przede wszystkim pamiętajmy, że mamy uporządkowany ciąg zmiennych, będziemy mówić, że coraz cięższych:
[;x'\ x''\ x'''\ x''''\ \ldots;]
Łatwo porównać wagę dwóch zmiennych, na przykład przystawiając jedną do drugiej. Ta która wystaje jest cięższa:
[;x''''''';]
[;x'''';]
Powyżej, wcześniejsza wystaje poza późniejszą, więc wcześniejsza jest cięższa.
Zmienna nie jest cięższa od samej siebie.
UWAGA 0 Uporządkowanie zmiennych nie jest absolutnie potrzebne, ale może być wygodne.
Występowanie zmiennej w jednomianie definiujemy następująco:
Oczywiście jedna i ta sama zmienna może występować w jednomianie więcej niż raz. Tak jest na przykład w przypadku jednomianów postaci [;(A\Upsilon A);].
Niech [;x\ y;] będą dwoma różnymi zmiennymi. Powiedzmy, że zmienna [;y;] występuje w jednomianie [;A;]. Wiemy, że [;y;] albo występuje w jednomianie [;y;], i jeżeli [;A;] jest tym jednomianem, to [;A;] nie jest [;x;]. Pozostała możliwość, to występowanie [;y;] w jednomianie [;A;] postaci [;(B\Upsilon C);]. Wtedy jednomian [;A;] znowu nie jest [;x;] (ani żadną inną zmienną), gdyż na przykład zawiera nawiasy. Tym samym zakończyliśmy dowód następującego
TWIERDZENIE 0 Niech [;x\ y;] będą dwoma różnymi zmiennymi. Wtedy zmienna [;y;] nie występuje w jednomianie [;x;].
PRZYKŁAD Pokażmy, że zmienna [;x';] nie występuje w jednomianie [;C;], bedącym [;(x''\Upsilon x''';]. Rzeczywiście, jednomian ten nie jest zmienną, lecz jest postaci [;(A\Upsilon B;], gdzie jednomiany [;A\ B;] są odpowiednio zmiennymi [;x''\ x''';]. Na mocy przepisu 2 występowania w jednomianie, zmienna [;x';], żeby występować w [;C;], musiałaby występować w [;A;] lub w [;B;]. Jednak na mocy Twierdzenia 0 tak nie jest, więc zmienna [;x';] w jednomianie [;C;] nie wystepuje.
A teraz sformułuję i udowodnię dwa twierdzenia nieco poważniejsze od ważnego przecież Twierdzenia 0 :-)
TWIERDZENIE 1 Niech [;\vdash\,A\equiv B;]. Wtedy zmienna [;x;] występuje w [;A;] [;\Leftrightarrow;] [;x;] występuje w [;B;].
DOWÓD Każda równoważność otrzymana jest z reguły dowodzenia (będącej być może aksjomatem). Zatem wystarczy rozpatrzyć wszystkie 7 po kolei, przy tym zakładając (indukcyjnie), że twierdzenie zachodzi dla założeń reguł dowodzenia (dla zdań poprzedzających znaczek [;\vdash;]).
Powyższe twierdzenie mówi nam, że dla dwóch równoważnych jednomianów zbiór występujących w nich zmiennych jest ten sam. W dalszym ciągu niniejszej noty okaże się, że i na odwrót, gdy zbiór zmiennych jest ten sam, to dwa jednomiany są równoważne (innymi słowy, nierównoważne jednomiany różnią się zbiorem występujących w nich zmiennych - pewna zmienna występuje w jednym z nich, ale nie w drugim). Żeby to udowodnić, to pierwszym krokiem, chyba głównym, będzie poniższe Twierdzenie 2. Jeszcze wtrącę uwagę o tym, że mówienie o zbiorach jest tylko dla podtrzymania uwagi czytelnika - ani w teorii operacji {;\Upsilon;}, ani w metateorii tej teorii nie mamy symboli mnogościowych, nie mamy pojęcia zbioru, i w szczególności nie mamy pojęcia skończoności. A żyć trzeba :-) Damy sobie z tym wszystkim radę wkrótce, bo zamiast niepustych, skończonych zbiorów zmiennych będziemy mieć jednomiany standardowe.
TWIERDZENIE 2 Niech [;x\ A;] będą odpowiednio dowolną zmienną i dowolnym jednomianem. Wtedy albo [;x;] nie występuje w [;A;], albo [;A;] jest [;x;], albo istnieje jednomian [;B;], w którym [;x;] nie występuje, i taki, że zachodzi twierdzenie teorii:
[;\vdash\ (B\,\Upsilon\,x)\ \equiv\ A;]
DOWÓD Jeżeli [;x;] nie występuje w [;A;], to Twierdzenie 2 zachodzi. Odtąd będziemy więc rozpatrywać przypadek w którym [;x;] występuje w [;A;].
Jeżeli jednomian [;A;] jest zmienną, to na mocy Twierdzenia 0 wiemy, że [;A;] jest zmienną [;x;], i wtedy Twierdzenie 2 zachodzi.
Pozostał przypadek, w którym zmienna [;x;] występuje w jednomianie [;A;], przy czym jednomian ten nie jest zmienną. Istnieją wtedy jednomiany [;B\ C;] takie, że [;A;] jest [;(B\Upsilon C);] (więc [;x;] musi występować przynajmniej w jednym z jednomianów [;B\ C;]). Wtedy (indukcja) jednomiany [;B\ C;] spełniają Twierdzenie 2, czyli mamy następujące podprzypadki:
Część 0 oraz Część 1
Wstęp
Ze zbioru wszystkich jednomianów (patrz Część 0) wydzielimy tak zwane standardowe, tak by w każdej klasie jednomianów równoważnych znajdował się dokładnie jeden standardowy. Dzięki temu będziemy znali strukturę jednomianów kompletnie, z dokładnością do równoważności.
Zmienne i ich uporządkowanie
Przede wszystkim pamiętajmy, że mamy uporządkowany ciąg zmiennych, będziemy mówić, że coraz cięższych:
[;x'\ x''\ x'''\ x''''\ \ldots;]
Łatwo porównać wagę dwóch zmiennych, na przykład przystawiając jedną do drugiej. Ta która wystaje jest cięższa:
[;x''''''';]
[;x'''';]
Powyżej, wcześniejsza wystaje poza późniejszą, więc wcześniejsza jest cięższa.
Zmienna nie jest cięższa od samej siebie.
UWAGA 0 Uporządkowanie zmiennych nie jest absolutnie potrzebne, ale może być wygodne.
Występowanie zmiennych w jednomianach
Występowanie zmiennej w jednomianie definiujemy następująco:
- Zmienna [;x;] występuje w jednomianie [;x;].
- Zmienna [;x;] występuje w jednomianie [;(A\Upsilon B)\quad\Leftarrow:\Rightarrow\quad x;] występuje w [;A;] lub w [;B;] (lub w obu).
- Zmienna występuje w jednomianie [;\Leftarrow:\Rightarrow;] istnieje ciąg zastosowań powyższych dwóch zasad, prowadzący do takiego wniosku
Oczywiście jedna i ta sama zmienna może występować w jednomianie więcej niż raz. Tak jest na przykład w przypadku jednomianów postaci [;(A\Upsilon A);].
Niech [;x\ y;] będą dwoma różnymi zmiennymi. Powiedzmy, że zmienna [;y;] występuje w jednomianie [;A;]. Wiemy, że [;y;] albo występuje w jednomianie [;y;], i jeżeli [;A;] jest tym jednomianem, to [;A;] nie jest [;x;]. Pozostała możliwość, to występowanie [;y;] w jednomianie [;A;] postaci [;(B\Upsilon C);]. Wtedy jednomian [;A;] znowu nie jest [;x;] (ani żadną inną zmienną), gdyż na przykład zawiera nawiasy. Tym samym zakończyliśmy dowód następującego
TWIERDZENIE 0 Niech [;x\ y;] będą dwoma różnymi zmiennymi. Wtedy zmienna [;y;] nie występuje w jednomianie [;x;].
PRZYKŁAD Pokażmy, że zmienna [;x';] nie występuje w jednomianie [;C;], bedącym [;(x''\Upsilon x''';]. Rzeczywiście, jednomian ten nie jest zmienną, lecz jest postaci [;(A\Upsilon B;], gdzie jednomiany [;A\ B;] są odpowiednio zmiennymi [;x''\ x''';]. Na mocy przepisu 2 występowania w jednomianie, zmienna [;x';], żeby występować w [;C;], musiałaby występować w [;A;] lub w [;B;]. Jednak na mocy Twierdzenia 0 tak nie jest, więc zmienna [;x';] w jednomianie [;C;] nie wystepuje.
A teraz sformułuję i udowodnię dwa twierdzenia nieco poważniejsze od ważnego przecież Twierdzenia 0 :-)
TWIERDZENIE 1 Niech [;\vdash\,A\equiv B;]. Wtedy zmienna [;x;] występuje w [;A;] [;\Leftrightarrow;] [;x;] występuje w [;B;].
DOWÓD Każda równoważność otrzymana jest z reguły dowodzenia (będącej być może aksjomatem). Zatem wystarczy rozpatrzyć wszystkie 7 po kolei, przy tym zakładając (indukcyjnie), że twierdzenie zachodzi dla założeń reguł dowodzenia (dla zdań poprzedzających znaczek [;\vdash;]).
- [;A\equiv A;] — ten przypadek (gdy struny [;A;] i [;B;] są tę samą struną) jest oczywisty; zachodzi masło maślane.
- [;(A\ \equiv\ B)\ \vdash\ (B\ \equiv\ A);] — znowu przypadek oczywisty; bo nie ważne w jakiej kolejności wymieniamy dwa jednomiany, gdy mówimy o jednoczesnej przynależności zmiennej do nich obu lub do żadnego.
- [;(A\equiv B)\ (B\equiv C)\ \vdash\ (A\equiv\ C);] — zmienna występuję w [;A;] [;\Leftrightarrow;] wystepuje w [;B;] [;\Leftrightarrow;] wystepuje w [;C;].
- [;\vdash\ (A\Upsilon A)\ \equiv\ A;] — ten przypadek zachodzi na mocy zasady 2. przynależności zmiennej do jednomianu (patrz powyżej).
- [;\vdash\ (A\Upsilon B)\ \equiv\ (B\Upsilon A);] — rzeczywiście, nie ważne w jakiej kolejności wymieniamy dwa jednomiany, gdy mówimy o przynależności zmiennej do jednego z nich - ważne że do jednego z nich przynależy (lub nie)
- [;\vdash\ ((A\Upsilon B)\Upsilon C)\ \equiv\ (A\Upsilon(B\Upsilon C));] — zmienna występuje w lewym jednomianie [;\Leftrightarrow;] wystepuje w prawym, gdyż w obu wypadkach jest tak, gdy występuje przynajmniej w jednym z trzech jednomianów [;A\ B\ C;].
- [;(A\equiv B)\ \vdash\ ((A\Upsilon C)\, \equiv\, (B\Upsilon C));] — chcemy pokazać, że gdy zachodzi równoważność [;(A\equiv B);], to zmienna występuje w [;(A\Upsilon C)\ \ \Leftrightarrow;] występuje w [;(B\Upsilon C);]. Mamy trzy przypadki. Gdy zmienna występuje w [;C;] to teza zachodzi, bo [;C;] jest częścią obu jednomianów na prawo od [;\vdash;]. Drugi przypadek, gdy zmienna występuje w [;(A\Upsilon B);] na konto występowania w [;A;]. Na mocy założenia [;A\equiv B;], występuje wtedy ta zmienna także w [;B;]. Zatem występuje w jednomianie [;(B\Upsilon C);] (tym po prawej). Podobnie w trzecim wypadku, gdy zmienna występuje w [;(B\Upsilon C);] dzięki temu, że występuje w [;B;], pokazujemy, że występuje także w [;(A\Upsilon C);] (czyli po stronie lewej).
Powyższe twierdzenie mówi nam, że dla dwóch równoważnych jednomianów zbiór występujących w nich zmiennych jest ten sam. W dalszym ciągu niniejszej noty okaże się, że i na odwrót, gdy zbiór zmiennych jest ten sam, to dwa jednomiany są równoważne (innymi słowy, nierównoważne jednomiany różnią się zbiorem występujących w nich zmiennych - pewna zmienna występuje w jednym z nich, ale nie w drugim). Żeby to udowodnić, to pierwszym krokiem, chyba głównym, będzie poniższe Twierdzenie 2. Jeszcze wtrącę uwagę o tym, że mówienie o zbiorach jest tylko dla podtrzymania uwagi czytelnika - ani w teorii operacji {;\Upsilon;}, ani w metateorii tej teorii nie mamy symboli mnogościowych, nie mamy pojęcia zbioru, i w szczególności nie mamy pojęcia skończoności. A żyć trzeba :-) Damy sobie z tym wszystkim radę wkrótce, bo zamiast niepustych, skończonych zbiorów zmiennych będziemy mieć jednomiany standardowe.
TWIERDZENIE 2 Niech [;x\ A;] będą odpowiednio dowolną zmienną i dowolnym jednomianem. Wtedy albo [;x;] nie występuje w [;A;], albo [;A;] jest [;x;], albo istnieje jednomian [;B;], w którym [;x;] nie występuje, i taki, że zachodzi twierdzenie teorii:
[;\vdash\ (B\,\Upsilon\,x)\ \equiv\ A;]
DOWÓD Jeżeli [;x;] nie występuje w [;A;], to Twierdzenie 2 zachodzi. Odtąd będziemy więc rozpatrywać przypadek w którym [;x;] występuje w [;A;].
Jeżeli jednomian [;A;] jest zmienną, to na mocy Twierdzenia 0 wiemy, że [;A;] jest zmienną [;x;], i wtedy Twierdzenie 2 zachodzi.
Pozostał przypadek, w którym zmienna [;x;] występuje w jednomianie [;A;], przy czym jednomian ten nie jest zmienną. Istnieją wtedy jednomiany [;B\ C;] takie, że [;A;] jest [;(B\Upsilon C);] (więc [;x;] musi występować przynajmniej w jednym z jednomianów [;B\ C;]). Wtedy (indukcja) jednomiany [;B\ C;] spełniają Twierdzenie 2, czyli mamy następujące podprzypadki:
- Zmienna [;x;] nie występuje w [;B;], oraz jednomian [;C;] jest [;x;] - wtedy Twierdzenie 2 zachodzi.
- Zmienna [;x;] nie występuje w [;B;], oraz jednomian [;C;] nie jest [;x;] - wtedy (indukcja) istnieje jednomian [;D;], w którym [;x;] nie występuje, przy czym zachodzi
[;\vdash\ (D\,\Upsilon\,x)\ \equiv\ C;]
Wtedy
[;\vdash\ (B\,\Upsilon\,(D\,\Upsilon\,x))\ \equiv\ (B\,\Upsilon\,C);]
Ale prawa strona to po prostu [;A;] (dosłownie, jako struna, znak po znaku). Czyli otrzymaliśmy:
[;\vdash\ (B\,\Upsilon\,(D\,\Upsilon\,x))\ \equiv\ A;]
Ponieważ (łączność operacji [;\Upsilon;])
[;\vdash\ ((B\,\Upsilon\,D)\,\Upsilon\,x)\ \equiv\ (B\,\Upsilon\,(D\,\Upsilon\,x));]
to ostatecznie:
[;\vdash\ ((B\,\Upsilon\,D)\,\Upsilon\,x)\ \equiv\ A;]
Zatem Twierdzenie 2 zachodzi, gdzie istniejące [;B;] jest jednomianem [;(B\,\Upsilon\,D);] - zauważmy, że zmienna [;x;] nie występuję w [;(B\,\Upsilon\,D);], gdyż nie występuje ani w [;B;] ani w [;D;]. - Zmienna [;x;] nie występuję w [;C;] - ponieważ operacja [;\Upsilon;] jest przemienna, to podprzypadek ten sprowadza sie do poprzednich, kiedy to [;x;] nie występowało w [;B;]; mamy bowiem ciąg:
[;\vdash\ (C\Upsilon B)\,\equiv\,(B\Upsilon C);]
[;\vdash\ (E\Upsilon x)\,\equiv\,(B\Upsilon C);]
czyli
[;\vdash\ (E\Upsilon x)\,\equiv\,A;]
dla pewnego jednomianu [;E;], w którym nie występuje [;x;]. - Pozostały (pod)przypadki, kiedy [;x;] występuje w obu jednomianach [;B\ C;]. Wtedy mamy cztery dalsze (pod)podprzypadki (gdyby stosować pustą strunę, to zlałyby się one w jeden):
- Jednomiany [;B\ C;] są oba zmienną [;x;] - Wtedy [;A;] jest jednomianem [;(x\Upsilon x);], który jest równoważny jednomianowi [;x;], czyli Twierdzenie 2 znowu zachodzi.
- Jednomian [;C;] jest [;x;], ale [;B;] nie jest - wtedy istnieje jednomian [;D;], w którym [;x;] nie występuje, taki, że
[;\vdash\ (D\Upsilon x)\ \equiv B;]
tak, że po kolei dostajemy:
[;\vdash\ ((D\Upsilon x)\,\Upsilon\,x)\ \equiv A;]
[;\vdash\ (D\Upsilon\,(x\Upsilon x))\ \equiv A;]
[;\vdash\ (D\Upsilon\,x)\ \equiv A;]
Więc Twierdzenie 2 zachodzi. - Jednomian [;B;] jest [;x;], ale [;C;] nie jest - wtedy istnieje jednomian [;D;], w którym [;x;] nie występuje, taki, że
[;\vdash\ (D\Upsilon x)\ \equiv C;]
tak, że po kolei dostajemy:
[;\vdash\ (x\,\Upsilon\,(D\Upsilon x))\ \equiv A;]
[;\vdash\ ((D\Upsilon x)\,\Upsilon\,x)\ \equiv A;]
[;\vdash\ (D\Upsilon\,(x\Upsilon x))\ \equiv A;]
[;\vdash\ (D\Upsilon x) \equiv A;]
Więc Twierdzenie 2 zachodzi. - Ani [;B;] ani [;C;] nie jest [;x;] - wtedy istnieją jednomiany [;D\ E;], w których [;x;] nie występuje, i takie, że
[;\vdash\ (D\Upsilon x)\ \equiv B;]
[;\vdash\ (E\Upsilon x)\ \equiv C;]
tak, że po kolei dostajemy:
[;\vdash\ ((D\Upsilon x)\,\Upsilon\,(E\Upsilon x))\ \equiv A;]
[;\vdash\ (D\Upsilon\,(x\,\Upsilon\(E\Upsilon x)))\ \equiv A;]
[;\vdash\ (D\Upsilon\,((x\Upsilon\E)\,\Upsilon x)))\ \equiv A;]
[;\vdash\ (D\Upsilon\,((E\Upsilon x)\Upsilon x))\ \equiv A;]
[;\vdash\ (D\Upsilon\,(E\Upsilon\,(x\Upsilon x)))\ \equiv A;]
[;\vdash\ (D\Upsilon\,(E\Upsilon x))\ \equiv A;]
[;\vdash\ ((D\Upsilon\,E)\Upsilon x)\ \equiv A;]
Więc Twierdzenie 2 zachodzi.
Tuesday, November 23, 2010
Teoria operacji łącznej, przemiennej i idempotentnej (Cz.1)
Niniejsza nota jest kontynuacją poprzedniej:
Część 0
Gdy zachodzi reguła dowodzenia postaci
[;K\vdash L;]
przy czym [;\vdash K;] (czyli [;K;] jest twierdzeniem), to także L jest twierdzeniem; rzeczywiście, niech
[;K_0\,\ldots\,K_n;]
będzie dowodem zdania [;K;] (więc [;K_n;] jest identyczne z [;K;]). Wtedy ciąg:
[;K_0\,\ldots\,K_n\,L;]
jest dowodem zdania [;L;].
Podobnie dla reguły dowodzenia postaci
[;K\ L\ \vdash\ M;]
jeżeli zdania [;K\ L;] są twierdzeniami, to także zdanie [;M;] jest twierdzeniem; rzeczywiście, niech ciągi zdań
[;K_0\,\ldots\,K_k;]
oraz
[;L_0\,\ldots\,L_{\ell};]
będą odpowiednio dowodami zdań [;K\ L;]. Wtedy ciąg
[;K_0\,\ldots\,K_k\,L_0\,\ldots\,L_{\ell}\,M;]
jest dowodem zdania [;M;].
I o to właśnie chodzi z regułami dowodzenia - prowadzą one od twierdzeń do twierdzeń. Gdy założenia reguły, czyli zdania po lewej stronie znaczka [;\vdash;], są twierdzenami, to twierdzeniem jest także teza reguły, czyli zdanie po prawej stronie znaczka [;\vdash;].
Uogólnimy powyższą obserwację, dotyczącą reguł dowodzenia.
Formalne dowody są na ogół niemiłosiernie długie. Nie tylko człowiek, ale nawet komputer musiałby tracić na ich czytanie nierealnie wiele czasu, nie mówiąc o pisaniu takich dowodów. Na szczęście w pełni wystarczą szkice dowodów, jako że gwarantują one automatycznie istnienie pełnych, formalnych dowodów. Szkic dowodowy definiujemy na podobieństwo dowodu. Szkicem dowodowym zdania (lub schematu zdania) [;Z;] nazywamy skończony ciąg zdań (lub schematów zdań), z których każde jest albo twierdzeniem (lub schematem twierdzeń) albo jest otrzymane z jednej z reguł dowodzenia, przy czym ostatnie zdanie ciągu jest zdaniem [;Z;].
Ze szkicu dowodu otrzymujemy dowód przez poprzedzenie szkicu kolejnymi dowodami twierdzeń zdań, które wystąpiły w szkicu jako (wcześniej udowodnione, nim szkic istniał) twierdzenia. Jest to dokładnie ta sama procedura, która wystąpiła w poprzednim paragrafie; tyle że stosujemy ją tym razem na większą skalę.
Dzięki szkicom, gdy raz twierdzenie udowodnimy, to może ono służyć za skrót w dowodach następnych twierdzeń; nie ma konieczności dosłownie wciąż powtarzać dowód twierdzenia raz udowodnionego.
Pójdźmy po tej samej linii jeszcze dalej. Najpierw zdefiniujmy ogólny krok dowodowy czyli wyrażenia postaci tej samej, co reguła dowodzenia:
[;K_0\,\ldots\,K_n\ \vdash\ L;]
przy czym spełniony jest warunek (który zachodzi dla reguł dowodzenia):
kiedykolwiek wszystkie zdania [;K_0\,\ldots\,K_n;] są twierdzeniami, to twierdzeniem jest także zdanie [;L;].
Ogólny krok dowodowy jest dla nas pojęciem na ogół za ogólnym, i nawet budzi pewne niepokoje filozoficzne. Dlatego w niniejszyxh rozważaniach metateoretycznych ograniczymy się do jednostajnych kroków dowodowych, które będziemy nazywać po prostu krokami dowodowymi. Wyrażenie
[;K_0\,\ldots\,K_n\ \vdash\ L;]
nazywamy jednostajnym krokiem dowodowym [;\Leftarrow:\Rightarrow;] istnieje ciąg schematów zdaniowych
[;M_0\,\ldots\,M_m;]
taki, że każde [;M_j;] jest albo jednym z [;K_i;], albo jest schematem aksjomatów lub wcześniej udowodnionym schematem twierdzeń, albo jest tezą reguły dowodzenia, której założenia występują wcześniej w ciągu [;M_0\,\ldots\,M_n;] - przed wyrazem [;M_j;]; przy czym ostatnie [;M_m;] jest tym samym co [;L;].
Jest jasnym, że gdy wszystkie schematy zdań [;K_0\,\ldots\,K_n;] są schematami aksjomatów lub wcześniej dowiedzionych schematów twierdzeń, to ciąg [;M_0\,\ldots\,M_m;] zamienia się w szkic dowodowy schematu [;L;]. Oznacza to, że każdy (jednostajny) krok dowodowy jest ogólnym krokiem dowodowym; innymi słowy, krok dowodowy, tak jak reguła dowodzenia, prowadzi od twierdzeń do twierdzeń.
Na przykład, reguła 7 dowodzenia mówi, że klasa równoważności jednomianu [;A\Upsilon C;] nie zmieni się, gdy lewy argument zastąpimy równoważnym - dla wygody podaję poniżej wszystkie siedem reguł teorii operacji [;\Upsilon;], uzupełnionych o krok dowodowy 8, który uzasadnię (udowodnię) tym, że wynika z poprzednich siedmiu:
Oto goły dowód kroku 8 (bez objaśnień):
I to już jest cały dowód. Opiera się na przemienności [;\Upsilon;], oraz na regule dowodzenia 7.
Skrót dowodowy schematu zdań [;Z;] jest ciągiem schematów zdań, który przypomina dowód tegoż schematu [;Z;], tyle, że oprócz schematów aksjomatów oraz reguł dowodzenia wolno stosować także schematy twierdzeń wcześniej dowiedzionych oraz wcześniej dowiedzione kroki dowodowe. Jest jasnym, że podanie skrótu dowodowego schematu zdań [;Z;] można wypełnić do dowodu schametu [;Z;], co oznacza, że zachowdzi wtedy [;\vdash;\,Z;], czyli [;Z;] jest wtedy schematem twierdzeń.
Część 0
Korzystanie z twierdzeń
Gdy zachodzi reguła dowodzenia postaci
[;K\vdash L;]
przy czym [;\vdash K;] (czyli [;K;] jest twierdzeniem), to także L jest twierdzeniem; rzeczywiście, niech
[;K_0\,\ldots\,K_n;]
będzie dowodem zdania [;K;] (więc [;K_n;] jest identyczne z [;K;]). Wtedy ciąg:
[;K_0\,\ldots\,K_n\,L;]
jest dowodem zdania [;L;].
Podobnie dla reguły dowodzenia postaci
[;K\ L\ \vdash\ M;]
jeżeli zdania [;K\ L;] są twierdzeniami, to także zdanie [;M;] jest twierdzeniem; rzeczywiście, niech ciągi zdań
[;K_0\,\ldots\,K_k;]
oraz
[;L_0\,\ldots\,L_{\ell};]
będą odpowiednio dowodami zdań [;K\ L;]. Wtedy ciąg
[;K_0\,\ldots\,K_k\,L_0\,\ldots\,L_{\ell}\,M;]
jest dowodem zdania [;M;].
I o to właśnie chodzi z regułami dowodzenia - prowadzą one od twierdzeń do twierdzeń. Gdy założenia reguły, czyli zdania po lewej stronie znaczka [;\vdash;], są twierdzenami, to twierdzeniem jest także teza reguły, czyli zdanie po prawej stronie znaczka [;\vdash;].
Szkic dowodowy
Uogólnimy powyższą obserwację, dotyczącą reguł dowodzenia.
Formalne dowody są na ogół niemiłosiernie długie. Nie tylko człowiek, ale nawet komputer musiałby tracić na ich czytanie nierealnie wiele czasu, nie mówiąc o pisaniu takich dowodów. Na szczęście w pełni wystarczą szkice dowodów, jako że gwarantują one automatycznie istnienie pełnych, formalnych dowodów. Szkic dowodowy definiujemy na podobieństwo dowodu. Szkicem dowodowym zdania (lub schematu zdania) [;Z;] nazywamy skończony ciąg zdań (lub schematów zdań), z których każde jest albo twierdzeniem (lub schematem twierdzeń) albo jest otrzymane z jednej z reguł dowodzenia, przy czym ostatnie zdanie ciągu jest zdaniem [;Z;].
Ze szkicu dowodu otrzymujemy dowód przez poprzedzenie szkicu kolejnymi dowodami twierdzeń zdań, które wystąpiły w szkicu jako (wcześniej udowodnione, nim szkic istniał) twierdzenia. Jest to dokładnie ta sama procedura, która wystąpiła w poprzednim paragrafie; tyle że stosujemy ją tym razem na większą skalę.
Dzięki szkicom, gdy raz twierdzenie udowodnimy, to może ono służyć za skrót w dowodach następnych twierdzeń; nie ma konieczności dosłownie wciąż powtarzać dowód twierdzenia raz udowodnionego.
Krok dowodowy
Pójdźmy po tej samej linii jeszcze dalej. Najpierw zdefiniujmy ogólny krok dowodowy czyli wyrażenia postaci tej samej, co reguła dowodzenia:
[;K_0\,\ldots\,K_n\ \vdash\ L;]
przy czym spełniony jest warunek (który zachodzi dla reguł dowodzenia):
kiedykolwiek wszystkie zdania [;K_0\,\ldots\,K_n;] są twierdzeniami, to twierdzeniem jest także zdanie [;L;].
Ogólny krok dowodowy jest dla nas pojęciem na ogół za ogólnym, i nawet budzi pewne niepokoje filozoficzne. Dlatego w niniejszyxh rozważaniach metateoretycznych ograniczymy się do jednostajnych kroków dowodowych, które będziemy nazywać po prostu krokami dowodowymi. Wyrażenie
[;K_0\,\ldots\,K_n\ \vdash\ L;]
nazywamy jednostajnym krokiem dowodowym [;\Leftarrow:\Rightarrow;] istnieje ciąg schematów zdaniowych
[;M_0\,\ldots\,M_m;]
taki, że każde [;M_j;] jest albo jednym z [;K_i;], albo jest schematem aksjomatów lub wcześniej udowodnionym schematem twierdzeń, albo jest tezą reguły dowodzenia, której założenia występują wcześniej w ciągu [;M_0\,\ldots\,M_n;] - przed wyrazem [;M_j;]; przy czym ostatnie [;M_m;] jest tym samym co [;L;].
Jest jasnym, że gdy wszystkie schematy zdań [;K_0\,\ldots\,K_n;] są schematami aksjomatów lub wcześniej dowiedzionych schematów twierdzeń, to ciąg [;M_0\,\ldots\,M_m;] zamienia się w szkic dowodowy schematu [;L;]. Oznacza to, że każdy (jednostajny) krok dowodowy jest ogólnym krokiem dowodowym; innymi słowy, krok dowodowy, tak jak reguła dowodzenia, prowadzi od twierdzeń do twierdzeń.
Na przykład, reguła 7 dowodzenia mówi, że klasa równoważności jednomianu [;A\Upsilon C;] nie zmieni się, gdy lewy argument zastąpimy równoważnym - dla wygody podaję poniżej wszystkie siedem reguł teorii operacji [;\Upsilon;], uzupełnionych o krok dowodowy 8, który uzasadnię (udowodnię) tym, że wynika z poprzednich siedmiu:
- [;\vdash\ A\ \equiv\ A;]
- [;(A\ \equiv\ B)\ \vdash\ (B\ \equiv\ A);]
- [;(A\equiv B)\ \ (B\equiv C)\quad \vdash\quad (A\equiv\ C);]
- [;\vdash\ (A\Upsilon A)\ \equiv\ A;]
- [;\vdash\ (A\Upsilon B)\ \equiv\ (B\Upsilon A);]
- [;\vdash\ ((A\Upsilon B)\Upsilon C)\ \equiv\ (A\Upsilon(B\Upsilon C));]
- [;(A\equiv B)\ \vdash\ ((A\Upsilon C)\, \equiv\, (B\Upsilon C));]
- [;(B\equiv C)\ \vdash\ ((A\Upsilon B)\, \equiv\, (A\Upsilon C));]
Oto goły dowód kroku 8 (bez objaśnień):
- [;(A\Upsilon B)\ \equiv\ (B\Upsilon A);]
- [;B\equiv C;]
- [;(B\Upsilon A)\ \equiv\ (C\Upsilon A);]
- [;(A\Upsilon B)\ \equiv\ (C\Upsilon A);]
- [;(C\Upsilon A)\ \equiv\ (A\Upsilon C);]
- [;(A\Upsilon B)\ \equiv\ (A\Upsilon C);]
I to już jest cały dowód. Opiera się na przemienności [;\Upsilon;], oraz na regule dowodzenia 7.
Skrót dowodowy
Skrót dowodowy schematu zdań [;Z;] jest ciągiem schematów zdań, który przypomina dowód tegoż schematu [;Z;], tyle, że oprócz schematów aksjomatów oraz reguł dowodzenia wolno stosować także schematy twierdzeń wcześniej dowiedzionych oraz wcześniej dowiedzione kroki dowodowe. Jest jasnym, że podanie skrótu dowodowego schematu zdań [;Z;] można wypełnić do dowodu schametu [;Z;], co oznacza, że zachowdzi wtedy [;\vdash;\,Z;], czyli [;Z;] jest wtedy schematem twierdzeń.
Sunday, November 21, 2010
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:
- Zmienna jest jednomianem (na przykład [;x'''';] jest jednomianem).
- Jeżeli struny znaków [;A;] i [;B;] są jednomianami, to także struna:
[;(A\Upsilon B);]
jest jednomianem. - 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:
- [;\vdash\ A\ \equiv\ A;]
- [;(A\ \equiv\ B)\ \vdash\ (B\ \equiv\ A);]
- [;(A\equiv B)\ \ (B\equiv C)\quad \vdash\quad (A\equiv\ C);]
- [;\vdash\ (A\Upsilon A)\ \equiv\ A;]
- [;\vdash\ (A\Upsilon B)\ \equiv\ (B\Upsilon A);]
- [;\vdash\ ((A\Upsilon B)\Upsilon C)\ \equiv\ (A\Upsilon(B\Upsilon C));]
- [;(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):
- [;(x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x');]
- [;((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ ((x''\,\Upsilon\,x')\,\Upsilon\,x''');]
- [;((x''\,\Upsilon\,x')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x'));]
- [;((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.):
- [;\vdash\ ((x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x'));] - schemat aksjomatyczny 5.
- [;(x'\,\Upsilon\,x'')\ \equiv\ (x''\,\Upsilon\,x')\ \vdash\ ((x'\,\Upsilon\,x'')\,\Upsilon\,x''')\ \equiv\ ((x''\,\Upsilon\,x')\,\Upsilon\,x''');] - schemat reguł 7.
- [;\vdash\ (((x''\,\Upsilon\,x')\,\Upsilon\,x''')\ \equiv\ (x'''\,\Upsilon\,(x''\,\Upsilon\,x')));] - schemat aksjomatyczny 5.
- [;\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:
- [;(A\,\Upsilon\,B)\ \equiv\ (B\,\Upsilon\,A);]
- [;((A\,\Upsilon\,B)\,\Upsilon\,C)\ \equiv\ ((B\,\Upsilon\,A)\,\Upsilon\,C);]
- [;((B\,\Upsilon\,A)\,\Upsilon\,C)\ \equiv\ (C\,\Upsilon\,(B\,\Upsilon\,A));]
- [;((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.
Subscribe to:
Posts (Atom)