Опишем формальную теорию, которая называется системой K:
Аксиомы
1) Если А(Р1, …, Рn) – тавтология исчисления высказываний, а В1, …, Вn – модальные формулы, то А(В1, …, Вn) – аксиома системы K (пропозициональные тавтологии).
2) Для любых формул А и В формула 
(А ® В) ® (А ® В) является аксиомой системы K (аксиома нормальности).
Правила вывода
; 
.
Формальная теория, содержащая систему K, называется системой Гильберта.
Строгие системы Гильберта
Добавляя аксиомы к системе K, получаем её усиления. Эти аксиомы соответствуют различным (указанным далее в квадратных скобках) свойствам шкал Крипке (речь о свойствах пойдёт далее):
Т: А ® А [рефлексивность];
D: А ® àА [определённость всюду];
4: А ® А [транзитивность];
В: А ® àА [симметричность];
5: àА ® àА [с аксиомой Т – отношение эквивалентности].
Система К вместе с аксиомой Т обозначается через KТ или S. Такое определение записывается как:
S = K + {А ® А}.
Аналогично, добавляя к K другие аксиомы, получаем следующие системы Гильберта:
K4 = K + {А ® А };
S4 = K + {А ® А, А ® А};
S5 = K + {А ® А, àА ® àА}.
Выводимость. Пусть H – система Гильберта. (Согласно определению, она должна содержать аксиомы и правила вывода системы K).
Определение. Запись 
HA означает, что существует последовательность формул А1, …, Аn таких, что
1) An = A;
2) Каждая формула Ai является либо аксиомой системы H, либо получена аз некоторых формул последовательности A1, …, Ai-1 с помощью правил вывода системы H.
В этом случае А называется теоремой в H, а последовательность A1, …, An – выводом формулы (или доказательством теоремы) А. Число n называется длиной вывода (доказательства).
Пример 1
Последовательность:
A & B ® A, (A & B ® A), (A & B ® A) ® ((A & B) ® A), (A & B) ® 
A
является доказательством длины 4 теоремы (A & B) ® A.
Корректность и полнота систем Гильберта
Можно показать, что 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) (А & В)* = А* & В*; (А Ú В)* = А* Ú В*;
1) (
А)*(х) = ("y(xRy ® A*(y)));
2) (àА)*(х) = ($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);
1) заменяем р*(y) на формулу $z(R(t4, z) & R(z, y)) Ú R(t6, y);
2) аналогично для подформул р*(z), р*(t), р*(t4) и т.д.;
3) заменяем все q*(х) на x = t2, q*(y) на y = t2 и т.д.;
4) вместо (
… р)* подставляем 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)).