logo
МЛиТА 6 - 7

Пример 2

Найдём формулу (t) для формулы А = (р  р). С этой целью представим А как р & р. Делаем 1 шаг перевода А*(t) = р*(t) & р*(t). Заменяем строго позитивную формулу р*(t) на 1, ибо ленивая оценка делает её истинной. Поскольку р*(t) даёт ленивое определение р*(х) = R(t, x), то А*()=1 & р*(t)=R(t, t). Получаем: (t) = = R(t, t). Если А – тавтология, то (W, R) |= t(t). Следовательно, (W,R) |= tR(t, t).