Правила естественного вывода

Формальная теория вывода ставит своей главной задачей образование из некоторой совокупности исходных тавтологий новых формул, которые также являются тавтологиями. Эта задача решается с помощью правил вывода:

1. если А - тавтология, то заменяя в ней букву Х везде, где она входит, произвольной формулой В, получаем также тавтологию (правило подстановки);
2. если А и A → B - тавтологии, то В также тавтология (правило заключения или modus ponens - MP).

Формула называется выводимой в логике высказываний, если она может быть получена из конечной совокупности исходных формул путем конечного числа шагов применения правил вывода.

Вообще говоря, не все тождественно истинные формулы могут быть выведены из произвольного множества тавтологий. В то же время, строго доказано, что можно выбрать такую конечную совокупной исходных тавтологий (аксиом логики высказываний), из которой выводимы все тождественно истинные формулы.

Это важное положение решает проблему полноты логики высказываний.

Пример