Формализация логики предикатов методом аналитических таблиц
Метод аналитических таблиц является опровергающей процедурой. Поиск обоснования общезначимости формулы осуществляется по определенным правилам и начинается с предположения, что формула не общезначима. Это предположение ведет к противоречию, если формула на самом деле общезначима.
Логика предикатов неразрешима: не существует эффективной процедуры (алгоритма), который позволяет в конечное число шагов проверить общезначимость формул логики предикатов. Это объясняется тем, что надо рассмотреть все модели, каждая из которых может содержать бесконечную область и всевозможные приписывания значений переменным, на каждом из которых формула принимает значение «истинно». Но логика высказываний разрешима на основании таблиц истинности. Аналитические таблицы на основании рассуждения от противного позволяют найти модель с конечной областью, в которой формула опровергается, если она общезначима. Правила редукции логики предикатов надстраиваются над правилами редукции логики высказываний, так как и в логике предикатов мы используем логические связки. Формула, расположенная над чертой правила, называется посылкой правила редукции, а формула под чертой правила - называется заключением правила. Вертикальная черта в заключении правила означает ветвление результата применения правила редукции (правила с ветвлением). Каждое правило редукции, кроме правил V: и ~ (3):, разбивает формулу посылки на подформулы за счет устранения логической связки. Правила ~(V): и 3: вводят (при построении аналитической таблицы формулы) новые константы. Правила V: и ~(3): используют старые (прежде введенные) константы. Если структура формулы такова, что вынуждает применить вначале правило V: или ~(3):, то мы вводим произвольную константу, а дальше действуем на основании остальных правил, т. е. вводим на основании правил ~ (V): и 3: новые константы. В ходе построения аналитической таблицы некоторой формулы она разлагается на списки формул, представляющие собой подформулы исходной формулы. Определение 1 (аналитической таблицы). Аналитической таблицей называется конечная или бесконечная последовательность строк Сг, ... Ск, ... списков формул такая, что каждая последующая строка получается из предыдущей применением правила редукции.
Замечание. Отметим, что если мы применяем правило редукции с ветвлением, то мы получаем два списка формул. Определение 2 (замкнутого списка формул). Список формул называется замкнутым, если в нем встречается некоторая формула и ее отрицание, т. е. А и ~А (противоречие). Определение 3 (завершенного списка). Список формул называется завершенным, если к формулам этого списка невозможно при - менять правила редукции, т. ев списке встречаются атомарные формулы или отрицание атомарных формул. Определение 4 (замкнутой таблицы). Аналитическая таблица замкнута, если все ее списки формул замкнуты (противоре - чивы). Определение 5 (завершенной таблицы). Аналитическая таблица называется завершенной, если она замкнута или имеет завер - шенные списки формул. Определение 6 (общезначимой формулы в терминах аналитической таблицы). Формула А называется общезначимой, если ее аналитическая замкнута. Замечание. Завершенный список или завершенная таблица не обязательно замкнута, т. е. может быть замкнутой, но не являть ся противоречивой. Достаточно построить аналитическую таблицу для выполнимой формулы, чтобы в этом убедиться. Методические рекомендации 1. Надо обнаружить связь аналитических таблиц логики высказываний с обыкновенными таблицами истинности. 2. Усвойте различие между правилами, которые вводят новые константы и правилами, которые не вводят новых констант, а ис пользуют прежде введенные константы. 3. Усвойте определения и подберите соответствующие этим определениям примеры. Вопросы для самоконтроля 1. Что такое аналитическая таблица? 2. В чем различие между правилами с ветвлением и правилами без ветвления? 3. Может ли список формул быть завершенным, но не быть противоречивым? 4. Что получится, если мы построим аналитическую таблицу для противоречивой формулы, но не будем рассуждать от противного, т. е не поставим отрицание перед формулой. Литература 1. Бочаров В. А., Маркин В. И. Основы логики. М., 1998, 1999, 2000, 2002, 2004. Гл. 3, § 3. 2. Войшвилло Е. К. Символическая логика. Классическая и релевантная. М., 1989. Гл. 2, § 4, 5. 2.