Zaprezentowana w poprzednim rozdziale procedura szukania dowodu, która została tam wprowadzona dla udowodnienia rozstrzygalności, pokazuje, że do problemu adekwatności RS bez (Cut) można podejść w sposób bezpo-średni, tzn. zbudować konstruktywny dowód pełności. W przeciwieństwie do dowodu metodą Lindenbauma-Henkina otrzymujemy dla każdego przypadku sekwentu nietautologicznego konkretny przepis na model falsyfikujący.
Dla potrzeb wykazania pełności ARS wprost (tj. bez odwoływania się do twierdzenia o pełności dla wersji z (Cut) i do faktu jej eliminowalności), po-trzebujemy nowego pojęcia, które jest osłabieniem pojęcia maksymalności. Chodzi o pojęcie nasycania w dół, albo saturacji, wprowadzone przez Hin-tikkę (por. paragraf 1.4.3). Obecnie dostosujemy je do ujęcia sekwentowego, tzn. zdefiniujemy dla par zbiorów formuł, a nie dla pojedynczych zbiorów.
Oczywiście można w przypadku KRZ obyć się bez całego aparatu, który dalej wprowadzimy, biorąc pod uwagę prosty dowód pełności dla ARS oparty na semantycznej odwracalności reguł i przedstawiony przez nas w rozdziale 4. Jednak konstrukcje przedstawione poniżej są bardziej ogólne i można je zastosować do dowodzenia pełności wielu innych logik, w tym takich, których sekwentowe formalizacje zawierają reguły nieodwracalne. Kluczowe pojęcie pary zbiorów nasyconych można wprowadzić na co najmniej dwa sposoby:
7.2. DOWÓD ANALITYCZNY PEŁNOŚCI 153 a. bezpośrednio definiując pojęcie nasyconej pary zbiorów formuł; b. pośrednio (np. Goré [54]) sprowadzając nasycanie do pojęcie
domknię-cia na zastosowanie reguły.
7.2.1 Metoda bezpośrednia
Zacznijmy od pierwszej metody, przy której pojęcie pary zbiorów nasyconych wprowadza się definicyjnie.
Definicja 7.3 (Γ, ∆) jest (w dół) nasycona wtw spełnia warunki: 1. jeżeli ¬ϕ ∈ Γ, to ϕ ∈ ∆ 2. jeżeli ¬ϕ ∈ ∆, to ϕ ∈ Γ 3. jeżeli ϕ ∧ ψ ∈ Γ, to ϕ ∈ Γ i ψ ∈ Γ 4. jeżeli ϕ ∧ ψ ∈ ∆, to ϕ ∈ ∆ lub ψ ∈ ∆ 5. jeżeli ϕ ∨ ψ ∈ Γ, to ϕ ∈ Γ lub ψ ∈ Γ 6. jeżeli ϕ ∨ ψ ∈ ∆, to ϕ ∈ ∆ i ψ ∈ ∆ 7. jeżeli ϕ → ψ ∈ Γ, to ϕ ∈ ∆ lub ψ ∈ Γ 8. jeżeli ϕ → ψ ∈ ∆, to ϕ ∈ Γ i ψ ∈ ∆
Uwaga 7.2: Niektórzy dodają warunek niesprzeczności do definicji satura-cji. Ma to wpływ na prostsze sformułowanie twierdzeń o istnieniu modelu, ale w przypadku, gdy chcemy definiować algorytmy szukania dowodu po-przez saturację, to lepiej tego nie przesądzać, gdyż przecież nie wiemy z góry, czy sprawdzany sekwent jest dowiedlny czy nie, tzn. czy odpowiadająca mu para zbiorów jest niesprzeczna. Porównując podaną tu definicję z własno-ściami maksymalnych par wyrażonymi w lemacie 7.7 widzimy, że zamiast równoważności mamy implikacje. Związek tych warunków z regułami ARS czytanymi od wniosku do przesłanek jest oczywisty. Zauważmy, że dowolna para zbiorów zmiennych (nawet pusta) będzie parą Hintikki.
Lemat 7.8 (lemat prawdziwościowy – wersja analityczna) Jeżeli (Γ, ∆) jest nasycona i niesprzeczna, to istnieje model M, taki, że:
• jeżeli ϕ ∈ Γ, to M ϕ; • jeżeli ϕ ∈ ∆, to M 2 ϕ.
Dowód: Definiujemy model przyjmując, że M = ZZ(Γ) i dowodzimy, że spełnia warunki przez indukcję po długości formuł. Baza wynika z definicji. Niech ϕ := ¬ψ:
Jeżeli ¬ψ ∈ Γ, to – przez warunek 1. definicji – ψ ∈ ∆. Z założenia indukcyjnego M 2 ψ ale wtedy M ¬ψ. Przypadek gdy ¬ψ ∈ ∆ dowodzimy symetrycznie.
Analogicznie pozostałe przypadki.
Musimy wykazać, że dla dowolnego sekwentu niedowiedlnego istnieje na-sycona para, która jest jego niesprzecznym poszerzeniem.
Lemat 7.9 (Saturacja) Jeżeli 0 Γ ⇒ ∆, to istnieje nasycona (Π, Σ), taka, że:
(a) Π ∪ Σ ⊆ SF (Γ ∪ ∆);
(b) Π 0 Σ (tzn. (Π, Σ) jest niesprzeczna).
Przypomnijmy, że SF (Γ ∪ ∆) oznacza zbiór wszystkich podformuł wy-stępujących w formułach z Γ ∪ ∆.
Dowód: jest prosty gdyż możemy się odwołać do istnienia procedury szu-kania dowodu zdefiniowanej w rozdziale 6. Jeżeli 0 Γ ⇒ ∆, to w kom-pletnym drzewie dowodowym istnieje co najmniej jedna gałąź, której liść jest nieaksjomatyczny i atomowy. Jest ona skończonym ciągiem sekwentów: Γ ⇒ ∆, ..., Γn⇒ ∆n
Zdefiniujmy: Π =S Γi, Σ =S ∆i, gdzie i ≤ n (tzn. Γi ⇒ ∆i to dowolny sekwent występujący na tej gałęzi) Należy wykazać, że (Π, Σ) jest nasycona oraz spełnia warunki (a) i (b).
Nasycenie wynika z faktu, że warunki definiujące parę nasyconą odpo-wiadają regułom zastosowanym w konstrukcji rozważanej gałęzi.
(a) jest konsekwencją własności podformuł; (b) jest spełniony z definicji (otwarta gałąź).
7.2. DOWÓD ANALITYCZNY PEŁNOŚCI 155 Twierdzenie 7.2 (Pełność:) Jeżeli |= Γ ⇒ ∆, to ` Γ ⇒ ∆.
Dowód:
1. 0 Γ ⇒ ∆ (założenie),
2. istnieje nasycone i niesprzeczne (Π, Σ) (Lemat 7.9. o saturacji), 3. istnieje model falsyfikujący dla (Π, Σ) (Lemat 7.8. prawdziwościowy), 4. istnieje model falsyfikujący dla (Γ, ∆) bo Γ ⊆ Π a ∆ ⊆ Σ,
5. 6|= Γ ⇒ ∆.
W łatwy sposób można dodatkowo przeprowadzić dowód konwersu lema-tu prawdziwościowego.
Lemat 7.10 Jeżeli Γ ⇒ ∆ ma model falsyfikujący, to może być poszerzony do (niesprzecznego) nasyconego sekwentu Π ⇒ Σ.
Dowód: Niech M będzie modelem falsyfikującym Γ ⇒ ∆. Przyjmijmy, że Π = {ϕ : M ϕ}, a Σ = {ϕ : M 2 ϕ}. Jest oczywiste, że Π ∩ Σ = ∅, oraz że Γ ⊆ Π i ∆ ⊆ Σ. Porównując warunki nasycenia z definicją relacji speł-niania widzimy, że (Π, Σ) musi spełniać te warunki, zatem jest nasycony i niesprzeczny.
Zatem mamy twierdzenie:
Twierdzenie 7.3 Γ ⇒ ∆ ma model falsyfikujący wtw może być poszerzona do (niesprzecznego) nasyconego sekwentu.
7.2.2 Dowód pośredni
Alternatywny dowód konstruktywny pełności uzyskujemy pośrednio (np. Go-ré [54]) sprowadzając nasycanie do pojęcie domknięcia na zastosowanie re-guły.
Definicja 7.4 Para (Γ, ∆) jest (w dół) nasycona wtw: (i) jest niesprzeczna;
(ii) Γ ⇒ ∆ jest domknięty na każdą regułę.
Definicja taka jest prostsza, ale oczywiście najpierw trzeba zdefiniować pojęcie domknięcia sekwentu na daną regułę, np. w taki sposób:
Definicja 7.5 Γ ⇒ ∆ jest domknięty na regułę
a) jednoprzesłankową wtw, jeżeli formuła zasadnicza tej reguły należy do sekwentu, to formuły poboczne też należą;
b) dwuprzesłankową wtw, jeżeli formuła zasadnicza tej reguły należy do sekwentu, to co najmniej jedna formuła poboczna też należy.
Uwaga 7.3: Nie tylko brak w definicji 7.4. definiujących warunków, ale wy-magamy też niesprzeczności (w poprzedniej definicji nie było to wymagane – para zbiorów nasyconych mogła być sprzeczna). W konsekwencji w sformu-łowaniu lematu prawdziwościowego wymagamy tylko aby para (Γ, ∆) była nasycona, a w sformułowaniu lematu o saturacji pomijamy warunek (b).
Dowód lematu prawdziwościowego przebiega w podobny sposób choć za-miast do warunków charakteryzujących pary zbiorów Hintikki odwołujemy się do pojęcia domknięcia na reguły. Pozostawiamy to czytelnikowi.
Dowodząc lematu o saturacji tym razem definiujemy algorytm nasycania dla dowolnej niesprzecznej pary formuł (a nie szukania dowodu dla dowolnego sekwentu!). Natomiast wykazać należy, że otrzymana para spełnia warunek (i) i (ii) (tj. niesprzeczność i domknięcie na reguły). W dowodzie wykorzy-stujemy ponadto lemat 4.11 o odwracalności reguł w ARS.1 Przedstawimy poniżej alternatywny dowód lematu o nasycaniu.
Dowód: Definiujemy rekurencyjnie skończony ciąg sekwentów: Γ0 ⇒ ∆0, ... , Γn⇒ ∆n.
a) Γ0 ⇒ ∆0 := Γ ⇒ ∆, jeżeli nie da się zastosować żadna reguła logiczna, to jest to poszukiwany przez nas sekwent nasycony.
b) Rozważmy przejście od i do i + 1. Niech Γi ⇒ ∆i będzie sekwentem otrzymanym w etapie i, który jest niesprzeczny. Jeżeli nie da się zastoso-wać żadna reguła logiczna, to jest to poszukiwany przez nas niesprzeczny sekwent nasycony. W przeciwnym wypadku wybierz formułę ze względu, na którą (Γi, ∆i) nie jest domknięty. Należy rozważyć z osobna przypadek każ-dej formuły złożonej w Γi i w ∆i.
Dla przykładu niech to będzie ϕ ∧ ψ ∈ ∆i.
Zatem Γi ⇒ ∆i := Γi ⇒ ∆0i, ϕ ∧ ψ i w grę wchodzi zastosowanie reguły (⇒ ∧) z przesłanek Γi⇒ ∆0i, ϕ i Γi ⇒ ∆0i, ψ.
1 Oczywiście nie możemy wykorzystać lematu 4.8 o odwracalności reguł podanego w podrozdziale 4.2, gdyż tamten dowód wykorzystywał (Cut), my natomiast chcemy się odwołać do faktu, że reguły rachunku bez (Cut) też tę własność posiadają.
7.3. PEŁNOŚĆ RS Z ANALITYCZNYM (CUT) 157