Dowody zaªo»eniowe w KRZ
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 24xi2015
Wst¦p
Plan na dzi±
Podamy reguªy pierwotne wykorzystywane w dowodach zaªo»eniowych w KRZ (w stylu Sªupeckiego-Borkowskiego).
Podamy przykªady dowodów wprost oraz nie wprost.
Wska»emy niektóre reguªy wtórne systemu.
Rozwa»ymy przykªady dowodów z dodatkowymi zaªo»eniami.
Rozwa»ymy przykªady dowodów rozgaª¦zionych.
Podamy informacje o bardziej wspóªczesnych uj¦ciach dedukcji naturalnej.
Wst¦p
Ideologia
Systemy dedukcji naturalnej pochodz¡ od Gerharda Gentzena (19091945) oraz Stanisªawa Ja±kowskiego (19061965).
Systemy te miaªy m.in. reprezentowa¢ praktyk¦ dowodow¡
matematyków.
Twierdzenia matematyczne skªadaj¡ si¦ z zaªo»e« oraz tezy.
Zakªadamy, »e zachodz¡ zaªo»enia i staramy si¦ wyprowadzi¢ z nich tez¦. Tak wi¦c, twierdzenie o zaªo»eniach ψ1, ψ2, . . . , ψn oraz tezie ϕ ma struktur¦:
ψ1→ (ψ2 → (. . . → (ψn→ ϕ) . . .))
Reguªy pierwotne
Reguªa odrywania
Zbiór reguª pierwotnych systemu zaªo»eniowego oznaczymy przez jas.
Nale»¡ do«:
(RO) Reguªa odrywania. Je±li do dowodu nale»y implikacja oraz jej poprzednik, to do dowodu wolno doª¡czy¢ nast¦pnik tej implikacji.
W zapisie symbolicznym:
ϕ → ψ ϕ ψ
Ta reguªa to zatem reguªa opuszczania implikacji. Reguªa doª¡czania implikacji ma w tym systemie dowodowym specjalny status: tradycyjnie mówi si¦ przy tym o tzw. dodatkowych zaªo»eniach dowodu (o czym za
Reguªy pierwotne
Reguªy pierwotne: koniunkcja
(DK)Reguªa doª¡czania koniunkcji. Do dowodu wolno doª¡czy¢
koniunkcj¦, o ile oba jej czªony nale»¡ do dowodu.
ϕ ψ
ϕ ∧ ψ
(OK)Reguªa opuszczania koniunkcji. Je±li do dowodu nale»y koniunkcja, to wolno doª¡czy¢ do dowodu ka»dy z jej czªonów.
ϕ ∧ ψ ϕ
ϕ ∧ ψ ψ
Reguªy pierwotne
Reguªy pierwotne: alternatywa
(DA)Reguªa doª¡czania alternatywy. Je±li do dowodu nale»y jaka±
formuªa, to do dowodu wolno doª¡czy¢ alternatyw¦, której jednym z czªonów jest ta formuªa.
ϕ ϕ ∨ ψ
ψ ϕ ∨ ψ
(OA)Reguªa opuszczania alternatywy. Je±li do dowodu nale»y alternatywa oraz negacja jednego z jej czªonów, to do dowodu doª¡czy¢ mo»na pozostaªy czªon tej alternatywy:
ϕ ∨ ψ ¬ϕ ψ
ϕ ∨ ψ ¬ψ ϕ
Reguªy pierwotne
Reguªy pierwotne: równowa»no±¢
(DR)Reguªa doª¡czania równowa»no±ci. Do dowodu wolno doª¡czy¢
równowa»no±¢, o ile nale»y do dowodu implikacja, której
poprzednikiem jest pierwszy czªon tej równowa»no±ci, a nast¦pnikiem drugi jej czªon, jak i implikacja odwrotna.
ϕ → ψ ψ → ϕ ϕ ≡ ψ
(OR) Reguªa opuszczania równowa»no±ci. Je±li do dowodu nale»y równowa»no±¢, to wolno doª¡czy¢ do dowodu zarówno implikacj¦, której poprzednikiem jest pierwszy czªon tej równowa»no±ci, a nast¦pnikiem drugi jej czªon, jak i implikacj¦ odwrotn¡.
ϕ ≡ ψ ϕ → ψ
ϕ ≡ ψ ψ → ϕ
Reguªy pierwotne
Oryginalny system Ja±kowskiego
W systemie zaproponowanym przez Ja±kowskiego nie zakªadano reguªy opuszczania alternatywy jako reguªy pierwotnej, przyjmowano natomiast jeszcze nast¦puj¡ce reguªy pierwotne:
(RK) Reguªa kontrapozycji. Je±li do dowodu nale»y implikacja, której poprzednikiem jest negacja jednej formuªy, a nast¦pnikiem negacja drugiej formuªy, to do dowodu mo»na doª¡czy¢ implikacj¦, której poprzednikiem jest druga formuªa, a nast¦pnikiem pierwsza formuªa.
¬ϕ → ¬ψ ψ → ϕ
Reguªy pierwotne
Oryginalny system Ja±kowskiego
(DP)Reguªa dodawania poprzedników. Je±li do dowodu nale»¡ dwie implikacje o takim samym nast¦pniku, to do dowodu wolno doª¡czy¢
implikacj¦ o tym»e nast¦pniku i o poprzedniku b¦d¡cym alternatyw¡
poprzedników tych implikacji.
ϕ → χ ψ → χ (ϕ ∨ ψ) → χ
Korzystaj¡c z reguª pierwotnych z jas mo»na wyprowadzi¢ (RK) oraz (DP).
Reguª¦ (OA) mo»na wyprowadzi¢ w oryginalnym systemie Ja±kowskiego.
Tezy systemu zaªo»eniowego Tezy
Dowody zaªo»eniowe: nieformalna charakterystyka
Dowodem zaªo»eniowym (wprost)formuªy
(ψ1 → (ψ2 → . . . → (ψn→ ϕ) . . .))nazywamy ka»dy ci¡g formuª taki, »e:
1 pierwsze n elementów tego ci¡gu to formuªy ψ1, ψ2, . . . , ψn (zaªo»enia dowodu)
2 wszystkie pozostaªe elementy tego ci¡gu (kroki dowodowe) powstaj¡ z elementów wcze±niejszych poprzez zastosowanie której± z pierwotnych reguª dowodowych, reguª wtórnych lub tez wcze±niej udowodnionych
3 ostatnim elementem tego ci¡gu jest formuªa ϕ.
Piszemy {ψ1, ψ2, . . . , ψn} `jas ϕ, gdy formuªa
(ψ1 → (ψ2 → . . . → (ψn→ ϕ) . . .))ma dowód zaªo»eniowy.
Dowody zaªo»eniowe zapisujemy w postaci ci¡gów formuª, z komentarzami
Tezy systemu zaªo»eniowego Tezy
Indukcyjna de nicja tezy
Przez indukcj¦ okre±lamy zbiór Tjas tez systemu zaªo»eniowego KRZ opartego na reguªach jas:
χ ∈Tjas0 wtedy i tylko wtedy, gdy istnieje liczba naturalna n > 0 oraz formuªy ψ1, ψ2, . . . , ψn, ϕtakie, »e: χ jest identyczna z
(ψ1 → (ψ2→ . . . → (ψn→ ϕ) . . .))oraz ϕ ∈ Cjas({ψ1, ψ2, . . . , ψn}) (gdzie Cjas to operacja konsekwencji wyznaczona przez reguªy z jas, zob. wykªad drugi).
α ∈Tjask+1 wtedy i tylko wtedy, gdy χ ∈ Tjask lub istniej¡ liczby naturalne n > 0, i < n oraz formuªy ψ1, ψ2, . . . , ψn, ϕtakie, »e:
χjest identyczna z (ψ1→ (ψ2→ . . . → (ψi→ ϕ) . . .)) ψi+1, ψi+2, . . . , ψn∈Tjask
ϕ ∈Cjas({ψ1, ψ2, . . . , ψn}).
χ ∈Tjas wtedy i tylko wtedy, gdy istnieje m taka, »e χ ∈ Tjasm.
Tezy systemu zaªo»eniowego Tezy
Tezy systemu zaªo»eniowego KRZ: komentarz
Je±li χ ∈ Tjasm, to mówimy, »e χ jesttez¡ stopnia m systemu
zaªo»eniowego KRZ. Je±li χ jest tez¡ stopnia m i m 6 n, to χ jest te»
oczywi±cie tez¡ stopnia n. Je±li χ ∈ Tjas, to mówimy, »e χ jesttez¡
systemu zaªo»eniowego KRZ.
Podan¡ tu indukcyjn¡ de nicj¦ zbioru tez systemu zaªo»eniowego KRZ przytaczamy za: Pogorzelski, W.A. 1975. Klasyczny rachunek zda«.
Zarys teorii. PWN, Warszawa (strona 188).
Zbiory tez i zbiory reguª wyprowadzalnych aksjomatycznego i zaªo»eniowego systemu KRZ s¡ równe.
Tezy systemu zaªo»eniowego Kilka przykªadów
Prawo komutacji
(ϕ → (ψ → χ)) → (ψ → (ϕ → χ)) (prawo komutacji) Nale»y dowie±¢, »e z zaªo»e« ϕ → (ψ → χ), ψ, ϕ mo»na otrzyma¢ χ, u»ywaj¡c reguª ze zbioru jas.
1. ϕ → (ψ → χ) zaªo»enie
2. ψ zaªo»enie
3. ϕ zaªo»enie
4. ψ → χ RO: 1,3
5. χ RO: 4,2.
Zauwa»my, »e ten dowód jest taki sam, jak dowód prawa komutacji w aksjomatycznym uj¦ciu KRZ, przy wykorzystaniu Twierdzenia o Dedukcji Wprost.
Tezy systemu zaªo»eniowego Kilka przykªadów
Prawo eksportacji
((ϕ ∧ ψ) → χ) → (ϕ → (ψ → χ)) prawoeksportacji Trzeba pokaza¢, »e z zaªo»e« (ϕ ∧ ψ) → χ, ϕ, ψ mo»na otrzyma¢ χ.
1. (ϕ ∧ ψ) → χ zaªo»enie
2. ϕ zaªo»enie
3. ψ zaªo»enie
4. ϕ ∧ ψ DK: 2,3
5. χ RO: 1,4.
Zauwa», »e planowaniedowodu jest w tej metodzie prostsze, ni» w metodzie aksjomatycznej.
Tezy systemu zaªo»eniowego Kilka przykªadów
Prawo importacji
(ϕ → (ψ → χ)) → ((ϕ ∧ ψ) → χ) prawoimportacji Trzeba pokaza¢, »e z zaªo»e« ϕ → (ψ → χ), ϕ ∧ ψ mo»na otrzyma¢ χ.
1. ϕ → (ψ → χ) zaªo»enie 2. ϕ ∧ ψ zaªo»enie
3. ϕ OK: 2
4. ψ OK: 2
5. ψ → χ RO: 1,3
6. χ RO: 5,4.
Zwró¢ uwag¦ na ró»ne mo»liwo±ci kolejno±ci wykonania poszczególnych kroków dowodu.
Tezy systemu zaªo»eniowego Kilka przykªadów
Prawo sylogizmu hipotetycznego
(ϕ → ψ) → ((ψ → χ) → (ϕ → χ)) prawo sylogizmu hipotetycznego
Trzeba pokaza¢, »e z zaªo»e«: ϕ → ψ, ψ → χ oraz ϕ mo»na otrzyma¢ χ.
1. ϕ → ψ zaªo»enie 2. ψ → χ zaªo»enie 3. ϕ zaªo»enie
4. ψ RO: 1,3
5. χ RO: 2,3.
Tezy systemu zaªo»eniowego Kilka przykªadów
Prawo Fregego
(ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ)) prawo Fregego Trzeba pokaza¢, »e z zaªo»e«: ϕ → (ψ → χ), ϕ → ψ oraz ϕ mo»na otrzyma¢ χ.
1. ϕ → (ψ → χ) zaªo»enie 2. ϕ → ψ zaªo»enie
3. ϕ zaªo»enie
4. ψ RO: 2,3
5. ψ → χ RO: 1,3
6. χ RO: 5,4.
Przykªady reguª wtórnych
Reguªa sylogizmu hipotetycznego
ϕ → ψ ψ → χ
ϕ → χ
Trzeba pokaza¢, »e z zaªo»e«: ϕ → ψ i ψ → χ mo»na otrzyma¢ ϕ → χ.
1. ϕ → ψ zaªo»enie
2. ψ → χ zaªo»enie
3. (ϕ → ψ) → ((ψ → χ) → (ϕ → χ)) prawo sylogizmu hipotetycznego
4. (ψ → χ) → (ϕ → χ) RO: 3,1
5. ϕ → χ RO: 4,2.
Przykªady reguª wtórnych
Reguªa Fregego
ϕ → (ψ → χ) ϕ → ψ
ϕ → χ
Trzeba pokaza¢, »e z zaªo»e«: ϕ → (ψ → χ) oraz ϕ → ψ mo»na otrzyma¢
ϕ → χ.
1. ϕ → (ψ → χ) zaªo»enie
2. ϕ → ψ zaªo»enie
3. (ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ)) prawo Fregego
4. (ϕ → ψ) → (ϕ → χ) RO: 3,1
5. ϕ → χ RO: 4,2.
Dowody nie wprost
Dowody nie wprost
Zachodzi Twierdzenie o Dowodach Nie Wprost:
Je±li {ψ1, ψ2, . . . , ψn} ∪ {¬ϕ} `jas χ oraz {ψ1, ψ2, . . . , ψn} ∪ {¬ϕ} `jas ¬χ dla pewnej formuªy χ, to {ψ1, ψ2, . . . , ψn} `jas ϕ.
Twierdzenie to pozwala zatem na stosowanie w systemie zaªo»eniowym dowodów nie wprost: aby pokaza¢, »e z zaªo»e« {ψ1, ψ2, . . . , ψn}mo»na wyprowadzi¢ ϕ, wystarczy pokaza¢, »e z zaªo»e« {ψ1, ψ2, . . . , ψn, ¬ϕ}
mo»na wyprowadzi¢ w systemie zaªo»eniowym KRZ par¦ formuª wzajem sprzecznych.
Nadto, z twierdzenia tego mo»emy korzysta¢ równie» przy dowodzeniu wyprowadzalno±ci reguª wtórnych systemu zaªo»eniowego KRZ.
Dowody nie wprost
Dowody nie wprost: przykªady
W dowodzie nie wprost formuªy ψ1 → (ψ2 → (. . . → (ψn→ ϕ) . . .))(czyli wyprowadzeniu ϕ z zaªo»e« {ψ1, ψ2, . . . , ψn} metod¡ nie wprost)
dopisujemy do zaªo»e« ¬ϕ, czyli zaªo»enie dowodu nie wprost(w skrócie:
z.d.n.) i staramy si¦ wyprowadzi¢ z tych zaªo»e« par¦ formuª wzajem sprzecznych. Gdy to si¦ powiedzie, ϕ jest konsekwencj¡ ψ1, ψ2, . . . , ψn w systemie zaªo»eniowym KRZ. Symbolu ⊥ u»ywamy tu na oznaczenie sprzeczno±ci.
Dla przykªadu, dowód nie wprost formuªy ¬¬ϕ → ϕjest nast¦puj¡cy:
1. ¬¬ϕ zaªo»enie 2. ¬ϕ z.d.n.
3. ⊥ sprzeczno±¢: 1, 2.
Na mocy powy»szego, mo»emy w dalszych dowodach stosowa¢ wtórn¡
reguª¦ opuszczania negacji ON: ¬¬ϕϕ .
Dowody nie wprost
Dowody nie wprost: przykªady
ϕ → ¬¬ϕ
1. ϕ zaªo»enie 2. ¬¬¬ϕ z.d.n.
3. ¬ϕ ON: 2
4. ⊥ sprzeczno±¢: 1, 3.
Z tez ϕ → ¬¬ϕ i ¬¬ϕ → ϕ otrzymujemy, na mocy reguªy DR tez¦:
ϕ ≡ ¬¬ϕ.
Na mocy powy»szego, mo»emy w dalszych dowodach stosowa¢ wtórn¡
reguª¦ doª¡czania negacji DN:
ϕ .
Dowody nie wprost
Dowody nie wprost: przykªady
(ϕ → ψ) → (¬ψ → ¬ϕ) prawokontrapozycji
1. ϕ → ψ zaªo»enie
2. ¬ψ zaªo»enie
3. ¬¬ϕ z.d.n.
4. ¬¬ϕ → ϕ prawo podwójnej negacji
5. ϕ RO: 4,3
6. ψ RO: 1,5
7. ⊥ sprzeczno±¢: 2, 6.
Par¦ formuª wzajem sprzecznych znajdujemy w wierszach 2 i 6.
Dowody nie wprost
Dowody nie wprost: przykªady
{ϕ → ψ, ¬ψ} `jas ¬ϕ 1. ϕ → ψ zaªo»enie 2. ¬ψ zaªo»enie 3. ¬¬ϕ z.d.n.
4. ϕ ON: 3
5. ψ RO: 1,4
6. ⊥ sprzeczno±¢: 2, 5.
Pokazali±my wi¦c, »e reguª¡ wtórn¡ jest reguªamodus tollendo tollens MT:
ϕ → ψ, ¬ψ
¬ϕ .
Dowody z dodatkowymi zaªo»eniami
Dodatkowe zaªo»enia dowodu
Kolejna wielce u»yteczna technika dowodowa w systemie zaªo»eniowym KRZ polega na korzystaniu z tzw. dodatkowych zaªo»e« dowodu. Jest to procedura nast¦puj¡ca:
Czynimy w dowodzie dodatkowe zaªo»enieϕ.
Je±li z zaªo»enia ϕ (oraz wcze±niejszych kroków dowodu) mo»emy wyprowadzi¢ formuª¦ ψ, to do dowodu wolno wª¡czy¢ formuª¦ ϕ → ψ.
Z kroków wyprowadzenia ψ z ϕ nie wolnokorzysta¢ poza tym wyprowadzeniem. Zwykle stosuje si¦ stosown¡ numeracj¦: je±li dodatkowe zaªo»enie ϕ ma numer n.1., a wyprowadzona z niego formuªa ma numer n.m., to z kroków o numerach od n.1. do n.m.nie korzystamy w dowodzie gªównym.
Dowody z dodatkowymi zaªo»eniami
Dodatkowe zaªo»enia dowodu: przykªad 1
((ϕ ∨ ψ) → (χ ∧ ϑ)) → ((ϕ → χ) ∧ (ψ → ϑ)) 1. (ϕ ∨ ψ) → (χ ∧ ϑ) zaªo»enie
1.1. ϕ zaªo»enie dodatkowe
1.2. ϕ ∨ ψ DA: 1.1.
1.3. χ ∧ ϑ RO: 1,1.2.
1.4. χ OK: 1.3.
2. ϕ → χ 1.1.⇒1.4.
2.1. ψ zaªo»enie dodatkowe
2.2. ϕ ∨ ψ DA: 2.1.
2.3. χ ∧ ϑ RO: 1,2.2.
2.4. ϑ OK: 2.3.
3. ψ → ϑ 2.1.⇒2.4.
4. (ϕ → χ) ∧ (ψ → ϑ) DK: 2,3.
Dowody z dodatkowymi zaªo»eniami
Dodatkowe zaªo»enia dowodu: przykªad 2
(ϕ → ψ) → ((χ → ϑ) → (¬(ψ ∨ ϑ) → ¬(ϕ ∨ χ))) 1. ϕ → ψ zaªo»enie
2. χ → ϑ zaªo»enie 3. ¬(ψ ∨ ϑ) zaªo»enie 4. ¬¬(ϕ ∨ χ) z.d.n.
5. ϕ ∨ χ ON: 4
5.1. ϕ zaªo»enie dodatkowe
5.2. ψ RO: 1,5.1.
5.3. ψ ∨ ϑ DA: 5.2.
6. ϕ → (ψ ∨ ϑ) 5.1.⇒5.3.
7. ¬ϕ MT: 6,3
8. χ OA: 5,7
9. ϑ RO: 2,8
10. ψ ∨ ϑ DA: 9
11. ⊥ sprzeczno±¢: 3, 10.
Dalsze przykªady
Dowody dalszych tez
Poka»emy, »e wyprowadzalna jest reguªa ϕ,¬ϕψ .
1. ϕ zaªo»enie 2. ¬ϕ zaªo»enie 3. ϕ ∨ ψ DA: 1 4. ψ OA: 3,2.
Reguª¦ ϕ,¬ϕψ nazywamy reguª¡Dunsa Scotusa(RDS).
Dalsze przykªady
Dowody dalszych tez
ϕ → (¬ϕ → ψ) 1. ϕ zaªo»enie 2. ¬ϕ zaªo»enie 3. ψ RDS: 1,2.
Dalsze przykªady
Dowody dalszych tez
¬(ϕ ∨ ψ) → ¬ϕ ∧ ¬ψ.
1. ¬(ϕ ∨ ψ) zaªo»enie
1.1. ϕ zaªo»enie dodatkowe 1.2. ϕ ∨ ψ DA: 1.1.
2. ϕ → (ϕ ∨ ψ) 1.1.⇒1.2.
3. ¬ϕ MT: 2,1
3.1. ψ zaªo»enie dodatkowe 3.2. ϕ ∨ ψ DA: 3.1.
4. ψ → (ϕ ∨ ψ) 3.1.⇒3.2.
5. ¬ψ MT: 4,1
5. ¬ϕ ∧ ¬ψ DK: 3,5.
Dalsze przykªady
Dowody dalszych tez
(¬ϕ ∧ ¬ψ) → ¬(ϕ ∨ ψ). 1. ¬ϕ ∧ ¬ψ zaªo»enie 2. ¬¬(ϕ ∨ ψ) z.d.n.
3. ϕ ∨ ψ ON: 2
4. ¬ϕ OK: 1
5. ¬ψ OK: 1
6. ψ OA: 3,4
7. ⊥ sprzeczno±¢: 5, 6.
Dwie udowodnione wy»ej tezy daj¡ ª¡cznie prawo negowania alternatywy
¬(ϕ ∨ ψ) ≡ ¬ϕ ∧ ¬ψ. Reguª¡ wtórn¡ jest zatem reguªanegowania alternatywy NA: ¬(ϕ∨ψ)¬ϕ∧¬ψ.
Dalsze przykªady
Dowody dalszych tez
¬(ϕ ∧ ψ) → ¬ϕ ∨ ¬ψ. 1. ¬(ϕ ∧ ψ) zaªo»enie 2. ¬(¬ϕ ∨ ¬ψ) z.d.n.
3. ¬¬ϕ ∧ ¬¬ψ NA: 2
4. ¬¬ϕ OK: 3
5. ¬¬ψ OK: 3
6. ϕ ON: 4
7. ψ ON: 5
8. ϕ ∧ ψ DK: 6,7.
9. ⊥ sprzeczno±¢: 1, 8.
Dalsze przykªady
Dowody dalszych tez
(¬ϕ ∨ ¬ψ) → ¬(ϕ ∧ ψ). 1. ¬ϕ ∨ ¬ψ zaªo»enie 2. ¬¬(ϕ ∧ ψ) z.d.n.
3. ϕ ∧ ψ ON: 2
4. ϕ OK: 3
5. ψ OK: 3
6. ¬¬ϕ DN: 4
7. ¬ψ OA: 1,6.
8. ⊥ sprzeczno±¢: 5, 7.
Dwie udowodnione wy»ej tezy daj¡ ª¡cznie prawo negowania koniunkcji
¬(ϕ ∧ ψ) ≡ ¬ϕ ∨ ¬ψ. Reguª¡ wtórn¡ jest zatem reguªanegowania koniunkcji NK: ¬(ϕ∧ψ)¬ϕ∨¬ψ.
Dalsze przykªady
Dygresja: Teodycea i kule w pªocie
Poka»emy, »e nast¦puj¡ce wnioskowanie jest dedukcyjne:
Bóg jest miªosierny, o ile jest doskonaªy. Je±li Bóg jest doskonaªy i stworzyª
wiat, to w wiecie nie ma Zªa. Jednak w wiecie jest Zªo. Ponadto, Bóg przecie» stworzyª wiat. Zatem Bóg nie jest doskonaªy lub nie jest
miªosierny.
p Bóg jest doskonaªy.
q Bóg jest miªosierny.
r Bóg stworzyª wiat.
s W wiecie jest Zªo.
Dalsze przykªady
Dygresja: Teodycea i kule w pªocie
{p → q, (p ∧ r) → ¬s, s, r} `jas ¬p ∨ ¬q.
1. p → q zaªo»enie 2. (p ∧ r) → ¬s zaªo»enie
3. s zaªo»enie
4. r zaªo»enie
5. ¬¬s DN: 3
6. ¬(p ∧ r) MT: 2,5 7. ¬p ∨ ¬r NK: 6
8. ¬¬r DN: 4
9. ¬p OA: 7,8
10. ¬p ∨ ¬q DA: 9.
Zauwa»my, »e w dowodzie nie korzystano z pierwszego zaªo»enia.
Sprzeczne zbiory formuª
Sprzeczne zbiory formuª
Zbiór formuª X jest (syntaktycznie) sprzeczny, je±li istnieje formuªa ϕ taka,
»e X `jas ϕoraz X `jas ¬ϕ. Je±li X nie jest sprzeczny, to mówimy, »e X jest (syntaktycznie) niesprzeczny.
Na mocy Twierdzenia o Zwarto±ci wykazanie syntaktycznej sprzeczno±ci zbioru formuª X polega na zbudowaniu dowodu zaªo»eniowego, którego przesªankami s¡ elementy jakiego± sko«czonego podzbioru zbioru X i w którego wierszach znajduje si¦ para formuª wzajem sprzecznych.
Sprzeczne zbiory formuª
Sprzeczne zbiory formuª: przykªady
Poka»emy, »e {ϕ ∨ ¬ψ, χ → ψ, ¬(ϑ ∧ ¬χ), ϑ ∧ ¬ϕ} jest sprzecznym zbiorem formuª.
1. ϕ ∨ ¬ψ zaªo»enie 2. χ → ψ zaªo»enie 3. ¬(ϑ ∧ ¬χ) zaªo»enie 4. ϑ ∧ ¬ϕ zaªo»enie
5. ϑ OK: 4
6. ¬ϕ OK: 4
7. ¬ψ OA: 1,6
8. ¬χ MT: 2,7
9. ϑ ∧ ¬χ DK: 5,8
10. ⊥ sprzeczno±¢: 3, 9.
Sprzeczne zbiory formuª
Sprzeczne zbiory formuª: przykªady
Poka»emy, »e{¬χ ∧ ψ, ϕ → (ψ → (χ ∨ ¬ϑ)), ϕ, ϑ ∧ (ψ → χ)}jest sprzeczny.
1. ¬χ ∧ ψ zaªo»enie
2. ϕ → (ψ → (χ ∨ ¬ϑ)) zaªo»enie
3. ϕ zaªo»enie
4. ϑ ∧ (ψ → χ) zaªo»enie
5. ¬χ OK: 1
6. ψ OK: 1
7. ψ → (χ ∨ ¬ϑ) RO: 2,3
8. χ ∨ ¬ϑ RO: 7,6
9. ¬ϑ OA: 8,5
10. ψ → χ OK: 4
11. χ RO: 10,6
12. ⊥ sprzeczno±¢: 5, 11.
Dowody rozgaª¦zione
Dowody rozgaª¦zione wprost
Podamy jeszcze par¦ przykªadów dowodów rozgaª¦zionych (dowodów przez rozwa»enie przypadków).
Dowód rozgaª¦ziony wprost formuªy (ψ1 → (ψ2 → . . . (ψn→ χ) . . .)) uwa»amy za zako«czony, je±li:
(a) istnieje wyprowadzenie χ z ka»dego z dodatkowych zaªo»e«
χ1, χ2, . . . , χm
(b) alternatywa χ1∨ χ2∨ . . . ∨ χm jest jednym z wierszy wyprowadzenia formuªy χ.
Uzasadnienie. Je±li (a), to do dowodu χ mo»na doª¡czy¢ wszystkie implikacje χi → χ, dla 1 6 i 6 m. Na mocy reguªy dodawania
poprzedników, mo»na te» doª¡czy¢ formuª¦: (χ1∨ χ2∨ . . . ∨ χm) → χ. Na mocy (b) i reguªy odrywania otrzymujemy χ.
Dowody rozgaª¦zione
Dowody rozgaª¦zione wprost: przykªady
(ϕ ∨ (ψ ∧ χ)) → (ϕ ∨ ψ) 1. ϕ ∨ (ψ ∧ χ) zaªo»enie
1.1. ϕ zaªo»enie dodatkowe 1.2. ϕ ∨ ψ DA: 1.1.
2.1. ψ ∧ χ zaªo»enie dodatkowe
2.2. ψ OK: 2.1.
2.3. ϕ ∨ ψ DA: 2.2.
3. ϕ ∨ ψ 1; 1.1.⇒1.2.; 2.1.⇒2.3.
Komentarz w ostatnim wierszu czytamy: mamy alternatyw¦ 1, wyprowadzenie 1.1.⇒1.2. formuªy ϕ ∨ ψ z pierwszego czªonu alternatywy 1 oraz wyprowadzenie 2.1.⇒2.3. formuªy ϕ ∨ ψ z drugiego czªonu alternatywy 1, czyli dowód
rozgaª¦ziony formuªy (ϕ ∨ (ψ ∧ χ)) → (ϕ ∨ ψ) jest zako«czony.
Dowody rozgaª¦zione
Dowody rozgaª¦zione wprost: przykªady
(ϕ → ψ) → ((ϕ ∨ χ) → (ψ ∨ χ)) 1. ϕ → ψ zaªo»enie 2. ϕ ∨ χ zaªo»enie
2.1. ϕ zaªo»enie dodatkowe
2.2. ψ RO: 1,2.1.
2.3. ψ ∨ χ DA: 2.2.
3. ψ → (ψ ∨ χ) 2.1.⇒2.3.
3.1. χ zaªo»enie dodatkowe 3.2. ψ ∨ χ DA: 3.1.
4. χ → (ψ ∨ χ) 3.1.⇒3.2.
5. ψ ∨ χ 2; 3; 4
Inny (bardziej skrupulatny) zapis dowodu rozgaª¦zionego.
Dowody rozgaª¦zione
Dowody rozgaª¦zione wprost: przykªady
((ϕ → ψ) ∧ (χ → ϑ)) → ((ϕ ∨ χ) → (ψ ∨ ϑ)) 1. (ϕ → ψ) ∧ (χ → ϑ) zaªo»enie
2. ϕ ∨ χ zaªo»enie
3. ϕ → ψ OK: 1
4. χ → ϑ OK: 1
4.1. ϕ zaªo»enie dodatkowe
4.2. ψ RO: 3,4.1.
4.3. ψ ∨ ϑ DA: 4.2.
5. ϕ → (ψ ∨ ϑ) 4.1.⇒4.3.
5.1. χ zaªo»enie dodatkowe
5.2. ϑ RO: 4,5.1.
5.3. ψ ∨ ϑ DA: 5.2.
6. χ → (ψ ∨ ϑ) 5.1.⇒5.3.
7. ψ ∨ ϑ 2; 5; 6
Dedukcja naturalna w innych stylizacjach
Propozycja w Fitting 1990
Reguªa wprowadzania implikacji: [ϕ...ψ]ϕ→ψ Reguªy dla staªych: ⊥ϕ, >
Reguªy dla negacji: ϕ ¬ϕ⊥ , [ϕ...⊥]¬ϕ , [¬ϕ...⊥]ϕ
Reguªy dla α-formuª: αα1, αα2, α1αα2
Reguªy dla β-formuª: ¬ββ12 β, ¬ββ21 β, [¬β1β...β2], [¬β2β...β1]
Zapis [ϕ . . . ψ] nale»y tu rozumie¢ tak samo, jak w omówionych wy»ej przypadkach dowodów z dodatkowymi zaªo»eniami: oznacza on, »e mamy wyprowadzenie ψ z zaªo»enia ϕ. Stosowane bywaj¡ ró»ne kaligra e:
pudeªka otaczaj¡ce wyprowadzenia, kreski pionowe wyró»niaj¡ce poddowody, drzewa, itd.
Wykorzystywana literatura
Dowody zaªo»eniowe
Borkowski, L. 1991. Wprowadzenie do logiki i teorii mnogo±ci.
Wydawnictwo Naukowe KUL, Lublin.
Georgacarakos, G.N., Smith, R. 1979. Elementary formal logic.
McGraw-Hill Book Company.
Pogorzelski, W.A. 1975. Klasyczny rachunek zda«. Zarys teorii.
PWN, Warszawa.
Pogorzelski, W.A. 1992. Elementarny sªownik logiki formalnej.
Biaªystok.
Sªupecki, J., Borkowski, L. 1962. Elementy logiki matematycznej i teorii mnogo±ci. Pa«stwowe Wydawnictwo Naukowe, Warszawa.
Sªupecki, J., Haªkowska, K, Piróg-Rzepecka, K. 1999. Logika matematyczna. Wydawnictwo Naukowe PWN, Warszawa.
Surma, S. 1967. Twierdzenia o dedukcji niewprost. Studia Logica XX,
Wykorzystywana literatura
Uj¦cia bardziej nowoczesne
Fitting, M. 1996. First-Order Logic and Automated Theorem Proving.
Springer, Berlin.
Negri, S., von Plato, J. 2001. Structural Proof Theory. Cambridge University Press, Cambridge.
Troelstra, A.S., Schwichtenberg, H. 2000. Basic Proof Theory.
Cambridge University Press, Cambridge.
