- АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД
- АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД
-
АНАЛИТИЧЕСКИХ ТАБЛИЦ МЕТОД — разрешающий метод для проблемы общезначимости формул классической, интуиционистской и модальной (система 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], lé 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.
.