АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД
АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД – разрешающий метод для проблемы общезначимости формул классической, интуиционистской и модальной (система S4) логики высказываний [ЛОГИКА ВЫСКАЗЫВАНИЙ]. В сочетании с некоторыми дополнительными приемами этот метод применим и для классической и интуиционистской логики предикатов [ЛОГИКА ПРЕДИКАТОВ]. В последнем случае метод аналитических таблиц представляет собой полуразрешающую процедуру, поскольку положительное решение вопроса об общезначимости достижимо для любой общезначимой формулы, а отрицательное – не для всякой необщезначимой формулы. Так как к вопросу об общезначимости формул сводятся вопросы о наличии логического следования, а также несовместимости по истинности (ложности) формул языков соответствующих логических систем, то аналитические таблицы применимы и для решения этих вопросов.
Построение аналитической таблицы для некоторой формулы A начинается с предположения о ее ложности. Далее по правилам построения осуществляется сведение этого предположения к все более простым условиям ложности A в виде выражений TB («истинно B») и FB («ложно В»), называемых отмеченными формулами (далее «TF-формулы»), где B – формула соответствующей системы. В случае общезначимости A процесс редукции приводит к противоречию.
Правила построения аналитических таблиц специфичны для каждой системы, а также зависят от способа их построения. Имеются два таких способа: в виде дерева, или множества столбцов (когда ветви дерева рассматриваются как столбцы), и в виде последовательности семейств множеств TF-формул, называемых конфигурациями. (При этом исходной конфигурацией для A является .) Первый способ, предложенный Р.Смаллианом как результат модификации семантических таблиц [СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ] (таблиц Бета), применим лишь для классической логики. Второй – результат дальнейшей модификации семантических таблиц для синтаксической (финитной) процедуры доказательства. Этот способ предложен Фиттингом. Согласно Фиттингу, каждое правило применяется к какому-либо множеству TF-формул (далее «TF-множество») в составе некоторой конфигурации и ведет к преобразованию некоторой TF-формулы этого множества. Результатом применения является одно или пара TF-множеств, которыми заменяется исходное в данной конфигурации. Таким образом, применение правила является также и преобразованием конфигурации. В приводимых ниже правилах S обозначает некоторое, возможно пустое, TF-множество.
1) Для пропозициональной классической логики:
2) для интуиционистской пропозициональной логики те же, кроме T
где ST – результат исключения из S всех формул вида FB;
3) для S4 – те же, что в 1) с добавлением
где S⎕ –результат исключения из S всех формул, не имеющих вида T⎕B;
4) для классической и интуиционистской логики предикатов те же, что в 1) и 2) соответственно, с добавлением:
где a – основная произвольная предметная постоянная константа, b – вспомогательная постоянная, каждый раз новая (не встречавшаяся в исходном множестве), а A(a) (A(b)) – результат их подстановки вместо x в формулу A(x). TF-множество называется замкнутым, если и только если в нем имеются TB и FB для какой-нибудь формулы B языка соответствующей системы. TF-множество называется исчерпанным, если и только если оно замкнуто или никакое применение правил к нему не приводит к новой конфигурации. Т.о., аналитической таблицей некоторой формулы A называется непустая конечная последовательность конфигураций, первая из которых есть , а каждая из последующих конфигураций получается из предыдущей по одному из правил. Аналитическая таблица называется завершенной, если и только если каждое TF-множество ее последней конфигурации является исчерпанным. Неразрешимость исчисления предикатов относительно проблемы общезначимости и доказуемости равносильна неразрешимости вопроса о существовании завершенной аналитической таблицы для произвольной формулы ее языка. Таблица является замкнутой, если и только если каждое TF-множество ее последней конфигурации является замкнутым.
Формула A языка любой из рассматриваемых систем общезначима (для классической пропозициональной логики – тождественно-истинна), если и только если для нее существует замкнутая таблица. (Последнее существенно при построении аналитических таблиц для формул интуиционистской и модальной логики, т.к. варьирование порядка применения правил может привести к построению различных таблиц для одной и той же формулы.) Для классической логики завершенная незамкнутая таблица указывает возможные элементарные условия ее ложности (опровергающие примеры). Ими являются незамкнутые исчерпанные множества последней конфигурации.
Примеры:
1) Формула ((⎕p
1. ;
2. ;
3. {{T⎕p, F⎕(p
4. {{T⎕p, F(p
5. {{ T⎕p, Fp, Fq}, { T⎕q, Fp, Fq}};
6. {{ T⎕p, Tp, Fp, Fq}, { T⎕q, Tq, Fp, Fq}}.
2) Аналитическая таблица для формулы интуиционистской логики p
Для классической логики имеется непосредственная связь между способом построения таблицы для некоторой формулы и доказательством ее в некотором секвенциальном исчислении (см. Исчисление секвенций [ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ]), получаемом переформулировкой правил построения таблицы. Аналитическая таблица классической формулы A в виде дерева (множества столбцов) также может быть получена перестройкой ее таблицы, представленной в виде последовательности конфигураций.
Возможность применения метода аналитических таблиц для решения задач как семантического (теоретико-модельного), так и формально-дедуктивного (теоретико-доказательственного) характера позволяет выявить гносеологически весьма важное обстоятельство, состоящее в том, что основу дедукции составляют некоторые отношения содержательно-семантического характера. Очевидны также широкие эвристические возможности этого метода для поиска и построения выводов и доказательств.
Литература:
1. Fitting M.С. Intuitionistic Logic Model Theory and Forcing. Amst.–L., 1969;
2. Кангер С. Упрощенный метод доказательства для элементарной логики. – В кн.: Математическая теория вывода. М., 1967;
3. Костюк В.Н. Логика. Киев – Одесса, 1975;
4. Смирнова Е.Д. Упрощение бетовско-хинтикковского доказательства полноты исчисления предикатов первого порядка. – В кн.: VII Всесоюзный симпозиум по логике и методологии науки. Тезисы. Киев, 1976.
Е.К.Войшвилло
Новая философская энциклопедия