|
где Dom • область интерпретации, Dorn" • n-я декартова степень множества Dom и P(Domn) множество всех подмножеств множества Dorn". Таким образом, ори любом конкретном присваивании часов, для любого t е ск (р) в соответствии с данным частичным отображением найдётся некоторое подмножество множества Domn, между тем, как для моментов времени, не входящих в ск (р), образ не определён. Формула определяется только на моменты времени, появляющиеся на ее часах при данном присваивании часов. Поэтому для данных часов t еш значение формулы может быть истина ложно или неопределено в зависимости от локальных часов, ассоциированных с ней в соответствии с определением 5. Временная интерпретация совместно с присваиванием часов присваивает значения всем основным элементам TLC. По определению нотация [X Y] обозначает множество функций из множества X в множество Y. Определение 7. Временная интерпретация I любой формулы TLC при данном присваивании часов ск определяется посредством задания некоторого непустого множества Dom, называемого областью интерпретации, и установления однозначного соответствия: (1) между каждой индивидной константой и элементом Dom; (2 ) между каждым m-местными функциональным символом и элементом [Dornm D om ]; (3) между каждым п-местным предикатным символом р и элементом [ск(р) Р( Dom")]. Дадим определение отношения выполнимости 1= . Нотация t А будет означать, что формула А истинна в момент времени teckj при данной временной интерпретации I . Когда ckj не пустая последовательность, используется нотация K,ckj А для обозначения факта, что А истинна для любого момента времени на локальных часах ckj при временной 155 |
В дальнейшем для простоты представления будем использовать нотацию скА в для скЛ i скв и ск^д для cknextа • Из определений 1-5 следует, что ckBvc = скв_>с = скВос = сквс и для квантора существования 3 имеем ск(ЗХ )В= скв. Справедливо утверждение, что каждое присваивание часов индуцирует однозначное соответствие каждой формулы TLC некоторым конкретным локальным часам [167]. Определение 6. Для данных локальных часов ck¡ Инверсно, можно записать t„ ~ ck,(n), что означает, что tn является моментом времени на локальных часах ck¡, имеющим ранг п. Для глобальных часов gck имеем: rank (t, gck) = t и gck(t)= t. Интерпретация формул (семантика) вводится следующим образом. В TLC значением любого предикатного n-местного символа р фактически является частичное отображение из со в P(Domn), где Dora область интерпретации, Dom" n-я декартова степень множества Dom и P(Dom") множество всех подмножеств множества Dom". Таким образом, при любом конкретном присваивании часов, для любого t е ск (р) в соответствии с данным частичным отображением найдётся некоторое подмножество множества Dom", между тем, как для моментов времени, не входящих в ск (р), образ не определён. Формула определяется только на моменты времени, появляющиеся на ее часах при данном присваивании часов. Поэтому для данных часов te w значение формулы может быть истина , ложно или неопределено в зависимости от локальных часов, ассоциированных с ней в соответствии с определением 5. 90 Временная интерпретация совместно с присваиванием часов присваивает значения всем основным элементам TLC. По определению нотация [X — » Y] обозначает множество функций из множества X в множество Y. Определение 7. Временная интерпретация I любой формулы TLC при данном присваивании часов ск определяется посредством задания некоторого непустого множества Dom, называемого областью интерпретации, и установления однозначного соответствия: (1) между каждой индивидной константой и элементом Dom; (2 ) между каждым m-местными функциональным символом и элементом [Domrn — > Dom] ; (3) между каждым n-местным предикатным символом р и элементом [ck(p) -> Р( Dom")]. Дадим определение отношения выполнимости 1= . Нотация (=i,C ki, t А будет означать, что формула А истинна в момент времени teck¡ при данной временной интерпретации I . Когда ck¡ не пустая последовательность, используется нотация Ц cki А для обозначения факта, что А истинна для любого момента времени на локальных часах ck¡ при временной интерпретации I. Для обозначения факта, что Ц,С 1« А для любой временной интерпретации I используется нотация bdd А. В частности, если =[ck¡А , то говорят , что временная интерпретация I на ск есть модель формулы А. Используется также нотация Ц для обозначения того, что I есть модель формулы А, а также 1=А для обозначения того, что для любой модели имеем Ц А. Определение 8. Пусть I временная интерпретация при данном присваивании часов ск, А и В формулы TLC. Семантика элементов TLC определяется рекурсивно следующим образом: 91 |