Wstęp
8 stycznia 2011Aksjomatyczne ujęcie rachunku zdań polegało na tym, że obracaliśmy się tylko i wyłącznie w obszarze tautologii. W wielu sytuacjach, zdarzeniach, procesach rzeczywistych na strukturę logiczną tych procesów składają się elementy logiczne, które tautologiami nie są. Powstaje pytanie, jak w takich przypadkach wykazywać, że jednak proces jako całość tworzy twierdzenie logiki, czyli tautologię. Można ogólnie powiedzieć, że w rozumowaniach potocznych posługujemy się elementami logicznymi, które osobno wzięte nie muszą tworzyć twierdzeń logiki. Tworzone dla takiego rozumowania systemy nazywają się systemami dedukcji naturalnej. W systemach tych formułuje się dokładnie reguły, według których – w sposób intuicyjny – przeprowadzamy nasze dowody. Ponadto dowody w systemach założeniowych są na ogół łatwiejsze od dowodów w aksjomatycznych systemach logicznych.
Reguły systemu założeniowego określają, jak zbudowane są dowody założeniowe. Wśród reguł tworzących dowody założeniowe można wyróżnić dwa rodzaje reguł:
1. reguły dołączania nowych wierszy do dowodu,
2. reguły tworzenia dowodów.
Reguły typu 1. stwierdzają, że z wyrażeń o określonej postaci wynikają logicznie wyrażenia o określonej postaci, które można do dowodu dołączyć na podstawie wierszy dotychczasowych. Istnieje niewielka ilość takich reguł, które przyjmuje się bez dowodu, jako reguły pierwotne (zapisane w postaci schematów).