Аналитические таблицы для логики предикатов

Аналитические таблицы для логики предикатов

Аналитические таблицы для логики предикатов образуются в некотором смысле как расширение аналитических таблиц для логики высказываний. К уже известным правилиам для логических связок добавляются 4 правила для кванторов.

Правило t∀. Предположим, что в некоторой цепи имеется отмеченная формула вида t∀αA. Это означает утверждение об истинности ∀αA. В соответствии с логическим смыслом квантора общности, формула ∀αA истинна, если и только если любой индивид предметной области удовлетворяет условию А. Поэтому в случае истинности ∀αA истинной оказывается также любая формула вида A(k), которая является результатом подстановки вместо всех свободных вхождений α в А произвольного замкнутого терма k. Но так как в языке логики предикатов таких термов бесконечно много, список подставляемых термов ограничивается следующим условием – в качестве k можно брать содержащийся уже в отмеченных формулах данной цепи замкнутый терм, а если таковых нет в цепи, то любую индивидную константу.

Все правила редукции, рассмотренные до сих пор, применяются при построении аналитической таблицы локально, т. е. один раз в некотором конкретном месте. Правило же редукции t∀ является не локальным, а глобальным. Это означает, что оно может применяться неоднократно для того, чтобы повторным применением получать утверждения об истинности A(k1), A(k2),… для замкнутых термов уже содержащихся в таблице и отличных от терма k. Итак, с учетом указанных выше обстоятельств, правило t∀ формулируется следующим образом:

t∀	t∀αA
tA(k),

где A(k) – результат подстановки вместо всех свободных вхождений переменной α в формуле А замкнутого терма k.

Правило f∀. Пусть в некоторой цепи имеется отмеченная формула f∀αA. Это означает утверждение о ложности ∀αA. Ложность формулы ∀aA означает существование объекта, не удовлетворяющего условию А. Введем в качестве имени этого объекта новую, не встречающуюся в отмеченных формулах цепи, предметную константу k. Ясно, что поскольку k не удовлетворяет условию А, формула A(k) оказывается ложной. Поэтому в эту же цепь помещаем отмеченную формулу fA(k).

Смысл того ограничения, что константа k должна быть новой, состоит в следующем. Если k входит в отмеченные формулы цепи, то не исключается возможность, что эти формулы содержат информацию об истинности A(k). Тогда делать вывод, что именно объект k не удовлетворяет условию А, было бы некорректно. Итак, с учетом указанных выше обстоятельств, формулировка правила f∀ имеет следующий вид:

f∀	f∀αA
fA(k),

где A(k) – результат подстановки вместо всех свободных вхождений переменной α в формуле А предметной константы k, которая не содержится в данной цепи.

Правило t∃. Пусть в какой-то цепи содержится отмеченная формула t∃αA,
т. е. содержится утверждение об истинности ∃αA. Согласно смыслу квантора ∃, истинность ∃αA означает существование объекта, удовлетворяющего условию А. В качестве имени этого объекта вводится новая, не встречающаяся в отмеченных формулах цепи, предметная константа k. Ясно, что A(k) истинно в силу того, что k удовлетворяет условию А.

t∃	t∃αA
tA(k),

где A(k) – результат подстановки вместо всех свободных вхождений переменной α в формуле А предметной константы k, которая не содержится в данной цепи.

Правило f∃. Предположим, что в некоторой цепи содержится отмеченная формула f∃αA. Это говорит о ложности ∃αA. Ложность формулы ∃αA означает, что любой индивид предметной области не удовлетворяет условию А. Поэтому эта же цепь пополняется отмеченной формулой вида fA(k), где k удовлетворяет тем же самым условиям, которые были сформулированы для правила t∀. Таким образом, правило редукции f∃ тоже является глобальным.

f∃	f∃αA
fA(k),

где A(k) – результат подстановки вместо всех свободных вхождений переменной α в формуле А замкнутого терма k.

Среди кванторных правил редукции рекомендуется в первую очередь применять правила f∀ и t∃, которые требуют введения новых предметных констант, и только потом правила t∀ и f∃, не содержащие ограничений на терм k, подставляемый вместо подкванторной переменной.

И еще одно важное замечание. Правила редукции всегда применяются к тем логическим константам, содержащимся в формуле А, идущей после отметки t или f, которые являются в ней главными знаками.

Проиллюстрируем действие кванторных правил редукции на примере обоснования общезначимости формулы

∃x∀yR(x, у) ⊃ ∀y∃xR(x, у).

В начальную цепь таблицы помещаем допущение о ложности формулы:

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))

Применим единственно возможное правило f⊃.

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))
2.	t∃x∀yR(x, у)	f⊃ 1
3.	f∀y∃xR(x, у)	f⊃ 1

Далее можно применить правило t∃, либо правило f∀. Они оба требуют введения новой предметной константы, поэтому порядок их применения не существен. Используем правило t∃. Так как в построенной таблице нет замкнутых термов (простых или сложных), можно использовать при применении этого правила любую индивидную константу. Заменим свободные вхождения переменной х в ∀yR(x, у), стоящей за квантором ∃ в формуле ∃x∀yR(x, у), на константу а:

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))
2.	t∃x∀yR(x, у)	f⊃ 1
3.	f∀y∃xR(x, у)	f⊃ 1
4.	t∀yR(a, y)	t∃ 2

Теперь можно применить либо правило t∀, либо f∀, но первое из них не требует введения новой константы, а второе требует. Поэтому применяем f∀. Переменную у, стоящую в формуле ∃xR(x, у), заменяем новой константой b:

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))
2.	t∃x∀yR(x, у)	f⊃ 1
3.	f∀y∃xR(x, у)	f⊃ 1
4.	t∀yR(a, y)	t∃ 2
5.	f∃xR(x, b)	f∀ 3

На следующем шаге можно использовать любое из правил – t∀ или f∃, так как они оба не требуют введения новых констант. Применим правило t∀. В результате в цепь добавиться отмеченная формула tR(a, k), где k – любой терм. Поскольку в нашей цепи присутствуют только индивидные константы а и b, то снятие квантора общности надо осуществлять по той, или по другой константе. Нетрудно установить, что для достижения цели – получения противоречия – в качестве k следует взять константу b:

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))
2.	t∃x∀yR(x, у)	f⊃ 1
3.	f∀y∃xR(x, у)	f⊃ 1
4.	t∀yR(a, y)	t∃ 2
5.	f∃xR(x, b)	f∀ 3
6.	tR(a, b)	t∀ 4

Аналогичным образом надо применить и правило f∃. Тогда в нашу цепь добавится отмеченная формула fR(k, b), где k – любой терм, содержащийся в цепи. Легко установить, что в качестве k надо взять терм а. Итак:

1.	f(∃x∀yR(x, у) ⊃ ∀y∃xR(x, у))
2.	t∃x∀yR(x, у)	f⊃ 1
3.	f∀y∃xR(x, у)	f⊃ 1
4.	t∀yR(a, y)	t∃ 2
5.	f∃xR(x, b)	f∀ 3
6.	tR(a, b)	t∀ 4
7.	fR(a, b)	f∃ 5

Единственная цепь аналитической таблицы содержит противоречие, так как в ней находятся отмеченные формулы tR(a, b) и fR(a, b), а потому аналитическая таблица замкнута, и формула ∃x∀yR(x, у) ⊃ ∀y∃xR(x, у) общезначима.

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

В ряде случаев построенная аналитическая таблица может свидетельствовать о необщезначимости некоторой формулы А или о том, что из A1, A2,..., An не следует логически В. Это имеет место в том случае, когда таблица содержит только цепи конечной длины, ни в одной цепи нельзя применить никакое правило редукции и в таблице содержаться незамкнутые цепи.

Рассмотрим в качестве примера аналитическую таблицу:

1.	f(∃xP(x) ⊃ ∀xP(x))
2.	t∃xP(x)	f⊃
3.	f∀xP(x)	f⊃
4.	tP(a)	t∃
5.	fP(b)	f∀

Очевидно, что цепь не содержит отмеченных формул вида tC и fC. Вместе с тем дальнейшее применение правил редукции невозможно. Поэтому таблица свидетельствует о необщезначимости формулы ∃xP(x) ⊃ ∀xP(x).

Однако имеется и другая возможность. Аналитическая таблица, начинающаяся с отмеченной формулы fA (или с формул tA1, tA2,..., tAn, fB), на каждом шаге своего построения оказывается незамкнутой, но при этом остается возможность дальнейшего применения правил редукции. Указанная ситуация может возникнуть в силу специфики правил t∀ и f∃, применение которых глобально и потому может быть многократно применено по отношению к одним и тем же формулам.

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