Встречающиеся здесь И и ИЛИ не являются прямыми аналогами связок исчисления высказываний.

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

Читатели могут сами убедиться в том, что при всех комбинациях истинности и ложности формул α, β и γ четыре выписанные аксиомы всегда являются истинными. Такие аксиомы принято называть абсолютными или логическими.

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

Первое правило носит название правило подстановки. Согласно ему в формулу, которая уже выведена, можно вместо некоторого высказывания подставить любое другое при непременном условии, что эта подстановка сделана во всех местах вхождения заменяемого высказывания в данную формулу. Такая подстановка сохраняет свойство формулы быть тождественно истинной. Если в аксиому (α

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

Второе правило называется модус поненс (лат. modus ponens) или правило заключения и выглядит следующим образом: если α и (α

β) являются истинными формулами, то формула β также истинна. Если α является истинной, то истинность (αβ) означает, что β является истинной. Поэтому правило заключения не портит истинности выводимых формул.

Мы полностью описали исчисление высказываний. Заметим еще раз, что оно устроено так, что в результате выводов из аксиом получаются лишь тождественно истинные формулы. Можно показать, что система логических аксиом может быть выбрана таким образом, что для любой тождественно истинной формулы всегда найдется цепочка выводов (логических рассуждений), с помощью которой она будет выведена из системы аксиом путем применения правил подстановки и заключения. Другими словами, может быть построена полная система аксиом, из которой будут выводиться все тождественно истинные формулы и только они. Как показали исследования логиков, таких полных систем аксиом существует много. Система из четырех аксиом, которую мы только что рассмотрели является полной. Ее предложил известный немецкий математик и логик Д. Гильберт.

Подобное свойство исчисления высказываний позволяет достаточно легко ответить на кардинальный вопрос, возникающий для любой формальной системы: принадлежит ли некоторая правильная формула к множеству формул, выводимых в данной формальной системе? Для ответа на этот вопрос надо построить таблицу, в которой в левой части перечислены все возможные комбинации значений истины и лжи для высказываний, входящих в эту формулу (легко видеть, что при n различных таких высказываниях число комбинаций будет равно 2ⁿ), а в правой части выписаны значения истинности проверяемой формулы. Если правый столбец состоит только из значений «истина», то формула выводима в исчислении высказываний. В противном случае ее выводимость не имеет места.

Пусть, например, надо узнать, выводима ли в исчислении высказываний формула ((

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

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

Проиллюстрируем эту процедуру еще на одном примере. Проверим, является ли выводимой формула ((α

β)((αγ)&β)). В этой формуле (будем обозначать ее ƒ) имеется три высказывания, что приводит к необходимости рассмотрения истинного значения ƒ на 2³=8 комбинациях. Эти комбинации и соответствующие шаги по определению истинностного значения ƒ на них даны в табл. 3, в которой И и Л означают соответственно значения «истина» и «ложь».

Таблица 3

Появление в пятой строке в столбце ƒ значения Л свидетельствует о невыводимости исследуемой формулы. На этом шаге процесс вывода можно прекратить. Остальные строки в таблице приведены лишь для полноты картины.

«Логик-теоретик»

Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ƒ₁ и ƒ₂ равны между собой, и записывать этот факт обычным образом ƒ₁=ƒ₂, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ƒ₁ и ƒ₂ одинакова.