3.1 Rachunek sekwentów LK Gentzena
3.1.2 Dowody
Zorganizowane zastosowania reguł RS pozwalają budować dowody sekwen-tów. Intuicyjnie, dowodem sekwentu w RS jest drzewo binarne, którego każdy liść jest sekwentem aksjomatycznym, korzeń jest dowodzonym sekwentem, a poszczególne węzły są uzyskane w wyniku zastosowania wymienionych wyżej reguł. Precyzyjną definicję sformułujemy następująco:
Definicja 3.4 (Dowód sekwentu) 1. Każde jednoelementowe drzewo, którego węzeł jest sekwentem aksjomatycznym S jest dowodem sekwentu S.
2. Jeżeli D jest dowodem sekwentu S, to drzewo uzyskane przez dopisanie sekwentu S’ poniżej sekwentu S jest dowodem sekwentu S’, pod wa-runkiem, że S jest podstawieniem przesłanki a S’ jest podstawieniem wniosku jednej z reguł jednoprzesłankowych.
3. Jeżeli D jest dowodem sekwentu S a D0 jest dowodem S’, to drzewo uzyskane przez dopisanie sekwentu S” poniżej sekwentów S i S’ jest dowodem sekwentu S”, pod warunkiem, że S jest podstawieniem lewej przesłanki, S’ jest podstawieniem prawej przesłanki, a S” jest podsta-wieniem wniosku jednej z reguł dwuprzesłankowych.
4. Nic więcej nie jest dowodem sekwentu w RS.
To, że sekwent Γ ⇒ ∆ ma dowód będziemy zaznaczać pisząc ` Γ ⇒ ∆. W szczególności dowód sekwentu ⇒ ϕ (pusty poprzednik, jednoelementowy następnik) oznacza, że formuła ϕ ma dowód, czyli jest tezą.
Podana definicja dowodu jest indukcyjna. Ma to ważne konsekwencje, gdyż do dowodów w LK czy innych wariantach RS można będzie stosować dowody przez indukcję po rozmiarach dowodu. Rozmiary dowodu można rozmaicie definiować, poniżej wprowadzimy trzy najczęściej stosowane miary.
• długość dowodu
• wysokość dowodu (height) • wielkość dowodu
Jako pierwszą miarę wprowadzimy pojęcie długości dowodu, które defi-niujemy następująco:
3.1. RACHUNEK SEKWENTÓW LK GENTZENA 51 Definicja 3.5 (długość dowodu) • Dowód aksjomatu ma długość 0
• jeżeli S został wydedukowany z S’ za pomocą reguły jedno-przesłankowej, to jeżeli dowód S’ ma długość n, to dowód S ma długość n + 1
• jeżeli S został wydedukowany z S’ i S” za pomocą reguły dwu-przesłankowej, to jeżeli dowód S’ ma długość n, a dowód S” ma długość m, to dowód S ma długość max(n, m) + 1
Jeżeli D oznacza dowód, to długość dowodu oznaczymy przez | D |. Czasem wygodnie będzie w obliczaniu wielkości abstrachować od zasto-sowania reguł strukturalnych, za wyjątkiem (Cut). Wprowadzimy osobną miarę – wysokość dowodu (por. Negri, von Plato [101]):
Definicja 3.6 (wysokość dowodu) • Dowód aksjomatu ma wysokość 0
• jeżeli S został wydedukowany z S’ za pomocą logicznej reguły jedno-przesłankowej, to jeżeli dowód S’ ma wysokość n, to dowód S ma wy-sokość n + 1
• jeżeli S został wydedukowany z S’ i S” za pomocą reguły dwu-przesłankowej, to jeżeli dowód S’ ma wysokość n, a dowód S” ma wysokość m, to dowód S ma wysokość max(n, m) + 1
Jeżeli Γ ⇒ ∆ ma dowód wysokości n, to będziemy to czasami zaznaczać pisząc Γ ⇒n∆ lub `nΓ ⇒ ∆.
Pokrewną miarą do wysokości jest pojęcie wielkości dowodu (por. Buss [20]), w którym też abstrachujemy od reguł strukturalnych (z wyjątkiem (Cut)) ale pod uwagę bierzemy absolutną ilość wystąpień reguł logicznych w dowodzie (sumujemy wielkości gałęzi w przypadku reguły dwu-przesłankowej zamiast wybierać większą). Formalnie:
Definicja 3.7 (wielkość dowodu) • Dowód aksjomatu ma wielkość 0 • jeżeli S został wydedukowany z S’ za pomocą logicznej reguły jedno-przesłankowej, to jeżeli dowód S’ ma wielkość n, to dowód S ma wiel-kość n + 1
• jeżeli S został wydedukowany z S’ i S” za pomocą reguły dwu-przesłankowej, to jeżeli dowód S’ ma wielkość n, a dowód S” ma wielkość m, to dowód S ma wielkość n + m + 1
Jeżeli D oznacza dowód, to wielkość dowodu oznaczymy przez k D k. W rozdziale 5 uwzględnimy jeszcze sposób mierzenia rozmiaru dowodu przez Gentzena w jego oryginalnym dowodzie eliminacji cięcia, nazwany przez nas głębokością.
Zazwyczaj zapisuje się dowody w RS jako drzewa z korzeniem na dole, co oddaje strukturę zależności logicznych (procesu inferencji) od aksjomatów w dół do sekwentu dowodzonego. Konstruując dowód postępuje się zazwy-czaj odwrotnie, tzn. zaczyna od sekwentu dowodzonego i dopisuje kolejno przesłanki zastosowanych reguł. Rzecz jasna ze względu na występowanie (Cut), oraz inne własności pewnych reguł Gentzena, takie postępowanie nie musi zakończyć się sukcesem. Do kwestii warunków gwarantujących sukces w poszukiwaniu dowodu, a nawet automatyzację tego procesu, powrócimy w rozdziale 6.
Przykład 3.2: Zaprezentujemy dowód tzw. sylogizmu Fregego, często wystę-pującego w roli jednego z aksjomatów KRZ w systemie H z rozdziału 1.
p ⇒ p p ⇒ p q ⇒ q (→⇒) p → q, p ⇒ q r ⇒ r (→⇒) q → r, p → q, p ⇒ r (→⇒) p → (q → r), p, p → q, p ⇒ r (P ⇒) p, p → (q → r), p → q, p ⇒ r (P ⇒) p, p → (q → r), p, p → q ⇒ r (P ⇒) p, p, p → (q → r), p → q ⇒ r (C ⇒) p, p → (q → r), p → q ⇒ r (⇒→) p → (q → r), p → q ⇒ p → r (P ⇒) p → q, p → (q → r) ⇒ p → r (⇒→) p → (q → r) ⇒ (p → q) → (p → r) (⇒→) ⇒ (p → (q → r)) → ((p → q) → (p → r))
W przedstawionym dowodzie zwraca uwagę duża ilość zastosowań reguł strukturalnych. Jego długość wynosi 11, choć wysokość jedynie 6 (równa wielkości w tym przypadku). W dalszym ciągu zazwyczaj takie “oczywiste” kroki w dowodzie będziemy pomijać zaznaczając miejsce ich występowania za pomocą podwójnej kreski. Powyższy dowód w takiej skondensowanej for-mie, która oddaje jedynie jego wysokość i wielkość, będzie więc wyglądał następująco:
3.1. RACHUNEK SEKWENTÓW LK GENTZENA 53 p ⇒ p p ⇒ p q ⇒ q (→⇒) p → q, p ⇒ q r ⇒ r (→⇒) q → r, p → q, p ⇒ r (→⇒) p → (q → r), p, p → q, p ⇒ r (⇒→) p → (q → r), p → q ⇒ p → r (⇒→) p → (q → r) ⇒ (p → q) → (p → r) (⇒→) ⇒ (p → (q → r)) → ((p → q) → (p → r))
Poniższy lemat pozwala zauważyć pewne zależności między formułami w poprzedniku i następniku dowiedlnego sekwentu i uświadomić sobie pewne intuicje związane z pojęciem sekwentu. Zarazem podaje formalne podstawy dla trzech interpretacji sekwentu omówionych w poprzednim rozdziale. Lemat 3.1 Dla dowolnego sekwentu ϕ1, ..., ϕi ⇒ ψ1, ..., ψk, (i, k > 0) podane niżej cztery formy są równoważne:
1. ` ϕ1, ..., ϕi ⇒ ψ1, ..., ψk 2. ` ϕ1, ..., ϕi, ¬ψ1, ..., ¬ψk⇒ 3. `⇒ ¬ϕ1, ..., ¬ϕi, ψ1, ..., ψk 4. ` ϕ1∧ .... ∧ ϕi⇒ ψ1∨ ... ∨ ψk Dowód:
1. =⇒ 2. Z 1. otrzymujemy ` ¬ψ1, ..., ¬ψk, ϕ1, ..., ϕi, ⇒ przez k zastoso-wań (¬ ⇒), skąd przez wielokrotną permutację mamy 2.
2. =⇒ 1. Po pierwsze zauważmy, że dla każdego i ≤ k przez obie re-guły dla ¬ otrzymujemy ` ¬¬ψi ⇒ ψi. Z 2. przez wielokrotną permu-tację mamy ` ¬ψ1, ..., ¬ψk, ϕ1, ..., ϕi, ⇒, skąd przez (⇒ ¬) otrzymujemy ` ¬ψ2, ..., ¬ψk, ϕ1, ..., ϕi, ⇒ ¬¬ψ1. Stosując (Cut) na ` ¬¬ψ1 ⇒ ψ1 otrzy-mujemy ` ¬ψ2, ..., ¬ψk, ϕ1, ..., ϕi, ⇒ ψ1. Powtarzamy tę dedukcję k − 1 razy aż do otrzymania 1.
1. ⇐⇒ 3. analogicznie
1. =⇒ 4. Wykonujemy następującą dedukcję: ϕ1, ..., ϕi ⇒ ψ1, ..., ψk (∧ ⇒) ϕ1∧ ϕ2, ϕ2, ..., ϕi⇒ ψ1, ..., ψk (P ⇒) ϕ2, ϕ1∧ ϕ2, ϕ3, ..., ϕi ⇒ ψ1, ..., ψk (∧ ⇒) ϕ1∧ ϕ2, ϕ1∧ ϕ2, ϕ3, ..., ϕi ⇒ ψ1, ..., ψk (C ⇒) ϕ1∧ ϕ2, ϕ3, ..., ϕi⇒ ψ1, ..., ψk
Powtarzamy tę dedukcję tak długo aż otrzymamy ϕ1∧, ..., ∧ϕi ⇒ ψ1, ..., ψk, następnie przeprowadzamy analogiczną dedukcję z wykorzystaniem (⇒ ∨), (⇒ P ) i (⇒ C) na następniku aż otrzymamy 4.
4. =⇒ 1. Odnotujmy wpierw, że dla k ≥ 2 zachodzi ` ψ1∨ ... ∨ ψk ⇒ ψ1, ..., ψk, oto początek dowodu:
ψ1⇒ ψ1 (⇒ W ) ψ1⇒ ψ1, ψ2 ψ2⇒ ψ2 (⇒ W ), (⇒ P ) ψ2⇒ ψ1, ψ2 (∨ ⇒) ψ1∨ ψ2⇒ ψ1, ψ2 (⇒ W ) ψ1∨ ψ2 ⇒ ψ1, ψ2, ψ3 ψ3⇒ ψ3 (⇒ W ), (⇒ P ) ψ3 ⇒ ψ1, ψ2, ψ3 (∨ ⇒) ψ1∨ ψ2∨ ψ3⇒ ψ1, ψ2, ψ3
Analogicznie, dla i ≥ 2 udowadniamy, że zachodzi ` ϕ1, ...., ϕi ⇒ ϕ1 ∧ .... ∧ ϕi. stosując dwa razy (Cut) do 4. i do otrzymanych sekwentów otrzy-mujemy 1.
Ograniczenie się do sekwentów z jednoelementowym następnikiem po-zwala dodatkowo ujawnić związek ⇒ z implikacją, co oddaje poniższy: Lemat 3.2 Dla dowolnego sekwentu ϕ1, ..., ϕi⇒ ψ(i > 0), podane niżej trzy formy są równoważne: 1. ` ϕ1, ..., ϕi⇒ ψ 2. `⇒ ϕ1 → (ϕ2→ ..., (ϕi → ψ)...) 3. `⇒ ϕ1∧ .... ∧ ϕi → ψ Dowód: 1. =⇒ 2. Z 1. za pomocą (P ⇒) otrzymujemy ` ϕi, ..., ϕ1 ⇒ ψ, skąd przez i-krotne zastosowanie (⇒→) otrzymujemy 2.
2. =⇒ 1. Zauważ, że dla dowolnych ϕ, ψ zachodzi ` ϕ → ψ, ϕ ⇒ ψ, w szczególności ` ϕ1 → (ϕ2 → ..., (ϕi → ψ)...), ϕ1 ⇒ ϕ2 → (ϕ3 → ..., (ϕi → ψ)...). Stąd przez 2. i (Cut) otrzymujemy ` ϕ1 ⇒ ϕ2 → (ϕ3 → ..., (ϕi → ψ)...). Powtarzamy tę dedukcję i − 1 razy (z kolejnymi podstawieniami ` ϕk→ χ, ϕk⇒ χ, k ≤ i) aż uzyskamy 1.
1. =⇒ 3. Przez lemat 3.1, 1. =⇒ 4. i (⇒→)
3. =⇒ 1. Ponieważ ` ϕ1∧ .... ∧ ϕi → ψ, ϕ1∧ .... ∧ ϕi ⇒ ψ, więc przez (Cut) na 3. mamy ` ϕ1∧ .... ∧ ϕi ⇒ ψ, skąd przez lemat 3.1 mamy 1.
Oczywiście z obu lematów wynika, że jeżeli jakiś sekwent podpadający pod jeden ze schematów jest niedowiedlny, to jego równoważniki również.
3.1. RACHUNEK SEKWENTÓW LK GENTZENA 55 Dla dalszych rozważań nad dowodami w LK (lub innych wariantach RS) wygodnie jest wprowadzić dodatkową terminologię.
Definicja 3.8 1. Ciąg sekwentów tworzy gałąź w dowodzie S wtw jego pierwszym elementem jest sekwent aksjomatyczny, a ostatnim jest S oraz każdy sekwent w tym ciągu oprócz ostatniego jest (jedną) przesłan-ką pewnej reguły, której wnioskiem jest kolejny sekwent z tego ciągu. 2. Sekwent S1 jest nad sekwentem S2 lub poprzedza S2 (a S2 jest pod
S1 lub następuje po S1) w dowodzie wtw istnieje gałąź w tym dowo-dzie, która zawiera S1 jako wcześniejszy a S2 jako późniejszy element. Jeżeli między S1 a S2 nie ma żadnego innego sekwentu, to mówimy o bezpośrednim poprzedzaniu (następowaniu po).
3. Zastosowanie reguły R poprzedza lub jest nad zastosowaniem reguły R’ (R’ następuje po R lub jest pod R) w dowodzie wtw wniosek R jest nad wnioskiem R’. Jeżeli dodatkowo wniosek R jest przesłanką zastosowania R’ to mamy bezpośrednie poprzedzanie (następowanie po).
4. Jeżeli S występuje w dowodzie D, to zbiór zawierający S oraz wszystkie sekwenty, które są nad S w D jest poddowodem D (i dowodem S). Jeżeli D0 jest poddowodem D, to D jest jego dowodem nadrzędnym (naddowodem).
5. Jeżeli S1 bezpośrednio poprzedza S2, to ϕ ∈ S2 jest bezpośrednim po-tomkiem (jedynym) ψ wtw (a) ψ jest formułą parametryczną w S1, a ϕ := ψ i występuje w tej samej pozycji w S2 co ψ w S1, albo (b) ψ jest formułą poboczną w S1, a ϕ formułą zasadniczą S2. ϕ jest potomkiem ψ wtw istnieje ciąg 0 lub więcej bezpośrednich potomków od ψ do ϕ (relacja potomstwa jest zwrotnym, tranzytywnym domknięciem relacji bezpośredniego potomstwa).
6. ϕ jest bezpośrednim przodkiem (niekoniecznie jedynym) ψ wtw ψ jest bezpośrednim potomkiem ϕ. ϕ jest przodkiem ψ wtw ψ jest potomkiem ϕ.
Warto odnotować, że:
Fakt 3.1 1. Formuła zasadnicza (Cut) oraz wszystkie formuły sekwentu dowodzonego nie mają bezpośredniego potomka.
2. Formuły w (AX) oraz formuły zasadnicze (W) nie mają bezpośrednich przodków.
3. W przypadku (P) bezpośrednimi przodkami (potomkami) formuł zasad-niczych są ich przestawione wystąpienia w bezpośrednio sąsiadującym sekwencie.
Wprowadzimy też pewne ważne uogólnienie pojęcia dowodu sekwentu S. Definicja 3.9 (Dedukcja) Drzewo, w którym niekoniecznie każdy liść jest sekwentem aksjomatycznym, ale które spełnia pozostałe dwa warunki defini-cji dowodu, to dedukcja sekwentu S. Niech D będzie dedukcją S, a X oznacza zbiór wszystkich liści drzewa D, które nie są sekwentami aksjomatycznymi, wtedy D jest dedukcją S z X. Jeżeli istnieje dedukcją S z X, to S jest dedu-kowalne z X, co zaznaczamy X ` S.
W szczególności dedukcja z pustym X jest dowodem S. Z punktu widze-nia zastosowawidze-nia RS jako metody rozstrzygalnej szczególne znaczenie będą miały dedukcje z (nieaksjomatycznych) sekwentów atomowych i sposoby ich konstruowania. Oczywiście terminologia z poprzedniej definicji stosuje się też do dedukcji, z tym, że gałąź w dedukcji nie musi się zaczynać od sekwentu aksjomatycznego. W przypadku dedukcji mówimy też o poddedukcji, chociaż w szczególnych wypadkach poddedukcja może być poddowodem nawet jeżeli nadrzędna dedukcja nie jest dowodem.
Uwaga 3.4: Zauważmy, że powyżej użyliśmy ` jeszcze w jednej funkcji, dla zaznaczenia relacji dedukowalności między zbiorami sekwentów a sekwenta-mi. Jest to naturalne uogólnienie symbolu ` w funkcji dowiedlności S, tak jak relacja dedukowalności między zbiorami formuł i formułami jest natu-ralnym uogólnieniem ` w funkcji asercji tezy. Natomiast zauważmy, że nie należy mylić zdefiniowanej wyżej sekwentowej relacji dedukowalności z rela-cją zachodzącą między poprzednikiem a następnikiem sekwentu, którą też czasem oznaczamy przez ` zamiast ⇒ (por. podrozdział 2.4).
Definicja 3.10 (Podsekwenty, złożenie sekwentów) • Γ ⇒ ∆ jest podsekwentem Π ⇒ Σ wtw Γ ⊆ Π i ∆ ⊆ Σ; relację “S jest podsekwen-tem S0” zaznaczymy przez S v S0
• Dla Γ ⇒ ∆ i Π ⇒ Σ ich złożeniem jest Γ, Π ⇒ ∆, Σ oraz dowolna permutacja jego elementów; dla S i S0 ich złożenie oznaczymy przez S ◦ S0.
3.2. ADEKWATNOŚĆ LK 57