1105140232

ROZDZIALI. RACHUNEK ZDAŃ

Zdania p\,..., p_n nazywają się założeniami twierdzenia, a ty jego tezą. W rozdziale tym omówimy kilka często spotykanych schematów rozumowań matematycznych. Z innymi schematami rozumowań spotkamy się w dalszych rozdziałach. Z formalnym pojęciem dowodu omówimy w dalszych rozdziałach tej książki.

Definicja 1.8 Mówimy, że zdanie ty wynika ze zdań pi, ..., p_n, co zapisujemy jako

{^l,...,V5„} |=V>,

jeśli dla dowolnej waluacji 7r takiej, że Tt(pi) = 1, ..., 7r{p_n) = 1 mamy również it(ty) = 1.

Prawdziwe wyrażenia postaci {p\,..., p_n] |= ty nazywamy regułami wnioskowania. Twierdzenie 1.3 Następujące dwa zdania są równoważne

1. \=i/>

2. |= {pi A ... A p_n) —> ty

Dowód. (1) —> (2). Załóżmy, że {p\,... ,p_n} f= ty- Musimy pokazać, że zdanie (pi A ... A p_n) —» ty jest tautologią. Niech ir będzie dowolną waluacją. Z definicji operatora =>■ wynika, że jest n(a —> /5) = 0 tylko w przypadku 7r(o:) = 1 oraz 7r(_y6) = 0. Lecz jeśli it(pi A ... A p_n), to założenia (1) wynika, że n(ty) = t.

(2) —> (1). Załóżmy, że |= (pi A ... A p_n) —> ty- Niech n będzie taką waluacją, że Tt(pi) = 1,..., 7r(p_n) = 1. Wtedy n(pi A ... A p_n) = 1. Ponownie, korzystając z założenia i definicji operatora =>, otrzymujemy 7r(ty) = 1. □

Oto kilka najważniejszych reguł wnioskowania:

Twierdzenie 1.4

M h V,

2- {p, -p} |= 9.

3- {p,«} h P A q,

4. {p A q] \= p,

5. {p,p —> q} \= q (modus ponens),

6. {p V q, ->p V q} \= q (rezolucja).

Interpretacja reguły {p, ->p} |= q jest następująca: ze sprzecznej rodziny zdań wyprowadzić możemy dowolne inne zdanie. Interpretacja reguły „modus ponens”, zwanej również regułą odrywania, jest następująca: jeśli potrafię pokazać p oraz potrafię pokazać, żep q, to potrafię również pokazać zdanie q. Równoważną postacią reguły rezolucji jest reguła {p —> q,~'P -> <?} |= q-

Uwaga. Większość wykładów z logiki matematycznej stosuje regułę Modus Ponens jako podstawową regułę wnioskowania. Reguła rezolucji jest często stosowana w systemach automatycznego dowodzenia twierdzeń.

Metoda rezolucji dowodzenia twierdzeń bazuje na regule rezolucji oraz na następującej charakteryzacji relacji wynikania: