Метод семантических таблиц

Метод семантических таблиц — это формальная разрешающая процедура для формул логики высказываний (см. Логика высказываний) и логики предикатов (см. Логика предикатов), позволяющая чисто синтаксическими (см. Синтактика) средствами решать семантические (см. Семантика) проблемы формализованных исчислений. Метод семантических таблиц создал голландский философ и логик Э. В. Бет (Е. W. Beth) в 1955 году.

Эквивалентность семантического и формального подходов установил ещё К. Гёдель в 1930 году в теореме о полноте, однако эта связь устанавливалась сложным и окольным путём. Метод семантических таблиц, разработанный Бетом, делал эту связь простой и прямой. Различие между семантическим следованием и формальной выводимостью было известно со времён Г. Фреге. Бет формулирует его следующим образом:

1. Формула V семантически следует из формул U₁, U₂, … U_n тогда и только тогда, когда в каждой модели D, в которой истинны формулы U₁, U₂, … U_n, также истинна формула V.
2. Формула V формально следует из формул U₁, U₂, … U_n тогда и только тогда, когда существует конечная последовательность таких формул p₁, p₂, … p_k, что каждое p_i (i = 1, 2, … k) является одной из формул U₁, U₂, … U_n или получается из формул предшествующих p_i в последовательности p₁, p₂, … p_k на основании применений установленной системы правил R, и p_k совпадает с V.

Оба понятия логического следования неявно использовались и в традиционной логике (см. Логика). До появления бетовских таблиц отдельно существовали таблицы истинности и отдельно различные системы исчислений.

Правила построения семантических таблиц специфичны для каждой системы, а также зависят от способа их построения. В общем случае семантическая таблица состоит из двух сопряжённых столбцов; в левом столбце пишутся формулы, соответствующие высказываниям, принимаемым за истинные, а в правом — принимаемым за ложные. Рассуждение осуществляется «от противного». Если необходимо выяснить, следует ли формула B из формул A₁, … A_n, то в левом столбце таблицы пишут формулы A₁, … A_n, а в правом — формулу B. Если необходимо установить общезначимость формулы D, то в правом столбце таблицы пишут эту формулу. Если необходимо установить, является ли формула противоречивой, то эту формулу пишут в левом столбце таблицы.

Правила редукции, позволяющие переходить от формул, содержащих n логических терминов, к формулам, содержащим меньше чем n логических терминов, являются правилами построения таблицы. Для формул языка логики предикатов, содержащих знаки отрицания, конъюнкции, нестрогой дизъюнкции, материальной импликации, кванторы общности и существования, используются следующие правила редукции:

•  ¬ Л. Если формула ¬ A находится в левом столбце таблицы (подтаблицы), то в правом столбце той же таблицы (подтаблицы) пишем А
•  ¬ Пр. Если формула ¬ A находится в правом столбце, то в левом столбце пишем A.
• ∧ Л. Если формула A ∧ B находится в левом столбце таблицы (подтаблицы), то в том же столбце пишем формулы A и B.
• ∧ Пр. Если формула A ∧ B находится в правом столбце таблицы (подтаблицы), то в каждом из столбцов образуем две новые альтернативные подтаблицы этого столбца и в левой подтаблице правого столбца пишем A, а в правой таблице того же столбца — B.
• ∨ Л. Если формула A ∨ B находится в левом столбце таблицы (подтаблицы), то в каждом из столбцов образуем две новые альтернативные подтаблицы и в левой из них (левого столбца) пишем A, а в правой (того же столбца) — B.
• ∨ Πр. Если формула A ∨ B находится в правом столбце таблицы (подтаблицы), то в том же столбце пишем формулы A и B.
• ⊃ Л. Если формула A ⊃ B находится в левом столбце таблицы (подтаблицы), то в каждом из столбцов образуем две новые альтернативные подтаблицы и в правой подтаблице левого столбца пишем формулу B, а в левой подтаблице правого столбца пишем A.
• ⊃ Пр. Если формула Α ⊃ Β находится в правом столбце таблицы (подтаблицы), то в левом столбце той же таблицы пишем формулу A, а в правом — B.
• ∀ Л. Если формула ∀αA (α) находится в левом столбце таблицы (подтаблицы), то в том же столбце помещаем формулу A (β), где β — произвольная индивидная переменная или константа, A (β) есть результат правильной подстановки β вместо α в A (α). Эвристический совет: в качестве β нужно взять индивидную константу, которая уже встречается в подтаблице, или переменную, которая имеет свободные вхождения в какую-то из формул подтаблицы; если таковых нет, то вводится произвольная индивидная константа.
• ∀ Пр. Если формула ∀αA (α) находится в правом столбце таблицы (подтаблицы), то в тот же столбец помещаем формулу A (β), где β — новая индивидная константа, то есть константа, не встречающаяся ещё ни в левом, ни в правом столбцах, а A (β) есть результат правильной подстановки β в A (α) вместо α.
• ∃ Л. Если формула ∃αA (α) находится в левом столбце таблицы (подтаблицы), то в тот же столбец помещаем формулу A (β), где β — новая индивидная константа; A (β) — результат правильной подстановки индивидной константы β в A (α) вместо α.
• ∃ Пр. Если формула ∃α A (α) находится в правом столбце таблицы (подтаблицы), то в тот же столбец помещаем формулу A (β), где β — произвольная индивидная переменная или константа, а A (β) — то же, что и в пояснении к правилу ∀Л. Эвристический совет тот же, что описан при формулировке правила ∀Л.

Альтернативная подтаблица (а если таковых нет, то таблица) является замкнутой, если некоторая формула входит в её левый и правый столбцы. Таблица является замкнутой, если замкнуты все её альтернативные подтаблицы.

Метод исследования рассуждений посредством логики предикатов, заданной семантическими таблицами, заключается в следующем. На первом шаге переводим на язык логики предикатов посылки и заключение рассуждения. Например, рассуждение: «Всякий, кто находится в здравом уме, может понимать логику. Ни один из сыновей Крокса не может понимать логику. Сумасшедшие не допускаются к голосованию. Следовательно, никто из сыновей Крокса не допускается к голосованию» на язык логики предикатов переводится так: первой, второй и третьей посылками являются соответственно формулы: ∀x (P(x) ⊃ Q(x)), ∀x (R(x, a) ⊃ ¬ Q(x)), ∀x (¬ P(x) ⊃ ¬ S(x)), а заключением — формула ∀x (R(x, a) ⊃ ¬ S(x)). Второй шаг состоит в построении семантической таблицы, в левый столбец которой пишем формулы, соответствующие посылкам, а в правый — формулу, соответствующую заключению. Далее применяются правила редукции.

Из приведённой выше таблицы видно, что всё её подтаблицы замкнуты, следовательно и сама семантическая таблица замкнута. Можно сделать вывод, что анализируемое рассуждение является правильным. В силу неразрешимости логики предикатов возможны три результата: таблица оказывается замкнутой (в этом случае исследуемое рассуждение является правильным, а если анализировалось отдельное высказывание — это высказывание является логически истинным); все возможные правила применены, а таблица не замкнулась (рассуждение является неправильным, а если анализировалось отдельное высказывание — это высказывание не является логически истинным); процесс построения таблицы оказывается бесконечным (в этом случае задача не решена).

Метод семантических таблиц Бета занимает важное место в современной логике. С определёнными модификациями он применяется для других логических систем, например для систем модальной логики (см. Логика модальная). Близкие ему идеи разработаны также Я. Хинтиккой (метод модельных множеств), Р. М. Смуллианом (метод аналитических таблиц). В конце 1950-х годов П. Лоренцен построил диалоговую логику аналогичную правилам построения семантических таблиц.

В последнее время получены новые результаты в области автоматического доказательства теорем, где также используется метод таблиц. Сам Бет также развивал свой метод дальше. В 1956 году он постоил с помощью него семантику для интуиционистской логики. Затем он построил модальную логику на основе семантических правил. Табличный метод также позволил Бету получить новые результаты относительно метода А. Падоа в теории определимости. Это достижение известно как «Теорема Бета». В целом, возможность применения метода семантических таблиц для решения задач как семантического (теоретико-модельного), так и формально-дедуктивного (теоретико-доказательственного) характера позволяет выявить гносеологически весьма важное обстоятельство, состоящее в том, что основу дедукции составляют некоторые отношения содержательно-семантического характера. Очевидны также широкие эвристические возможности этого метода для поиска и построения выводов и доказательств.