Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

ется понятие возможного мира. Под возможным миром понимается мыслимое положение дел или возможный ход развития событий (состоятий). § 8. Модели Крипке Среди различных семантических интерпретаций модальных логик важное место занимает семантика (модель) Крипке. Модели Крипке являются некото­ рыми (по крайней мере, терминологическими) подходами к моделям возмож­ ных миров. Пусть Р - множество (атомарных) высказываний. Моделью Крипке над множеством Р высказываний называется система: М= (S,R,L), где 1)5"- конечное множество состояний (или множество возможных миров); 2) R - бинарное отношение переходов, которое обязано быть тотальным, т.е. для каждого состояния seS должно существовать такое состояние s 'eS, что имеет место sRs' (или, что мир s ' достижим из мира 5'); 3) L: 8^2^ - функция, которая помечает каждое состояние, множеством атомарных высказываний, истинных в этом состоянии. Иногда при определении модели Крипке вводят еще множество начальных состояний SonS. Иногда же модель Крипке задают, полагая, что М= {S,R), где S и R заданы как выше по 1), 2) и полагая известным, что функция L задана со­ гласно 3). Последовательность п = S0SiS2... - путь в модели Крипке из состояния sq , если для всех i, i>0, {Si,Si+i) е R. По определению необходимость в модели Крипке означает истинность во всех достижимых мирах, а возможность - истинность хотя бы в одном из дос­ тижимых моров. Таким образом, в модели Крипке оператор необходимости ве­ дет себя как квантор всеобщности, а оператор возможности - как квантор су­ ществования. Рис. 6.6. Граф переходов или модель Крипке Рис.6.7. Бесконечное дерево, развернутое из графа переходов 208