Wstęp

Aksjomatyczne 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).