В основе МР лежит идея доказательства от противного.
Теорема. Если , где F противоречие, то Г |- S.
Доказательство (для теории £).
1. По теореме дедукции, если Г – множество формул, А и B Î Г и A|-£B, то Г|-А→В.
2. , следовательно .
3. Следствие из теоремы дедукции: А |- B, то |- A ® B.
4. Из 2 и 3 получаем . Т.к. F – противоречие, т. е. F=0, то
5. По теореме дедукции Г®S, следовательно, Г|-S.
Пустая формула не является истинной или ложной ни в какой интерпретации и, по определению, является противоречием. В качестве формулы F при доказательстве от противного по МР принято использовать пустую формулу ().
МР работает с особой стандартной формой формул, которая называется предложением или дизъюнктом.
Дизъюнкт — безкванторная ДНФ.