• ψ ⇒ ϕ ∨ ψ • ϕ ∨ ψ ⇒ ϕ, ψ • ϕ → ψ, ϕ ⇒ ψ • ¬ψ, ϕ → ψ ⇒ ¬ϕ • ⇒ ϕ, ϕ → ψ • ψ ⇒ ϕ → ψ
Uważny czytelnik, który dowiódł wszystkie aksjomaty w lemacie 3.3 z pewnością mógł odnotować dowiedlność tych sekwentów już wtedy.
4.3 Eliminacja reguł strukturalnych
Jak widać w przypadku samego LK, który jest przykładem c-systemu moż-na przez modyfikację reguł otrzymać wiele wariantów, oprócz LK-K również M-wariant (multiplikatywny) lub A-wariant (addytywny). W każdej wersji można też przyjąć którąś z czterech form aksjomatów, choć – ze względu na obecność (W) – niezbędne są tylko formy proste. Nie chodzi nam jed-nak tylko o kombinatoryczne wytwarzanie coraz to nowych systemów. Racją wprowadzenia nowych wersji RS musi być ich przydatność do pełnienia pew-nych funkcji. Np. jedne wersje lepiej się nadają do tego, żeby udowadniać dla nich pewne metalogiczne wyniki, inne jako praktyczne systemy poszukiwa-nia dowodów itd. Stąd też wyodrębnimy tylko takie warianty, które znajdą później zastosowania.
Wszystkie wymienione wyżej wersje LK są równoważne i stanowią od-miany wariantu ogólnego, czyli takiego, w którym mamy obecność zarówno reguł strukturalnych jak i logicznych. W paragrafie 2.2.2 wspominaliśmy o wariantach logicznym i strukturalnym RS. Wariant strukturalny scharakte-ryzujemy w rozdziale 10, gdzie omówimy pozostałe typy RS. Teraz bardziej interesujący będzie dla nas wariant logiczny, w którym udział reguł struktu-ralnych jest wyeliminowany. W tym celu przejdziemy do innych alternatyw RS jakimi są m-systemy i z-systemy (sekwenty definiowane na multizbio-rach/zbiorach). Zauważmy, że zmiana ciągów na multizbiory automatycznie prowadzi do eliminacji reguł permutacji, a na zbiory dodatkowo eliminuje kontrakcję. W tej ostatniej alternatywie, jeżeli przyjmiemy aksjomaty uogól-nione, to dodatkowo możemy wyeliminować (W), a ponieważ (Cut) też jest
eliminowalne, co wykażemy w rozdziale 5, więc otrzymujemy wariant logiczny bez reguł strukturalnych. Dodatkowo, po przyjęciu wariantów reguł Ketone-na mamy też pełną semantyczną odwracalność reguł, co czyni taki system bardzo przydatnym w praktyce. Wyprzedzając rozważania z rozdziału 6 na-zwiemy ten system analitycznym RS (ARS). Oto jego reguły:
(U AX) Γ, ϕ ⇒ ϕ, ∆ (¬⇒) ¬ϕ, Γ⇒ ∆Γ⇒ ∆, ϕ (⇒¬) Γ⇒ ∆, ¬ϕϕ, Γ⇒ ∆ (∧⇒) ϕ, ψ, Γ⇒ ∆ ϕ∧ψ, Γ⇒ ∆ (⇒∧) Γ⇒ ∆, ϕ Γ⇒ ∆, ψ Γ⇒ ∆, ϕ∧ψ (⇒∨) Γ⇒ ∆, ϕ, ψ Γ⇒ ∆, ϕ∨ψ (∨⇒) ϕ, Γ⇒ ∆ ψ, Γ⇒ ∆ ϕ∨ψ, Γ⇒ ∆ (⇒→) Γ⇒ ∆, ϕ → ψϕ, Γ⇒ ∆, ψ (→⇒) Γ⇒ ∆, ϕϕ → ψ, Γ⇒ ∆ψ, Γ⇒ ∆ Definicje dowodu, dedukcji itp. bez zmian, jak dla LK.
Uwaga 4.3: W ARS brak jest reguł strukturalnych (w tym (Cut)!), lecz teraz ;itery Γ, ∆ oznaczają niekoniecznie zbiory. Jak pokażemy niżej, ten sam zestaw reguł, ale podany jako m-system, też jest adekwatną formaliza-cją KRZ. Ma to ważne konsekwencje, gdyż w wielu przypadkach multizbiory są wygodniejszym obiektem syntaktycznych operacji niż zbiory, a ponadto m-systemy pozwalają na formalizację wielu logik nieklasycznych, np. pod-strukturalnych (por. uwaga 4.1), dla których z-systemy są niewystarczające. Tam gdzie w grę będzie wchodziło rozróżnienie obu alternatyw ARS będzie-my pisać odpowiednio z-ARS lub m-ARS. Zauważbędzie-my jednak, że aby wykazać adekwatność m-ARS musimy udowodnić dopuszczalność kontrakcji, co zro-bimy niżej.
Uwaga 4.4: Można skonstruować również wersję ARS, która jest c-systemem (np. system w Gallier [48]). Jest to o tyle istotne, że operowanie c-sekwentami bywa wygodniejsze w przypadku zastosowań RS na potrzeby automatycznej dedukcji, gdyż ciągi są z punktu widzenia implementacji wygodniejszymi strukturami danych do przetwarzania. W tym celu trzeba przeformułowć reguły tak by wykluczyć potrzebę stosowania (P). Aby osiągnąć taki efekt należy zarówno formuły poboczne jak i formułę główną umieścić w schema-cie w neutralny sposób, a nie na skraju poprzednika czy następnika. Dla przykładu reguły dla ¬ i ∧ wyglądają następująco:
4.3. ELIMINACJA REGUŁ STRUKTURALNYCH 73 (∧⇒) Π, ϕ∧ψ, Γ⇒ ∆Π, ϕ, ψ, Γ⇒ ∆ (⇒∧) Γ⇒ ∆, ϕ, ΣΓ⇒ ∆, ϕ∧ψ, ΣΓ⇒ ∆, ψ, Σ
Oczywiście, każdy z ciągów parametrów w schemacie może być pusty. Przy tak zdefiniowanych regułach, jeżeli zadamy pewien porządek stosowania re-guł na formułach, np. od lewej do prawej, to mamy gwarancję, że do każ-dej złożonej formuły w pewnym momencie zostanie zastosowana reguła, a otrzymane formuły poboczne zostaną wzięte pod uwagę w następnej fazie procedury szukania dowodu (por. podrozdział 6.2).
Zauważmy też, że dowolne alternatywy ARS mogą występować z aksjo-matem uogólnionym z ϕ dowolnym (wersja lepsza dla praktycznych zasto-sowań) lub atomowym (wersja wygodniejsza dla dowodów dopuszczalności rozmaitych reguł, w tym (Cut)). W zależności od potrzeb będziemy wybie-rali w dalszym ciągu jedną z wersji. Ich równoważność wynika z twierdzenia 4.1.
Ustalimy teraz szereg interesujących własności ARS.
Twierdzenie 4.2 (Adekwatność) `ARS Γ ⇒ ∆ wtw |= Γ ⇒ ∆.
Dowód: Przystosowanie wynika z lematu 3.6. Co do pełności, to nie mo-żemy odwołać się do lematu 3.3., gdyż w jego dowodzie wykorzystywaliśmy (Cut), które nie należy do zestawu reguł pierwotnych ARS. Wprawdzie w rozdziale 5 dowiedziemy twierdzenie o dopuszczalności (Cut) w ARS i w ten sposób pośrednio uzyskamy dowód twierdzenia o pełności, to jednak już tu-taj wykażemy ten rezultat bezpośrednio w prosty sposób przez odwołanie się do semantycznej odwracalności wszystkich reguł ARS (lemat 4.7). W tym celu udowodnimy lemat, który dodatkowo ustala nam górne ograniczenia dla wielkości dowodów w ARS.
Lemat 4.9 (Pełność ARS) Jeżeli |= Γ ⇒ ∆ i w Γ ⇒ ∆ jest n wystąpień stałych logicznych, to ` Γ ⇒ ∆ i istnieje dowód D dla Γ ⇒ ∆ taki, że kDk < 2n
Dowód: Przez indukcję po n.
Baza: n = 0 oznacza, że Γ ⇒ ∆ jest sekwentem atomowym, a skoro jest tautologią, to jest aksjomatem z dowodem o wielkości 0.
Założenie indukcyjne mówi, że lemat zachodzi dla dowolnego Γ0 ⇒ ∆0 o ilości stałych < n. Pokazujemy, że zajdzie również dla sekwentu zawierają-cego n stałych. Musimy rozważyć przypadki wszystkich formuł złożonych w Γ ⇒ ∆. Rozważymy przypadek koniunkcji.
ϕ ∧ ψ w poprzedniku. Zatem Γ ⇒ ∆ := ϕ ∧ ψ, Γ0⇒ ∆. Z odwracalności mamy, że |= ϕ, ψ, Γ0 ⇒ ∆, a ponieważ sekwent ten ma n − 1 stałych więc podpada pod założenie indukcyjne, zatem ` ϕ, ψ, Γ0 ⇒ ∆ i kDk < 2n−1. Dodając do D, ϕ ∧ ψ, Γ0 ⇒ ∆ jako kolejny sekwent uzyskany przez (∧ ⇒) otrzymujemy dowód D0 tegoż sekwentu taki, że kD0k < 2n−1+ 1 ≤ 2n.
ϕ ∧ ψ w następniku. Zatem Γ ⇒ ∆ := Γ ⇒ ∆0, ϕ ∧ ψ. Z odwracalności mamy, że zarówno |= Γ ⇒ ∆0, ϕ jak i |= Γ ⇒ ∆0, ψ. a ponieważ każdy z tych sekwentów ma n − 1 stałych, więc podpada pod założenie indukcyjne i ma dowód kDk < 2n−1. Do obu dowodów dodajemy Γ ⇒ ∆0, ϕ ∧ ψ uzyskany przez (⇒ ∧) i otrzymujemy dowód D0 tegoż sekwentu taki, że kD0k < 2n, gdyż dla dowolnych i, j < 2n−1, i + j + 1 < 2n.
Dla dalszych zastosowań przydatne jest udowodnienie następującego le-matu
Lemat 4.10 (Dopuszczalność osłabiania) Jeżeli `ARS Γ0 ⇒ ∆0, to `ARS Γ ⇒ ∆, dla Γ0 ⊆ Γ, ∆0 ⊆ ∆, ponadto długość dowodu nie jest większa. Dowód indukcyjny po długości dowodu Γ0⇒ ∆0.
Baza: Dowód Γ0⇒ ∆0ma długość 0, zatem jest to aksjomat. Więc Γ ⇒ ∆ też jest aksjomatem o dowodzie długości 0.
Założenie indukcyjne mówi, że lemat zachodzi dla dowolnego dowodu Γ0 ⇒ ∆0 o długości < n. Pokazujemy, że zajdzie również, gdy dowód ma długość n.
Musimy rozważyć przypadki zastosowania wszystkich reguł do uzyskania Γ0 ⇒ ∆0. Rozważmy przypadek (∧ ⇒).
Mamy zatem dowód D długości n zakończony sekwentem ϕ ∧ ψ, Γ00 ⇒ ∆0 := Γ0 ⇒ ∆0 (Γ0 = Γ00∪ {ϕ ∧ ψ}). Przesłanka ϕ, ψ, Γ00 ⇒ ∆0 ma dowód długości n − 1 zatem podpada pod założenie indukcyjne, czyli ϕ, ψ, Γ00, Π ⇒ ∆, gdzie Π = Γ − Γ0, ma dowód tej samej długości, tj. n − 1. Przez (∧ ⇒) otrzymujemy ϕ ∧ ψ, Γ00, Π ⇒ ∆ := Γ ⇒ ∆; dowód ma długość n.
Uwaga 4.5: Można przeprowadzić dowód dopuszczalności (W) w ARS w inny, bardziej bezpośredni sposób przez odwołanie się do pewnej własności reguł ARS, zwanej niezależnością kontekstową (por. podrozdział 4.5), a przez Avrona [7] ‘czystością’ reguł, a sprowadzającej się do tego, że żadna reguła nie wprowadza warunków ograniczających na kształt parametrów. Wobec tego, jeśli mamy dowód Γ ⇒ ∆, to zawsze można go przerobić na dowód (tej samej długości) dla ϕ, Γ ⇒ ∆ lub Γ ⇒ ∆, ϕ przez dopisanie ϕ do każdego sekwentu w dowodzie w poprzedniku lub następniku. Niestety w RS dla innych logik, np. modalnych wiele reguł nie posiada tej własności.
4.3. ELIMINACJA REGUŁ STRUKTURALNYCH 75 Dla dowiedzenia dopuszczalności kontrakcji w m-ARS potrzebujemy do-wodu syntaktycznej odwracalności reguł logicznych. Oczywiście nie możemy skorzystać z lematu 4.8 o odwracalności reguł dla LK-K, gdyż tamten był dowiedziony przy użyciu (Cut), a w ARS jej nie posiadamy. Na szczęście można dowieść tego samego rezultatu bez użycia (Cut) dla wariantu z ak-sjomatami, w których formuła po obu stronach ⇒ jest atomowa. Dowód podany niżej jest w istocie dowodem dopuszczalności konwersu każdej re-guły pierwotnej ARS, w przeciwieństwie do dowodu lematu 4.8, w którym wykazaliśmy ich wyprowadzalność ale przy użyciu (Cut) (por. uwaga 4.2). Dowód dopuszczalności jest o wiele bardziej skomplikowany, ale przy oka-zji możemy też wykazać, że dowody przesłanek są nie dłuższe od dowodów wniosków. Dla odróżnienia od lematu 4.8 poniższy wynik określimy nazwą lematu o inwersji. Dla obu lematów (o inwersji i dopuszczalności kontrakcji) również przeprowadzimy dowód indukcyjny po długości dowodu.
Lemat 4.11 (o inwersji reguł ARS) Dla każdej reguły, jeżeli wniosek ma dowód (długości n), to przesłanki też mają dowody (długości ≤ n).
Dowód: Przeprowadzimy dowód indukcyjny po długości dowodu sekwentu-wniosku. Wymaga on rozpatrzenia każdej reguły z osobna. Rozważmy obie reguły dla ∧.
Baza: Dowód wniosku ma długość 0, zatem jest to aksjomat. Niech to będzie np. ϕ ∧ ψ, Γ ⇒ ∆, gdzie pewne χ ∈ Γ ∩ ∆. χ 6= ϕ ∧ ψ, gdyż jest formułą atomową, ale wtedy ϕ, ψ, Γ ⇒ ∆ też jest aksjomatem. Podobnie gdy Γ ⇒ ∆, ϕ ∧ ψ ma dowód długości 0, wtedy zarówno Γ ⇒ ∆, ϕ jak i Γ ⇒ ∆, ψ są dowiedlne, jako aksjomaty (analogicznie postępujemy w dowodzie bazy dla innych przypadków reguł).
Założenie indukcyjne mówi, że lemat zachodzi dla dowolnego dowodu wniosku o długości < n. Pokazujemy, że zajdzie również gdy dowód ma długość n.
Rozważmy przypadek (∧ ⇒). Mamy zatem dowód D długości n zakoń-czony sekwentem S := ϕ ∧ ψ, Γ ⇒ ∆. Należy rozważyć 2 podprzypadki:
a. ϕ ∧ ψ jest formułą zasadniczą S b. ϕ ∧ ψ nie jest formułą zasadniczą S
Jeżeli ostatnia reguła to (∧ ⇒) z ϕ ∧ ψ jako formułą zasadniczą, to po obcięciu ostatniego sekwentu z D mamy dowód ϕ, ψ, Γ ⇒ ∆ (długości n − 1). Rozważmy przypadek (∧ ⇒), podprzypadek b. Jeżeli ϕ∧ψ nie jest formu-łą zasadniczą S, to jest formuformu-łą parametryczną. Przykładowo, jeżeli ostatnio zastosowana reguła była 2-przesłankowa, to D kończy się następująco:
ϕ ∧ ψ, Γ0 ⇒ ∆0 ϕ ∧ ψ, Γ00⇒ ∆00 ϕ ∧ ψ, Γ ⇒ ∆
Ponieważ dowody obu przesłanek mają długość < n, to podpadają pod zało-żenie indukcyjne. Zatem mamy dowody sekwentów ϕ, ψ, Γ0 ⇒ ∆0i ϕ, ψ, Γ00⇒ ∆00. Ale wtedy za pomocą tej samej reguły 2-przesłankowej, która kończyła D wydedukujemy z nich sekwent ϕ, ψ, Γ ⇒ ∆.
Podobnie gdy Γ ⇒ ∆, ϕ ∧ ψ ma dowód długości n oraz dla przypadków innych reguł.
Na koniec dowiedziemy (dla m-ARS)
Lemat 4.12 (Dopuszczalność kontrakcji) Jeżeli `ARS ϕ, ϕ, Γ ⇒ ∆, to `ARS ϕ, Γ ⇒ ∆, oraz jeżeli `ARS Γ ⇒ ∆, ϕ, ϕ, to `ARS Γ ⇒ ∆, ϕ, ponadto długość dowodu nie jest większa.
Dowód: Przeprowadzimy dowód indukcyjny po długości dowodu ϕ, ϕ, Γ ⇒ ∆ (dla Γ ⇒ ∆, ϕ, ϕ analogicznie)
Baza: ϕ, ϕ, Γ ⇒ ∆ ma dowód długości 0, zatem jest aksjomatem i bez względu na to czy ψ ∈ (Γ ∪ {ϕ}) ∩ ∆ jest identyczne z ϕ czy nie, to ϕ, Γ ⇒ ∆ też jest aksjomatem.
Założenie indukcyjne mówi, że lemat zachodzi dla dowolnego dowodu wniosku o długości < n. Pokazujemy, że zajdzie również gdy dowód ma długość n. Należy rozważyć 2 podprzypadki:
a. ϕ nie jest formułą zasadniczą b. ϕ jest formułą zasadniczą
Jeżeli ϕ nie jest formułą zasadniczą w dowodzonym sekwencie, to ϕ, ϕ, Γ ⇒ ∆ został wydedukowany z ϕ, ϕ, Γ0 ⇒ ∆0 przez regułę jednoprzesłankową lub dodatkowo z ϕ, ϕ, Γ00⇒ ∆00 przez regułę dwuprzesłankową. W każdym przy-padku przesłanki podpadają pod założenia indukcyjne, zatem ϕ, Γ0⇒ ∆0 (i ϕ, Γ00⇒ ∆00) mają dowody długości mniejszej od n skąd przez zastosowanie tej samej reguły jedno (lub dwu) przesłankowej dostajemy dowód ϕ, Γ ⇒ ∆ o długości co najwyżej n.
Jeżeli ϕ jest formułą zasadniczą w dowodzonym sekwencie, to musimy rozważyć wszystkie przypadki formy ϕ. Niech ϕ := ψ ∧ χ. Wtedy rozważa-ny sekwent ma postać ψ ∧ χ, ψ ∧ χ, Γ ⇒ ∆, a przesłanka postać ψ, χ, ψ ∧ χ, Γ ⇒ ∆ i dowód długości n − 1. Z lematu poprzedniego (o odwracalności) ψ, χ, ψ, χ, Γ ⇒ ∆ też ma dowód o długości nie większej od n − 1. Z za-łożenia indukcyjnego zastosowanego dwukrotnie mamy dowód ψ, χ, Γ ⇒ ∆
4.4. RÓWNOWAŻNOŚĆ REGUŁ 77