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

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

Шаг n. Пусть уже построена таблица T_n-1. Особые вершины этой таблицы, которым соответствуют подформулы, не являющиеся атомами, продолжаются атомарными таблицами, соответствующими последней, выполняемой в каждой из таких ветвей, логической связкой. Результатом построения становится новая таблица T_n.

Шаг n+1. Пусть Х – особая вершина[2], которая еще не была раскрыта. Если такой вершины не существует, то семантическая таблица является замкнутой. Если такая вершина есть, строим таблицу T_n+1, продолжая каждую непротиворечивую ветвь, проходящую через вершину Х, присоединением атомарной таблицы, соответствующей находящейся в этой вершине подформуле.

Содержательно, в случаях t("x j(x)) и f($x j(x)) мы хотим избавиться от повторений, и объявляем j(с) истинной (ложной) последовательно для всех новых констант, выбирая их из списка констант, что может продолжаться бесконечно, как показано на рис. 9.

|

t["xA(x,x)]

|

t[$y(ØA(y,y)ÚB(y,y)]

В этом примере левая ветвь противоречива, тогда как правая ветвь продолжается бесконечно.

Замкнутая семантическая таблица в логике предикатов есть объединение всех таблиц T_n из предыдущего построения, т.е. Она может иметь бесконечное число вершин, тогда как семантические таблицы для логики высказываний всегда конечны.

Основные определения:

1. Замкнутая семантическая таблица называется противоречивой, если все ее ветви противоречивы.

2. Предложение s выводимо по Бету (опровержимо по Бету), если существует противоречивая замкнутая семантическая таблица с корнем fs (ts). Тот факт, что предложение s выводимо по Бету обозначается ├_В s.

3. Предложение s выводимо по Бету из множества S предложений логики предикатов, если существует противоречивая замкнутая семантическая таблица с корнем fs. и следующей вершиной t P, где Р – конъюнкция предложений множества S. Этот факт обозначается S ├_В s.