Dedukcja naturalna. Systemy założeniowe

W tej części będziemy sprawdzać poprawność rozumowań metodą syntaktyczną - czyli sprawdzać, czy ze zbioru przesłanek da się wyprowadzić wniosek. By to zrobić w systemie aksjomatycznym, musimy (zgodnie z definicją wyprowadzalności) podać ciąg formuł, który kończy się wnioskiem, a każdy z elementów tego ciągu poprzedzający wniosek jest albo przesłanką, albo aksjomatem, albo został uzyskany z poprzednich elementów poprzez zastosowanie reguły odrywania. 

Ponieważ w praktyce umiejętność wyprowadzania wniosków ze zbioru przesłanek i aksjomatów w oparciu o regułę odrywania wymaga wprawy, będziemy robili dowody w systemie założeniowym, który nie zawiera aksjomatów, a zamiast tego posiada (jedynie) rozbudowany zestaw reguł, które stwierdzają, że określone schematy wnioskowań są niezawodne. Takim systemem jest system dedukcji naturalnej, który zawiera dwa typy reguł - reguły wprowadzania oraz opuszczania dla poszczególnych spójników.

Reguły wnioskowania

System dedukcji naturalnej ma pierwotne reguły wnioskowania (przyjmowane bez dowodu) oraz wtórne reguły (które da się wyprowadzić, korzystając z reguł pierwotnych). Będziemy korzystali zarówno z jednych, jak i z drugich.

Jeśli nie wiesz do końca, jak działają reguły wyprowadzania, to możesz poćwiczyć na tym kalkulatorze reguł.

Przy dowodzeniu możemy korzystać również z innych praw logicznych. Teraz wprowadzimy kolejną regułę wnioskowania, z której będziemy korzystać w dowodzeniu. Zauważmy, że na razie w naszym zestawie reguł wnioskowania nie ma reguły wprowadzenia implikacji (dołączania do zbioru przesłanek nowej implikacji). Załóżmy na chwilę, że nie mamy w zestawie reguł prawa transpozycji i chcemy go udowodnić, czyli pokazać, że ze zbioru przesłanek {α→β} da się wyprowadzić wniosek ¬β→¬α. Jak to zrobić? - Hm, gdybyśmy mieli dodatkową przesłankę ¬β, to wyprowadzenie byłoby oczywiste: {α→β, ¬β} ⊢ ¬α (modus tollens, MT). Z kolei na mocy twierdzenia o dedukcji {α→β, ¬β} ⊢ ¬α wtedy i tylko wtedy, gdy {α→β} ⊢ ¬β→¬α. Zauważmy, że w tym ostatnim kroku powróciliśmy do wyjściowego zbioru przesłanek (w pewnym sensie wyeliminowaliśmy dodatkową przesłankę). Zależność ta pozwala na wprowadzenie "tymczasowych" dodatkowych założeń jako przesłanek i pozyskiwania za ich pomocą implikacji jako nowych przesłanek:

Reguła dołączania implikacji

Jeśli na podstawie "tymczasowego" dodatkowego założenia δ uzyskaliśmy formułę γ, to wolno nam dołączyć do dowodu formułę δ→γ.

A co w sytuacji, kiedy na podstawie "tymczasowego" dodatkowego założenia δ uzyskamy zarówno formułę γ, jak i ¬γ? - W takiej sytuacji mamy prawo (na mocy prawa redukcji do absurdu) dołączyć jako przesłankę formułę ¬δ.

Założeniowy dowód wprost

II. Spróbujmy udowodnić, że {(p∧q)→r} ⊢ p→(q→r).

1.  (p∧q)→r (przesłanka)

1.1. p (dodatkowe założenie)

2.1. q (dodatkowe założenie)

2.2. p∧q (DK 1.1, 2.1)

2.3. r (RO 1, 2.2)

1.2. q→r (wprowadzenie implikacji, 2.1,2.3)

2. p→(q→r) (wprowadzenie implikacji, 1.1, 1.2)

Czy dałoby się zrobić prostszy dowód? - Oczywiście, jeśli skorzystamy z twierdzenia o dedukcji. Wniosek, który mamy wyprowadzić, p→(q→r), ma postać implikacji. Możemy "urwać" poprzednik tej implikacji, przenieść do przesłanek i wyprowadzać formułę q→r. Ale ta ostatnia również ma postać implikacji, czyli również wolno nam "oderwać" poprzednik, dołączyć go do przesłanek i wyprowadzać samą formułę r. W taki sposób zamiast dowodzenia {(p∧q)→r} ⊢ p→(q→r) dowodzimy {(p∧q)→r, p, q} ⊢ r:

1. (p∧q)→r (przesłanka)

2. p (przesłanka)

3. q (przesłanka)

4. p∧q (DK 2,3)

5. r (RO 1,4)

Twierdzenie o dedukcji znacznie ułatwia dowodzenie, jeśli wniosek, który mamy wyprowadzić, ma postać implikacji.

III. Spróbujmy udowodnić, że rozumowanie "Jeśli pada, a majtek Jaś Wędrowniczek nie ma gumiaków, to przemoczy nogi. Ale Jaś nie przemoczył nóg. A padało. Zatem: Jaś miał gumiaki" jest oparte o schemat, w którym z przesłanek da się wyprowadzić wniosek. Czyli udowodnimy, że z {(α∧¬β)→γ, ¬γ, α} jest wyprowadzalny wniosek β.

1. (α∧¬β)→γ (przesłanka)

2. ¬γ (przesłanka)

3. α (przesłanka)

4. ¬γ→¬(α∧¬β) (PT, 1)

5. ¬(α∧¬β) (RO 2,4)

6. ¬α∨¬¬β (de Morgan, 5)

7. ¬¬β (OA 6,3)

8. β (O2N 7)

Założeniowy dowód nie wprost

II. Spróbujmy udowodnić, że formuła ¬((α→β)∧(α∧¬β)) jest tezą KRZ (czyli mamy wyprowadzić tę formułę bez przesłanek). Nie mamy przesłanek, a formuła nie jest implikacją (jej głównym spójnikiem jest negacja), w związku z czym nie możemy skorzystać z twierdzenia o dedukcji.... Co robić? - Próbować dowodzić nie wprost! Przy dowodzeniu nie wprost otrzymujemy (dodatkową) przesłankę - jest nią zanegowana formuła, której dowodzimy - oraz zmienia się cel dowodzenia - mamy pokazać, że z taką przesłanką jesteśmy w stanie wyprowadzić sprzeczność. Czyli:

1. ¬¬((α→β)∧(α∧¬β)) (założenie nie wprost)

2. (α→β)∧(α∧¬β) (O2N 1)

3. α→β (OK 2)

4. α∧¬β (OK 2)

5. α (OK 4)

6. β (RO 3,5)

7. ¬β (OK 4) ! Sprzeczność 6 i 7 ! 

Udowodniliśmy metodą nie wprost, że formuła ¬((α→β)∧(α∧¬β))  jest tezą KRZ.

III. Spróbujmy udowodnić, że rozumowanie "Jeśli jest sztorm, a na łajbie nie ma bosmana Jima Beama, to łajba roztrzaska się o skały. Ale nie roztrzaskała się. A sztorm był. Zatem: na łajbie był bosman Jim Beam" jest oparte o schemat (ten sam, co we wcześniejszym rozumowaniu), w którym z przesłanek da się wyprowadzić wniosek. Czyli udowodnimy, że z   {(α∧¬β)→γ, ¬γ, α} jest wyprowadzalny wniosek β metodą nie wprost.

1. (α∧¬β)→γ (przesłanka)

2. ¬γ (przesłanka)

3. α (przesłanka)

4. ¬β (z.d.n.)

5. ¬γ→¬(α∧¬β) (PT, 1)

6. ¬(α∧¬β) (RO 2,4)

7. α→β (PI 6)

8. β (RO 7,3) ! Sprzeczność ! (z 4)

Jeśli wniosek, który mamy wyprowadzić, ma postać implikacji, to twierdzenie o dedukcji w połączeniu z dowodzeniem nie wprost może stanowić niezłe KOMBO.

Tutoriale z Youtube

LogiCola - szkoła logiki online

Interaktywny kurs logiki autorstwa Harry'ego Genslera. Jest to kurs za darmo ale po angielsku. LINK Do tej części kursu - zestaw ćwiczeń F i G (inference rules). Ćwiczymy reguły jednej kreski w zestawie F, a dowody w zestawie G (E - easy level i H - hard level). 

Uwaga: w Logicoli formuły są ujmowane w zewnętrzne nawiasy, a na oznaczenie spójników są używane następujące symbole:

Informacja zwrotna