Dedukcja naturalna
Jest to zestaw reguł służący do dowodzenia twierdzeń w rachunku zdań oraz rachunku predykatów pierwszego rzędu. Reguły naturalnej dedukcji dla rachunku zdań zostały przedstawione na wykładzie 1, ich zestaw znajduje się tutaj. Laboratoria w tej części poświęcone będą prowadzeniu dowodów za pomocą reguł naturalnej dedukcji ze wspomaganiem systemu JAPE.
Edytor dowodów JAPE
Został napisany przez Bernarda Sufrina i Richarda Bornata z Uniwersytetu w Oksfordzie. Pozwala nie tylko prowadzić wnioskowania metodą dedukcji naturalnej dla rachunku zdań i rachunku predykatów, ale oferuje również wspomaganie dowodzenia w innych logikach, a także pozwala definiować własne systemy dedukcyjne (wymaga to oczywiście dodatkowej wiedzy :). W przypadku metody dedukcji naturalnej w wariancie intuicjonistycznym JAPE wspomaga również proces znajdywania kontrprzykładów metodą „wymuszania” (forsingu).
Instalacja JAPE-a pod Windows
Aby zainstalować JAPE-a pod Windows należy zacząć od pobrania pakietu instalacyjnego. Po jego uruchomieniu należy wybrać docelowy katalog instalacji. Ścieżka do niego powinna być w miarę krótka (załóżmy, że będzie to „x:\katalog\Jape”, dłuższe ścieżki mogą spowodować problem z definicją skrótu). Po wybraniu katalogu docelowego, zaznaczamy jeszcze opcję „Shortcut on Desktop” i naciskamy guzik Install, a potem Exit...
Po zakończeniu instalacji, pobieramy i zapisujemy do katalogu „x:\katalog\Jape\examples\natural_deduction” następujące pliki:
W przypadku drugiego pliku zastępujemy istniejącą już w katalogu docelowym inną jego wersję. Na zakończenie musimy jeszcze zmodyfikować właściwości skrótu służącego do uruchamiania JAPE-a. W tym celu do wartości pola „Element docelowy” dodajemy odstęp, a po nim „x:\katalog\Jape\examples\natural_deduction\I2L.jt”. Naciskamy Zastosuj i OK. JAPE jest już poprawnie zainstalowany pod Windows.
Praca z JAPE
Po wczytaniu pliku z sekwentami do udowodnienia pojawia się jeden lub więcej paneli z zadaniami. Nas będzie interesować opcja "prove" dla każdego wskazanego sekwentu. Po wybraniu tej opcji pojawia się okienko z przesłankami na górze (o ile są obecne) z wnioskiem na dole i wielokropkiem w środku. Należy doprowadzić do usunięcia wielokropka poprzez stosowanie reguł naturalnej dedukcji. Jest kilka możliwości
- można wybrać zdanie do udowodnienia i zastosować regułę wstecz, wówczas pojawia się jedno lub więcej innych zdań, które należy udowodnić
- można wskazać przesłankę lub założenie i zastosować regułę wprzód, wówczas
pojawi się inne zdanie wynikające z zastosowania reguły. Niektóre reguły wymagają
by zaznaczyć nie tylko przesłanki reguły, ale również zdanie, do którego zmierzamy.
Tak jest np. w regule eliminacji dyzjunkcji. Również w regule eliminacji implikacji
można zaznaczyć i implikację i cel, pojawiają się wówczas dwa nowe zdania.
(uwaga, w przypadku, gdy dowód komplikuje się i pojawiają się zdania pośrodku okienka, a część nieudowodniona jest po obu stronach, wówczas może być niejasne, w którą stronę zmierza zastosowanie reguły. Należy bacznie obserwować sposób zaznaczenia zdania.)
Dowody poszczególnych sekwentów można zachować na bieżąco w momencie zamykania okienka z dowodem. Można zapisać bieżący stan pracy (ale nie dowód pojedynczego sekwenty, jedynie wszystkich już udowodnionych). Można też wygenerować plik postscriptowy dla pojedynczego dowodu i wydrukować taki dowód.
Uwaga 2. JAPE nie oferuje jako „podstawowej” reguły eliminacji podwójnej negacji ¬¬e. Zamiast niej daje nam do dyspozycji regułę klasycznego dowodu nie wprost, w jego nomenklaturze: contra (classical)
| ¬φ | |
| ⋮ | |
| ⊥ | |
| –––– | (nie wprost) |
| φ |
Reguła ¬¬e jest konsekwencją zastosowania reguły contra (classical) oraz reguły eliminacji negacji ¬e. Z drugiej strony, reguła dowodu nie wprost wynika z ¬¬e i pozostałych reguł rachunku zdań. Jeszcze jedną różnicą w stosunku do zestawu reguł wprowadzonego na wykładzie jest fakt, że regułę eliminacji sprzeczności ⊥e JAPE nazywa regułą „konstruktywnego dowodu nie wprost” – contra (constructive).