Моделирование рассуждений. Опыт анализа мыслительных актов | страница 45

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

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

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

Таблица 3

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

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