q ⇒ p → q (⇒ W ) q ⇒ p → q, p (⇒→) ⇒ p → q, q → p (⇒ ∨) ⇒ (p → q) ∨ (q → p)
Wprowadzając warianty Ketonena na miejsce reguł Gentzena uzyskujemy nie tylko uproszczenie w repertuarze reguł (tylko jedna zamiast dwóch) i prostsze dowody, ale także ważną własność zwaną odwracalnością, której omówieniu poświęcimy następny podrozdział.
4.2 Odwracalność reguł
Rozróżnienie pomiędzy regułami k-jednolitymi i k-niezależnymi w przypadku reguł dwuprzesłankowych, oraz wariantami Gentzena i Ketonena dla reguł jednoprzesłankowych ma niebagatelne znaczenie. Po pierwsze, w rozdziale 2 wspominaliśmy, że dwuprzesłankowe reguły k-jednolite wraz z podwójnymi regułami jednoprzesłankowymi (tylko jedna formuła poboczna w przesłance) definiują w zasadzie inne stałe logiczne (addytywne) niż dwuprzesłankowe
4.2. ODWRACALNOŚĆ REGUŁ 67 reguły k-niezależne wraz z jednoprzesłankowymi regułami Ketonena (mul-tiplikatywne). Toteż w LK ∨ i ∧ są addytywne a → jest multiplikatywna. Zauważmy przy okazji, że dla addytywnej wersji → oprócz k-jednolitej reguły dwuprzesłankowej musielibyśmy użyć też dwóch reguł jednoprzesłankowych, mianowicie:
(⇒→1) Γ⇒ ∆, ϕ → ψϕ, Γ⇒ ∆ (⇒→2) Γ⇒ ∆, ϕ → ψΓ⇒ ∆, ψ
Jak widać moglibyśmy na podstawie tego rozróżnienia wprowadzić dwa warianty LK: LK-M (multiplikatywny) i LK-A (addytywny). Oba charak-teryzowałyby jednak KRZ, gdyż jak pokazaliśmy wyżej, przy użyciu reguł strukturalnych są one wzajemnie wyprowadzalne.
Uwaga 4.1: Należy pamiętać, że reguły te definiują różne stałe logiczne dopiero w systemach RS o zubożonym zestawie reguł strukturalnych. W ten sposób można uzyskać sekwentowe formalizacje bardzo wielu logik nie-klasycznych słabszych od logiki klasycznej, zwanych zbiorczo logikami pod-strukturalnymi, właśnie ze względu na to, że ich formalizacje uzyskuje się na drodze zubożenia zestawu reguł strukturalnych. Dokładniej o logikach podstrukturalnych informowaliśmy w uwadze 2.3.
W tym miejscu bardziej interesujący jest dla nas inny wariant – z reguła-mi Ketonena i k-jednolityreguła-mi. Oznaczmy go jako LK-K. Zawiera następujące reguły: (AX) ϕ ⇒ ϕ (Cut) Γ⇒ ∆, ϕΓ⇒ ∆ϕ, Γ⇒ ∆ (W⇒) ϕ, Γ⇒ ∆Γ⇒ ∆ (⇒W ) Γ⇒ ∆, ϕΓ⇒ ∆ (C⇒) ϕ, ϕ, Γ⇒ ∆ϕ, Γ⇒ ∆ (⇒C) Γ⇒ ∆, ϕ, ϕΓ⇒ ∆, ϕ (P⇒) Π, ϕ, ψ, Γ⇒ ∆Π, ψ, ϕ, Γ⇒ ∆ (⇒P ) Γ⇒ ∆, ψ, ϕ, ΠΓ⇒ ∆, ϕ, ψ, Π (¬⇒) ¬ϕ, Γ⇒ ∆Γ⇒ ∆, ϕ (⇒¬) Γ⇒ ∆, ¬ϕϕ, Γ⇒ ∆ (∧⇒) ϕ, ψ, Γ⇒ ∆ ϕ∧ψ, Γ⇒ ∆ (⇒∧) Γ⇒ ∆, ϕ Γ⇒ ∆, ψ Γ⇒ ∆, ϕ∧ψ (⇒∨) Γ⇒ ∆, ϕ∨ψΓ⇒ ∆, ϕ, ψ (∨⇒) ϕ, Γ⇒ ∆ϕ∨ψ, Γ⇒ ∆ψ, Γ⇒ ∆
(⇒→) Γ⇒ ∆, ϕ → ψϕ, Γ⇒ ∆, ψ (→⇒) Γ⇒ ∆, ϕϕ → ψ, Γ⇒ ∆ψ, Γ⇒ ∆
W stosunku do LK różnice są następujące: (Cut) jest w wersji k-jednolitej, reguły (⇒ ∨) i (∧ ⇒) są w wersji Ketonena, a (→⇒) w wersji k-jednolitej.
Wykazaliśmy wyżej, że wszystkie reguły LK-K są wyprowadzalne w LK i odwrotnie, zatem LK-K jest równoważny LK w sensie posiadania takiego samego zbioru sekwentów dowiedlnych. Zatem LK-K też jest adekwatną for-malizacją KRZ. Dla reguł LK-K (z wyjątkiem (W)) zachodzi jednak pewna ważna własność, która nie zachodzi dla wielu reguł LK. Określimy ją jako odwracalność (lub inwersję) i zdefiniujemy w dwóch wersjach:
Definicja 4.2 (Odwracalność reguły) • W wersji semantycznej: je-żeli wniosek jest tautologiczny, to przesłanki też są tautologiczne (reguła odwrotna jest niezawodna)
• W wersji syntaktycznej: przesłanki są dedukowalne z wniosku reguły. Oczywiście w przypadku adekwatności rachunku względem semantyki, na gruncie której definiujemy niezawodność reguł, obie własności są równo-ważne, co łatwo wykazać:
Lemat 4.5 Jeżeli RS jest adekwatne względem semantyki SEM, to reguła (r) jest semantycznie odwracalna wtw jest syntaktycznie odwracalna.
Dowód: Jeżeli reguła (r) nie jest syntaktycznie odwracalna, to dla pewnej przesłanki S1 i wniosku S2 mamy S2 0 S1. Z racji pełności S2 6|= S1, zatem istnieje model spełniający S2 i falsyfikujący S1 co oznacza, że (r) nie jest semantycznie odwracalna. Jeżeli (r) jest syntaktycznie odwracalna, to S2 ` Si, dla każdej przesłanki Si. Zatem, z racji przystosowania S2 |= Si, więc gdy |= S2, to |= Si, co oznacza, że (r) jest semantycznie odwracalna.
Ze względu na podany wyżej lemat i adekwatność LK i LK-K będziemy w dalszym ciągu mówić po prostu o odwracalności. Oczywiście znacznie łatwiej wykazać odwracalność danej reguły semantycznie niż syntaktycznie jednak poniżej zrobimy to dla obu wersji niezależnie. Na początek, korzystając z semantycznej interpretacji sekwentów z rozdziału poprzedniego, pokażemy czemu osłabianie, reguły k-niezależne i Gentzenowskie reguły jednoprzesłan-kowe nie są odwracalne.
Lemat 4.6 W LK własność odwracalności nie zachodzi dla następujących reguł: (Cut), (W ⇒), (⇒ W ), (→⇒), (∧ ⇒), (⇒ ∨)
4.2. ODWRACALNOŚĆ REGUŁ 69 Dowód: Podamy dwa przypadki.
Przypadek (∧ ⇒): Aby pokazać, że choć |= ϕ∧ψ, Γ ⇒ ∆ , to 6|= ϕ, Γ ⇒ ∆, wystarczy rozważyć M falsyfikujący ϕ, Γ ⇒ ∆ i przyjąć, że M 2 ψ, wtedy M 2 ϕ ∧ ψ i M ϕ ∧ ϕ, Γ ⇒ ∆. Analogicznie dla ψ, Γ ⇒ ∆.
Przypadek (→⇒): Podobnie, niech M 2 Γ ⇒ ∆, ϕ, czyli M Γ i M 2 ∆, ϕ. Wystarczy przyjąć, że jakiś element Π jest w M fałszywy lub jakiś element Σ prawdziwy aby M ϕ → ψ, Γ, Π ⇒ ∆, Σ. Analogicznie dla drugiej przesłanki ψ, Π ⇒ Σ.
Ponieważ odwracalność zachodzi dla wszystkich reguł pozostałych (włą-czając w to (Cut) w wersji k-jednolitej) więc sformułujemy to jako specyficz-ną własność LK-K.
Lemat 4.7 (o odwracalności (semantycznej) reguł w K) W LK-K dla każdej reguły oprócz osłabiania, jeżeli wniosek jest tautologiczny, to przesłanki też.
Dowód: Podamy dla porównania dwa przypadki reguł, które zastąpiły w LK-K analizowane powyżej reguły Gentzena.
Przypadek (∧ ⇒) w wersji Ketonena: Załóżmy, że |= ϕ ∧ ψ, Γ ⇒ ∆, ale 6|= ϕ, ψ, Γ ⇒ ∆. Wtedy istnieje M falsyfikujący ϕ, ψ, Γ ⇒ ∆, ale falsyfikuje on również ϕ∧ψ, Γ ⇒ ∆ gdyż M ϕ∧ψ, skoro M ϕ i M ψ. Sprzeczność. Przypadek (→⇒) w wersji k-jednolitej: Załóżmy, że |= ϕ → ψ, Γ ⇒ ∆ ale 6|= Γ ⇒ ∆, ϕ lub 6|= ψ, Γ ⇒ ∆. W pierwszym przypadku pewien M Γ i M 2 ∆, ϕ. Wtedy jednak M ϕ → ψ, a to powoduje, że M 2 ϕ → ψ, Γ ⇒ ∆ – sprzeczność. Analogicznie dla drugiej przesłanki ψ, Γ ⇒ ∆.
Lemat 4.8 (o odwracalności (syntaktycznej) reguł w K) W LK-K dla każdej reguły oprócz osłabiania, jeżeli wniosek ma dowód, to przesłanki też
Dowód: Pokażemy dowód dla (Cut) oraz obu reguł z ∧:
Przypadek (Cut): Każda z przesłanek da się wydedukować przez zasto-sowanie (W) do wniosku. Oczywiście dotyczy to tylko (Cut) w wersji k-jednolitej. Przypadek (∧ ⇒) ϕ ⇒ ϕ ψ ⇒ ψ (⇒ ∧) ϕ, ψ ⇒ ϕ ∧ ψ ϕ, ψ, Γ ⇒ ∆, ϕ ∧ ψ ϕ ∧ ψ, Γ ⇒ ∆ ϕ ∧ ψ, ϕ, ψ, Γ ⇒ ∆ (Cut) ϕ, ψ, Γ ⇒ ∆
Przypadek (⇒ ∧) Γ ⇒ ∆, ϕ ∧ ψ (⇒ W ) Γ ⇒ ∆, ϕ ∧ ψ, ϕ (⇒ P ) Γ ⇒ ∆, ϕ, ϕ ∧ ψ ϕ ⇒ ϕ (W ⇒) ψ, ϕ ⇒ ϕ (P ⇒) ϕ, ψ ⇒ ϕ (∧ ⇒) ϕ ∧ ψ ⇒ ϕ ϕ ∧ ψ, Γ ⇒ ∆, ϕ (Cut) Γ ⇒ ∆, ϕ
Analogicznie dla drugiej przesłanki (Γ ⇒ ∆, ψ) w (⇒ ∧). Dla innych reguł w podobny sposób.
Zauważmy, że w LK-K tylko osłabianie jest nieodwracalne. Jeżeli się go pozbędziemy wprowadzając aksjomaty uogólnione postaci Γ, ϕ ⇒ ∆, ϕ, to syntaktyczny dowód odwracalności wielu reguł w takiej postaci w jakiej po-daliśmy go wyżej, tj. z użyciem (W), stanie się problematyczny. W szcze-gólności, jak pokazaliśmy, syntaktyczny dowód odwracalności (Cut) bazował wyłącznie na użyciu (W). Jak pokażemy jednak w następnym podrozdzia-le jest możliwe uzyskanie wariantu RS z uogólnionymi aksjomatami i bez osłabiania oraz bez (Cut), który będzie systemem w pełni odwracalnym. Uwaga 4.2: Odnotujmy, że syntaktyczny dowód odwracalności reguł prze-prowadzony przy użyciu (Cut) sprowadza się do wykazania, że konwersy od-wracalnych reguł są wyprowadzalne w LK-K. Warto porównać to z dowodem przedstawionym w podrozdziale 4.3, gdzie wrócimy do problemu odwracal-ności reguł, ale w sytuacji braku reguły (Cut) jako pierwotnej.
Warto odnotować przy okazji dowodu poprzedniego lematu, dowiedlność kilku sekwentów, które będziemy dalej wykorzystywać. Pojawiają się one jako sekwenty wyprowadzalne z aksjomatów, a nie z przesłanek.
Fakt 4.1 W LK dowiedlne są następujące sekwenty: • ϕ ⇒ ¬¬ϕ
• ¬¬ϕ ⇒ ϕ • ϕ ∧ ψ ⇒ ϕ • ϕ ∧ ψ ⇒ ψ • ϕ, ψ ⇒ ϕ ∧ ψ
4.3. ELIMINACJA REGUŁ STRUKTURALNYCH 71