4.2. Доказательствоот противного

В основе МР лежит идея доказательства от противного.

Теорема. Если , где F противоречие, то Г |- S.

Доказательство (для теории £).

1. По теореме дедукции, если Г – множество формул, А и B Î Г и A|-_£B, то Г|-А→В.

2. , следовательно .

3. Следствие из теоремы дедукции: А |- B, то |- A ® B.

4. Из 2 и 3 получаем . Т.к. F – противоречие, т. е. F=0, то

5. По теореме дедукции Г®S, следовательно, Г|-S.

Пустая формула не является истинной или ложной ни в какой интерпретации и, по определению, является противоречием. В качестве формулы F при доказательстве от противного по МР принято использовать пустую формулу ( ).

МР работает с особой стандартной формой формул, которая называется предложением или дизъюнктом.

Дизъюнкт - безкванторная ДНФ.