Корректность и полнота систем Гильберта

Можно показать, что KA имеет место тогда и только тогда, когда А – тавтология; утверждение KТA равносильно тому, что А – тавтология относительно класса всех рефлексивных шкал Крипке; S4A равносильно тому, что А – тавтология относительно класса транзитивных шкал.

Свойства шкал Крипке

Мы раньше доказывали, что аксиома Т ( q ® q) является тавтологией относительно шкалы F = (W, R) тогда и только тогда, когда R – рефлексивно. Можно доказать, что аксиома 4 ( q ® q) является тавтологией относительно F = (W, R), если и только если R транзитивно. Аксиома D( q ® àq) будет тавтологией относительно (W, R) тогда и только тогда, когда Dom R = W (т.е. "tÎW$uÎW (tRu)). Возникает вопрос о способе нахождения свойства шкал, относительно которых заданная формула является тавтологией. Опишем один из путей решения этой проблемы, принадлежащий Салквисту. С этой целью рассмотрим символы: 1, 0, &, Ú, , à как примитивные (не связанные между собой). Но А ® В будет по-прежнему сокращением для формулы: Ø(А & ØВ).

Строго позитивными будем называть формулы: р, p, p, …, где р – атом. Позитивной называется формула, не использующая Ø. Негативная формула – это отрицание некоторой позитивной формулы. Несвязной называется формула, полученная из негативных и строго позитивных формул с помощью операций & и à. Формулой Салквиста называется отрицание некоторой несвязной формулы. Например:

формула р ® р эквивалентна формуле Салквиста Ø([ p] & [Øp]);

р ® р – формуле Салквиста Ø([ р] & [Ø р])

и формуле Салквиста Ø([ р] & àà[Øр]);

àр ® àр – формулам Салквиста Ø(à[р] & [Ø àр]) и Ø(à[р] & à[Øàр]);

à р ® àр – формуле Салквиста Ø(à[ р] & [Ø àр]).

Однако ( p®p) не эквивалентна никакой формуле Салквиста.

Теорема Салквиста. В 1973 году Салквист установил, что каждой формуле Салквиста соответствует некоторое свойство шкалы. Перед формулировкой этой теоремы введём определения и докажем лемму.

Пусть F = (W, R) – шкала Крипке, и пусть h, h¢ : P ® P(W) – оценки. Полагая h£h¢, если h(p) £ h¢(p) для всех p Î P, получим отношение порядка на множестве оценок. Если h£h¢, то h называется сужением h¢, а h¢ – расширением h.

Лемма. Пусть А – позитивная формула, F = (W, R) – шкала Крипке, h £ h¢ – оценки, t Î W – произвольный мир. Тогда, если (W, R, h), t |= A, то (W, R, h¢), t |= A.

Доказательство. С помощью индукции по количеству логических связок и модальностей в формуле А. Для атомов р:

(W, R, h), t |= р Þ t Î h(p) Þ t Î h¢(p) Þ (W, R, h¢), t |= р.

Если А = 1, или А = 0, то утверждение справедливо. Случаи А & В и А È В проверяются легко. Случай ØА не возникает в силу позитивности формулы А. Докажем утверждение для ÿА (аналогично для àА), в предположении, что для А оно верно. Пусть (W, R, h), t |= А. Тогда для всех u Î W, для которых tRu, будет верно (W, R, h),
t |= А. Для А утверждение верно, значит, (W, R, h¢), t |= А. Следовательно, (W, R, h¢),
t |= А, что и требовалось доказать.

Мы можем переводить модальные формулы в формулы языка первого порядка.

Пусть х – переменная. Переводом формулы А будет некоторая формула А*(х) языка первого порядка, имеющая не более одной свободной переменной и определённая по индукции:

1) атом р Î Р переводится в р*(х), где р* – символ унарного отношения;

2) 1* = 1; 0* = 0;

3) (ØА)* = Ø(А*);

4) (А & В)* = А* & В*; (А Ú В)* = А* Ú В*;

5) ( А)*(х) = ("y(xRy ® A*(y)));

6) (àА)*(х) = ($y(xRy & A*(y))).

Здесь R – отношение доступности. Например:

( р ® р)*(х) = Ø( р & Øр)*(х) = Ø( р*(х) & Øр*(х)) = Ø("y(xRy ® p*(y)) & Øр*(х));

( (p Ú àq))*(x) = "y(xRy ® (pÚ àq)*(y)) = "y(xRy ® (p*(y) Ú $z(yRz & q*(z)))).

Теорема (о соответствии Салквиста). Каждой формуле Салквиста А соответствует некоторое свойство первого порядка шкал Крипке. Шкала Крипке будет обладать этим свойством тогда и только тогда , когда А будет тавтологией относительно этой шкалы. Существует алгоритм получения этого свойства из формулы А.

Замечание. Салквист установил, что после добавления формулы Салквиста к системе K в качестве аксиомы получается корректная и полная формальная теория.

Доказательство теоремы. Пусть А – несвязная формула. Например:

А = à(àq & à([Øc] & à[ p])) & àà[ p],

где р – позитивная формула. Здесь А построена из строго позитивных p, p, q и негативной Øc формул с помощью & и à. Предположим, что ØА не является тавтологией относительно шкалы F = (W, R). Тогда существует модель (W, R, h) и мир tÎW такие, что M, t |= A. Для нашего примера:

M, t |= à(àq & à(Øc & à[ p])) & àà[ p].

Это означает, что существует схема из шести миров, соответствующих ромбикам, связанных с помощью путей в графе R с миром t. Для этих миров ti справедливы утверждения: M, ti |= Bi, где Bi – либо строго позитивные, как … р, либо негативные, как Øс.

Далее будем использовать префиксную форму записи R(x, y) для xRy. Таким образом, R(x, y) = 1, если и только если (x, y) Î R.

Чтобы получить имена миров, будем использовать стандартный перевод А*(t). В нашем примере А*(t) будет утверждением о существовании миров t1, …, t6, удовлетворяющих следующим условиям:

R(t, t1), R(t1, t2), R(t1, t3), R(t3, t4), R(t, t5), R(t5, t6); M, t2 |= q; M, t3 |= Øс; M, t4| = p; M, t4 |= p.

По лемме, если мы ‘сузим’ h, сделав атомы истинными в меньшем подмножестве миров, то негативные формулы, например Øс, все останутся верными в их собственных мирах в схеме (в нашем примере в t3). Существует наименьшая оценка h, которая сохраняет все полученные формулы истинными в их мирах. Можно доказать, что наименьшая оценка, делающая истинной А в мире t будет из тех, которые делают истинными все строго позитивные формулы … р в их мирах.

В нашем случае истинность р в мире t4 означает, что в каждом мире, доступном за 2 шага из t4, истинна формула р. Значит, р будет истинной для всех х, удовлетворяющих формуле:

$y(R(t4, y) & R(x, y)).

Аналогично р будет означать истинность р для таких х, что R(t6, x). Формула q верна для всех таких х, что х = t2. Таким образом, если мы сделаем p и q верными только в тех мирах, которые строятся по строго позитивным формулам, то А будет верным в мире t.

Эта интерпретация h¢ называется ленивой. Она определяется с помощью формул языка первого порядка:

Мы делаем р истинным в мирах х тогда и только тогда, когда формула:

p*(x) = $y(R(t4, y) & R(y, x)) Ú R(t6, x)

истинна в шкале. А q истинна в x, если и только если x = t2. Значит, q*(x) = (x = t2).

Преобразуем далее формулу A*(t):

1) перемещаем кванторы $ti в начало формулы;

2) заменяем р*(х) нашим ленивым выражением $y(R(t4, y) & R(y, x)) Ú R(t6, x);

3) заменяем р*(y) на формулу $z(R(t4, z) & R(z, y)) Ú R(t6, y);

4) аналогично для подформул р*(z), р*(t), р*(t4) и т.д.;

5) заменяем все q*(х) на x = t2, q*(y) на y = t2 и т.д.;

6) вместо ( … р)* подставляем 1.

Полученную в результате формулу обозначим: a(t). Эквивалентны следующие свойства:

1) (W, R, h), t |= A для некоторых t Î W и h;

2) (W, R, h), t |= A для некоторых t Î W и t1, …, t6;

3) (W, R), t |= a(t) для некоторого t Î W (в смысле классической логики).

В этом случае формула ØА будет тавтологией относительно шкалы (W, R) тогда и только тогда, когда (W, R) |= Ø$ta(t). Мы построили алгоритм, который каждой формуле А сопоставляет формулу a(t), которой должна удовлетворять шкала (W, R).

Опишем шаги алгоритма Салквиста, сопоставляющего формуле ØА формулу Ø$ta(t) для шкалы (W, R), относительно которой формула ØА будет тавтологией.

Будем предполагать, что ØА – формула Салквиста. Например, в случае

ØА = ( р ® р) = Ø([ р] & [Øр])

на входе будет формула Ø([ р] & [Øр]), а на выходе – формула "x R(x, x).

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

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

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

Действия:

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

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

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

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

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

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

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

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

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

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

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

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

р*(х) = (x = t) Ú R(t, x) Ú $x1(R(t, x1) & R(x1, x)) Ú …

Ú $x1$x2…$xm(R(t, x1) & R(x1, x2) & … & R(xm, x)).

Пример 2

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

Пример 3

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

Ø"x(R(t, x) ® р*(x)) = Ø"x"y(R(t, x) ® (R(x, y) ® р*(y))).

Следовательно, a(t) = Ø"x"y(R(t, x) & R(x, y) ® R(t, y)). Утверждение (W, R) |= Øa(t) превращается в

(W, R) |= "t"x"y(R(t, x) & R(x, y) ® R(t, y)).

Пример 4

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

А*(t) = Øp*(t) & $t1(R(t, t1) & p*(t1)).

Переводим $t1 в начало формулы:

А*(t) = $t1(Øp*(t) & R(t, t1) & p*(t1)).

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

(W, R) |= Ø$t$t1(ØR(t1, t) & R(t, t1)).

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

"t"t1(R(t, t1) ® R(t1, t)).

Пример 5

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

A = à(àq & à([Ø( p Ú q)] & à[ p])) & àà[ p].

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

А*(t) = R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & q*(t2) & Øc*(t3) & p*(t4) & p*(t6).

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

р*(х) = $y(R(t4, y) & R(y, x)) Ú R(t6, x);

q*(x) = (x = t2).

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

А*(t) = R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & Ø( p*(t3) Ú q*(t3));

a(t) = $x1$x2$x3$x4$x5$x6(R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & Ø("x(R(t3, x) ® p*(x)) Ú (t3 = t2)) = $x1$x2$x3$x4$x5$x6(R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & Ø("x(R(t3, x) ® $y(R(t4, y) & R(y, x)) Ú R(t6, x)) Ú (t3 = t2))

Пример 6

По заданной формуле Ø(àà[ p] & à[ q] & [Ø( p Ú q)] найдём свойство шкал (W, R), относительно которых эта формула является тавтологией. Положим:

А = àà[ p] & à[ q] & [Ø( p Ú q)];

a(t) = $t1$t2$t3R(t, t1) & R(t1, t2) & p*(t2) & R(t, t3) & q*(t3) & (Ø( p*(t) Ú q*(t))).

Из условий истинности:

p*(t2) = "x(R(t2, x) ® p*(x)),

q*(t3) = "x(R(t3, x) ® q*(x)),

найдём ленивые определения:

p*(x) = R(t2, x); q*(x) = R(t3, x).

Подставляя их в a(t) и учитывая, что p*(t2) = 1 и , q*(t3) = 1, получим:

a(t) = $t1$t2$t3R(t, t1) & R(t1, t2) & R(t, t3) & Ø("x(R(t, x) ® R(t2, x)) Ú R(t3, x)).

Утверждение (W, R) |= Ø$ta(t) приводит к формуле 1-го порядка:

"t"t1"t2"t3(ØR(t, t1) Ú ØR(t1, t2) Ú ØR(t, t3) Ú "x(R(t, x) ® R(t2, x)) Ú R(t3, x).


Упражнения

Найти свойства шкал Крипке, соответствующих формулам:

1) А ® àА (Ответ: $u(wRu));

2) àА ® àА (Ответ: wRu & wRu ® vRu);

3) àА ® А (Ответ: wRv & wRu ® v = u);

4) А ® А (Ответ: wRv ® $u(wRu & uRv));

5) à А ® àА (Ответ: wRv & wRx ® $u(vRu & xRu)).

Темпоральная логика

Для темпоральной логики вместо символа используются символы [F] – «будет» и [P] – «было». Аналогично символу à определяются символы <F> = Ø[F]Ø и
<Р> = Ø[Р]Ø. Модель Крипке M = (W, R, h) была определена как граф вместе с оценкой h : P ® P(W). Напомним, что истинность формул [F]A и [P]A устанавливается с помощью выражений:

M, t |= [F]A, если и только если M, u |= A для всех u Î W, таких, что R(t, u);