74606 Scan0018 (2)

26 Tautologie. Wynikanie logiczne. Systemy dowodzenia

Definicja 2.5 Wyprowadzeniem (dowodem) formalnym w systemie dowodzenia nazywamy ciąg formuł takich, ze każda formuła tego ciągu jest aksjomatem lub może być wyprowadzona z poprzednich formuł ciągu przy użyciu pewnej reguły dowodzenia. Jeśli ostatnim elementem ciągu jest formuła A, to formułę A nazywamy twierdzeniem lub mówimy, że A jest wyprowadzalne, co zapisujemy b A.

2.4.2 Metoda aksjornatyczna a zero-jedynkowa

Aksjomaty i reguły dowodzenia powinny być tak dobrane, aby system spełniał dwa warunki:

•    poprawność — każda wyprowadzałna formuła musi być tautologią¹:

jeśli b A, to A,

•    pełność — można wyprowadzić wszystkie tautologie logiki zdaniowej:

jeśli j= A, to b A.

System, który spełnia obydwa warunki spełnia tzw. twierdzenie o poprawności i pełności, które mówi o równoważności metody aksjomaty-cznej i zero-jedynkowej:

(= A wtw, gdy b A.

Istnieje wiele systemów dowodzenia, różniących się między sobą doborem aksjomatów oraz reguł dowodzenia. Do najbardziej znanych należą systemy Hilberta, Gentzena i metoda rezolucji.

2.4.3 System Hilberta

Definicja 2.6 (System Hilberta) Dla dowolnych formuł A, B iC mamy:

•    aksjomat A\: A =>- (B => A),

• aksjomat A2: (A =$■ (B => C)) =>■ ((A => B) => (A    C)),

•    aksjomat A3; (~ B => ~ A) => {A =>• B),

1

Zapis |= A oznacza, że formuła A jest tautologią.