Крипке модели

- структуры, состоящие из нек-рого множества обычных моделей для классической логики, упорядоченных между собой нек-рым отношением, н служащие для интерпретации в них различных неклассических логик (интуипионистской, модальных и др.). Точнее, К. м. для языка Lимеют вид [img: http://localhost:8080/file/031210-108.jpg] где S- некоторое непустое множество ("миров", "ситуаций"); R - некоторое бинарное отношение на S(напр., для системы J интуиционистской логики R является частичным порядком, для модальной системы 54 - предпорядком, для системы S5 - отношением эквивалентности); отображение Dсопоставляет каждому [img: http://localhost:8080/file/031210-109.jpg] _ нек-рую непустую область Da. так, что если [img: http://localhost:8080/file/031210-110.jpg] то [img: http://localhost:8080/file/031210-111.jpg] оценка Wсопоставляет всякой индивидной константе аэлемент [img: http://localhost:8080/file/031210-112.jpg] всякой индивидной переменной х- элемент [img: http://localhost:8080/file/031210-113.jpg], для каждого [img: http://localhost:8080/file/031210-114.jpg] всякой пропозициональной переменной р - истинностное значение [img: http://localhost:8080/file/031210-115.jpg] (для системы J требуется также, чтобы если [img: http://localhost:8080/file/031210-116.jpg] то [img: http://localhost:8080/file/031210-117.jpg]), всякой n-местной [img: http://localhost:8080/file/031210-118.jpg] предикатной константе Р- некоторое подмножество [img: http://localhost:8080/file/031210-119.jpg] [для системы J, если [img: http://localhost:8080/file/031210-120.jpg] то [img: http://localhost:8080/file/031210-121.jpg] ], всякой n-местной функциональной константе f - функцию [img: http://localhost:8080/file/031210-122.jpg] [для системы /, если [img: http://localhost:8080/file/031210-123.jpg] то [img: http://localhost:8080/file/031210-124.jpg] есть ограничение [img: http://localhost:8080/file/031210-125.jpg] ]. Для всяких [img: http://localhost:8080/file/031210-126.jpg] и формулы Аязыка Lтакой, что для любой свободной переменной хв А [img: http://localhost:8080/file/031210-127.jpg] индуктивно определяется истинностное значение [img: http://localhost:8080/file/031210-128.jpg]. Для системы Jзначение [img: http://localhost:8080/file/031210-129.jpg] определяется следующим образом: а) если А - элементарная формула, то значение [img: http://localhost:8080/file/031210-130.jpg] уже задано моделью; [img: http://localhost:8080/file/031210-131.jpg] г) [img: http://localhost:8080/file/031210-132.jpg] [img: http://localhost:8080/file/031210-133.jpg] (для всякого [img: http://localhost:8080/file/031210-134.jpg] если [img: http://localhost:8080/file/031210-135.jpg] и д) [img: http://localhost:8080/file/031210-136.jpg] [img: http://localhost:8080/file/031210-137.jpg] (для всякого [img: http://localhost:8080/file/031210-138.jpg] если [img: http://localhost:8080/file/031210-139.jpg] то е) [img: http://localhost:8080/file/031210-140.jpg] (для всяких [img: http://localhost:8080/file/031210-141.jpg] и [img: http://localhost:8080/file/031210-142.jpg] если [img: http://localhost:8080/file/031210-143.jpg] ж) [img: http://localhost:8080/file/031210-144.jpg] (существует [img: http://localhost:8080/file/031210-145.jpg] такое, что [img: http://localhost:8080/file/031210-146.jpg] (здесь [img: http://localhost:8080/file/031210-147.jpg] означает, что оценка W' совпадает с Wвсюду, кроме, быть может, на х). Иногда вместо [img: http://localhost:8080/file/031210-148.jpg] пишут [img: http://localhost:8080/file/031210-149.jpg] Для модальных логик определение [img: http://localhost:8080/file/031210-150.jpg] в случаях (г), (д) и (ж) происходит иначе: [img: http://localhost:8080/file/031210-151.jpg] [img: http://localhost:8080/file/031210-152.jpg] (для всякого [img: http://localhost:8080/file/031210-153.jpg] если [img: http://localhost:8080/file/031210-154.jpg] кроме того, добавляется з) [img: http://localhost:8080/file/031210-155.jpg] (для всякого [img: http://localhost:8080/file/031210-156.jpg] если [img: http://localhost:8080/file/031210-157.jpg] то [img: http://localhost:8080/file/031210-158.jpg] Формула Аназ. истинной в К. м. K=(S, R, D, W).(пишут [img: http://localhost:8080/file/031210-159.jpg]), если [img: http://localhost:8080/file/031210-160.jpg] для всякого [img: http://localhost:8080/file/031210-161.jpg] Для каждой из систем J, 54, 55 справедлива теорема о полноте: всякая формула выводима в этой системе тогда и только тогда, когда она истинна во всех К. м. из соответствующего класса. Существенно, что области [img: http://localhost:8080/file/031210-162.jpg] являются, вообще говоря, различными, поскольку формула [img: http://localhost:8080/file/031210-163.jpg] где хне входит свободно в А, не выводима в системе J, но истинна во всех К. м. с постоянной областью. Система, полученная из J добавлением схемы (*), полна относительно К. м. с постоянной областью (см. [4]). Пропозициональный фрагмент каждой из систем J, S4, S5 является финитно аппроксимируемым, т. е. всякая невыводимая в нем формула опровержима на нек-рой конечной К. м. из соответствующего класса. Понятие "К. м." родственно понятию вынуждения (см. Вынуждения метод). К. м. введены С. А. Крипке (S. A. Kripke).