Analizując kwestię czy aparat Gentzena daje potencjalnie mocniejszą teorię konsekwencji od teorii Tarskiego musimy pamiętać, że mamy do rozważenia co najmniej 3 możliwe sposoby generowania relacji konsekwencji przez RS:
1. Konsekwencja w sensie Scotta, czyli generowana przez ⇒ w sekwentach złożonych ze zbiorów.
2. Konsekwencja w sensie Avrona, czyli generowana przez ⇒ w sekwen-tach złożonych z multizbiorów i z osłabionym zestawem warunków strukturalnych.
3. Konsekwencja w sensie Jansany, czyli generowana przez sekwenty, ` ⊆ P(Sek) × Sek gdzie Sek to zbiór wszystkich sekwentów.
2.4. RS A RELACJE KONSEKWENCJI 41 Można oczywiście rozważać jeszcze inne możliwości, np. w punkcie 2 z multizbiorów przejść na ciągi, a w 3 w następniku ` też przyjąć zbiory se-kwentów, a nie sekwenty. Co więcej, raz uogólniwszy pojęcie konsekwencji z formuł na sekwenty można rozbudowywać tę hierarchię dalej i rozważać kon-sekwencje, które zachodzą między zbiorami reguł sekwentowych itd. (por. Zucker, Tragesser [154]).
Porównując konsekwencje w sensie Scotta z operacjami konsekwencji w sensie Tarskiego przypomijmy, że operacja konsekwencji w sensie Tarskiego Cn : P(F OR) −→ P(F OR) ma następujące podstawowe własności struktu-ralne:
• (ZWR) Γ ⊆ Cn(Γ)
• (MON) Jeżeli Γ ⊆ ∆, to Cn(Γ) ⊆ Cn(∆) • (TR) Cn(Cn(Γ)) ⊆ Cn(Γ)
Które można w ujęciu relacyjnym wyrazić następująco (poprzez Γ |= ϕ := ϕ ∈ Cn(Γ)):
• (ZWR) ϕ |= ϕ
• (MON) Jeżeli Γ |= ϕ, to Γ, ψ |= ϕ
• (TR) Jeżeli Γ |= ϕ oraz ϕ, Γ |= ψ, to Γ |= ψ
Konkretnym przykładem takiej relacji zdefiniowanym syntaktycznie by-ła relacja dowiedlności w systemie aksjomatycznym podana w paragrafie 1.2.2. Dodatkowo konsekwencja jest finitarna wtw dla dowolnego ϕ i Γ, je-żeli ϕ ∈ Cn(Γ), to można znaleźć skończony zbiór ∆ ⊆ Γ, którego ϕ jest konsekwencją.
Charakterystyka klasycznych stałych logicznych w teorii operacji konse-kwencji wygląda następująco:
• (¬) ϕ ∈ Cn(Γ) wtw Cn(Γ ∪ {¬ϕ}) = F OR • (∧) Cn({ϕ, ψ}) = Cn({ϕ ∧ ψ})
• (∨) Cn({ϕ}) ∩ Cn({ψ}) = Cn({ϕ ∨ ψ}) • (→) ψ ∈ Cn(Γ ∪ {ϕ}) wtw ϕ → ψ ∈ Cn(Γ) lub (w ujęciu relacyjnym):
• (¬) Γ |= ϕ wtw Γ, ¬ϕ |= • (∧) ϕ, ψ |= γ wtw ϕ ∧ ψ |= γ
• (∨) Γ, ϕ |= γ i Γ, ψ |= γ wtw Γ, ϕ ∨ ψ |= γ • (→) Γ, ϕ |= ψ wtw Γ |= ϕ → ψ
Dowolna relacja konsekwencji Scotta |= ⊆ P(F OR) × P(F OR) jest cha-rakteryzowana następująco:
• (ZWR) ϕ |= ϕ
• (MON) Jeżeli Γ ⊆ Γ0 i ∆ ⊆ ∆0 oraz Γ |= ∆, to Γ0 |= ∆0
• (TR) Jeżeli Γ |= ∆, ϕ i ϕ, Γ |= ∆, to Γ |= ∆
Charakterystykę stałych logicznych można ująć za pomocą następujących warunków:
• (¬) |= ϕ, ¬ϕ, oraz ϕ, ¬ϕ |=
• (∧) Γ, ϕ, ψ |= ∆ wtw Γ, ϕ ∧ ψ |= ∆ • (∨) Γ |= ∆, ϕ, ψ wtw Γ |= ∆, ϕ ∨ ψ • (→) Γ, ϕ |= ∆, ψ wtw Γ |= ∆, ϕ → ψ
Oczywiście spójniki te można zdefiniować za pomocą innych równoważ-ności:
• (∧0) Γ |= ∆, ϕ i Γ |= ∆, ψ wtw Γ |= ∆, ϕ ∧ ψ • (∨0) ϕ, Γ |= ∆ i ψ, Γ |= ∆ wtw ϕ ∨ ψ, Γ |= ∆ • (→0) Γ |= ∆, ϕ i ψ, Γ |= ∆ wtw ϕ → ψ, Γ |= ∆
Obie charakterystyki są równoważne4. Dla przykładu wykażemy to dla koniunkcji.
(∧) implikuje (∧0):
=⇒ Załóżmy, że Γ |= ∆, ϕ i Γ |= ∆, ψ. Z ϕ ∧ ψ |= ϕ ∧ ψ, które jest instancją (ZWR) wynika, przez (∧), ϕ, ψ |= ϕ ∧ ψ. To ostatnie przez dwa użycia (TR) (i (MON)) do założeń daje Γ |= ∆, ϕ ∧ ψ.
2.4. RS A RELACJE KONSEKWENCJI 43 ⇐= Załóżmy, że Γ |= ∆, ϕ ∧ ψ. Ponieważ (ZWR) i (MON) daje ϕ, ψ, Γ |= ∆, ϕ, skąd, przez (∧), mamy ϕ ∧ ψ, Γ |= ∆, ϕ, więc przez (TR) otrzymujemy Γ |= ∆, ϕ. W analogiczny sposób otrzymujemy Γ |= ∆, ψ.
(∧0) implikuje (∧):
=⇒ Załóżmy, że Γ, ϕ, ψ |= ∆. Z ϕ ∧ ψ |= ϕ ∧ ψ otrzymujemy przez (∧0) zarówno ϕ ∧ ψ |= ϕ jak i ϕ ∧ ψ |= ψ. Dwa zastosowania (TR) i (MON) do założenia prowadzą do Γ, ϕ ∧ ψ |= ∆.
⇐= ϕ, ψ, Γ |= ∆, ϕ i ϕ, ψ, Γ |= ∆, ψ, które uzyskujemy przez (ZWR) i (MON) prowadzą, przez (∧0) do ϕ, ψ, Γ |= ∆, ϕ ∧ ψ. Stąd i z założenia Γ, ϕ ∧ ψ |= ∆ przez (TR) otrzymujemy Γ, ϕ, ψ |= ∆.
Scott analizując stosunek swojej teorii do teorii Tarskiego odnotował, że związek wyznaczony wzorem:
Γ ` ϕ wtw ϕ ∈ Cn(Γ)
nie musi być wzajemnie jednoznaczny. Wprawdzie każda konsekwencja Scot-ta jednoznacznie definiuje konsekwencję w sensie Tarskiego, ale konwers w ogólności nie zachodzi, tzn. każda operacja Cn wyznacza pewną klasę relacji konsekwencji `. Dokładniej rzecz ujmując mamy co następuje:
1. Każda relacja ` ⊆ P(F OR) × P(F OR) spełniająca warunki (ZWR), (MON), (TR) wyznacza operację konsekwencji Cn`(Γ) = {ϕ : ∆ ` ϕ}, gdzie ∆ to dowolny skończony podzbiór Γ.
2. Dla danej operacji Cn zdefiniujemy dwie relacje: Γ `min∆ wtw Cn(Γ) ∩ ∆ 6= ∅ oraz
Γ `max∆ wtw T
ϕ∈∆Cn(Γ0∪ {ϕ}) ⊆ Cn(Γ0), dla dowolnego Γ0 ⊇ Γ. Obie są relacjami konsekwencji w sensie Scotta a ponadto wyznaczają klasę relacji konsekwencji C taką, że dla każdej ` ∈ C:
• `min ⊆ ` ⊆ `max
• Cn = Cn` wtw `min ⊆ ` ⊆ `max
Wynik ten pokazuje, że aparat teorii relacji Scotta może być bardziej subtelnym narzędziem badawczym. Wprawdzie w przypadku zbiorów skoń-czonych oba podejścia są wzajemnie definiowalne: w bezpośredni sposób, gdy w języku dysponujemy alternatywą i w trochę bardziej złożony w przypadku
jej braku5. Jednak w przypadku zbiorów nieskończonych sytuacja jest inna. Rozważmy zbiór H` dopuszczalnych waluacji, które spełniają pewną (Tar-skiego lub Scotta) ` (tzn. h ∈ H` wtw dla żadnego Γ ` ∆ nie zachodzi, że hΓ ⊆ {1} i h∆ ⊆ {0}).
Naturalnie, ponieważ każda semantyka generuje relację konsekwencji mo-żemy rozważać relację generowaną przez H`, tzn. `H` jak również H`H, tzn., zbiór dopuszczalnych waluacji, które spełniają `H. łatwo można dowieść, że zachodzą następujące własności Galois:
1. `1⊆ `2 implikuje H`2 ⊆ H`1 2. H1 ⊆ H2 implikuje `H2⊆ `H1 3. H ⊆ H`H
4. ` ⊆ `H`
Dowody punktów 1 i 2 można znaleźć np. w Wójcicki [150] dla konsekwencji Tarskiego i łatwo uogólnić na przypadek relacji Scotta. Dowód pominiemy, gdyż bardziej interesujące są przypadki 3 i 4.
Punkt 4 można wzmocnić do równości dzięki abstrakcyjnej wersji twier-dzenia Lindenbauma. Wynik ten zachodzi też dla relacji Scotta, ale wyma-ga innej konstrukcji, nazywanej atlasem Scotta przez Dunna i Hardegree [36]. Ważna różnica między konsekwencją w sensie Tarskiego i Scotta leży w punkcie 3. W przypadku konsekwencji Tarskiego każda relacja determinuje semantykę, ale niekoniecznie jedną. Z drugiej strony, dla konsekwencji Scot-ta własność 3 może być wzmocniona do równości co znaczy, że każda Scot-taka relacja determinuje dokładnie jedną taką semantykę. Zauważmy, że jest to własność dualna do pełności; Dunn i Hardegree [36] nazywają tę własność absolutnością i podkreślają jej ważność, wskazując, że jest ona analogiczna do własności kategoryczności teorii.
Jak wspomnieliśmy w poprzednim podrozdziale, okazuje się, że gdy zbio-ry zastąpimy multizbiorami, to znacznie wzrośnie ilość logik, które można scharakteryzować. Avron [9] przedstawia następującą klasyfikację relacji kon-sekwencji:
• Dowolna relacja ` na skończonych multizbiorach formuł spełniająca warunki (ZWR) i (TR) (zwrotna i przechodnia) jest prostą relacją konsekwencji.
5
Szczegóły konstrukcji oraz dowód podanego wyżej rezultatu można znaleźć w Wój-cicki [150].
2.4. RS A RELACJE KONSEKWENCJI 45 • Prosta relacja konsekwencji spełniająca warunek (C) (kontrakcji) i jego konwers (czyli zdefinowana na zbiorach) jest regularną relacją konse-kwencji.
• Regularna relacja konsekwencji spełniająca warunek (MON) (monoto-niczności) jest relacją konsekwencji w sensie Scotta.
• Regularna relacja konsekwencji spełniająca warunek (MON) (monoto-niczności) typu many-one jest relacją konsekwencji w sensie Tarskiego. W przypadku prostych relacji konsekwencji, nawet tych, które dodat-kowo spełniają warunek (MON) uzyskujemy możliwość generowania wielu logik, których nie zdefiniujemy nawet na gruncie teorii konsekwencji Scotta. Wspominaliśmy już wcześniej (uwaga 2.3) o przypadku logik podstruktural-nych dokonując rozróżnienia między spójnikami addytywnymi i multiplika-tywnymi. Użyte przez nas wyżej warunki (∧), (∨), (→) definiowały spójniki multiplikatywne, natomiast warunki (∧0), (∨0), (→0) definiowały spójniki ad-dytywne. Jeżeli oba zestawy warunków porównamy z podanymi w paragrafie 2.2.1 regułami dla koniunkcji, to łatwo zauważymy, że (d0) otrzymujemy bez-pośrednio z warunku (∧), a (c00) z (∧0). Wyprowadzenie reguły (c0) z (∧) oraz reguł (d001) i (d002) z (∧0) wymaga trochę więcej wysiłku – zachęcamy do jego podjęcia, ewentualnie do skorzystania z lematu 4.13.
Na koniec wspomnijmy, że można też rozważać konsekwencje generowane nie przez sekwenty, ale przez reguły sekwentowe. W tym przypadku ` nie odpowiada ⇒, ale linii oddzielającej przesłanki od konkluzji w regułach, czyli ` ⊆ P(Sek) × Sek. Takie podejście było rozwinięte przez hiszpańskich logików skupionych wokół ośrodka w Barcelonie (Font, Jansana). Ściśle rzecz biorąc ograniczyli oni swoje rozważania do konsekwencji definiowanych na sekwentach typu intuicjonistycznego, ale podejście to można uogólnić na inne rodzaje sekwentów. Wprowadzenie do tak rozumianych relacji konsekwencji zawiera Font [44].
LK Gentzena dla KRZ
W tym rozdziale zaprezentujemy zdaniową część oryginalnego systemu Gent-zena LK. Sposób prezentacji i wprowadzona terminologia odbiega jednak od oryginalnego ujęcia Gentzena, a zgodna jest ze sposobami prezentacji we współczesnych opracowaniach. Wprowadzona poniżej terminologia będzie miała charakter uniwersalny w tym sensie, że zdefiniowane pojęcia stosują się nie tylko do LK ale również do innych wersji RS wprowadzonych w kolej-nych rozdziałach. Ograniczymy się zasadniczo do prezentacji czysto syntak-tycznych aspektów RS. Omówimy reguły LK, konstrukcję dowodów i pewne własności dowolnego RS (3.1) oraz wykażemy adekwatność LK przez dowód równoważności z H-systemem z rozdziału 1 (3.2). W ostatnim podrozdzia-le wyjdziemy poza syntaktyczne aspekty – poszerzymy semantykę KRZ na sekwenty i udowodnimy semantyczne przystosowanie LK.