Пример 3

Пусть А = (р  р). Легко видеть, что А = р & р. Отсюда А*(t) = р*(t) & р*(t). Оценка р*(t) = 1 даёт ленивое определение р*(х) = R(t, x). Ленивая оценка превращает формулу р*(t) в истинную:

x(R(t, x)  р*(x)) = xy(R(t, x)  (R(x, y)  р*(y))).

Следовательно, (t) = xy(R(t, x) & R(x, y)  R(t, y)). Утверждение (W, R) |= (t) превращается в

(W, R) |= txy(R(t, x) & R(x, y)  R(t, y)).

Пример 4

Рассмотрим формулу р  р. Она эквивалентна формуле (р & р). Получаем формулу Салквиста ([р] & [p]). Положим А = [р] & [p]. Стандартный перевод равен:

А*(t) = p*(t) & t₁(R(t, t₁) & p*(t₁)).

Переводим t₁ в начало формулы:

А*(t) = t₁(p*(t) & R(t, t₁) & p*(t₁)).

Из условия истинности p*(t₁) получаем ленивое определение: р*(х) =R(t₁, x). Следовательно, А*(t) = t₁(R(t₁, t) & R(t, t₁)). Формула А будет тавтологией относительно (W, R) тогда и только тогда, когда

(W, R) |= tt1(R(t₁, t) & R(t, t₁)).

Получаем, что отношение R симметрично:

tt₁(R(t, t₁)  R(t₁, t)).

Пример 5

Пусть А – формула, рассмотренная при доказательстве теоремы Салквиста. Найдём А*(t) в случае, когда с = p  q:

A = (q & ([(p  q)] & [p])) & [p].

Мы получили формулу:

А*(t) = R(t, t₁) & R(t₁, t₂) & R(t₁, t₃) & R(t₃, t₄) & R(t, t₅) & R(t₅, t₆) & q*(t₂) & c*(t₃) & p*(t₄) & p*(t₆).

Ленивое определение получаем из условия: p*(t₄) & p*(t₆) = 1. Мы установили, что

р*(х) = y(R(t₄, y) & R(y, x))  R(t₆, x);

q*(x) = (x = t₂).

Поставив с*(t₃) = p*(t₃)  q*(t₃) в формулу для А*(t), получим:

А*(t) = R(t, t₁) & R(t₁, t₂) & R(t₁, t₃) & R(t₃, t₄) & R(t, t₅) & R(t₅, t₆) & (p*(t₃)  q*(t₃));

(t) = x₁x₂x₃x₄x₅x₆(R(t, t₁) & R(t₁, t₂) & R(t₁, t₃) & R(t₃, t₄) & R(t, t₅) & R(t₅, t₆) & (x(R(t₃, x)  p*(x))  (t₃ = t₂)) = x₁x₂x₃x₄x₅x₆(R(t, t₁) & R(t₁, t₂) & R(t₁, t₃) & R(t₃, t₄) & R(t, t₅) & R(t₅, t₆) & (x(R(t₃, x)  y(R(t₄, y) & R(y, x))  R(t₆, x))  (t₃ = t₂))