Rachunki sekwentów
Jerzy Pogonowski
Zakªad Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka
pogon@amu.edu.pl
MDTiAR 1xii2015
Plan na dzi±
Poznamy reguªy rachunku sekwentów Gentzena.
Prze±ledzimy kilka(na±cie) dowodów w tym rachunku.
Sformuªujemy kilka wa»nych faktów metalogicznych dotycz¡cych rachunku sekwentów.
Zastanowimy si¦ chwil¦ nad porównaniem poznanych dot¡d metod dowodowych.
Kontekst historyczny
Rachunki sekwentów bior¡ swój pocz¡tek z prac Gentzena.
Zaproponowane przez niego systemy: LK (dla logiki klasycznej pierwszego rz¦du) oraz LJ (dla logiki intuicjonistycznej pierwszego rz¦du) miaªy pocz¡tkowo peªni¢ rol¦ pomocnicz¡ w rozwa»aniach metalogicznych dotycz¡cych opracowanych tak»e przez niego
systemów dedukcji naturalnej: NK (dla logiki klasycznej) oraz NJ (dla logiki intuicjonistycznej).
Obecnie ró»ne odmiany rachunku sekwentów (dla wielu systemów logiki) s¡ coraz bardziej popularnymi metodami dowodowymi, zarówno w dowodzeniu r¦cznym, jak i w automatycznym dowodzeniu
twierdze«.
Kontekst historyczny
Celem Gentzena byªo tak»e wykazanie niesprzeczno±ci wa»nych teorii matematycznych (arytmetyki, analizy). Przypomnijmy, »e w 1931 roku Kurt Gödel udowodniª dwa wa»ne twierdzenia metalogiczne dotycz¡ce teorii wystarczaj¡co bogatych, aby zawrze¢ w nich arytmetyk¦ liczb naturalnych (o tych wynikach opowiemy na wykªadach w styczniu):
1 Je±li arytmetyka (pierwszego rz¦du) jest niesprzeczna, to jest niezupeªna oraz istotnie nierozstrzygalna.
2 Je±li arytmetyka (pierwszego rz¦du) jest niesprzeczna, to nie istnieje dowód jej niesprzeczno±ci w niej samej.
Wykluczona zostaªa zatem mo»liwo±¢ udowodnienia niesprzeczno±ci arytmetyki metodami ±ci±le nitystycznymi, zalecanymi w Programie Hilberta. Gentzen uzyskaª dowód niesprzeczno±ci arytmetyki, posªuguj¡c si¦
szczególnym rodzajem indukcji (tzw. indukcja pozasko«czona do ε0).
J¦zyk rachunku sekwentów
Rachunek sekwentów, który tu przedstawimy opiera si¦ na aksjomatach oraz zestawie reguª logicznych, dotycz¡cych wprowadzania staªych logicznych, a tak»e zestawie reguª strukturalnych.
J¦zyk formalny, w którym mówimy o sekwentach ma sªu»y¢
formalizacji zale»no±ci mi¦dzy zbiorami formuª polegaj¡cej na wyprowadzalno±ci jednego zbioru formuª (w szczególno±ci: zbioru jednoelementowego, czyli jednej formuªy) z innego zbioru formuª.
Reguªy rachunku sekwentów charakteryzuj¡ t¦ zale»no±¢ poprzez ustalanie, »e je±li owa relacja zachodzi mi¦dzy pewnymi zbiorami formuª, to zachodzi tak»e mi¦dzy innymi takimi zbiorami.
Notacja
Sekwentem jest dowolna para (Γ, ∆) sko«czonych zbiorów formuª.
Sekwenty zapisujemy, korzystaj¡c z jakiej± przyj¦tej konwencji. Cz¦sto u»ywane zapisy to:
1 Γ =⇒ ∆
2 Γ ⇒ ∆
3 Γ ` ∆.
Wybieramy tutaj trzeci¡ z tych notacji. Ponadto, zwykªo si¦ dokonywa¢
pewnych uproszcze« notacji, np.:
1 Zamiast {ϕ1, . . . , ϕn} ` {ψ1, . . . , ψm}piszemy ϕ1, . . . , ϕn` ψ1, . . . , ψm.
2 Zamiast Γ ∪ {ψ} ` ∆ piszemy Γ, ψ ` ∆, a zamiast Γ ` ∆ ∪ {ψ}
piszemy Γ ` ∆, ψ.
3 Zamiast Γ ` ∅ piszemy Γ `, a zamiast ∅ ` ∆ piszemy ` ∆.
Sekwenty: semantyka
Mo»na nadawa¢ ró»ne interpretacje (semantyczne) sekwentom. Za najbardziej naturaln¡ uwa»a si¦ do±¢ powszechnie interpretacj¦, wedle której sekwent Γ ` ∆ stwierdza, »e je±li wszystkie formuªy z Γ s¡
prawdziwe, to co najmniej jedna formuªa z ∆ jest prawdziwa.
Formalnie interpretacj¦ tak¡ okre±lamy rozszerzaj¡c warto±ciowania boolowskie z formuª na sekwenty. Je±li v jest warto±ciowaniem, 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±li v(ϕ) = 1 dla wszystkich ϕ ∈ Γ, to v(ψ) = 1 dla co najmniej jednej ψ ∈ ∆.
Sekwenty: semantyka
Je±li zatem Γ = {ϕ1, ϕ2, . . . , ϕn} oraz ∆ = {ψ1, ψ2, . . . , ψm}, to nast¦puj¡ce warunki s¡ równowa»ne:
1 v(Γ ` ∆) = 1
2 v((ϕ1∧ ϕ2∧ . . . ∧ ϕn) → (ψ1∨ ψ2∨ . . . ∨ ψm)) =1
3 v(¬ϕ1∨ ¬ϕ2∨ . . . ∨ ¬ϕn∨ ψ1∨ ψ2∨ . . . ∨ ψm) =1.
Zauwa»my, »e: v(∅ ` ∅) = 0 oraz v(` ψ) = v(ψ), dla dowolnej formuªy ψ.
Czasami konieczne bywa rozumienie sekwentów nie jako par zbiorów formuª, ale jako par ci¡gów formuª. W niektórych stylizacjach rachunku sekwentów rozwa»a si¦ tak»e multizbiory, czyli zbiory, w których pewne elementy mog¡ si¦ powtarza¢.
Aksjomaty
Rachunek RS ma nast¦puj¡ce aksjomaty:
1 ϕ ` ϕ
2 ⊥ `
3 ` >
Reguªy logiczne dotycz¡ poszczególnych spójników prawdziwo±ciowych (tu podamy je dla: negacji, koniunkcji, alternatywy oraz implikacji) i zwi¡zane s¡ z wprowadzaniem tych funktorów w poprzedniku lub nast¦pniku sekwentu.
Najpierw podamy reguªy logiczne dla funktorów prawdziwo±ciowych w jednej tabeli, potem po kolei wszystkie reguªy systemu:
Reguªy logiczne
(L¬) Γ,¬ϕ`∆Γ`∆,ϕ Γ`∆,¬ϕΓ,ϕ`∆ (R¬)
(L∧) Γ,ϕ∧ψ`∆Γ,ϕ,ψ`∆ Γ`∆,ϕ Γ`∆,ψ
Γ`∆,ϕ∧ψ (R∧)
(L∨) Γ,ϕ`∆ Γ,ψ`∆
Γ,ϕ∨ψ`∆
Γ`∆,ϕ,ψ
Γ`∆,ϕ∨ψ (R∨)
(L→) Γ`∆,ϕ Γ,ψ`∆
Γ,ϕ→ψ`∆
Γ,ϕ`∆,ψ
Γ`∆,ϕ→ψ (R→) Omówimy teraz po kolei te reguªy:
Reguªy dla negacji oraz dla implikacji
Negacja:
Γ ` ∆, ϕ
Γ, ¬ϕ ` ∆ (L¬) Γ, ϕ ` ∆ Γ ` ∆, ¬ϕ (R¬) Implikacja:
Γ ` ∆, ϕ Γ, ψ ` ∆
Γ, ϕ → ψ ` ∆ (L→) Γ, ϕ ` ∆, ψ
Γ ` ∆, ϕ → ψ (R→)
Reguªy dla koniunkcji oraz dla alternatywy
Koniunkcja:
Γ, ϕ, ψ ` ∆
Γ, ϕ ∧ ψ ` ∆ (L∧) Γ ` ∆, ϕ Γ ` ∆, ψ Γ ` ∆, ϕ ∧ ψ (R∧) Alternatywa:
Γ, ϕ ` ∆ Γ, ψ ` ∆
Γ, ϕ ∨ ψ ` ∆ (L∨) Γ ` ∆, ϕ, ψ Γ ` ∆, ϕ ∨ ψ (R∨)
Reguªy dla kwanty katorów
ϕ(x/t), Γ ` ∆
∀xϕ, Γ ` ∆ (L∀) Γ ` ∆, ϕ(x/a) Γ ` ∆, ∀xϕ (R∀) ϕ(x/a), Γ ` ∆
∃xϕ, Γ ` ∆ (L∃) Γ ` ∆, ϕ(x/t) Γ ` ∆, ∃xϕ (R∃) Zastrze»enia:
1 W reguªach dla formuª z kwanty katorami sekwenty rozumiane s¡ jako pary ci¡gów (formuª).
2 W reguªach: (L∃) oraz (R∀) symbol a jest parametrem, który nie mo»e wyst¡pi¢ we wniosku reguªy.
3 W reguªach: (R∃) oraz (L∀) symbol t jest termem domkni¦tym.
Reguªy strukturalne
Osªabienie (weakening):
Γ ` ∆
ϕ, Γ ` ∆ (LW ) Γ ` ∆
Γ ` ∆, ϕ (RW ) Skrócenie (contraction):
ϕ, ϕ, Γ ` ∆
ϕ, Γ ` ∆ (LC) Γ ` ∆, ϕ, ϕ Γ ` ∆, ϕ (RC) Przestawienie (exchange):
Γ1, ϕ, ψ, Γ2 ` ∆
Γ1, ψ, ϕ, Γ2 ` ∆ (LE) Γ ` ∆1, ϕ, ψ, ∆2 Γ ` ∆1, ψ, ϕ, ∆2 (RE) System o tych reguªach oraz aksjomatach b¦dziemy oznaczali przez RS (rachunek sekwentów dla logiki klasycznej).
1 Rozwa»amy tylko reguªy wprowadzania staªych logicznych (a nie, jak w systemach dedukcji naturalnej, tak»e reguªy eliminacji staªych logicznych).
2 We wniosku ka»dej reguªy mamy formuª¦ gªówn¡, czyli t¦, która jest wprowadzana na mocy przesªanek. Pozostaªe formuªy tworz¡ kontekst.
3 Formuªami aktywnymi nazywamy te formuªy w przesªankach reguªy, z których otrzymujemy formuª¦ gªówn¡ tej reguªy.
4 Jak zobaczymy pod koniec wykªadu, wszystkie reguªy systemu RS s¡
odwracalne.
5 Zauwa»my wreszcie, »e ka»da reguªa dotyczy tylko jednej staªej logicznej oraz »e we wniosku ka»dej reguªy formuªa gªówna jest tylko jedna.
6 Rachunek sekwentów dla logiki intuicjonistycznej otrzymujemy z podanego wy»ej zestawu aksjomatów oraz reguª poprzez dodanie warunku, »e po prawej stronie sekwentów wyst¦powa¢ mo»e jedynie pojedyncza formuªa (a nie sko«czony zbiór formuª).
Dowody
Dowodem sekwentu Γ ` ∆ w systemie RS nazywamy sko«czone drzewo dwójkowe speªniaj¡ce nast¦puj¡ce warunki:
1 W korzeniu drzewa znajduje si¦ sekwent Γ ` ∆.
2 W li±ciach drzewa znajduj¡ si¦ aksjomaty systemu RS.
3 Dla ka»dego wierzchoªka w drzewa, który nie jest li±ciem:
1 Je±li rz¡d w jest równy jeden (czyli w ma dokªadnie jednego bezpo±redniego potomka), to istnieje reguªa systemu RS taka, »e w wierzchoªku w znajduje si¦ wniosek tej reguªy, a w bezpo±rednim potomku wierzchoªka w znajduje si¦ przesªanka tej reguªy.
2 Je±li rz¡d w jest równy dwa (czyli w ma dokªadnie dwóch
bezpo±rednich potomków), to istnieje reguªa systemu RS taka, »e w wierzchoªku w znajduje si¦ wniosek tej reguªy, a w bezpo±rednich potomkach w znajduj¡ si¦ przesªanki tej reguªy.
Tezy
Je±li sekwent Γ ` ∆ ma dowód w systemie RS, to piszemy `RS Γ ` ∆.
Mo»emy równie» mówi¢, »e w rachunku RS dowodzimy formuª (j¦zyka KRZ lub j¦zyka KRP). Powiemy mianowicie, »e formuªa ϕ jest tez¡
systemu RS, gdy sekwent ∅ ` ϕ ma dowód w systemie RS.
Tradycja ka»e pisa¢ dowody w systemie RS w postaci drzew, których korze« znajduje si¦ na dole, a li±cie 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» do zako«czenia dowodu poprzez dotarcie do li±ci drzewa, b¦d¡cych
aksjomatami systemu. Oczywi±cie nie ma zakazu, aby zaczyna¢ budow¦
dowodu od aksjomatów systemu, docieraj¡c do uzasadnianej tezy.
Dowody: praktyka
Chuck Norris potra ka»dy dowód w rachunku sekwentów RS przeprowadzi¢ wªa±nie w ten sposób: raz, dwa znajduje aksjomaty potrzebne w dowodzie, a potem (z póªobrotu) wdzi¦cznie korzysta z dost¦pnych reguª.
Wi¦kszo±¢ osób, które znam prowadzi jednak dowody w RS metod¡
backward proof search: zaczynamy od dowodzonego segmentu (w korzeniu drzewa) i dla ka»dego kolejnego wierzchoªka w budowanym dowodzie wybieramy w nim formuª¦ gªówn¡ oraz tworzymy bezpo±redniego potomka lub dwóch bezpo±rednich potomków, z odpowiednimi formuªami
aktywnymi.
Kontynuujemy to post¦powanie tak dªugo, a» na ka»dej gaª¦zi tworzonego drzewa znajdzie si¦ aksjomat rachunku RS.
Oczywi±cie, je±li w korzeniu drzewa znajduje si¦ sekwent, który nie posiada dowodu, to w drzewie znajdzie si¦ co najmniej jedna gaª¡¹, której nie uda si¦ zako«czy¢ aksjomatem systemu RS.
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
` 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
` ( 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
` 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
` ¬¬ p → p
1. p ` p aksjomat 2. ` p, ¬p R¬ :1 3. ¬¬p ` p L¬:2 4. ` ¬¬p → p R→:3
` ( p → (p → q)) → (p → q)
` (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
` (ϕ → ψ) → ((ψ → χ) → (ϕ → χ)) ϕ → ψ ` (ψ → χ) → (ϕ → χ)
ψ → χ, ϕ → ψ ` ϕ → χ ϕ, ψ → χ, ϕ → ψ ` χ
χ, ϕ, ϕ → ψ ` χ ψ, χ, ϕ ` χ
χ, ϕ ` χ χ ` χ
χ, ϕ ` χ, ϕ ϕ ` χ, ϕ
ϕ ` ϕ
ϕ, ϕ → ψ ` χ, ψ ψ, ϕ ` χ, ψ
ψ ` χ, ψ ψ ` ψ
ϕ ` χ, ψ, ϕ ϕ ` ψ, ϕ
ϕ ` ϕ
` p ∨ ¬p
p ` p
`p, ¬p
`p ∨ ¬p
` ( p → q) ∨ (q → p)
q ` q q ` p, q p, q ` p, q q ` p → q, p
`p → q, q → p
` (p → q) ∨ (q → p)
` ((( 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
` ((ϕ →⊥) →⊥) → ϕ
` ((ϕ →⊥) →⊥) → ϕ (ϕ →⊥) →⊥` ϕ
⊥` ϕ
` ϕ →⊥, ϕ ϕ `⊥, ϕ
ϕ ` ϕ
∃ y∀xP(x, y) → ∀x∃yP(x, y)
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 6. ` ∃y∀xP(x, y) → ∀x∃yP(x, y) R→:5
` ¬∃ xP(x) → ∀x¬P(x)
P(a) ` P(a) P(a) ` ∃xP(x)
¬∃xP(x), P(a) `
¬∃xP(x) ` ¬P(a)
¬∃xP(x) ` ∀x¬P(x)
` ¬∃xP(x) → ∀x¬P(x)
wiczenia
wiczenie 1. 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))
5 ` (∃xP(x) ∨ ∃xQ(x)) → ∃x(P(x) ∨ Q(x))
wiczenie 2. Wybierz Twoj¡ ulubion¡ tez¦ (KRZ lub KRP) i zbuduj: jej dowód w systemie RS oraz jej dowód tablicowy.
Jakie± re eksje?
Semantyka reguª
1 Je±li Γ ` ∆ jest aksjomatem systemu RS, to v(Γ ` ∆) = 1 dla dowolnego warto±ciowania v.
2 Je±li przesªanka reguªy: (L∧), (R∨), (R →), (L¬), (R¬) ma warto±¢ 1 przy warto±ciowaniu v, to wniosek tej reguªy tak»e ma warto±¢ 1 przy warto±ciowaniu v.
3 Je±li obie przesªanki reguªy: (R∧), (L∨), (L →) maj¡ warto±¢ 1 przy warto±ciowaniu v, to wniosek tej reguªy tak»e ma warto±¢ 1 przy warto±ciowaniu v.
4 Je±li wniosek reguªy: (L∧), (R∨), (R →), (L¬), (R¬) ma warto±¢ 1 przy warto±ciowaniu v, to tak»e przesªanka tej reguªy ma warto±¢ 1 przy warto±ciowaniu v.
5 Je±li wniosek reguªy: (R∧), (L∨), (L →) ma warto±¢ 1 przy
warto±ciowaniu v, to tak»e obie przesªanki tej reguªy maj¡ warto±¢ 1 przy warto±ciowaniu v.
Trafno±¢ i peªno±¢
Trafno±¢ systemu RS (dla KRZ) jest oczywista: aksjomaty s¡
tautologiami KRZ (je±li ϕ ` ϕ jest aksjomatem systemu RS, to oczywi±cie ϕ → ϕ jest tautologi¡ KRZ). Ponadto, je±li przesªanki reguªy rachunku RS s¡ tautologiami KRZ, to i wniosek tej reguªy jest tautologi¡ KRZ.
Peªno±¢ rachunku RS udowodni¢ mo»na na ró»ne sposoby. W podr¦czniku Fitting 1990 zaleca si¦ oczywi±cie dowód poprzez wykorzystanie Twierdzenia o Istnieniu Modelu.
Wprowad¹my u»yteczny skrót: ¬S = {¬ϕ : ϕ ∈ S}.
Je±li S jest sko«czonym zbiorem formuª, to sekwentem
stowarzyszonym z S nazwiemy dowolny sekwent Γ ` ¬∆, gdzie para (Γ, ∆) jest podziaªem S, czyli: Γ ∩ ∆ = ∅ oraz Γ ∪ ∆ = S.
Trafno±¢ i peªno±¢
Fakt. Je±li jaki± sekwent stowarzyszony z S ma dowód w systemie RS, to ka»dy sekwent stowarzyszony z S ma dowód w systemie RS.
Powiemy, »e sko«czony zbiór formuª S jest sekwentowo sprzeczny, gdy dowolny (a w konsekwencji, ka»dy) sekwent stowarzyszony z S ma dowód w RS. Powiemy, »e sko«czony zbiór formuª S jest sekwentowo
niesprzeczny, gdy nie jest on sekwentowo sprzeczny.
Fakt. Rodzina wszystkich zbiorów sekwentowo niesprzecznych jest zdaniow¡ wªasno±ci¡ niesprzeczno±ci.
Fakt. Zachodz¡ nast¦puj¡ce implikacje:
1 Je±li sekwent Γ ` ∆, ¬ϕ ma dowód w systemie RS, to sekwent Γ, ϕ ` ∆równie» ma dowód w systemie RS.
2 Je±li sekwent Γ, ¬ϕ ` ∆ ma dowód w systemie RS, to sekwent Γ ` ∆, ϕrównie» ma dowód w systemie RS.
Trafno±¢ i peªno±¢
Twierdzenie o Peªno±ci Systemu RS dla KRZ. Je±li ϕ jest tautologi¡
KRZ, to ϕ jest tez¡ systemu RS (czyli: `RS ` ϕ).
Dowód. Przypu±¢my, »e ϕ nie jest tez¡ systemu RS. Wtedy sekwent
∅ ` ϕ nie ma dowodu w RS. Oznacza to, »e zbiór {¬ϕ} jest sekwentowo niesprzeczny, gdy» w przeciwnym przypadku dowód posiadaªby sekwent
¬ϕ ` ∅, a zatem dowód posiadaªby równie» sekwent ∅ ` ϕ. Na mocy Twierdzenia o Istnieniu Modelu zbiór {¬ϕ} jest speªnialny, a zatem ϕ nie jest tautologi¡ KRZ.
Reguªa ci¦cia
Reguª¡ ci¦cia (cut rule) nazywamy reguª¦ o nast¦puj¡cej postaci:
Γ ` ∆, ϕ ϕ, Γ ` ∆ Γ ` ∆
W szczególno±ci, je±li ∆ = {ψ}, to reguªa ci¦cia przybiera posta¢:
Γ ` ψ, ϕ ϕ, Γ ` ψ Γ ` ψ
Reguªa ta odpowiada zatem nast¦puj¡cej procedurze dowodowej:
1 Przypu±¢my, »e z jakich± zaªo»e« Γ otrzymujemy lemat ϕ oraz tez¦ ψ.
2 Przypu±¢my tak»e, »e z lematu ϕ oraz zaªo»e« Γ otrzyma¢ mo»emy tez¦ ψ.
3 Na mocy reguªy ci¦cia mo»emy wtedy uzyska¢ z zaªo»e« Γ tez¦ ψ.
Hauptsatz Gentzena
Reguªa ci¦cia wyst¦powaªa w oryginalnym systemie Gentzena. Pokazaª on jednak, »e u»ycia tej reguªy mog¡ zosta¢ w tym systemie
wyeliminowane:
Hauptsatz. Ka»dy dowód sekwentu Γ ` ∆ (w systemie RS z reguª¡
ci¦cia), w którym wyst¦puje reguªa ci¦cia mo»e zasta¢ zast¡piony dowodem w systemie RS bez u»ycia tej reguªy.
Zamiast mówi¢ o eliminowaniu reguªy ci¦cia, mo»na te» mówi¢, »e reguªa ci¦cia jest reguª¡ dopuszczaln¡ w systemie RS (zob. wykªad drugi).
Porównajmy reguª¦ ci¦cia z poznanymi wcze±niej reguªami:
1 Reguªa odrywania. ϕ→ψψ ϕ
2 Reguªa rezolucji. ϕ∨ψ ϕϕ∨¬ψ.
Komentarze
Dowody, które nie zawieraj¡ u»y¢ reguªy ci¦cia nazywa si¦ analitycznymi.
Dowody analityczne zalecaj¡ si¦ wieloma wªasno±ciami przydatnymi w automatycznym dowodzeniu twierdze« (m.in.: odwoªywanie si¦ wyª¡cznie do podformuª u»ywanych w dowodzie formuª). Jednak dowody analityczne bywaj¡ cz¦sto o wiele dªu»sze od dowodów, które analityczne nie s¡.
Ka»dy dowód w systemie RS mo»na do±¢ ªatwo przeksztaªci¢ na dowód w systemie aksjomatycznym w stylu Hilberta. Aby pokaza¢, »e jest równie»
na odwrót, czyli »e ka»dy dowód w systemie aksjomatycznym w stylu Hilberta mo»na przeksztaªci¢ na dowód w systemie RS, trzeba odpowiednio
zadba¢ o reguª¦ odrywania. Do tego wªa±nie sªu»y doª¡czenie reguªy ci¦cia do systemu RS. Nast¦pnie korzystamy oczywi±cie z twierdzenia o eliminacji reguªy ci¦cia.
Fitting, M. 1996. First-Order Logic and Automated Theorem Proving.
Springer, Berlin.
Gentzen, G. 1935. Untersuchungen über das logische Schliessen.
Mathematische Zeitschrift 39, 176210, 405431.
Negri, S., von Plato, J. 2001. Structural Proof Theory. Cambridge University Press, Cambridge.
Rasiowa, H., Sikorski, R. 1963. The Mathematics of
Metamathematics. Pa«stwowe Wydawnictwo Naukowe, Warszawa.
Pogorzelski, W.A. 1981. Klasyczny rachunek kwanty katorów. Zarys teorii. Pa«stwowe Wydawnictwo Naukowe, Warszawa.
Smullyan, R. 1968. First-Order Logic. Springer Verlag, Berlin.
Troelstra, A.S., Schwichtenberg, H. 2000. Basic Proof Theory.
Cambridge University Press, Cambridge.
