1Wst˛ep W 8:R S IA R M D T

M

D

T

I A

R

W YKŁAD 8: R ACHUNKI S EKWENTÓW

III rok kognitywistyki UAM, 2016–2017

1 Wst˛ep

Rachunki sekwentów bior ˛a swój pocz ˛atek z prac Gentzena. Zaproponowane przez niego systemy: LK (dla logiki klasycznej pierwszego rz˛edu) oraz LJ (dla logiki intuicjonistycznej pierwszego rz˛edu) miały pocz ˛atkowo pełni´c rol˛e pomocnicz ˛a w rozwa˙zaniach metalogicznych dotycz ˛acych opracowanych tak˙ze przez niego sys- temów dedukcji naturalnej: NK (dla logiki klasycznej) oraz NJ (dla logiki intu- icjonistycznej). Obecnie ró˙zne odmiany rachunku sekwentów (dla wielu systemów logiki) s ˛a coraz bardziej popularnymi metodami dowodowymi, zarówno w dowo- dzeniu „r˛ecznym”, jak i w automatycznym dowodzeniu twierdze´n.

Celem Gentzena było tak˙ze wykazanie niesprzeczno´sci wa˙znych teorii ma- tematycznych (arytmetyki, analizy). Przypomnijmy, ˙ze w 1931 roku Kurt Gödel udowodnił dwa wa˙zne twierdzenia metalogiczne dotycz ˛ace teorii wystarczaj ˛aco bogatych, aby zawrze´c w nich arytmetyk˛e liczb naturalnych (o tych wynikach opo- wiemy na wykładach w styczniu):

1. Je´sli arytmetyka (pierwszego rz˛edu) jest ω-niesprzeczna, to jest niezupełna oraz istotnie nierozstrzygalna.

2. Je´sli arytmetyka (pierwszego rz˛edu) jest niesprzeczna, to nie istnieje dowód jej niesprzeczno´sci w niej samej.

Wykluczona została zatem mo˙zliwo´s´c udowodnienia niesprzeczno´sci arytme- tyki metodami ´sci´sle finitystycznymi, zalecanymi w Programie Hilberta. Gentzen uzyskał dowód niesprzeczno´sci arytmetyki, posługuj ˛ac si˛e szczególnym rodzajem indukcji (tzw. indukcja pozasko´nczona do 0).

Rachunek sekwentów, który tu przedstawimy opiera si˛e na aksjomatach oraz zestawie reguł logicznych, dotycz ˛acych wprowadzania stałych logicznych, a tak˙ze reguł strukturalnych.

J˛ezyk formalny, w którym mówimy o sekwentach ma formalizowa´c zale˙z- no´s´c mi˛edzy zbiorami formuł polegaj ˛ac ˛a na wyprowadzalno´sci jednego zbioru for- muł (w szczególno´sci: zbioru jednoelementowego, czyli jednej formuły) z innego zbioru formuł. Reguły rachunku sekwentów charakteryzuj ˛a t˛e zale˙zno´s´c poprzez ustalanie, ˙ze je´sli owa relacja zachodzi mi˛edzy pewnymi zbiorami formuł, to za- chodzi tak˙ze mi˛edzy innymi takimi zbiorami.

2 Sekwenty

Sekwentemjest dowolna para (Γ, ∆) sko´nczonych zbiorów formuł. Sekwenty za- pisujemy, korzystaj ˛ac z jakiej´s przyj˛etej konwencji. Cz˛esto u˙zywane zapisy to:

1. Γ =⇒ ∆ 2. Γ ⇒ ∆ 3. Γ ` ∆.

Wybieramy tutaj trzeci ˛a z tych notacji. Ponadto, zwykło si˛e dokonywa´c pew- nych uproszcze´n notacji, np.:

1. Zamiast {ϕ1, . . . , ϕ_n} ` {ψ<sub>1</sub>, . . . , ψ<sub>m</sub>} piszemy ϕ<sub>1</sub>, . . . , ϕ<sub>n</sub>` ψ₁, . . . , ψ_m. 2. Zamiast Γ ∪ {ψ} ` ∆ piszemy Γ, ψ ` ∆, a zamiast Γ ` ∆ ∪ {ψ} piszemy

Γ ` ∆, ψ.

3. Zamiast Γ ` ∅ piszemy Γ `, a zamiast ∅ ` ∆ piszemy ` ∆.

Mo˙zna nadawa´c ró˙zne interpretacje (semantyczne) sekwentom. Za najbardziej naturaln ˛a uwa˙za si˛e do´s´c powszechnie interpretacj˛e, wedle której sekwent Γ `

∆ stwierdza, ˙ze je´sli wszystkie formuły z Γ s ˛a prawdziwe, to co najmniej jedna formuła z ∆ jest prawdziwa.

Formalnie interpretacj˛e tak ˛a okre´slamy rozszerzaj ˛ac warto´sciowania boolow- skie z formuł na sekwenty. Je´sli v jest warto´sciowaniem, to piszemy v(Γ ` ∆) = 1 wtedy i tylko wtedy, gdy v(ϕ) = 0 dla pewnej formuły ϕ ∈ Γ lub v(ψ) = 1 dla pewnej formuły ψ ∈ ∆. Innymi słowy, v(Γ ` ∆) = 1 wtedy i tylko wtedy, gdy:

je´sli v(ϕ) = 1 dla wszystkich ϕ ∈ Γ, to v(ψ) = 1 dla co najmniej jednej ψ ∈ ∆.

Je´sli zatem Γ = {ϕ1, ϕ₂, . . . , ϕ_n} oraz ∆ = {ψ₁, ψ₂, . . . , ψ_m}, to nast˛epuj ˛ace warunki s ˛a równowa˙zne:

1. v(Γ ` ∆) = 1

2. v((ϕ1∧ ϕ₂∧ . . . ∧ ϕ_n) → (ψ1∨ ψ₂∨ . . . ∨ ψ_m)) = 1 3. v(¬ϕ1∨ ¬ϕ₂∨ . . . ∨ ¬ϕ_nψ1∨ ψ₂∨ . . . ∨ ψ_m) = 1.

Zauwa˙zmy, ˙ze: v(∅ ` ∅) = 0 oraz v(` ψ) = v(ψ), dla dowolnej formuły ψ.

Uwaga. Czasami konieczne bywa rozumienie sekwentów nie jako par zbiorów for- muł, ale jako par ci ˛agówformuł. W niektórych stylizacjach rachunku sekwentów rozwa˙za si˛e tak˙ze multizbiory, czyli zbiory, w których pewne elementy mog ˛a si˛e powtarza´c.

3 Reguły

Rachunek ma nast˛epuj ˛ace aksjomaty:

1. ϕ ` ϕ 2. ⊥ ` 3. ` >

Reguły logiczne dotycz ˛a poszczególnych spójników prawdziwo´sciowych (tu podamy je dla: negacji, koniunkcji, alternatywy oraz implikacji) i zwi ˛azane s ˛a z wprowadzaniem tych spójników w poprzedniku lub nast˛epniku sekwentu (naj- pierw reguły logiczne dla funktorów prawdziwo´sciowych w jednej tabeli, potem po kolei wszystkie reguły systemu):

(L¬) <sub>Γ,¬ϕ`∆</sub><sup>Γ`∆,ϕ</sup> <sub>Γ`∆,¬ϕ</sub><sup>Γ,ϕ`∆</sup> (R¬)

(L∧) <sub>Γ,ϕ∧ψ`∆</sub><sup>Γ,ϕ,ψ`∆</sup> Γ`∆,ϕ Γ`∆,ψ

Γ`∆,ϕ∧ψ (R∧)

(L∨) Γ,ϕ`∆ Γ,ψ`∆

Γ,ϕ∨ψ`∆

Γ`∆,ϕ,ψ

Γ`∆,ϕ∨ψ (R∨)

(L→) Γ`∆,ϕ Γ,ψ`∆

Γ,ϕ→ψ`∆

Γ,ϕ`∆,ψ

Γ`∆,ϕ→ψ (R→)

Reguły dla negacji:

Γ ` ∆, ϕ

Γ, ¬ϕ ` ∆ (L¬) Γ, ϕ ` ∆ Γ ` ∆, ¬ϕ (R¬) Reguły dla koniunkcji:

Γ, ϕ, ψ ` ∆

Γ, ϕ ∧ ψ ` ∆ (L∧) Γ ` ∆, ϕ Γ ` ∆, ψ Γ ` ∆, ϕ ∧ ψ (R∧) Reguły dla alternatywy:

Γ, ϕ ` ∆ Γ, ψ ` ∆

Γ, ϕ ∨ ψ ` ∆ (L∨) Γ ` ∆, ϕ, ψ

Γ ` ∆, ϕ ∨ ψ (R∨) Reguły dla implikacji:

Γ ` ∆, ϕ Γ, ψ ` ∆

Γ, ϕ → ψ ` ∆ (L→) Γ, ϕ ` ∆, ψ

Γ ` ∆, ϕ → ψ (R→)

Zauwa˙zmy, ˙ze niektóre reguły wymagaj ˛a dwóch sekwentów w przesłankach.

Niech uciech ˛a na konwersatorium b˛edzie ustalenie, jak powinny wygl ˛ada´c re- guły dla pozostałych funktorów prawdziwo´sciowych.

Reguły dla formuł zawieraj ˛acych kwantyfikatory:

ϕ(x/t), Γ ` ∆

∀xϕ, Γ ` ∆ (L∀) Γ ` ∆, ϕ(x/a) Γ ` ∆, ∀xϕ (R∀) ϕ(x/a), Γ ` ∆

∃xϕ, Γ ` ∆ (L∃) Γ ` ∆, ϕ(x/t) Γ ` ∆, ∃xϕ (R∃) Zastrze˙zenia:

1. W regułach dla formuł z kwantyfikatorami sekwenty rozumiane s ˛a jako pary ci ˛agów.

2. W regułach: (L∃) oraz (R∀) symbol a jest parametrem, który nie mo˙ze wy- st ˛api´c we wniosku reguły.

3. W regułach: (R∃) oraz (L∀) symbol t jest termem domkni˛etym.

Reguły strukturalne:

Osłabienie (weakening):

Γ ` ∆

ϕ, Γ ` ∆ (LW ) Γ ` ∆

Γ ` ∆, ϕ (RW )

Skrócenie (contraction):

ϕ, ϕ, Γ ` ∆

ϕ, Γ ` ∆ (LC) Γ ` ∆, ϕ, ϕ Γ ` ∆, ϕ (RC) Przestawienie (exchange):

Γ1, ϕ, ψ, Γ2 ` ∆

Γ₁, ψ, ϕ, Γ₂ ` ∆ (LE) Γ ` ∆1, ϕ, ψ, ∆2

Γ ` ∆₁, ψ, ϕ, ∆₂ (RE)

System o tych regułach oraz aksjomatach b˛edziemy oznaczali przez RS (ra- chunek sekwentów dla logiki klasycznej).

Rachunek sekwentów dla logiki intuicjonistycznej otrzymujemy z podanego wy˙zej zestawu aksjomatów oraz reguł poprzez dodanie warunku, ˙ze po prawej stro- nie sekwentów wyst˛epowa´c mo˙ze jedynie pojedyncza formuła (a nie sko´nczony zbiór formuł).

Opatrzmy jeszcze komentarzami przedstawione wy˙zej reguły:

1. Rozwa˙zamy tylko reguły wprowadzania stałych logicznych (a nie, jak w sys- temach dedukcji naturalnej, tak˙ze reguły eliminacji stałych logicznych).

2. We wniosku ka˙zdej reguły mamy formuł˛e główn ˛a, czyli t˛e, która jest wpro- wadzana na mocy przesłanek. Pozostałe formuły tworz ˛a kontekst.

3. Formułami aktywnymi nazywamy te formuły w przesłankach reguły, z któ- rych otrzymujemy formuł˛e główn ˛a tej reguły.

4. Jak zobaczymy pod koniec wykładu, wszystkie reguły systemu RS s ˛a od- wracalne.

5. Zauwa˙zmy wreszcie, ˙ze ka˙zda reguła dotyczy tylko jednej stałej logicznej oraz ˙ze we wniosku ka˙zdej reguły formuła główna jest tylko jedna.

4 Dowody

W rachunku RS, jak nazwa wskazuje, rachujemy na sekwentach, w tym sensie,

˙ze wyprowadzamy jedne sekwenty z innych. Takie wyprowadzenia maj ˛a posta´c drzew.

Definicja. Dowodem sekwentu Γ ` ∆ w systemie RS nazywamy sko´nczone drzewo dwójkowe spełniaj ˛ace nast˛epuj ˛ace warunki:

1. W korzeniu drzewa znajduje si˛e sekwent Γ ` ∆.

2. W li´sciach drzewa znajduj ˛a si˛e aksjomaty systemu RS.

3. Dla ka˙zdego wierzchołka w drzewa, który nie jest li´sciem:

(a) Je´sli rz ˛ad w jest równy jeden (czyli w ma dokładnie jednego bezpo-

´sredniego potomka), to istnieje reguła systemu RS taka, ˙ze w wierz- chołku w znajduje si˛e wniosek tej reguły, a w bezpo´srednim potomku wierzchołka w znajduje si˛e przesłanka tej reguły.

(b) Je´sli rz ˛ad w jest równy dwa (czyli w ma dokładnie dwóch bezpo´sred- nich potomków), to istnieje reguła systemu RS taka, ˙ze w wierzchołku w znajduje si˛e wniosek tej reguły, a w bezpo´srednich potomkach w znajduj ˛a si˛e przesłanki tej reguły.

Je´sli sekwent Γ ` ∆ ma dowód w systemie RS, to piszemy `RS Γ ` ∆.

Mo˙zemy równie˙z mówi´c, ˙ze w rachunku RS dowodzimy formuł (j˛ezyka KRZ lub j˛ezyka KRP). Powiemy mianowicie, ˙ze formuła ϕ jest tez ˛a systemu RS, gdy sekwent ∅ ` ϕ ma dowód w systemie RS.

5 Przykłady dowodów

Tradycja ka˙ze pisa´c dowody w systemie RS w postaci drzew, których korze´n znaj- duje si˛e na dole, a li´scie na górze. Praktyka znajdowania takich dowodów polega jednak zwykle na przechodzeniu od dowodzonego sekwentu do sekwentów, z któ- rych jest on wyprowadzany, a˙z do zako´nczenia dowodu poprzez dotarcie do li´sci drzewa, b˛ed ˛acych aksjomatami systemu. Oczywi´scie nie ma zakazu, aby zaczyna´c budow˛e dowodu od aksjomatów systemu, docieraj ˛ac do uzasadnianej tezy. Tak jest np. w przykładzie podanym w Fitting 1990, 84:

Przykład 1: ` ¬(p ∧ q) → (¬p ∨ ¬q)

10. ` ¬(p ∧ q) → (¬p ∨ ¬q) R→: 9 9. ¬(p ∧ q) ` ¬p ∨ ¬q R∨ : 8

8. ¬(p ∧ q) ` ¬p, ¬q L¬ : 7 7. ` p ∧ q, ¬p, ¬q R¬ : 6

6. q ` p ∧ q, ¬p R¬: 5 5. p, q ` p ∧ q R∧: 3, 4

4. p, q ` q LW : 2 2. q ` q 3. p, q ` p LW : 1

1. p ` p

Chuck Norris potrafi ka˙zdy dowód w rachunku sekwentów RS przeprowadzi´c wła´snie w ten sposób: raz, dwa znajduje aksjomaty potrzebne w dowodzie, a potem (z półobrotu) wdzi˛ecznie korzysta z dost˛epnych reguł. Wi˛ekszo´s´c osób, które znam prowadzi jednak dowody w RS metod ˛a backward proof search: zaczynamy od do- wodzonego segmentu (w korzeniu drzewa) i dla ka˙zdego kolejnego wierzchołka w budowanym dowodzie wybieramy w nim formuł˛e główn ˛a oraz tworzymy bez- po´sredniego potomka lub dwóch bezpo´srednich potomków, z odpowiednimi for- mułami aktywnymi. Kontynuujemy to post˛epowanie tak długo, a˙z na ka˙zdej gał˛ezi tworzonego drzewa znajdzie si˛e aksjomat rachunku RS. Oczywi´scie, je´sli w korze- niu drzewa znajduje si˛e sekwent, który nie posiada dowodu, to w drzewie znajdzie si˛e co najmniej jedna gał ˛a´z, której nie uda si˛e zako´nczy´c aksjomatem systemu RS.

Kilka dalszych prostych przykładów (z u˙zyciem powy˙zszego sposobu zapisy- wania dowodów):

Przykład 2: ` p → (q → p)

1. p ` p aksjomat

2. q, p ` p LW : 1

3. p ` q → p R→: 2 4. ` p → (q → p) R→: 3 Przykład 3: ` (p ∧ q) → p

1. p ` p aksjomat

2. p, q ` p LW : 1

3. p ∧ q ` p L∧ : 2 4. ` (p ∧ q) → p R→: 3 Przykład 4: ` p → (p ∨ q)

1. p ` p aksjomat

2. p ` p, q RW : 1

3. p ` p ∨ q R∨ : 2 4. ` p → (p ∨ q) R→: 3 Przykład 5: ` ¬¬p → p

1. p ` p aksjomat 2. ` p, ¬p R¬ : 1 3. ¬¬p ` p L¬ : 2 4. ` ¬¬p → p R→: 3

Kilka bardziej zło˙zonych przykładów (aksjomat, jaki jest, ka˙zdy widzi, wi˛ec opuszczamy komentarze dotycz ˛ace aksjomatów):

Przykład 6

7. ¬q, p → q ` ¬p L→5, 6 8. p → q ` ¬q → ¬p R→7 9. ` (p → q) → (¬q → ¬p) R→8

2. q ` q 4. q ` ¬p, q RW 2 6. q, ¬q ` ¬p L¬4 1. p ` p

3. p, ¬q ` p LW 1 5. ¬q ` ¬p, p R¬3

Przykład 7

Pomijamy tym razem numery sekwentów (z lewej) oraz informacj˛e o u˙zytych regułach (z prawej). Słuchacze zechc ˛a dokona´c stosownych uzupełnie´n samodziel- nie. Jak pami˛etamy z poprzednich wykładów, tego typu informacje nie s ˛a cz˛e´sci ˛a samego dowodu, a jedynie komentarzami ułatwiaj ˛acymi jego czytanie.

` (p → (p → q)) → (p → q) p → (p → q) ` p → q

p, p → (p → q) ` q p → q, p ` q

q, p ` q q ` q p ` q, p

p ` p

p ` q, p p ` p

Przykład 8

Oto dowód prawa sylogizmu hipotetycznego w RS:

` (ϕ → ψ) → ((ψ → χ) → (ϕ → χ)) ϕ → ψ ` (ψ → χ) → (ϕ → χ)

ψ → χ, ϕ → ψ ` ϕ → χ ϕ, ψ → χ, ϕ → ψ ` χ

χ, ϕ, ϕ → ψ ` χ ψ, χ, ϕ ` χ

χ, ϕ ` χ χ ` χ

χ, ϕ ` χ, ϕ ϕ ` χ, ϕ

ϕ ` ϕ

ϕ, ϕ → ψ ` χ, ψ ψ, ϕ ` χ, ψ

ψ ` χ, ψ ψ ` ψ

ϕ ` χ, ψ, ϕ ϕ ` ψ, ϕ

ϕ ` ϕ

W powy˙zszych przykładach nie zaznaczono korzystania z reguł przestawiania (zaczynaj ˛a one by´c istotne, gdy pracujemy nie na zbiorach, lecz na ci ˛agach for- muł). Czasami stosuje si˛e te˙z inne jeszcze uproszczenie: je´sli w poprzedniku i na- st˛epniku segmentu wyst˛epuje ta sama formuła, powiedzmy ϕ, to uznaje si˛e, ˙ze taki sekwent wyprowadzi´c mo˙zna z aksjomatu ϕ ` ϕ (poprzez, by´c mo˙ze wielokrotne, stosowanie reguł osłabiania).

Przykład 9: ` p ∨ ¬p

p ` p

` p, ¬p

` p, p ∨ ¬p

` p ∨ ¬p, p ∨ ¬p

` p ∨ ¬p Przykład 10: ` (p → q) ∨ (q → p)

q ` q q ` p, q p, q ` p, q q ` p → q, p

` p → q, q → p

` p → q, (p → q) ∨ (q → p)

` (p → q) ∨ (q → p), (p → q) ∨ (q → p)

` (p → q) ∨ (q → p) Przykład 11: ` (((p → q) → q) → q) → (p → q)

` (((p → q) → q) → q) → (p → q) ((p → q) → q) → q ` p → q

p, ((p → q) → q) → q ` q q ` q p ` (p → q) → q

p, p → q ` q q ` q p ` p

Przykład 12: ` ((ϕ →⊥) →⊥) → ϕ

` ((ϕ →⊥) →⊥) → ϕ (ϕ →⊥) →⊥` ϕ

⊥` ϕ

` ϕ →⊥, ϕ ϕ `⊥, ϕ

ϕ ` ϕ

Przykład 13: ∃y∀xP (x, y) → ∀x∃yP (x, y)

W tym przykładzie ponumerujemy kroki dowodowe (z lewej strony) oraz po- damy (z prawej strony) komentarze dotycz ˛ace ich prawomocno´sci:

1. P (a, b) ` P (a, b) aksjomat 2. ∀xP (x, b) ` P (a, b) L∀ : 1 3. ∀xP (x, b) ` ∃yP (a, y) R∃ : 2 4. ∃y∀xP (x, y) ` ∃yP (a, y) L∃ : 3 5. ` ∃y∀xP (x, y) → ∀x∃yP (x, y) R∀ : 4 Przykład 14: ` ¬∃xP (x) → ∀x¬P (x)

P (a) ` P (a) P (a) ` ∃xP (x)

¬∃xP (x), P (a) `

¬∃xP (x) ` ¬P (a)

¬∃xP (x) ` ∀¬P (x)

` ¬∃xP (x) → ∀x¬P (x) Przykład 15: ` (∃xP (x) ∨ ∃xQ(x)) → ∃x(P (x) ∨ Q(x))

` ∃(P (x) ∨ Q(x)) → (∃xP (x) ∨ ∃xQ(x))

∃x(P (x) ∨ Q(x)) ` ∃xP (x) ∨ ∃xQ(x) P (a) ∨ Q(a) ` ∃xP (x) ∨ ∃xQ(x)

Q(a) ` ∃xP (x) ∨ ∃xQ(x) Q(a) ` ∃xQ(x)

Q(a) ` Q(a)

P (a) ` ∃xP (x) ∨ ∃xQ(x) P (a) ` ∃xP (x)

P (a) ` P (a)

Cwiczenia. Podaj dowody sekwentów:´

1. ` (p → q) → ((p → r) → (p → (q ∧ r))) 2. ` (p → q) → ((q → r) → ((p ∨ q) → r)) 3. ` ∀x¬P (x) → ∃x¬P (x)

4. ` (∃xP (x) ∨ ∃xQ(x)) → ∃x(P (x) ∨ Q(x))

6 Fakty metalogiczne

6.1 Trafno´s´c i pełno´s´c systemu RS

Zauwa˙zmy, ˙ze reguły logiczne dla spójników prawdziwo´sciowych maj ˛a nast˛epu- j ˛ace własno´sci (semantyczne):

1. Je´sli Γ ` ∆ jest aksjomatem systemu RS, to v(Γ ` ∆) = 1 dla dowolnego warto´sciowania v.

2. Je´sli przesłanka reguły: (L∧), (R∨), (R →), (L¬), (R¬) ma warto´s´c 1 przy warto´sciowaniu v, to wniosek tej reguły tak˙ze ma warto´s´c 1 przy warto´scio- waniu v.

3. Je´sli obie przesłanki reguły: (R∧), (L∨), (L →) maj ˛a warto´s´c 1 przy warto-

´sciowaniu v, to wniosek tej reguły tak˙ze ma warto´s´c 1 przy warto´sciowaniu v.

4. Je´sli wniosek reguły: (L∧), (R∨), (R →), (L¬), (R¬), ma warto´s´c 1 przy warto´sciowaniu v to tak˙ze przesłanka tej reguły ma warto´s´c 1 przy warto-

´sciowaniu v.

5. Je´sli wniosek reguły: (R∧), (L∨), (L →), ma warto´s´c 1 przy warto´sciowa- niu v to tak˙ze obie przesłanki tej reguły maj ˛a warto´s´c 1 przy warto´sciowaniu v.

Pierwsze dwie z tych własno´sci dotycz ˛a trafno´sci reguł rachunku RS, pozo- stałe dwie mówi ˛a o odwracalno´sci tych reguł.

Trafno´s´c systemu RS (dla KRZ) jest oczywista: aksjomaty s ˛a tautologiami KRZ (je´sli ϕ ` ϕ jest aksjomatem systemu RS, to oczywi´scie ϕ → ϕ jest tautolo- gi ˛a KRZ). Ponadto, je´sli przesłanki reguły rachunku RS s ˛a tautologiami KRZ, to i wniosek tej reguły jest tautologi ˛a KRZ.

Pełno´s´c rachunku RS udowodni´c mo˙zna na ró˙zne sposoby. W podr˛eczniku Fitting 1990 zaleca si˛e oczywi´scie dowód poprzez wykorzystanie Twierdzenia o Istnieniu Modelu.

Wprowad´zmy u˙zyteczny skrót: ¬S = {¬ϕ : ϕ ∈ S}.

Je´sli S jest sko´nczonym zbiorem formuł, to sekwentem stowarzyszonym z S nazwiemy dowolny sekwent Γ ` ¬∆, gdzie para (Γ, ∆) jest podziałem S, czyli:

Γ ∩ ∆ = ∅ oraz Γ ∪ ∆ = S.

Fakt. Je´sli (dowolny) sekwent stowarzyszony z S ma dowód w systemie RS, to ka˙zdy sekwent stowarzyszony z S ma dowód w systemie RS.

Powiemy, ˙ze sko´nczony zbiór formuł S jest sekwentowo sprzeczny, gdy do- wolny (a w konsekwencji, ka˙zdy) sekwent stowarzyszony z S ma dowód w RS.

Powiemy, ˙ze sko´nczony zbiór formuł S jest sekwentowo niesprzeczny, gdy nie jest on sekwentowo sprzeczny.

Fakt. Rodzina wszystkich zbiorów sekwentowo niesprzecznych jest zdaniow ˛a wła- sno´sci ˛a niesprzeczno´sci.

Fakt. Zachodz ˛a nast˛epuj ˛ace implikacje:

1. Je´sli sekwent Γ ` ∆, ¬ϕ ma dowód w systemie RS, to sekwent Γ, ϕ ` ∆ równie˙z ma dowód w systemie RS.

2. Je´sli sekwent Γ, ¬ϕ ` ∆ ma dowód w systemie RS, to sekwent Γ ` ∆, ϕ równie˙z ma dowód w systemie RS.

Na mocy powy˙zszych faktów (których dowodami mo˙zna pobawi´c si˛e na kon- wersatorium, je´sli słuchaczy najdzie na to ochota) otrzymujemy:

Twierdzenie o Pełno´sci Systemu RS dla KRZ. Je´sli ϕ jest tautologi ˛a KRZ, to ϕ jest tez ˛a systemu RS (czyli: `RS ` ϕ).

Dowód. Przypu´s´cmy, ˙ze ϕ nie jest tez ˛a systemu RS. Wtedy sekwent ∅ ` ϕ nie ma dowodu w RS. Oznacza to, ˙ze zbiór {¬ϕ} jest sekwentowo niesprzeczny, gdy˙z w przeciwnym przypadku dowód posiadałby sekwent ¬ϕ ` ∅, a zatem dowód posiadałby równie˙z sekwent ∅ ` ϕ. Na mocy Twierdzenia o Istnieniu Modelu zbiór {¬ϕ} jest spełnialny, a zatem ϕ nie jest tautologi ˛a KRZ.

6.2 Reguła ci˛ecia

Reguł ˛a ci˛ecia(cut rule) nazywamy reguł˛e o nast˛epuj ˛acej postaci:

Γ ` ∆, ϕ ϕ, Γ ` ∆ Γ ` ∆

W szczególno´sci, je´sli ∆ = {ψ}, to reguła ci˛ecia przybiera posta´c:

Γ ` ψ, ϕ ϕ, Γ ` ψ Γ ` ψ

Reguła ta odpowiada zatem nast˛epuj ˛acej procedurze dowodowej:

1. Przypu´s´cmy, ˙ze z jakich´s zało˙ze´n Γ otrzymujemy lemat ϕ oraz tez˛e ψ.

2. Przypu´s´cmy tak˙ze, ˙ze z lematu ϕ oraz zało˙ze´n Γ otrzyma´c mo˙zemy tez˛e ψ.

3. Na mocy reguły ci˛ecia mo˙zemy wtedy uzyska´c z zało˙ze´n Γ tez˛e ψ.

Reguła ci˛ecia wyst˛epowała w oryginalnym systemie Gentzena. Pokazał on jed- nak, ˙ze u˙zycia tej reguły mog ˛a zosta´c w tym systemie wyeliminowane:

Hauptsatz. Ka˙zdy dowód sekwentu Γ ` ∆ (w systemie RS z reguł ˛a ci˛ecia), w którym wyst˛epuje reguła ci˛ecia mo˙ze zasta´c zast ˛apiony dowodem w systemie RS bez u˙zycia tej reguły.

Zamiast mówi´c o eliminowaniu reguły ci˛ecia, mo˙zna te˙z mówi´c, ˙ze reguła ci˛e- cia jest reguł ˛a dopuszczaln ˛a w systemie RS (zob. wykład drugi z materiałów na rok akademicki 2015/2016).

Słuchacze zechc ˛a porówna´c reguł˛e ci˛ecia ze znanymi z innych technik dowo- dowych regułami (dla KRZ):

1. Reguła odrywania. ^ϕ→ψ_ψ ^ϕ 2. Reguła rezolucji. ^ϕ∨ψ _ϕ^ϕ∨¬ψ.

Dowody, które nie zawieraj ˛a u˙zy´c reguły ci˛ecia nazywa si˛e analitycznymi. Do- wody analityczne zalecaj ˛a si˛e wieloma własno´sciami przydatnymi w automatycz- nym dowodzeniu twierdze´n (m.in.: odwoływanie si˛e wył ˛acznie do podformuł u˙zy- wanych w dowodzie formuł). Jednak dowody analityczne bywaj ˛a cz˛esto o wiele dłu˙zsze od dowodów, które analityczne nie s ˛a.

Zauwa˙zmy, ˙ze w przesłankach reguły ci˛ecia wyst˛epuje formuła (o dowolnej zło˙zono´sci), która nie wyst˛epuje we wniosku tej reguły.

Ka˙zdy dowód w systemie RS mo˙zna do´s´c łatwo przekształci´c na dowód w systemie aksjomatycznym w stylu Hilberta. Aby pokaza´c, ˙ze jest równie˙z na od- wrót, czyli ˙ze ka˙zdy dowód w systemie aksjomatycznym w stylu Hilberta mo˙zna przekształci´c na dowód w systemie RS, trzeba odpowiednio „zadba´c” o reguł˛e od- rywania. Do tego wła´snie słu˙zy doł ˛aczenie reguły ci˛ecia do systemu RS. Nast˛epnie korzystamy oczywi´scie z twierdzenia o eliminacji reguły ci˛ecia.

6.3 Konsekwencje twierdzenia o eliminacji ci˛ecia

Twierdzenie to ma liczne zastosowania w teorii dowodu. Wymienimy, przykła- dowo, dwa:

1. Dowody niesprzeczno´sci.

2. Automatyczne dowodzenie twierdze´n.

7 Wykorzystywana literatura

Fitting, M. 1996. First-Order Logic and Automated Theorem Proving. Springer, Berlin.

Gentzen, G. 1935. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift39, 176–210, 405–431.

Negri, S., von Plato, J. 2001. Structural Proof Theory. Cambridge University Press, Cambridge.

Rasiowa, H., Sikorski, R. 1963. The Mathematics of Metamathematics. Pa´nstwowe Wydawnictwo Naukowe, Warszawa.

Pogorzelski, W.A. 1981. Klasyczny rachunek kwantyfikatorów. Zarys teorii. Pa´n- stwowe Wydawnictwo Naukowe, Warszawa.

Smullyan, R. 1968. First-Order Logic. Springer Verlag, Berlin.

Troelstra, A.S., Schwichtenberg, H. 2000. Basic Proof Theory. Cambridge Uni- versity Press, Cambridge.

JERZYPOGONOWSKI

Zakład Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka pogon@amu.edu.pl