krót-sze zatem podpadają pod założenie indukcyjne, czyli Γ, ¬∆0, ¬ϕ `H ⊥ i Γ, ¬∆0, ¬ψ `H ⊥. Z lematu 1.1, własność 9, mamy Γ, ¬∆0`H ϕ i Γ, ¬∆0 `H ψ. Z aksjomatu 5 przez własność 6 lematu 1.1 mamy ϕ, ψ `H ϕ ∧ ψ, co po dwukrotnym zastosowaniu własności 4 daje Γ, ¬∆0 `H ϕ ∧ ψ, czyli (przez własność 9) Γ, ¬∆0, ¬(ϕ ∧ ψ) `H ⊥.
Z lematu 3.4 przy Γ pustym i ∆ := ϕ otrzymujemy przez lemat 1.1 konwers lematu 3.3, a to daje dowód twierdzenia 3.1.
3.3 Semantyczna interpretacja
Dla rozważań przeprowadzonych w następnym rozdziale wygodnie będzie już teraz wprowadzić semantyczne ujęcie LK, a w zasadzie dowolnego wariantu RS. Niezależnie od podanego wyżej dowodu udowodnimy też semantyczny lemat o przystosowaniu LK, co wymaga z kolei uprzedniego zdefiniowania sposobu semantycznej interpretacji sekwentów. Można oczywiście odwołać się do podanego wyżej sposobu przekładu sekwentów na formuły, wygodniej jest jednak zrobić to bezpośrednio, wzmacniając semantykę przez podanie dodatkowego warunku prawdziwości (spełniania) sekwentów o postaci: M Γ ⇒ ∆ wtw przynajmniej jedna formuła w poprzedniku jest fałszywa lub przynajmniej jedna w następniku jest prawdziwa.
Falsyfikację sekwentu definiujemy następująco:
M 2 Γ ⇒ ∆ wtw każda formuła w poprzedniku jest prawdziwa, a każda w następniku jest fałszywa.
W oczywisty sposób na sekwenty poszerza się inne ważne pojęcia seman-tyczne; tutaj ograniczymy się do tautologiczności. To, że sekwent jest tau-tologiczny będziemy zaznaczać w taki sam sposób jak w przypadku formuł poprzez użycie |=.
|= Γ ⇒ ∆ wtw ∀M, M Γ ⇒ ∆
Łatwo wykazać, że taki sposób semantycznej interpretacji sekwentu jest zgodny z syntaktyczną interpretacją zaproponowaną przez Gentzena. Ujmuje to poniższy fakt, którego dowód pominiemy:
Fakt 3.3 M ϕ1, ...ϕi⇒ ψ1, ...ψk wtw M ϕ1∧ ... ∧ ϕi→ ψ1∨ ... ∨ ψk Przy zadanej wyżej interpretacji możemy wykazać:
Lemat 3.5 Każda reguła LK jest niezawodna
Dowód: Należy pokazać, że jeżeli przesłanki reguły są tautologiczne, to wniosek też.
Przypadek (→⇒): Załóżmy, że |= Γ ⇒ ∆, ϕ i |= ψ, Π ⇒ Σ ale 6|= ϕ → ψ, Γ, Π ⇒ ∆, Σ. Zatem w pewnym modelu M zarówno ϕ → ψ jak i wszystkie elementy Γ i Π są spełnione natomiast wszystkie elementy ∆ i Σ są tam fał-szywe. Skoro M ϕ → ψ, to M 2 ϕ lub M ψ. Oba przypadki prowadzą do sprzeczności; przy pierwszym lewa, a przy drugim prawa przesłanka byłaby sfalsyfikowana w M.
Lemat 3.6 (Przystosowanie) Jeżeli ` Γ ⇒ ∆, to |= Γ ⇒ ∆
Dowód: Przez indukcję po długości dowodu Γ ⇒ ∆. Dowód bazy jest oczy-wisty, gdyż każdy jednoelementowy dowód to sekwent aksjomatyczny, który jest tautologią. Pokazujemy, że dowód sekwentu Γ ⇒ ∆ o długości n jest dowodem tautologii przy założeniu, że każdy dowód krótszy spełnia ten wa-runek. Ponieważ dowód każdej z przesłanek sekwentu Γ ⇒ ∆ ma długość mniejszą od n, więc przesłanki podpadają pod założenie indukcyjne i są se-kwentami tautologicznymi. Zgodnie z poprzednim lematem każda reguła LK jest niezawodna, więc wydedukowany sekwent też jest tautologiczny.
Ponieważ przedstawiona przez nas w rozdziale 1 aksjomatyka KRZ jest pełna, więc lemat 3.3 implikuje (słabą) pełność LK, a to wraz z ostatnim le-matem daje adekwatność LK względem semantycznie scharakteryzowanego KRZ. Niezależne od uzyskanego tutaj wyniku w dalszym ciągu podamy też bezpośrednie dowody pełności dla LK i innych wariantów RS, które zapre-zentujemy w rozdziale 7.
Rozdział 4
Warianty standardowego RS
dla KRZ
Istnieje wiele wariantów RS, które są równoważne rachunkowi LK w sensie posiadania dokładnie takiego samego zbioru sekwentów dowiedlnych. Zatem dają one również adekwatną formalizację KRZ, a ponadto, podobnie jak LK, można je modyfikować tak by dostarczyły charakteryzacji innych logik. Pomimo równoważności tych rachunków wybór takiej lub innej wersji ma wpływ na posiadanie lub brak wielu istotnych własności, które będziemy w dalszym ciągu rozważać. Dlatego w tym rozdziale zbiorczo omówimy kilka najważniejszych sposobów modyfikacji i ich bezpośrednich konsekwencji. Za-czniemy od omówienia podstawowych wariantów reguł: Gentzena i Ketonena oraz k-jednolitych i k-niezależnych. W podrozdziale 4.2 skupimy się na pro-blemie odwracalności reguł i wprowadzimy system LK-K. Następny podroz-dział będzie poświęcony omówieniu systemu ARS, w którym nie występują żadne reguły strukturalne, włączając w to (Cut). W kolejnych podrozdzia-łach udowodnimy rezultat pozwalający na łatwe generowanie rozmaitych wa-riantów reguł i udowadnianie ich równoważności (4.4), oraz omówimy istotne własności reguł RS (4.5). Na koniec (4.6) omówimy sposoby budowania RS dla KRZ na int-sekwentach.
4.1 Warianty reguł
Aby wykazać równoważność dwóch systemów RS i RS0 musimy pokazać, że każda reguła pierwotna RS jest regułą wtórną RS’ i odwrotnie. Wprowa-dzony w kontekście rachunków aksjomatycznych podział reguł wtórnych na wyprowadzalne i dopuszczalne przeniesiemy obecnie na RS.
Definicja 4.1 Reguła S1, ..., Sn
S jest wyprowadzalna w RS wtedy, gdy w RS mamy deduk-cję S z S1, ..., Sn.
Reguła S1, ..., Sn
S jest dopuszczalna w RS wtedy, gdy jeżeli w RS mamy dowody sekwentów S1, ..., Sn, to mamy też dowód S.
Oczywiście każda reguła wyprowadzalna jest regułą dopuszczalną, gdyż jeżeli do dedukcji S z S1, ..., Snmożemy dodać dowód każdej z przesłanek (tj. dopisać go nad odpowiednim sekwentem Si), to uzyskujemy w ten sposób dowód S. Zależność w drugą stronę nie zachodzi1.
Wykazywanie wyprowadzalności reguł jest zadaniem stosunkowo prostym – wymaga skonstruowania schematu dedukcji sekwentu wniosku z przesłanek przy użyciu reguł pierwotnych. Zabiegu takiego już wyżej dokonaliśmy (w dowodzie lematu 3.3) pokazując, że reguła MP postaci: ⇒ ϕ, ⇒ ϕ → ψ/ ⇒ ψ jest w LK wyprowadzalna. W tym rozdziale rozważymy wiele takich warian-tów reguł LK, które są w nim wyprowadzalne, ale prowadzą do uzyskania interesujących wariantów RS.
Dla odmiany, wykazywanie w sposób syntaktyczny dopuszczalności re-guły, która nie jest w danym systemie wyprowadzalna wymaga często sporo wysiłku i pomysłowości. Zazwyczaj sprowadza się to do wykazania, że każde zastosowanie takiej reguły w danym systemie można z dowodu wyelimino-wać, stąd często zamiast o dopuszczalności mówi się o eliminowalności takiej reguły z danego rachunku. W rozdziale 5 zaprezentujemy takie dowody dla (Cut), ale już w tym rozdziale przeprowadzimy dowody dopuszczalności roz-maitych reguł strukturalnych w pewnych wariantach RS. Zauważmy też, że choć syntaktyczne dowody dopuszczalności reguł są nietrywialne, to mamy proste kryterium semantyczne ich identyfikacji, które wyraża poniższy lemat. Lemat 4.1 Jeżeli RS jest adekwatne względem semantyki SEM i reguła (r) jest niezawodna w SEM, to jest dopuszczalna w RS.
Dowód: Załóżmy, że każda przesłanka (r) ma dowód w RS. Z racji przysto-sowania RS do SEM są one tautologiczne, a ponieważ (r) jest niezawodna w SEM, to wniosek (r) też jest tautologiczny. Z racji pełności RS wniosek ten musi mieć dowód w RS.
1
Pomijając przypadek strukturalnej zupełności pewnych aksjomatycznych formalizacji KRZ – por. uwaga 1.9.
4.1. WARIANTY REGUŁ 63 Lemat ten pozwala w prosty sposób wykazywać dopuszczalność reguł w danym RS, gdyż sprawdzenie ich niezawodności zazwyczaj nie sprawia kłopo-tu. Niestety często aby wykazać adekwatność RS względem danej semantyki potrzebujemy właśnie tych reguł, których dopuszczalność mamy wykazać, a w takiej sytuacji powyższe kryterium jest bezużyteczne.
4.1.1 Aksjomaty uogólnione
W sformułowaniu reguł wielu wariantów RS wymaga się, aby każde podsta-wienie (AX) było sekwentem atomowym. Przy okazji dowodu wielu twier-dzeń pokażemy potrzebę takiego obostrzenia, natomiast teraz wykażemy, że takie ograniczenie w stosunku do sekwentów aksjomatycznych nie powoduje osłabienia RS.
Lemat 4.2 Jeżeli w RS jedyne sekwenty aksjomatyczne są sekwentami ato-mowymi, to ` ϕ ⇒ ϕ dla dowolnego ϕ
Dowód przeprowadzimy przez indukcję po długości ϕ. Wystarczy zbudować schematy dowodów pokazujące, że ϕ ⇒ ϕ dla ϕ o dowolnej strukturze można wydedukować z sekwentów ψ ⇒ ψ, gdzie ψ jest formułą krótszą od ϕ. Jeżeli ϕ := ϕ ∧ ψ, to można zbudować następujący schemat dowodu:
ϕ ⇒ ϕ (∧ ⇒) ϕ ∧ ψ ⇒ ϕ ψ ⇒ ψ (∧ ⇒) ϕ ∧ ψ ⇒ ψ (⇒ ∧) ϕ ∧ ψ ⇒ ϕ ∧ ψ
Z drugiej strony dla ułatwienia dowodu wielu twierdzeń wygodne jest dysponowanie uogólnioną wersją aksjomatów, w której na miejscu ϕ może występować dowolna formuła. Przykładowo korzystaliśmy z tego faktu w do-wodzie lematu 3.1, gdyby aksjomaty w LK były ograniczone do atomowych, to wcześniej musielibyśmy i tak dowieść poprzedni lemat.
Zauważmy, że dopuszczalną postać aksjomatów można uogólnić jeszcze bardziej poprzez zastosowanie do sekwentów aksjomatycznych reguł osłabia-nia i permutacji. Odnotujmy to jako
Lemat 4.3 Jeżeli ciągi Γ i ∆ mają przynajmniej po jednym wystąpieniu takiej samej formuły, to ` Γ ⇒ ∆
Rozróżnijmy dla wygody możliwe formy aksjomatów: oryginalna forma Gentzena to (AXn), czyli sekwent nieatomowy, ale dwuelementowy. Jego
ograniczenie do formuł atomowych, to (AXa), czyli sekwent dwuelemento-wy atomodwuelemento-wy. Wersja uogólniona z podanego dwuelemento-wyżej lematu, to (U AXn). W szczególności możemy też ograniczyć się do takiej wersji uogólnionej, gdzie sekwent aksjomatyczny Γ ⇒ ∆ zawiera w poprzedniku i następniku wspólną formułę atomową; oznaczmy ją jako (U AXa). Jest ona dowiedlna bezpo-średnio z (AXa) przez osłabianie i permutację. Jeżeli w grę będzie wchodziła dowolna postać aksjomatu, to będziemy po prostu używać skrótu (AX). Po-nieważ (AXa) jest szczególnym przypadkiem wszystkich pozostałych wersji, a one z niego dadzą się wydedukować, więc możemy stwierdzić:
Twierdzenie 4.1 Wersje RS z następującymi formami sekwentów aksjoma-tycznych są równoważne:
1. ϕ ⇒ ϕ, dla dowolnej zmiennej ϕ 2. ϕ ⇒ ϕ, dla dowolnej formuły ϕ
3. Γ, ϕ, Π ⇒ Σ, ϕ, ∆, dla dowolnej zmiennej ϕ 4. Γ, ϕ, Π ⇒ Σ, ϕ, ∆, dla dowolnej formuły ϕ
4.1.2 Warianty reguł dwuprzesłankowych
Daleko ważniejsza różnica w konstrukcji przyjmowanych reguł dotyczy ro-li parametrów, czyro-li kontekstu danej reguły. Zauważmy, że w oryginalnym systemie Gentzena występuje istotna asymetria pomiędzy regułami (⇒ ∧) i (∨ ⇒) z jednej strony, a (Cut) i (→⇒) z drugiej. W regułach dla ∧ i ∨ obie przesłanki mają takie same listy parametrów jak wniosek; w pozostałych regułach 2-przesłankowych listy parametrów we wniosku to konkatenacja różnych list występujących w przesłankach. Reguły pierwszego typu, które wymagają dla swojego zastosowania jednolitego kontekstu w obu przesłan-kach, określiliśmy w rozdziale 2 jako k-jednolite (context-sharing), a regu-ły drugiego typu jako k-niezależne (niezależne od kontekstu, context-free, context-independent). Łatwo zauważyć, że LK Gentzena można zmodyfi-kować na dwa różne sposoby dokonując ujednolicenia kształtu reguł. Obie reguły dla ∧ i ∨ można zastąpić przez warianty k-niezależne stosowalne bez konieczności uzgodnienia list parametrów w przesłankach:
(⇒∧) Γ⇒ ∆, ϕΓ, Π⇒ ∆, Σ, ϕ∧ψΠ⇒ Σ, ψ (∨⇒) ϕ, Γ⇒ ∆ϕ∨ψ, Γ, Π⇒ ∆, Σψ, Π⇒ Σ Z drugiej strony możemy (Cut) i (→⇒) zastąpić przez warianty k-jednolite, w których listy parametrów w obu przesłankach są identyczne jak we wnio-sku. Obie reguły wyglądają wtedy następująco:
4.1. WARIANTY REGUŁ 65 (Cut) Γ⇒ ∆, ϕΓ⇒ ∆ϕ, Γ⇒ ∆ (→⇒) Γ⇒ ∆, ϕϕ → ψ, Γ⇒ ∆ψ, Γ⇒ ∆
Łatwo wykazać, że reguły k-niezależne są wyprowadzalne z reguł k-jednolitych, przy użyciu osłabiania i permutacji do przesłanek. Natomiast reguły k-jednolite są wyprowadzalne z reguł k-niezależnych przy użyciu kontrakcji na wniosku. To, że w systemie Gentzena występują oba rodzaje reguł wiązało się głów-nie z tym, że dokonał on równocześgłów-nie formalizacji logiki intuicjonistycznej (por. uwaga 3.3). Poniżej pokażemy, że wybór któregoś rodzaju reguł ma istotne znaczenie, najpierw jednak rozważymy jeszcze jeden wariant reguł sekwentowych.
4.1.3 Reguły Ketonena
Występowanie dwóch reguł (⇒ ∨) i (∧ ⇒) również wiązało się z kwestią formalizacji logiki intuicjonistycznej i w przypadku RS dla KRZ ujawnia pewne trudności:
• w wielu dowodach nie można uniknąć zastosowań kontrakcji;
• prowadzi do komplikacji w przypadku zastosowań LK jako procedury rozstrzygalnej;
• reguły te nie są odwracalne.
Co do pierwszego punktu, to najlepiej zilustruje go poniższy Przykład 4.1. p ⇒ p (W ⇒) q, p ⇒ p (⇒→) p ⇒ q → p (⇒ ∨) p ⇒ (p → q) ∨ (q → p) (⇒ W ) p ⇒ (p → q) ∨ (q → p), q (⇒→) ⇒ (p → q) ∨ (q → p), p → q (⇒ ∨) ⇒ (p → q) ∨ (q → p), (p → q) ∨ (q → p) (⇒ C) ⇒ (p → q) ∨ (q → p)
Taka konstrukcja reguł okazuje się jeszcze bardziej kłopotliwa w przy-padku zastosowań RS jako procedury rozstrzygalnej, co omówimy dokładnie w rozdziale 6. Z drugiej strony łatwo zauważyć, że sposób interpretacji po-przednika jako koniunkcji, a następnika jako alternatywy elementów pozwala
uniknąć tych problemów i wprowadzić pojedyncze reguły, tak jak w przypad-ku implikacji. Reguły takie o postaci:
(∧⇒) ϕ∧ψ, Γ⇒ ∆ϕ, ψ, Γ⇒ ∆ (⇒∨) Γ⇒ ∆, ϕ∨ψΓ⇒ ∆, ϕ, ψ jako pierwszy wprowadził Ketonen [82]. Łatwo dowieść:
Lemat 4.4 W dowolnym systemie RS z kontrakcją i osłabianiem reguły Gentzena i Ketonena są równoważne.
Dowód: Aby dowieść wyprowadzalność wariantu Ketonena wystarczy do przesłanki dwukrotnie zastosować wariant Gentzena, a następnie kontrakcję. Aby dowieść wyprowadzalność wariantu Gentzena wystarczy do przesłanki zastosować osłabianie by uzyskać brakującą formułę poboczną, a następnie użyć reguły Ketonena.
Dowód powyższego sekwentu z użyciem wariantu Ketonena wygląda na-stępująco: Przykład 4.2. q ⇒ q (W ⇒) p, q ⇒ q (⇒→) 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ł.