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ń.
No comments:
Post a Comment