Необходимо также подчеркнуть принятое в математической Л. неисключающее понимание дизъюнкции. Дизъюнкция (Р
Q), по определению, истинна и в том случае, когда истинны оба суждения Р и Q.
Формула В) можно утверждать тогда и только тогда, когда можно утверждать хотя бы одно из высказываний А и В. Отрицание ùА высказывания А можно утверждать тогда и только тогда, когда у нас есть построение, приводящее к противоречию предположение о том, что построение, требуемое высказыванием А, выполнено. (При этом «приведение к противоречию» считается первоначальным понятием.) Импликацию (АÉВ) можно утверждать тогда и только тогда, когда мы располагаем таким построением, которое, будучи объединено с любым построением, требуемым высказыванием А, даёт построение, требуемое высказыванием В.
Формула называется интуиционистски общезначимой тогда и только тогда, когда можно утверждать всякое высказывание, получаемое из в результате подстановки любых математических суждений вместо логических переменных; точнее говоря, в том случае, когда имеется общий метод, позволяющий при произвольной такой подстановке получать построение, требуемое результатом подстановки. При этом понятие общего метода интуиционисты также считают первоначальным.
Формулы 1—10 являются интуиционистски общезначимыми, тогда как формула 11, выражающая классический закон исключенного третьего, не является таковой.
В известном отношении близкой к интуиционизму является точка зрения конструктивной математики, уточняющая несколько расплывчатые интуиционистские понятия импликации и общего метода на основе точного понятия алгоритма. С этой точки зрения закон исключенного третьего также отвергается. Л. конструктивной математики находится в стадии разработки.
С методом формализации доказательств связано понятие формальной системы. Формальная система включает следующие элементы.
1. Формализованный язык с точным синтаксисом, состоящий из точных и формальных правил построения осмысленных выражений, называется формулами данного языка.
2. Чёткую семантику этого языка, состоящую из соглашений, определяющих понимание формул и тем самым условия их истинности.
3. Исчисление (см. выше), состоящее из формализованных аксиом и формальных правил вывода. При наличии семантики эти правила должны быть согласованы с ней, т. е. при применении к верным формулам давать верные формулы.
Исчисление определяет выводы (см. выше) и выводимые формулы — заключительные формулы выводов. Для выводов имеется распознающий алгоритм — единый общий метод, с помощью которого для любой цепочки знаков, применяемых в исчислении, можно узнавать, является ли она выводом. Для выводимых формул распознающий алгоритм может быть и невозможен (примером является исчисление предикатов, см. Логика предикатов).
Об исчислении говорят, что оно непротиворечиво, если в нём не выводима никакая формула вместе с формулой ù. Задача установления непротиворечивости применяемых в математике исчислений является одной из главных задач математической Л. Имея в виду охват той или иной содержательно определённой области математики, исчисление считают полным относительно этой области, если в нём выводима всякая формула, выражающая верное утверждение из этой области. Другое понятие полноты исчисления связано с требованием иметь для всякого утверждения, формулируемого в данном исчислении, либо его доказательство, либо его опровержение. Первостепенное значение в связи с этими понятиями имеет теорема Гёделя, утверждающая несовместимость требований полноты с требованием непротиворечивости для весьма широкого класса исчислений. Согласно теореме Гёделя, никакое непротиворечивое исчисление из этого класса не может быть полным относительно арифметики: для всякого такого исчисления может быть построено верное арифметическое утверждение, формализуемое, но не выводимое в исчислении. Эта теорема, не снижая значения математической Л. как мощного организующего средства в науке, убивает надежды на эту дисциплину как на нечто способное осуществить охват математики в рамках одной формальной системы. Надежды такого рода высказывались многими учёными, в том числе основоположником математического формализма Гильбертом.
В 70-е гг. 20 в. получила развитие идея полуформальной системы. Полуформальная система — это также система некоторых правил вывода. Однако некоторые из этих правил могут иметь существенно иной характер, чем правила вывода формальной системы. Они, например, могут допускать выведение новой формулы после того, как с помощью интуиции создалось убеждение в выводимости любой формулы такого-то вида. Сочетание этой идеи с идеей ступенчатого построения математической Л. лежит в основе одного из современных построений логики конструктивной математики. В приложениях математической Л. часто применяются исчисления предикатов — классическое и интуиционистское.
Математическая Л. органически связана с кибернетикой, в частности с математической теорией управляющих систем и математической лингвистикой. Приложения математической Л. к релейно-контактным схемам основаны на том, что всякая двухполюсная релейно-контактная схема в следующем смысле моделирует некоторую формулу классического исчисления высказываний. Если схема управляется n реле, то столько же различных пропозициональных переменных содержит , и если обозначить через i суждение «Реле номер i сработало», то цепь будет тогда и только тогда замкнута, когда будет верен результат подстановки суждений i вместо соответствующих логических переменных в . Построение такой моделируемой формулы, описывающей «условия работы» схемы, оказывается особенно простым для т. н. П-схем, получаемых из элементарных одноконтактных цепей путём параллельных и последовательных соединений. Это связано с тем, что параллельные и последовательные соединения цепей моделируют соответственно дизъюнкцию и конъюнкцию суждений. Действительно, цепь, полученная путём параллельного (последовательного) соединения цепей Ц1 и Ц2, тогда и только тогда замкнута, когда замкнута цепь Ц1 или (и) замкнута цепь Ц2. Применение исчисления высказываний к релейно-контактным схемам открыло плодотворный подход к важным проблемам современной техники. Это же применение обусловило постановку и частичное решение многих новых и трудных проблем математической Л., к числу которых в первую очередь относится т. н. проблема минимизации, состоящая в разыскании эффективных методов нахождения простейшей формулы, равносильной данной формуле.
Релейно-контактные схемы являются частным случаем управляющих схем, применяемых в современных автоматах. Управляющие схемы иных типов, в частности схемы из электронных ламп или полупроводниковых элементов, имеющие ещё большее практическое значение, также могут быть разрабатываемы с помощью математической Л., которая доставляет адекватные средства как для анализа, так и для синтеза таких схем. Язык математической Л. оказался также применимым в теории программирования, создаваемой в связи с развитием машинной математики. Наконец, созданный математической Л. аппарат исчислений оказался применимым в математической лингвистике, изучающей язык математическими методами.