Терпеть не могу логики. Она всегда банальна и нередко убедительна.
Оскар Уайльд
Формальная математика основывается на аксиоматическом методе. Вначале вводятся неопределяемые понятия и аксиомы, далее, на основании логических правил и заключений появляются теоремы. Проблема доказательства в математической логике состоит в установлении истинности формулы B (заключения), если предполагается истинность формул A1,...,An (посылок). Мы записываем это в виде
A1,A2,...,An |= B
и говорим, что B является логическим следствием A1,A2,...,An.
Основной метод решения этой проблемы следующий. Записываем посылки и применяем правила вывода, чтобы получить из них другие истинные формулы. Из этих формул и исходных посылок выводим последующие формулы и продолжаем этот процесс до тех пор, пока не будет получено нужное заключение. Мы называем это логическим выводом или доказательством; именно такой метод обычно применяется в математических доказательствах.
Два классических правила вывода были открыты очень давно. Одно из них носит латинское название modus ponens (модус поненс или сокращение посылки). Его можно записать следующим образом:
A, A É B |= B.
Второе правило (цепное) позволяет вывести новую импликацию из двух данных импликаций. Можно записать его следующим образом:
A É B, B É C |= A É C.
Во всей своей полноте понятие доказательства несомненно обладает и психологическими признаками. Надо обладать красноречием и умением убеждать, чтобы слушатели (или читатели) приняли ваше доказательство. Рассмотрим основные логические особенности доказательства и выделим некоторые из методов доказательства.
Доказательство с помощью математической индукции
Мы рассмотрели этот способ в разделе 2.4. Подчеркнем, что принцип математической индукции является одним из способов логического вывода и в математике принимается без доказательства.
Доказательство с введением допущения
Многие математические утверждения могут быть представлены в виде импликаций PÉQ. Доказательство такого утверждения может быть представлено в виде
A1,A2,...,An |= PÉQ.
Формулы A1,A2,...,An - суть посылки, истинность которых предполагается. Поэтому в данном случае доказательство логически эквивалентно доказательству того, что формула
(A1& A2&...&An)É(PÉQ)
является тавтологией. Последняя формула равносильна формуле
(A1& A2&...&An&P)ÉQ.
Доказательство истинности этой формулы мы можем записать в виде
A1& A2&...&An&P |=Q.
Таким образом, для непосредственного доказательства теоремы вида PÉQ, мы предполагаем истинность аксиом и ранее доказанных теорем и допускаем истинность высказывания P и далее показываем, что из всего этого с неизбежностью вытекает истинность Q.
Этот метод часто применяется в геометрии. Например, при доказательстве равенства боковых сторон треугольника, у которого углы при основании равны, допускается, что эти углы равны, а затем это используется в доказательстве равенства сторон.
Косвенные методы доказательства
Рассмотрим условное высказывание вида AÉB, где A - конъюнкция посылок, B - заключение. Иногда удобнее вместо доказательства истинности этого условного высказывания установить логическую истинность некоторого другого высказывания, равносильного исходному. Такие формы доказательства называются косвенными методами доказательства.
Еще одной формой косвенного метода доказательства, является доказательство по закону контрапозиции, основанное на равносильности
AÉB º ØBÉØA,
когда вместо истинности AÉB мы доказываем истинность ØBÉØA.
Преимущества этого метода доказательства проявляются при автоматизированном способе доказательства, т. е. когда доказательство совершают компьютер с помощью специальных программных систем доказательства теорем.
При построении выводов не всегда целесообразно ждать появления искомого заключения, просто применяя правила вывода. Именно такое часто случается, когда мы делаем допущение A для доказательства импликации AÉB. Мы применяем цепное правило и модус поненс к A и другим посылкам, чтобы в конце получить B. Однако можно пойти по неправильному пути, и тогда будет доказано много предложений, большинство из которых не имеет отношения к нашей цели. Этот метод носит название прямой волны и имеет тенденцию порождать лавину промежуточных результатов, если его запрограммировать для компьютера и не ограничить глубину.
Другая возможность - использовать контрапозицию и попытаться, например, доказать ØB É ØA вместо AÉB. Тогда мы допустим ØB и попробуем доказать ØA. Иными словами, допускается, что заключение B (правая часть исходной импликации) неверно, и делается попытка опровергнуть посылку A. Это позволяет двигаться как бы назад от конца к началу, применяя правила так, что старое заключение играет роль посылки. Такая организация поиска может лучше показать, какие результаты имеют отношение к делу. Она называется поиском от цели.
Доказательство приведением к противоречию
Частным случаем косвенных методов доказательства является приведение к противоречию (от противного). В этом методе используются следующие равносильности:
AÉB º Ø(AÉB) É (C&ØC) º (A&ØB)É(C&ØC),
AÉB º (A&ØB)ÉØA,
AÉB º (A&ØB)ÉB.
Используя вторую из приведенных равносильностей для доказательства AÉB мы допускаем одновременно A и ØB, т.е. предполагаем, что заключение ложно:
Ø(AÉB) º Ø(ØAÚB) º A & ØB.
Теперь мы можем двигаться и вперед от A, и назад от ØB. Если B выводимо из A, то, допустив A, мы доказали бы B. Поэтому, допустив ØB, мы получим противоречие. Если же мы выведем ØA из ØB, то тем самым получим противоречие с A. В общем случае мы можем действовать с обоих концов, выводя некоторое предложение C, двигаясь вперед, и его отрицание ØC, двигаясь назад. В случае удачи это доказывает, что наши посылки несовместимы или противоречивы. Отсюда мы выводим, что дополнительная посылка A&ØB должна быть ложна, а значит противоположное ей утверждение AÉB истинно. Метод приведения к противоречию часто используется в математике. Например, в геометрии мы можем допустить, что углы при основании некоторого треугольника равны, а противолежащие стороны не равны, и попробовать показать, что при этом и углы должны быть не равны, или получить еще какое-то противоречие.
Доказательство контрпримером
Многие математические гипотезы имеют в своей основе форму: "Все объекты со свойством A обладают свойством B". Мы можем записать это в виде формулы
"x (A(x)ÉB(x)),
где A(x) обозначает предикат "x обладает свойством A", B(x) - " x обладает свойством B". Если число возможных значений х является конечным, то в принципе доказательство может быть проведено с помощью разбора случаев, то есть непосредственной проверкой выполнимости гипотезы для каждого объекта. В случае, если число объектов не является конечным, то такой возможности не существует даже в принципе. Однако для доказательства ложности гипотезы достаточно привести хотя бы один пример (контрпример), для которого гипотеза не выполнима.
Нет ничего практичней хорошей теории.
Роберт Кирхгоф