АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД

АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД
    АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД — разрешающий метод для проблемы общезначимости формул классической, интуиционистской и модальной (система 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^B}
    [S, FA, FB]
    ?=): {S, ?(?=>?)\_ F=): [S, F(A^B)] 7-,: ? ?-^ ТВ} [S, TA, FB] {S, FA]
    {S, FA], {S, F-.: [S, F^A}_
    [S, TA} '
    2) для интуиционистской пропозициональной логики те же, кроме Т-з, Рз, T-i, F-,, которые заменяются на; Гэ: {S, Т(А^В)]____________ 7Ь: [S, F{A^B)}
    |S, T(A^?), FA], {S, ПЛэД), ТВ] {Sr, TA, FB] Т-,: IS, Т^А] F-,: [S, F-^A} {S, Т^А, FA] {ST, TA], где Sr— результат исключения из S всех формул вида FB; 3) для S4 —те же, что в 1) с добавлением та'• 1^ TDA} Fa: [S, FoA] {S, ТйА, ТА] {Sa, FA], le Sa — результат исключения из S всех формул, не имеющих вида TDB; 4) для классической и интуиционистской логики предикатов те же, что в 1) и 2) соответственно, с добавлением: TV: {S, Т^/хА(х)] j-V: {S, FrfxA(x)] 73: {S, T3xA(x)] {S, WxA(x), TA(a)] {S, FA(b)] {S, TA(b)] F3: {S, f3xA(x)]
    {S, F3xA(x), FA(a)], где а—основная произвольная предметная постоянная константа, и—вспомогательная постоянная, каждый раз новая (не встречавшаяся в исходном множестве), а А(а) {А(Ь)) — результат их подстановки вместо ? в формулу А(х). ТГ — множество называется замкнутым, если и только если в нем имеются ТВ и FBww какой-нибудь формулы В языка соответствующей системы. ТУ — множество называется исчерпанным, если и только если оно замкнуто или никакое применение правил к нему не приводит к новой конфигурации. Т. о., аналитической таблицей некоторой формулы А называется непустая конечная последовательность конфигураций, первая из которых есть {{FA]], a каждая из последующих конфигураций получается из предыдущей по одному из правил. Аналитическая таблица называется завершенной, если и только если каждое ТГ — множество ее последней конфигурации является исчерпанным. Не• разрешимость исчисления предикатов относительно проблемы общезначимости и доказуемости равносильна неразрешимости вопроса о существовании завершенной аналитической таблицы для произвольной формулы ее языка. Таблица является замкнутой, если и только если каждое ТУ — множество ее последней конфигурации является замкнутым.
    Формула Л языка любой из рассматриваемых систем общезначима (для классической пропозициональной логики— тождественно-истинна), если и только если для нее существует замкнутая таблица. (Последнее существенно при построении аналитических таблиц для формул интуиционистской и модальной логики, т. к. варьирование порядка применения правил может привести к построению различных таблиц для одной и той же формулы.) Для классической логики завершенная незамкнутая таблица указывает возможные элементарные условия ее ложности (опровергающие примеры). Ими являются незамкнутые исчерпанные множества последней конфигурации. Примеры: 1) Формула ((DpvDq)^ 0(pvq)) системы 54 общезначима, поскольку для нее существует замкнутая аналитическая таблица: ?. {F((Dp^oqW(pvq))]]; 2. {1DpvOq), Fa(pvq))]]: 3. {???, fO(p^q)], {TOq, F0(pvg)]]; 4. {TOp, F(p^q)], {TOq, F(pvq)]]: 5. {???, Fp, Fq], [TDq, Fp, Fq}; 6. [[-Юр, 1p, Fp, Fq, {TDq, Tq. Fp. Fq]].
    2) Аналитическая таблица для формулы интуиционистской логики pv-n^: 1. ((???-?))); 2. {Fp, F-?]]; 3. {??} не является замкнутой, и невозможно изменением порядка применения правил получить другую таблицу этой формулы, следовательно, данная формула не является законом интуиционистской логики.
    Для классической логики имеется непосредственная связь между способом построения таблицы для некоторой формулы и доказательством ее в некотором секвенциальном исчислении (см. Исчисление секвенций}, получаемом переформулировкой правил построения таблицы. Аналитическая таблица классической формулы А в виде дерева (множества столбцов) также может быть получена перестройкой ее таблицы, представленной в виде последовательности конфигураций.
    Возможность применения метода аналитических таблиц для решения задач как семантического (теоретико-модельного), так и формально-дедуктивного (теоретико-доказательственного) характера позволяет выявить гносеологически весьма важное обстоятельство, состоящее в том, что основу дедукции составляют некоторые отношения содержательно-семантического характера. Очевидны также широкие эвристические возможности этого метода для поиска и построения выводов и доказательств.
    Лет.: Fitting M. С. Intuitionistic Logic Model Theory and Forcing. Amst.—L., 1969; Камер С. Упрощенный метод доказательства для элементарной логики.—В кн.: Математическая теория вывода. М., 1967; Коспиок. В. в. Логика. Киев—Одесса, 1975; Смирнова Е.Д. Упрощение бетовско-хинтикковского доказательства полноты исчисления предикатов первого порядка.—В кн.: VII Всесоюзный симпозиум по логике и методологии науки. Тезисы. Киев, 1976.
    ?. К. Войшвилло

Новая философская энциклопедия: В 4 тт. М.: Мысль. Под редакцией В. С. Стёпина. 2001.