Большая Советская Энциклопедия (ЛО)

  Формулировки теорем и аксиом развиваемой теории полностью записываются в виде формул, для чего употребляется особая символика, пользующаяся, наряду с обычными математическими знаками, знаками для логических связок, применяемых в математике: «... и...», «... или...», «если..., то...», «неверно, что...», «при всяком...», «существует... такой, что...». Всем логическим средствам, с помощью которых теоремы выводятся из аксиом, ставятся в соответствие правила вывода новых формул из уже выведенных. Эти правила формальны, т. е. таковы, что для проверки правильности их применений нет надобности вникать в смысл формул, к которым они применяются, и формулы, получаемой в результате; надо лишь убедиться, что эти формулы построены из таких-то знаков, так-то расположенных. Доказательство теоремы отображается в выводе выражающей её формулы. Вывод же этот рассматривается как ряд формул, в конце которого стоит формула, подлежащая выводу. В выводе всякая формула либо выражает аксиому, либо получается из одной или нескольких предыдущих формул по одному из правил вывода. Формула считается выводимой, если может быть построен её вывод.

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

  Идея метода формализации доказательств принадлежит Д. Гильберту. Проведение этой идеи стало, однако, возможным благодаря предшествовавшей разработке математической Л. (см. раздел История логики).

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

  Простейшими из логических исчислений являются исчисления высказываний: классическое и интуиционистское. В них употребляются следующие знаки: 1) т. н. логические переменные — буквы А, В, С,..., означающие произвольные «высказывания» (смысл этого термина объясняется ниже); 2) знаки логических связок &, , 'E, `u, означающие соответственно «... и...», «... или...», «если..., то...», «неверно, что...»; 3) скобки, выявляющие строение формул. Формулами в этих исчислениях считаются логические переменные и всякие выражения, получаемые из них путём повторного применения следующих операций: 1) присоединение к ранее построенному выражению знака `u слева, 2) написание двух ранее построенных выражений рядом друг за другом со включением одного из знаков &,  или 'E между ними и с заключением всего в скобки. Например, следующие выражения являются формулами:

  1. (А'E(В'EА)),

  2. ((А'E(В'EС)) 'E((А'EВ) 'E(А'EС))),

  3. ((A&B) 'EA),

  4. ((А&. В) 'EВ),

  5. (A'E(B'E(A&B))),

  6. ((А'EС) 'E((В'EС) 'E((АВ) 'EС))),

  7. (А'E(АВ)),

  8. (B'E(AB)),

  9. (`uА'E(А'EВ)),

  10. ((A'EB) 'E((A'E`uB) 'E`uA)),

  11. (A`uA).

  В обоих исчислениях высказываний — классическом и интуиционистском — употребляются одни и те же правила вывода.

  Правило подстановки. Из формулы выводится новая формула путём подстановки всюду вместо какой-либо логической переменной произвольной формулы.

  Правило вывода заключений. Из формул  и () выводится формула Q), называется дизъюнкцией суждений Р и Q, есть суждение истинное, когда истинно хотя бы одно из этих суждений, и ложное, когда ложны оба. Суждение вида (Р 'E Q), называется импликацией суждений Р и Q, есть суждение ложное, когда истинно Р и ложно Q, и истинное во всех остальных случаях. Суждение вида `u Р, называется отрицанием суждения Р, есть суждение истинное, когда Р ложно, и ложное, когда Р истинно.

  Необходимо отметить, что, согласно данному выше определению, импликация не вполне совпадает по смыслу с житейским словоупотреблением связки «если..., то...». Однако в математике эта связка обычно применялась именно в смысле этого определения импликации. Доказывая теорему вида «если Р, то Q», где Р и Q суть некоторые математические суждения, математик делает предположение об истинности Р и тогда доказывает истинность Q. Он продолжает считать теорему верной, если впоследствии будет доказана ложность Р или истинность Q будет доказана и без предположения об истинности Р. Опровергнутой он считает эту теорему лишь тогда, когда установлена истинность Р и вместе с тем ложность Q. Всё это вполне согласуется с определением импликации (Р 'E Q).

  Необходимо также подчеркнуть принятое в математической Л. неисключающее понимание дизъюнкции. Дизъюнкция (РQ), по определению, истинна и в том случае, когда истинны оба суждения Р и Q.