Главная > Интеллектуальные системы > Системы искусственного интеллекта
<< Предыдущий параграф
Следующий параграф >>
<< Предыдущий параграф Следующий параграф >>
Макеты страниц

3.4.2. Разрешимость исчисления высказываний

Э. Пост доказал в 1921 г. следующую теорему:

Формула доказуема в исчислении высказываний, если и только если она является тождественно-истинной, т. е. истинной при всех интерпретациях исчисления высказываний.

Таким образом, исчисление высказываний характеризуется:

• непротиворечивостью, т. е. не могут быть одновременно выводимы;

• полнотой, т. е. теоремы точно соответствуют тождественно-истинным формулам;

• разрешимостью, т. е. существует процедура решения.

Действительно, теоремы исчисления высказываний являются тавтологиями, т. е. высказывания принимают значения истинности, равные ИСТИНЕ, всякий раз, когда значения истинности ИСТИНА (0) или ЛОЖЬ (1) принимает все пропозициональные переменные, входящие в них.

Таблицы истинности элементарных операторов определяются в соответствии с интуитивной интерпретацией. Ниже приведены таблицы истинности для операторов П и

В определенной таким образом интерпретации исчисления высказываний выражение имеет значение “ложь” только тогда, когда истинно, ложно. Это выражение эквивалентно выражению Обычная интерпретация символа как импликации достаточно неудачна, поскольку выражения являются истинными, лишь если ложно (как говорится, из ложного можно вывести все, что угодно), а в обычной речи с этим связывается вывод о чем-то плохом, из-за чего возникают недоразумения.

Хорошо известный метод таблиц истинности был строго обоснован в 1932 г. Постом: для того чтобы формула исчисления высказываний была теоремой, необходимо и достаточно, чтобы при интерпретации она принимала значение 0 (истина), каковы бы ни были значения пропозициональных переменных, входящих в нее.

В табл. 3.1 приведен пример доказательства на основе использования таблиц истинности.

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

Фундаментальный вывод, состоящий в том, что исчисление высказываний является разрешимой формальной системой, представляет собой теорему уже уровня метасистемы, которую

Таблица 3.1.

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

Этот результат Поста представляет особый интерес, так как он выявляет адекватность исчисления высказываний классическим логическим рассуждениям, а также понятиям обычного языка. Он утверждает, что мышление и его выражение с помощью языка формализуемы (по крайней мере частично) и представимы в краткой форме с помощью чисто символьных схем и представлений. Именно в этом ожидались наибольшие трудности в программе формализации математики, предложенной Гильбертом (1885 г.). И хотя данный этап был “пройден” с достаточной строгостью и элегантностью, в дальнейшем в теории чисел возникли серьезные трудности.

<< Предыдущий параграф Следующий параграф >>
Оглавление