Главная | Обратная связь | Поможем написать вашу работу!

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

Как и в логике высказываний, доказательство тождественной истинности формул может производиться с использованием семантических таблиц Бета. Семантические таблицы для логики предикатов содержат кроме элементарных семантических таблиц логики высказываний, элементарные семантические таблицы для формул с кванторами. В корень соответствующих таблиц помещается помеченная формула с квантором общности или существования. Ранее было определено, что логическое значение формулы, образованной с использованием квантора общности, определяется как минимум из логических значений формулы, находящейся в области действия квантора, при всевозможных подстановках термов из предметной области вместо всех вхождений переменной квантора. Семантические таблицы для формул, образованных с использованием кванторов представлены на рис. 5.

Рисунок 6 Элементарные семантические таблицы

для формул с кванторами

Семантические таблицы для формул f" xj(x) и t$ xj(x) вводят новую константу с, которая еще не появлялась в таблице. Последнее связано с функцией интерпретации формул с кванторами и будет продемонстрировано далее. Семантические таблицы для формул t" xj(x) и f$ xj(x) означают перебор всех возможных значений переменной x из предметной области. Поэтому семантическая таблица для формулы логики предикатов может оказаться бесконечной в отличие от таблиц в логике высказываний.

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

Семантические таблицы для t" xj(x) и f$ xj(x) означают, что при построении таблицы переменная x должна принимать все возможные значения, т.е. пробегать всю предметную область. Возможно, что таблица окажется бесконечной.

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

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

Доказать общезначимость формулы s: "x j(x)®$x j(x), где j - бескванторное предложение логики предикатов.

ª Для доказательства общезначимости формулы поместим в корень таблицы помеченную формулу fs, рис. 6.

Вершина 1 Вершина 2 Вершина 3 Вершина 4 Вершина 5

f(" x (j(x))®$ x( j(x)))

t" x( j(x))

f $ x j(x)

Для всех с Для всех с

Из вершины 3 Из вершины 2 Противоречие между 4 и 5

f j(c)

t j(c)

Рисунок 7 Пример замкнутой семантической таблицы

для формулы с кванторами

В вершинах 4 и 5 семантической таблицы использовалась одна и та же константа. Так разрешается делать, поскольку таблицы для t" x( j(x)) и f$ x( j(x)) позволяют использовать любую константу.

Приведенный вывод по Бету означает, что рассмотренное предложение общезначимо, так как все попытки опровергнуть его привели к противоречию.

Доказать общезначимость импликации

(("x(P(x)®Q(x))®("xP(x)®"xQ(x)))) с использованием замкнутой семантической таблицы.

Поместим в корень таблицы исследуемую формулу, пометив ее как ложную. Ход рассуждений понятен из рис. 7.

Примечание. Семантическая таблица для формул t" xj(x) или f$xj(x) позволяет объявлять формулу j(с) истинной для всех констант с. Семантическая таблица для t$xj(x) позволяет объявлять j(с₁) истинной только для той константы, которая еще не встречалась в семантической таблице, так как квантор существования «выбирает» минимум из значений подкванторной формулы в предметной области. Для формулы f"xj(x) достаточно объявить формулу j(с₁) ложной для новой константы, которая еще не встречалась в рассматриваемой ветви таблицы. Если эту особенность интерпретации формул с кванторами не учитывать, возможны грубые ошибки. Пример такого неверного построения приведен на Рис. 8.

На Рис. 7 приведен пример семантической таблицы для общезначимой формулы.

f[" x (P(x)®Q(x))®(" x P(x)®" x Q(x))]

(1) (2) (3) из (2) (4) из (2) (5) из (4) для новой с₁ (6) из (3) для всех с (7) из (1) для всех с (8)

t"x(P(x)®Q(x))

f(" x P(x)®" x Q(x))

t" x P(x)

f" x Q(x)

fQ(c₁)

tP(c)

t (P(c)®Q(c))

fP(c) tQ(c)

| |

Рисунок 8 Семантическая таблица для формулы с кванторами

Ä Ä

Следующий пример демонстрирует необходимость введения новой константы в каждой новой вершине семантического дерева.

Рассмотрим предложение $xj(x)®"xj(x).

Покажем, что это предложение не общезначимо. Например, пусть j(x) означает атом: х – вор. Тогда рассматриваемое предложение означает: существует человек, который является вором; следовательно, все люди – воры. Положим, что посылка импликации истинна, т.е. t$xj(x). В соответствии с определением логического значения формулы, образованной квантором существования, это означает, что в предметной области найдется такое значение переменной x, при котором формула j(x) истинна, т.е. $x:(I[j(x)]=1), так как логическое значение формулы, образованной квантором существования, определяется как максимум из логических значений формулы в предметной области. Но из этого не следует общезначимость j(x), поскольку логическое значение формулы, образованной квантором общности определяется как минимум из логических значений формулы в предметной области. Следовательно, логическое значение заключения импликации, а именно, формулы " x j(x) не равно тождественно 1. Следовательно, импликация не общезначима, так как 1®0=0.

Семантическая таблица с корнем f($ x(j(x)) ®" x(j(x))) приведена на рис. 8.

Вершина 1 Вершина 2 Вершина 3 Вершина 4 Вершина 5

f($x(j(x))®"x(j(x)))

t$x(j(x))

f"xj((x))

для новой с для новой с

tj(c)

fj(c)

Рисунок 9 Интерпретация формул с кванторами

В вершине 5 нельзя было использовать ту же константу, что и в предыдущей вершине 4. Поэтому удалось «доказать», что предложение $xj(x)®"xj(x) общезначимо, хотя это, очевидно, неверно.

Семантическая таблица может быть бесконечной, если хотя бы в одной из ее ветвей не удается получить противоречие. Это происходит потому, что семантические таблицы для формул, содержащих вершины t("x(j(x))) и f($x (j(x))), могут порождать бесконечные ветви, в которых выполняются проверки истинности формулы при присваивании переменной x последовательно различных значений констант из предметной области.

Как и в логике высказываний, семантическая таблица для предложения j может содержать произвольное число ветвей, соответствующих подформулам этого предложения. Но в отличие от логики высказываний некоторые ветви ЗСТ для формул логики предикатов могут иметь бесконечное число вершин, тогда как семантические таблицы для логики высказываний всегда конечны.

⇐ Предыдущая 5 6 7 8 91011 12 13 14 Следующая ⇒