Scan0017 (2)

2.4 Systemy dowodzenia 25

gdzie formuły nad kreską nazywamy przesłankami, a formułę pod kreską — wnioskiem lub konkluzją.

Przykład 2.6 Najczęściej stosowanej regułą dowodzenia, jest reguła odrywania:

P,P=^ Q Q

Reguła ta mówi, że jeżeli prawdziwa implikacja ma prawdziwy poprzednik, to również prawdziwy jest jej następnik.

2.3.2 Badanie poprawności wnioskowania

Do sprawdzenia, czy dane wnioskowanie jest poprawne (czy reguła wnioskowania jest poprawna) można wykorzystać metodę zero-jedynkową (patrz przykład 2.5) lub następujące twierdzenie.

Twierdzenie 2.4 Zbiór {A\,..., A_n] implikuje logicznie B wtw, gdy formula

(Ai A ... A A_n) => B

jest tautologią.

2.4 Systemy dowodzenia

Istnieją dwie metody udowodnienia, że dane zdanie jest prawdziwe:

•    metoda zero-jedynkowa opierająca się na pojęciu konsekwencji logicznej,

•    metoda aksjomatyczna wykorzystująca pojęcie dowodu formalnego.

Metodę zero-jedynkowa można nazwać metodą znaczeniową (semantyczną), gdyż dowód wykorzystuje znaczenie funktorów zdaniotwórczych. Metoda aksjomatyczna jest metodą składniową (syntaktyczną), gdyż dowód przeprowadza się analizując składnię (kształt) aksjomatów i reguł dowodzenia.

2.4.1 Dowody formalne

W metodzie aksjornatycznej dokonuje się wyboru zbioru formuł prawdziwych zwanych aksjomatami oraz zbioru reguł dowodzenia (wnioskowania), które służą do wyprowadzania nowych formuł, które także są prawdziwe. Aksjomaty i reguły dowodzenia tworzą system dowodzenia.