Упражнение 10. Метод аналитических таблиц для формул языка первого порядка

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

О. Коши [1] [2]

Теоретические сведения

Единственное средство усовершенствовать наши умозаключения состоит в том, чтобы сделать их столь же наглядными, как у математиков,такими, что их ошибочность можно было бы попросту увидеть, увидеть глазами, а в случае возникновения разногласий достаточно было бы только сказать: «Посчитаем, милостивый государь», чтобы без дальнейших околичностей стало ясно, кто прав.

Г. В. Лейбниц

Представление об аналитических таблицах

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

Более того, А. Чёрч показал, что не существует алгоритм распознавания общезначимости формул языка первого порядка, в силу чего решение указанного вопроса представляет собой творческую задачу.

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

Рассмотрим (по [4, с. 112—125]) один из них, который называется методом аналитических таблиц (см. также всесторонний анализ этого метода [1]).

Идея метода состоит в том, что утверждение о истинности (общезначимости) формулы А обосновывается посредством доказательства от противного, т. е. предположение о ложности формулы А должно привести к противоречию. Описанное рассуждение оформляется в виде последовательности шагов, называемая аналитической таблицей, причём каждому шагу рассуждения соответствует некоторая строка этой таблицы, содержащая один или несколько списков формул (различные списки разделяются буквой «|», (вертикальная черта). Присутствие формулы С в некотором списке соответствует утверждению о ее истинности, а наличие в списке -лС — утверждению о ее ложности.

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

Переход от строки аналитической таблицы с номером п к строке с номером (п + 1) осуществляется с помощью формальных правил, называемых правилами редукции. Эти правила выражают условия истинности и ложности формул вида (Л & В), (A v В), —> В), —А, УхА, ЗхА, указывая на следствия, которые могут быть получены из факта истинности или ложности формул приведённых типов. Каждое правило редукции позволяет заменять на (п + 1)-м шаге какой-либо из списков формул в строке с номером п на один или два новых формульных списка.

Так как целью доказательства от противного является демонстрация того, что исходное допущение с необходимостью приводит к противоречию, то задача состоит в получении такой строки аналитической таблицы, каждый формульный список которой содержит некоторую формулу С вместе с ее отрицанием -iС. При получении данного результата утверждение относительно общезначимости Л считается обоснованным.

  • [1] Обязательные результаты обучения: • знать основные понятия — метод доказательства общезначимости и логического следованияформул языка первого порядка с помощью аналитических таблиц; — правила редукции, применение правила редукции, посылки и заключение применения правила редукции, аналитическая таблица, замкнутыйсписок формул, замкнутая аналитическая таблица; — критерий общезначимости и критерий правильности логическогоследования в методе аналитических таблиц; — аналитические таблицы для отмеченных формул;
  • [2] уметь —конструировать доказательство общезначимости формул в языке первого порядка с помощью аналитических таблиц; —определять общезначимость формул языка первого порядка с помощьюаналитических таблиц; • владеть — основными понятиями, представленными выше; — методами решения задач, представленных в Упражнении.
 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >