Формула оЛ читается как «возможно Л».

Модальное исчисление, содержащее правило вывода Гёделя, называется нормальным. В противном случае ненормальным.

Исчисление S4, расширенное за счет добавления аксиомы Брауэра, эквивалентно исчислению S5 [44, с.255].

Теорема 3.1. Исчисления Т, S4 и S5 непротиворечивы.

Доказательство дано в [17, с.46].

3.3.4. Означивание формул

Пусть дана формула A{Xi,Хп). Означивание формулы Л - это отображение

Vm{A) : {0,1, ...,т}" {0,1,та}.

Другими словами, пропозициональным переменным Хг и самой формуле А придаются значения из множества {0,1, ...,та} по некоторым правилам. Значению О соответствует Т (истина).

Формула А называется та-общезначимой, если А = 0 при любых значениях своих переменных. Обозначение:

Означивание Vm называется характеристическим, если оно удовлетворяет двум условиям:

a) при та = 1 для формул без знаков П, О оно совпадает с классическими таблицами истинности;

b) класс теорем совпадает с классом та-общезначимых формул.

Теорема 3.2. Означивание

Dm (Л &В) = max(t)m(A),mm(B)); «m(AVB) =min(«™(A),TOm(B));

\ TO, г)т(Л) 0;

1 то, «ni(.4) = то.

удовлетворяет условию а) определения характеристического означивания.

Теорема 3.3. В модальных исчислениях Т, S4 и S5 если h Л, то И™ Л(то> 1).

Доказательство дано в [17, с.47].

Теорема 3.4. В исчислениях Т, S4 и S5 нет характеристического Vm-означивания.

Доказательство дано в [17, с.48].

Следствие 3.1. Модальные исчисления Т, S4 и S5 бесконечнознач-ны относительно Vm-означивания. Они отличны от классической логики и близки к интуиционистской.

3.3.5. Семантика Крипке

Среди различных семантических интерпретаций модальных логик особое место занимает семантика Крипке.

Крипке строит модели вида < W,R,G,v >, где W - фиксированное непустое множество, R - рефлексивное бинарное отношение на W, т.е. R G W X W, G а W - фиксированный элемент и « -Т-означивание формул, описываемое ниже. Для этого рассматриваются пары {A,w), где А = A(Xi,Хп) - формула и ю е W.

Элемент w трактуется как возможный мир. Поэтому W - это множество возможных миров. Элемент G называем действительным миром. Истинность отношения R(w,w) означает достижимость мира w из мира w.

Т-означивание - это отображение v{A,w) : {±, Т}" {±,Т}, задаваемое следующим образом:

v{-iA, w) =Т <= v{A, w) = ±;

v{A&i.B, w) =Т <= v{A, w) = v{B, w) = T;

v{Ay B,w) = T <= v{A,w) = T или v{B, w) = T;

v{A=> B,w) =T - v{A, w) = ± или v(B, w) = T;

v{DA,w) = T <= v{A,w) = T для любого w с R{w,w);

v{-iDA,w) = T <= v{A,w) = ± для любого w с R{w,w)\

v{oA,w) = T -( v{A,w) = T хотя бы для одного w с R{w,w)\

v{-i OA,w) = T <==> v{A,w) = ± хотя бы для одного w с R{w,w).

Как видим, высказывание необходимо, если оно «истинно во всех возможных достижимых мирах», и возможно, если оно истинно хотя бы в одном мире. Семантика Крипке реализует идеи Лейбница.

Если дополнительно потребовать, чтобы отношение R было симметричным, то имеем брауэровское означивание; в случае рефлексивного и транзитивного R - 84-означивание. Наконец, для рефлексивного, симметричного и транзитивного R получаем S5 -означивание.

Множество формул S Т-выполнимо (соотв.: S4-, S5-выполнимо), если и только если существует Т-означивание (соотв.: S4-, 85-означивание) такое, что для всякой А. € S имеем ii{A, G) = Т, и невыполнимо в противном случае.

Формула А 1-обще значима тогда и только тогда, когда множество формул {->А] невыполнимо. Символически Т-общезначимость записывается в виде:

Теорема 3.5. В исчислениях Т, S4 и S5 если \- А, тю \= А.

Доказательство дано в [17, с.50]. Следствие 3.2. Модальные исчисления Т, S4 и S5 непротиворе-