Алгоритм Салквиста

Вход: Формула А, где А – несвязная.

Выход: Свойство шкал, соответствующее А.

Действия:

1. Выделить негативные и строго позитивные части формулы А.

2. Нарисовать схему, показывающую, что означает выполнение А в мире t; включить имена миров (например, t₁, t₂, …), провести между ними рёбра отношения R и отметить миры, на которых верны строго позитивные формулы …р.

3. Определить ленивую оценку, делающую строго позитивные оценки истинными в их мирах.

4. Для перевода А в А*(t) сделать следующее:

• поставить впереди формулы А*(t) кванторы s, где s пробегает имена миров, соответствующих ромбикам ;

• найти строго позитивные подформулы и заменить их на 1;

• заменить все оставшиеся предикаты р*(х), q*(y), …, соответствующие атомам;

• произвести упрощения, если можно.

В результате работы алгоритма Салквиста получаем некоторую формулу (t), истинность которой означает, что формула А верна в шкале (W, R) в некотором мире t относительно некоторой оценки.

Значит, формула А будет тавтологией тогда и только тогда, когда (W, R) удовлетворяет формуле t(t) (как модель языка первого порядка, состоящего из единственного бинарного предикатного символа R).

Тем самым, теорема доказана.

Замечание. Ленивая оценка определяет формулы р*(х) следующим образом: Рассматриваем подформулы р, р, р, …, для которых существуют миры среди t, t₁, t₂, … . Пути к соответствующим мирам будут давать формулы:

р*(х) = (x = t)  R(t, x)  x₁(R(t, x₁) & R(x₁, x))  …

 x₁x₂…x_m(R(t, x₁) & R(x₁, x₂) & … & R(x_m, x)).