Логический вывод

Терпеть не могу логики. Она всегда банальна и нередко убедительна.

Оскар Уайльд

Формальная математика основывается на аксиоматическом методе. Вначале вводятся неопределяемые понятия и аксиомы, далее, на основании логических правил и заключений появляются теоремы. Проблема доказательства в математической логике состоит в установлении истинности формулы B (заключения), если предполагается истинность формул A₁,...,A_n (посылок). Мы записываем это в виде

A₁,A₂,...,A_n |= B

и говорим, что B является логическим следствием A₁,A₂,...,A_n.

Основной метод решения этой проблемы следующий. Записываем посылки и применяем правила вывода, чтобы получить из них другие истинные формулы. Из этих формул и исходных посылок выводим последующие формулы и продолжаем этот процесс до тех пор, пока не будет получено нужное заключение. Мы называем это логическим выводом или доказательством; именно такой метод обычно применяется в математических доказательствах.

Два классических правила вывода были открыты очень давно. Одно из них носит латинское название modus ponens (модус поненс или сокращение посылки). Его можно записать следующим образом:

A, A É B |= B.

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

A É B, B É C |= A É C.

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