Катречко С.Л.

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

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

1)      Если Ø X — истинна, то X — ложна.

2)      Если Ø X — ложна, то X — истинна.

3)      Если X&Y — истинна, то X, Y — обе истинны.

4)      Если X&Y — ложна, то X — ложна, или Y — ложна.

5)      Если XÚY — истинна, то X — истинна, или Y — истинна.

6)      Если XÚY — ложна, то X,Y — обе ложны.

7)      Если XÉY — истинна, то или X — ложна, или Y — истинна.

8)      Если XÉY — ложна, то X — истинна, и Y — ложна.

Эти факты являются основанием табличного метода, т.е. лежат в основе сформулированных ниже правил вывода или правил редукции.

Отмеченные формулы. Любая правильно построенная формула (ппф) языка логики предикатов (или логики высказываний как фрагмента логики предикатов), перед которой стоит знак T или знак F, называется означенной формулой.

Примеры означенных формул: F["х$y(Р(х) & R(х, у))]; T[((p v q) É (Øр É q))]; F[($хР(х) É "y(R(y, a) & p))].

Выражения TX и FX называются отмеченными формулами, где X — (неотмеченная) ппф исчисления предикатов (высказываний). Содержательно выражение ТX читается: формула А — истинна, а выражение FX: формула X — ложна.

Таким образом, истинностное значение выражения ТX совпадает со значением формулы X, а истинностное значение FX совпадает со значением ØX.

Означенные формулы не являются формулами языка логики предикатов, а представляют собой выражения метаязыка.

Правила вывода. С означенными формулами можно оперировать в соответствии со следующими правилами построения таблицы, или правилами редукции, где S — это некоторое множество означенных формул, а ТС или FC — те означенные формулы, к которым применяется данное правило. Заметим, что для каждого логического знака существует по два правила; одно для формул, которым предшествует символ “T” (истина), а другое, для формул, которым предшествует символ “F” (ложь) (ср. приводимые ниже правила редукции с содержательной интерпретацией пропозициональных связок, приведенной выше):

T_Ø    S, T_ØA                     F_Ø    S, F_ØA

             __________                                   _________

             S, FA                                S, TA

 

T_&   S, T(A & B)              F_&     S, F(A & B)  

           ______________                            _________________

           S, TA, TB                         S, FA | S, FB

 

T_Ú   S, T(A Ú B)                   F_Ú    S, F(A Ú B)

           _________________                      _______________

        S, TA | S, TB                     S, FA, FB

 

T_É     S, T(A É B)                  F_É    S, F(A É B)

          __________________                       ______________

          S, FA | S, TB                     S, TA, FB

 

Дадим краткое пояснение (интерпретацию) данных правил. Например, правило(а) для логического отрицания Ø (T(F)_Ø) означает, что из TØX непосредственно следует FX в том смысле, что мы можем присоединить FX к любому продолжению (столбцу, ветке) таблицы, непосредственно следующей за ТØX; и что из FØX непосредственно следует ТX. Правило(а) для & (T(F)_&) означает, что из T(X&Y) непосредственно следуют ТX и ТY, а таблица, содержащая F(X&Y) разветвляется ("расщепляется") на два подстолбца FX и FY. Аналогично интерпретируются правила É и Ú.

Данные правила редукции указывают, каким образом осуществляется переход по строкам сверху вниз. Всякая строка содержит некоторое множество означенных формул. При применении правила редукции к некоторой формуле данной строки она «расщепляется» (упрощается) и мы переходим к нижней строке с формулой меньшей «сложности». В результате подобных действий все сложные формулы исходной строки поочередно «расщепляются» вплоть до элементарных означенных переменных.

Аналитическая таблица для произвольной формулы С представляет собой последовательность строк, где первая строка состоит из единственной формулы FC, а каждая последующая строка получается из предыдущей применением правила редукции к некоторой (одной) означенной формуле.

Все правила редукции можно разделить на два типа. Правила, которые имеют непосредственные следствия, а именно: FØ, TØ, T_&, F_Ú, F_É (FØX, TØX, T(X&Y), F(XÚY), F(XÉY)), называются правилами без ветвления; а правила F_&, T_Ú, T_É  (F(X&Y), T(XÚY), T(XÉY); они соответствуют 4, 5 и 7 «факту», в которых есть «или»), которые увеличивают количество столбцов таблицы (на один), точнее расщепляют исходную таблицу надвое, называются правилами с ветвлением.

Первая строка таблицы представляет собой один-единственный столбец. В дальнейшем при построении аналитической таблицы количество столбцов (ветвей) может увеличиваться, а именно каждое применение любого правила с ветвлением разделяет предыдущий столбец на два других столбца (две ветви).

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

Аналитическая таблица замкнута, е. и т. е. каждый ее столбец замкнут.

Доказательство формулы С есть построение замкнутой аналитической таблицы для означенной формулы FC («формула С — ложна», т.е. метод аналитических таблиц основан на непрямом (косвенном) методе «рассуждение от противного».

Если аналитическая таблица для формулы С замкнута (доказуема), то эта формула общезначима. Это следует из теоремы о непротиворечивости (корректности) метода таблиц: метод аналитических таблиц воспроизводит отношение логического следования.

Если формула необщезначима, то для нее нельзя построить замкнутой аналитической таблицы, т.е. аналитическая таблица для этой формулы будет содержать такой столбец, что никакое применение какого-либо правила редукции не приводит к замыканию этого столбца.

В случае логики высказываний (в силу ее разрешимости) любая аналитическая таблица конечна и поэтому необщезначимость формул соответствует случаю, когда все подформулы исходной формулы редуцированы до элементарных, но замыкания получить не удалось. Тогда говорят, что построен контрпример (контрпримеры) к формуле, т.е. она действительно ложна (FC).

Пусть имеется множество посылок А₁, А₂, ... А_n и заключение В. Тогда если аналитическая таблица для формулы (А₁&А₂ & ... & А_n) É В замкнута, то из А₁, А₂, ... А_n следует B (т.е. метод аналитических таблиц воспроизводит отношение логического следования: теорема о непротиворечивости (корректности) метода таблиц).

То есть, если мы хотим вывести формулу (заключение) B из множества других формул (посылок) A₁, A₂, ... А_n, мы должны применить следующий алгоритм перестройки рассуждения в (сложную) формулу:

То есть, если мы хотим вывести формулу (заключение) B из множества других формул (посылок) A₁, A₂, ... А_n, мы должны применить следующий алгоритм перестройки рассуждения в (сложную) формулу:

1.       Объединить формулы A₁, A₂, ... А_n в одну формулу посредством конъюнкции.

2.       Присоединить с помощью импликации к этой вновь образованной формуле формулу B в качестве консеквента.

3.   Строить аналитическую таблицу, первая строка которой содержит означенную формулу F[(А₁&А₂ & ... & А_n) É В]. Если таблица окажется замкнутой, то между формулами A₁, A₂, ... А_n, с одной стороны, и формулой B, с другой, имеется отношение логического следования. А если отношения следования между посылками и заключением нет, то соответствующую замкнутую аналитическую таблицу построить нельзя.