|
|
Formalni dokazi propozicionog tipa
Na osnovu izsnih tautologija mogu se dobiti razna pravila izvodjenja pomoću kojih se konstruišu formalni dokazi u obliku izvodjenja zaključka iz premisa(hipoteza). Na osnovu tautologija: (p 'i' (p=>q))=>q ;
( 'not' q 'i' (p=>q) )=> 'not' p ; 'not' p 'i' (p V q))=>q ; 'not''not' p<=>p; Dobijamo redom sledeća pravila izvodjenja:
P1: p,p=>q (Modus ponens-MP) P2: 'not' q,p=>q (Modus tolens-MT) P3: 'not' p,p V q P4: 'not''not' p i p
q 'not' q q p 'not''not' p
Ovo su primeri opšteg pravila izvodjenja zasnovanog na tautologijama,koje se može formulisati na sledeći način.
Pravilo T. p1,p2,...,pn ako je (p1 'i' p2 'i' ... 'i' pn)=>q tautologija
q
Svaka tautologija je izvodljiva iz praznog skupa premisa. Koristeći takva pravila izvodjenja, polazeći od izvesnih premisa(hipoteza) mogu se formalno izvesti (dedukovati) odredjeni zaključci.
Osim navedenih pravila P1-P4,kao posebni slučajevi pravila T mogu se formulisati i koristiti razna druga pravila.Postojanje šireg skupa dozvoljenih pravila izvodjenja doprinosi i značajnijem skraćivanju samog izvodjenja. Pravilo uslovnog dokaza CP(Conditional Proof): Ako je q izvodljivo iz p i skupa premisa F,tada je p=>q izvodljivo samo iz F tj. Ako F,p|-q, onda F|- p=>q . Metoda dokazivanja opovrgavanjem može se formalizovati pomoću pravila indirektnog dokaza(IP): Ako je bilo koja kontradikcija q 'i' 'not' q( q proizvoljna iskazna formula) izvodljiva iz 'not' p i skupa premisa F, tada je p izvodljiva samo iz F tj. 'not' p,F|-q 'i' 'not' q,onda F|-p. Pravila T, CP i IP imaju centralno mesto u formalizaciji propozicione logike.