Философская энциклопедия - аналитических таблиц метод

АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД — разрешающий метод для проблемы общезначимости формул классической, интуиционистской и модальной (система S4) логики высказываний. В сочетании с некоторыми дополнительными приемами этот метод применим и для классической и интуиционистской логики предикатов. В последнем случае метод аналитических таблиц представляет собой полуразрешающую процедуру, поскольку положительное решение вопроса об общезначимости достижимо для любой общезначимой формулы, а отрицательное — не для всякой необщезначимой формулы. Так как к вопросу об общезначимости формул сводятся вопросы о наличии логического следования, а также несовместимости по истинности (ложности) формул языков соответствующих логических систем, то аналитические таблицы применимы и для решения этих вопросов.

Построение аналитической таблицы для некоторой формулы А начинается с предположения о ее ложности. Далее по правилам построения осуществляется сведение этого предположения к все более простым условиям ложности А в виде выражений ТВ (“истинно В”) и FB (“ложно В”), называемых отмеченными формулами (далее “ТГ — формулы”), где В— формула соответствующей системы. В случае общезначимости А процесс редукции приводит к противоречию.

Правила построения аналитических таблиц специфичны для каждой системы, а также зависят от способа их построения. Имеются два таких способа: в виде дерева, илимножества столбцов (когда ветви дерева рассматриваются как столбцы), и в виде последовательности семейств множеств ТУ — формул, называемых конфигурациями. (При этом исходной конфигурацией для А является {FA}].) Первый способ, предложенный Р. Смаллианом как результат модификации семантических таблиц (таблиц Бета), применим лишь для классической логики. Второй — результат дальнейшей модификации семантических таблиц для синтаксической (финитной) процедуры доказательства. Этот способ предложен Фиттингом. Согласно Фиттингу, каждое правило применяется к какому-либо множеству ТГ — формул (далее “ТУ — множество”) в составе некоторой конфигурации и ведет к преобразованию некоторой ТУ — формулы этого множества. Результатом применения является одно или пара ТУ — множеств, которыми заменяется исходное в данной конфигурации. Таким образом, применение правила является также и преобразованием конфигурации. В приводимых ниже правилах S обозначает некоторое, возможно пустое, TFмножество. 1) Для пропозициональной классической логики: Г&: [S, ΊΑ&Β)} F&: [S, F(A&£)} 7 v: {S, T(AvB)

[S, TA, TB} . [S, FA}, {S, FB} S, TA}. (.S, TBMS, F(A