Голованов М.И. Нестандартные логики. Реляционная семантика

Подождите немного. Документ загружается.

что W (x

) = V (γ

, ..., p

)). Используя определение истинности формул на модели

Крипке, получаем

∀j(W (α

) = V (α

(γ

, ..., p

)))),

W (β) = V (β(γ

, ..., p

))).

И, следовательно,

∀j(V (α

(γ

)) = K

)&V (β(γ

)) 6= K

Отсюда ∀j(K

(γ

)) и K

6°

β(γ

). Поскольку K

является n-характеристичес-

кой моделью для λ, то r не допустимо в λ. Теорема доказана.

Следствие 12.6. Для любой нормальной модальной логики λ, расширяющей логику

K, правило вывода r допустимо в логике λ тогда и только тогда, когда правило вы-

вода r истинно на канонической модели C

относительно формульно определимых

означиваний.

Однако для того, чтобы применять данный критерий для распознавания допус-

тимых правил вывода в модальных логиках, необходимо было построить удобные в

использовании n-характеристические модели Крипке для модальных логик. Ниже

приведём построение специальной конечной модели Крипке.

Напомним следующие определения и обозначения. Если F =< W, R > и X ⊆ F ,

то X

R≤

:= {a|a ∈ F &(∃b ∈ X)(bRa)}, X

:= {a|a ∈ F &(∃b ∈ X)(bRa)&(∀b ∈

X)¬(aRb)}.

Элемент a фрейма F имеет глубину n, если n - максимальная длина цепи во

фрейме F , начинающейся со сгустка C(a). Слоем глубины n фрейма F называется

множество всех элементов фрейма F глубины n, и обозначается Sl

(F ). Сгустки

фрейма F , входящие в верхний слой Sl

(F ), называют также максимальными в F .

Множество всех элементов фрейма F , глубины не больше n, обозначается следующим

образом: S

(F ). Количество сгустков n-го слоя обозначаем ||Sl

(F )||.

Сгусток C

называется непосредственным R-последователем сгустка C

, ес-

ли C

и нет сгустков C таких, что C

RC, CRC

и ¬(CRC

), ¬(C

RC). Сгусток

называется непосредственным R-предшественником C

Модель M

=< W

, R

, V

> называется открытой подмоделью M

=< W

, R

, V

если выполняется следующее:

1) фрейм < W

, R

> является открытым подфреймом фрейма < W

, R

2) Dom(V

) = Dom(V

3) ∀p ∈ Dom (V

)(V

(p) = V

(p) ∩ W

Основное свойство открытых подмоделей заключается в следующем утвержде-

нии.

Предложение 12.7. 1) Если M

=< W

, R, V > - открытая подмодель модели

=< W

, R, V >, то для каждой формулы α выполняется M

° α влечёт M

α.

2) Если фрейм F

является открытым подфреймом фрейма F

, то λ(F

) ⊆

λ(F

Построение модели Ch

(n), предложенное В.В. Рыбаковым.

Пусть λ - нормальная финитно аппроксимируемая модальная логика, расширяю-

щая K4 и P

:= {p

, ..., p

} - множество пропозициональных переменных. Модель

Крипке Ch

(n) определим следующим образом. Первый слой S

(Ch

(n)) модели

(n) состоит из множества всех сгустков со всевозможными означиваниями V

переменных из P

, которые не имеют дублирующих элементов с тем же самым озна-

чиванием и не имеют сгустков, которые изоморфны, как модели Крипке, причём

каждый сгусток из S

(Ch

(n)) является λ-фреймом. Пусть подмодель S

(Ch

(n))

построена. Построим подмодель S

m+1

(Ch

(n)) следующим образом. Выбираем лю-

бую антицепь Y сгустков из S

(Ch

(n)), имеющую по крайней мере один сгусток

глубины m, и добавляем в S

m+1

(Ch

(n)) сгусток C, полагая C непосредственным

предшественником сгустков из Y. При этом фрейм C

R≤

должен быть λ-фреймом и

если антицепь Y состоит только из одного рефлексивного сгустка C

, то сгусток C

не должен быть подмоделью сгутска C

. Продолжая этот процесс, получаем модель

(n).

Построенная модель обладает следующими свойствами.

Непосредственно из построения модели Ch

(n) следует следующее утверждение.

Предложение 12.8. Пусть λ

, λ

- финитно аппроксимируемые нормальные мо-

дальные логики, расширяющие K4. Тогда если λ

⊆ λ

, то Ch

(n) является от-

крытой подмоделью модели Ch

(n) для любого n.

Теорема 12.9. Для любой модальной логики λ, расширяющей K4, модель Крипке

(n) является n-характеристической.

Доказательство. В силу построения модели Ch

(n) ( добавляли толлько такие

сгустки C, что C

R≤

является λ-фреймом) все теоремы логики λ истинны на модели

(n). Пусть α - формула от n пропозициональных переменных и α 6∈ λ. Тогда в

силу финитной аппроксимируемости логики λ существует конечная модель Крипке

M :=< W, R, V > такая, что < W, R > является λ-фреймом и α не истинна на модели

M. Без ограничения общности можно считать, что Dom(V ) = {p

, ..., p

} на модели

M. Возьмём максимальный сгусток C модели M с элементом a, опровергающим α.

Тогда открытая подмодель a

R≤

модели M опровергает формулу α в силу предполо-

жения 12.7.

Далее индуктивно зададим следующее отображение модели a

R≤

В каждом сгустке склеим все элементы, имеющие одинаковое означивание. Далее

склеим сгустки глубины 1, изоморфные как модели. Полученная модель F

является

p-морфным образом модели a

R≤

и, следовательно, по лемме 12.3 модель F

опро-

вергает формулу α. Очевидно, что S

) является открытой подмоделью модели

(n).

Предположим, что модель F

построена, причём F

является λ-фреймом, глубина

фрейма F

не больше глубины модели M, F

опровергает α и S

) является от-

крытой подмоделью модели Ch

(n). Построим модель F

i+1

из модели F

следующим

образом.

1) Пусть C

- непосредственный последователь сгустка C из Sl

i+1

) такой, что

сгусток C изоморфен подмодели сгустка C

. Склеим все такие сгустки C из Sl

i+1

)

с соответстсвующими подмоделями сгустков C

2) Далее склеим сгустки из Sl

), которые изоморфны как модели и имеют

одинаковые множества непосредственных последователей.

Не трудно видеть, что полученная модель F

i+1

является p-морфным образом

модели F

. Поскольку F

i+1

является p-морфным образом модели F

, то по след-

ствию 12.4 F

i+1

является λ-фреймом. Кроме того, модель F

i+1

опровергает формулу

α и Sl

i+1

) открытая подмодель модели Ch

(n).

Продолжая данный процесс, на некотором шаге m, меньшим или равным глубине

модели M, получим модель, опровергающую формулу α и являющуюся открытой

подмоделью модели Ch

(n). И по указанному ранее предложению Ch

(n) опровер-

гает α. Теорема доказана.

Теорема 12.10. Любой элемент модели Ch

(n) является формульным. Для любой

финитно аппроксимируемой логики λ, расширяющей K4, любой элемент модели

(n) является формульно определимым.

Доказательство проведём индукцией по глубине элементов модели Ch

(n).

Для любого элемента a ∈ |Ch

(n)| определим

p(a) := {i|a °

}

α(a) :=

i∈p(a)

∧

i6∈p(a)

¬p

Покажем, что все элементы глубины 1 формульно определимы. Если a - иррефлек-

сивный элемент (вырожденный сгусток) глубины 1, то формула

β(a) := α(a) ∧ ¤(p

∧ ¬p

)

определяет элемент a, то есть данная формула истинна только на элемент a. Для

каждого невырожденного сгустка C из Ch

(n) определим формулу

α(C) :=

a∈C

3α(a).

Любой элемент a является членом сгустка C(a), порождённого a. Не трудно видеть,

что рефлексивный элемент a глубины 1 определяется формулой

β(a) := α(a) ∧ α(C(a)) ∧ ¤(α(C(a))).

Предположим, что все элементы a глубины не больше i, 1 ≤ i, определяются фор-

мулой β(a). Для каждого элемента a глубины, большей i, определим формулу

δ(a) :=

c∈{a}

3β(c) ∧

c∈S

(Ch

(n))&c6∈{a}

¬3β(c).

Для любого иррефлексивного элемента a из Sl

i+1

(Ch

(n)) определим

β(a) := α(a) ∧ δ(a) ∧ ¤(

c∈{a}

β(c) ∧

c∈S

(Ch

(n))

¬β(c)).

Формула β(a) определяет элемент a в модели Ch

(n). В самом деле, β(a) истинна

на a. Если d °

β(a), то a имеет глубину больше, чем i. Поскольку d °

δ(a), то

d видит только те элементы из S

(Ch

(n)), которые видит элемент a. Далее так

как d °

¤(

c∈{a}

β(c), то любой элемент, достижимый из d, является элементом

из S

(Ch

(n)). Следовательно, d имеет глубину (i + 1) и является иррефлексивным

элементом. Поскольку d °

α(a), то d = a.

Рассмотрим рефлексивный элемент a из Sl

i+1

(Ch

(n)) и сгусток C(a), содержа-

щий a. Для таких элементов a определеим следующие формулы:

γ(i) :=

c∈S

(Ch

(n))

¬β(c),

θ(a) :=

{3(α(d) ∧ δ(a) ∧ γ(i))|d ∈ C(a)}∧

{¬3(α(u) ∧ γ(i))|u ∈ S

(Ch

(n))&∀d ∈ C(a)(p(u) 6= p(d))},

φ(a) := ¤(

c∈{a}

β(c) ∨

d∈C(a)

(α(d) ∧ δ(a) ∧ θ(a))),

β(a) := α(a) ∧ δ(a) ∧ γ(i) ∧ θ(a) ∧ φ(a).

Покажем, что формула β(a) определяется элемент a в Ch

(n). Не трудно видеть,

что β истинна на a. Если d °

β(a), то, в силу d °

γ(i), элемент d имеет глубину

больше, чем i. Элемент d видит только те элементы, глубины не большей i, которые

достижимы из a, поскольку d °

δ(a). Если d является элементом глубины (i + 1),

то C(d) изоморфна C(a), поскольку d °

θ(a). Следовательно, C(d) = C(a) и, в силу

d °

α(a), имеем d = a.

Предположим, что d является элементом глубины ≥ (i + 2). Тогда d видит конеч-

ные элементы d

глубины (i + 1). Все такие элементы d

видят только те элементы

множества S

(Ch

(n)), которые достижимы из d, так как d °

φ(a). Если d ви-

дит два различных сгустка C

и C

глубины (i + 1), то получим противоречие с

d °

φ(a). Таким образом, элемент d видит только один сгусток C

глубины (i + 1).

Следовательно, существует сгусток C(d

) такой, что d видит C(d

) и C(d

) является

непосредственным предшественником C(d

). Тогда d имеет глубину (i + 2) и среди

сгустков глубины (i + 1) видит единственный сгусток C(d

). Поскольку d °

φ(a),

то C(d

) имеет единственного непосредственного последователя (сгусток C(d

)). По

построению Ch

(n) сгусток C(d

) имеет элемент e такой, что p(e) 6= p(c) для всех

c ∈ C(d

), что противоречит условию d °

φ(a). Таким образом, β(a) истинна только

на элементе a.

В завершении доказательства предположим, что λ - нормальная модальная фи-

нитно аппроксимируемая логика, расширяющая K4. По предложению 12.8 Ch

(n)

является открытой подмоделью Ch

(n). Следовательно, все элементы модели Ch

(n)

формульно определимы. Теорема доказана.

Вопросы и задания.

1. Сформулируйте определение p-морфного отображения фрейма F

на F

и мо-

дели M

на M

2. Определите основное свойство p-морфного отображения фреймов и докажите

его.

3. Приведите примеры фреймов F

, F

таких, что F

является p-морфным образом

4. Покажите, что если M

является открытой подмоделью модели M

, то M

° α

влечёт M

° α для каждой формулы α.

5. Покажите, что если фрейм F

является открытым подфреймом фрейма F

, то

λ(F

) ⊆ λ(F

6. Сформулируйте определение n-характеристической модели Крипке и приведи-

те построение специальной модели Крипке Ch

(), предложенной Рыбаковым.

7. Какими свойствами обладает n-характеристическая модель Chλ(n)?

8. Какими свойствами обладает элемент a из n-характеристической модели Ch

(n),

если a °

γ(i), где γ(i) - формула из доказательства теоремы 12.10 и V - означивание

на модели Ch

(n).

9. Какими свойствами обладает элемент a из n-характеристической модели Ch

(n),

если a °

θ(a), где θ(a) - формула из доказательства теоремы 12.10 и V - означивание

на модели Ch

(n).

10. Какими свойствами обладает элемент a из n-характеристической модели Ch

(n),

если a °

φ(a), где φ(a) - формула из доказательства теоремы 12.10 и V - означивание

на модели Ch

(n).

13 Лекция 14. Временные логики, семантика Крип-

ке для временных логик

Напомним, что временные логики могут быть рассмотрены как модальные логики с

двумя ¤-операторами. Язык L

временной логики базируется на языке исчисления

высказываний и имеет дополнительные логические временные связки: F и P, G и H.

Минимальная временная логика T

определяется следующим образом: аксиомами T

являются все аксиомы исчисления высказываний и временные аксиомы

1)G(p → q) → (Gp → Gq),

2)H(p → q) → (Hp → Hq),

3)p → HF p,

4)p → GP p.

Правилами вывода минимальной временной логики T

являются: x, x → y/y, x/Gx,

x/Hx.

Временной логикой является множество формул в языке L

, содержащее T

, и

замкнутое относительно подстановки и всех правил вывода логики T

Семантика Крипке для временных логик может быть получена из семантики

Крипке для нормальных модальных логик.

Произвольный фрейм может быть понят как временной фрейм. Временной

моделью Крипке называется тройка M =< W, R, V >, где < W, R > - фрейм, V -

означивание конечного множества пропозициональных переменных P на W , то есть

V : P → 2

, ∀p ∈ P (V (p) ⊆ W). Отметим, что элементами модели Крипке являются

моменты времени.

Определим истинность формул на элементе a временной модели M =<

W, R, V > индуктивно:

(∀p ∈ P )(∀c ∈ W)((c °

p) ⇔ (c ∈ V (p))),

(∀c ∈ W )((c °

α ∧ β) ⇔ (c °

α)&(c °

β)),

(∀c ∈ W )((c °

α ∨ β) ⇔ (c °

α) ∨ (c °

β)),

(∀c ∈ W )((c °

¬α) ⇔ (c 6°

α),

(∀c ∈ W )((c °

α → β) ⇔ (c 6°

α) ∨ (c °

β)),

(∀c ∈ W )((c °

Gα) ⇔ (∀b ∈ W (cRb ⇒ b °

α))),

(∀c ∈ W )((c °

Hα) ⇔ (∀b ∈ W (bRc ⇒ b °

α))),

(∀c ∈ W )((c °

F α) ⇔ (∃b ∈ W (cRb&b °

α))),

(∀c ∈ W )((c °

P α) ⇔ (∃b ∈ W (bRc&b °

α))).

Другими словами, истинноесть временных формул на модели Крипке понимается

следующим способом:

(c °

Gα) ⇔ в будущем после c всегда истинна формула α,

(c °

Hα) ⇔ в прошлом перед c всегда была истинна α,

(c °

F α) ⇔ в будущем после c будет момент времени такой, что формула α

будет истинна,

(c °

P α) ⇔ в прошлом перед c был момент времени такой, что формула α была

истинна.

Не трудно видеть, что G := ¬F ¬, H := ¬P ¬ и справедливы следующие экви-

валентности Gα ≡ ¬F ¬α, Hα ≡ ¬P ¬α, F α ≡ ¬G¬α, P α ≡ ¬H¬α в минимальной

временной логике T

Будем говорить, что временная формула α истинна на модели Крипке M =<

W, R, V > (обозначение M ° α) тогда и только тогда, когда для каждого c ∈ W

выполняется c °

α. Временная формула α истинна на фрейме F (обозначение

F ° α), если α истинна на любой модели Крипке, фреймом которой является F .

Фрейм F является адекватным для временной логики λ, если для любой α ∈ λ

выполняется F ° α. Класс фреймов K называется адекватным для временной логики

λ, если любой фрейм из K является адекватным для λ.

Введём следующие логики:

0,W

:= T

⊕ {Gp → p, Hp → p},

0,K4

:= T

⊕ {Gp → GGp, Hp → HHp},

0,S4

:= T

0,W

⊕ {Gp → GGp, Hp → HHp}.

Прежде, чем рассмотреть теорему об адекватных классах фреймов для времен-

ных логик T

, T

0,W

, T

0,K4

, T

0,S4

сформулируем утверждения, необходимые для дока-

зательства этой теоремы, которые были разобраны в предыдущих лекциях.

Лемма 13.1. Для любого класса Ω фреймов множество

{α|α ∈ F or

, (∀F ∈ Ω)F ° α}

замкнуто относительно правил вывода: x, x → y/y и x/¤x.

Лемма 13.2. Если F - фрейм и α - модальная формула, полученная подстановкой

некоторых аксиом из списка аксиом исчисления высказываний, то F ° α.

Теорема 13.3. 1) Класс всех фреймов является адекватным для логики K.

2) Класс всех рефлексивных фреймов является адекватным для логики T .

3) Класс всех транзитивных фреймов является адекватным для логики K4.

4) Класс всех рефлексивных и транзитивных фреймов является адекватным для

логики S4.

5) Класс всех фреймов с отношением эквивалентности как отношением дости-

жимости является адекватным для логики S5.

Теорема 13.4. 1) Класс всех фреймов является адекватным минимальной времен-

ной логике T

2) Класс всех рефлексивных фреймов является адекватным временной логике

0,W

3) Класс всех транзитивных фреймов является адекватным временной логике

0,K4

4) Класс всех рефлексивных и транзитивных фреймов является адекватным

временной логике T

0,S4

Доказательство. Достаточно показать, что все аксиомы временных логик T

0,W

, T

0,K4

, T

0,S4

истинны на всех соответствующих фреймах и правила вывода x, x →

y/y, x/Gx, x/Hx сохраняют истинность. В силу леммы 13.1 правило вывода x, x →

y/y сохраняет истинность в произвольном фрейме. Аналогично доказательству со-

хранения истинности формулы относительно правила x/¤x (см. теорему об адекват-

ных фреймах модальным логикам), можно показать, что правила x/Gx, x/Hx также

сохраняют истинность в произвольном фрейме. Далее, силу леммы 13.2 достаточно

рассмотреть истинность специальных временных аксиом на соответстсвующих фрей-

мах.

1) Временными аксиомами логики T

являются:

1)G(p → q) → (Gp → Gq),

2)H(p → q) → (Hp → Hq),

3)p → HF p,

4)p → GP p.

По теореме 13.3 класс всех фреймов является адекватным для логики K. Следо-

вательно, формула ¤(p → q) → (¤p → ¤q) истинна на всех фреймах. Логическую

связку G мы можем интерпретировать, как связку ¤ в любом заданном фрейме,

следовательно, аксиома 1) истинна на всех фреймах. Для любой заданной модели

M :=< W, R, V > истинность формулы Hp соответствует истинности формулы ¤p

в модели M

−1

:=< W, R

−1

, V >. Следовательно, аксиома 2) истинна на M. Пусть

M :=< W, R, V > - модель Крипке и α - временная формула. Предположим, что

a ∈ W и a °

α. Пусть b ∈ W и aRb. Тогда по определению временной связки F

имеем b °

F α и, следовательно, a °

HF α. Таким образом, для любого a ∈ W ,

a °

α → HF α, то есть аксиома 3) истинна на M. Далее, если a °

α и aRb, то

b °

P α. Следовательно, a °

GP α и аксиома 4) истинна на каждом фрейме.

2) Предположим, что F :=< W, R > - рефлексивный фрейм. В силу пункта 1)

все аксиомы логики T

истинны на F . По теореме 13.3 (пункт 2) модальная формула

¤p → p истинна на фрейме F . Поскольку истинностное значение формулы ¤γ со-

ответствует истинностному значению формулы Gγ, то формула Gp → p истинна на

F . Рассмотрим фрейм F

−1

:=< W, R

−1

>. Данный фрейм является рефлексивным,

следовательно, формула ¤p → p истинна на F

−1

. Истинностное значение формулы

¤γ во фрейме F

−1

соответствует истинностному значению формулы Hγ в F , следо-

вательно, Hp → p истинна во фрейме F . Пункт 2) доказан.

3) Пусть F :=< W, R > - транзитивный фрейм. Тогда по теореме 13.3 (пункт 3),

применяя рассуждения пункта 2) данной теоремы, получаем, что Gp → GGp истин-

на на фрейме F . Фрейм F

−1

:=< W, R

−1

> является также транзитивным. Следо-

вательно, по теореме 13.3 формула ¤p → ¤¤p истинна на F

−1

. Отсюда формула

Hp → HHp истинна на фрейме F .

Справедливость пункта 4) следует из пунктов 2) и 3). Теорема доказана.

Определение 13.5. Пусть λ - временная логика.

(i) Класс фреймов C называется характеристическим для логики λ, если

λ := λ(C) := {α|α ∈ F or

, (∀F ∈ C)(F ° α)}.

(ii) Временная логика λ полна по Крипке, если существует класс фреймов ха-

рактеристический для логики λ.

Далее будет показано, что логики T

, T

0,W

, T

0,K4

, T

0,S4

полны по Крипке. Для

доказательства этого утвержедения понадобятся определение множества временных

формул совместного с аксиоматической временной системой, определение полной

временной теории для заданной временной аксиоматической теории и следующие

два утвержедения:

Определение 13.6. Множество S временных формул совместно с временной ак-

сиоматической системой AS, если для любой последовательности α

, ..., α

формул

из S выполняется следующее

¬(α

∧ α

∧ ... ∧ α

Определение 13.7. Множество временных формул S называется полной модаль-

ной теорией для временной аксиоматической системы AS, если

1) Множество S совместно с AS,

2) Для любой временной формулы α справедливо α ∈ S либо ¬α ∈ S.

Лемма 13.8. Пусть AS - аксиоматическая система для временной логики λ.

(i) Если S - полная временная теория для AS, то S является максимальным

совместным с AS множеством формул.

(ii) Если S - максимальное совместное с AS множество временных формул, то

S является полной временной теорией для AS.

(iii) Если S - совместное с AS множество временных формул, то существует

полная временная теория S

, расширяющая S.

(iv) Если S - полная временная теория для AS, то выполняется следующее:

1) (∀α)(`

α ⇒ α ∈ S),

2) (α ∈ S&α → β ∈ S) ⇒ β ∈ S,

3) α ∧ β ∈ S ⇔ (α ∈ S&β ∈ S),

4) α ∨ β ∈ S ⇔ (α ∈ S ∨ β ∈ S),

5) α → β ∈ S ⇔ (α 6∈ S ∨ β ∈ S),

6) ¬α ∈ S ⇔ α 6∈ S,

7) ∀α((α ∈ S) ∨ (¬α ∈ S)).

Лемма 13.9. Пусть S - полная временная теория для аксиоматической временной

системы AS совместной временной логики λ.

(i) Пусть GS := {α|Gα ∈ S} и β - формула такая, что ¬Gβ ∈ S. Тогда суще-

ствует полная временная теория S

такая, что SG ⊆ S

и ¬β ∈ S

(ii) Пусть HS := {α|Hα ∈ S} и β - формула такая, что ¬Hβ ∈ S. Тогда

существует полная временная теория S

такая, что HG ⊆ S

и ¬β ∈ S

Учитывая связь модальной логической связки ¤ и временных связок, получаем,

что доказательство леммы 13.8 и леммы 13.9 повторяет доказательство аналогичных

лемм для модального случая.

Определение 13.10. Пусть λ - временная логика с аксиоматической системой

AS, C

- множество всех полных временных теорий для AS. Канонической мо-

делью Крипке для AS является модель M

:=< C

, R, V > такая, что

V (p) := {T

∈ C

, p ∈ T

⇔ ((∀α )(Gα ∈ T

⇒ α ∈ W

)&(∀β)(Hβ ∈ W

⇒ β ∈ T

)).

Теорема 13.11. (теореме о канонической модели для временных логик) Для лю-

бой временной формулы α и любой полной временной теории T

из модели M

выполняется следующее

α ⇔ α ∈ T

Доказательство проведём индукцией по длине формулы α . Для логических

связок ∧, ∨, →, ¬ и пропозициональной переменной p доказательство аналогично

случаям, рассмотренным в теореме о канонической модели для модальных логик.

Рассмотрим формулы вида Gβ и Hβ.

Предположим, что T

Gβ и Gβ 6∈ T

. Поскольку T

- полная временная теория,

то ¬Gβ ∈ T

. Тогда по лемме 13.9 (i) существует полная временная теория T

c,G

такая,

что GT

⊆ T

c,G

и ¬β ∈ T

c,G

. Покажем, что T

c,G

. В самом деле, из определения

имеем, что γ ∈ T

c,G

для всех формул γ таких, что Gγ ∈ T

. Пусть δ - формула такая,

что Hδ ∈ T

c,G

. Предположим, что δ 6∈ T

. Поскольку T

- полная временная теория,

то ¬δ ∈ T

. Так как

¬δ → G¬H¬¬δ

и, следовательно,

¬δ → G¬Hδ.

Применяя (iv) из леммы 13.8, получаем G¬Hδ ∈ T

. По определению GT

справед-

ливо ¬Hδ ∈ T

c,G

. Таким образом, Hδ, ¬Hδ ∈ T

c,H

, что противоречит совместности

c,H

. Следовательно, δ ∈ T

и T

c,G

. Поскольку ¬β ∈ T

c,G

и T

c,G

совместно, то

β 6∈ T

c,G

и по индуктивному предположению имеем, что T

c,G

6°

β. Так как T

c,G

то T

6°

Gβ, что противоречит предположению. Таким образом, Gβ ∈ T

Обратно, пусть Gβ ∈ T

и T

. Тогда β ∈ W

и по индуктивному предположе-

нию W

β. Следовательно, T

Gβ.

Рассмотрим случай временной связки H. Пусть T

Hβ. Предположим, что

Hβ 6∈ T

. Поскольку T

- полная временная теория, то ¬Hβ ∈ T

. Тогда по (ii)

леммы 13.9 существует полная временная теория T

c,H

такая, что HT

⊆ T

c,H

и 6= β ∈

c,H

. Покажем, что T

c,H

. По определению для всех формул γ таких, что Hγ ∈ T

выполняется γ ∈ T

c,H

. Предположим, что δ 6∈ T

. Поскольку T

- полная временная

теория, то ¬δ ∈ T

. Для системы AS справедливо:

¬δ → H¬G¬¬δ

¬δ → H¬Gδ.

Следовательно, по (iv) леммы 13.8 имеем H¬Gδ ∈ T

. Тогда по определению HT

вы-

полняется ¬Gδ ∈ T

c,H

. Откуда следует, что Gδ, ¬Gδ ∈ T

c,H

и противоречит совмест-

ности T

c,H

. Следовательно, δ ∈ T

и T

c,H

. Поскольку ¬β ∈ T

c,G

и T

c,H

совместно,

то β 6∈ T

c,H

. Отсюда по индуктивному предположению имеем, что T

c,H

6°

β. Так как

c,H

, то T

6°

Hβ, что противоречит предположению. Следовательно, Hβ ∈ T

Обратно, пусть Hβ ∈ T

и W

. Тогда β ∈ W

и по индуктивному предположе-

нию W

β. Следовательно, T

Hβ. Теорема доказана.

Будем говорить, что модель Крипке M является характеристической для вре-

менной логики λ, если множество всех теорем логики λ совпадает с множеством всех

формул, истинных на M на всех элементах.

Теорема 13.12. Пусть λ - временная логика с аксиоматической системой AS.

Каноническая модель C

является характеристической моделью для временной

логики λ.

Доказательство. Пусть α - теорема логики λ. Тогда `

α и по лемме 13.8 имеем,

что α ∈ T

, где T

- полная временная теория. По теореме 13.11 получаем T

α.

Следовательно, все теоремы логики λ истинны на модели C

Обратно, пусть α 6∈ λ. Тогда множество {¬ α} совместно с AS. И по лемме 13.8

(пункт (iii)) существует полная временная теория T

, содержащая ¬α. Отсюда по

теореме 13.11 получаем, что T

¬α и α ложна на модели C

на элементе T

Теорема доказана.

Теорема 13.13. Логики T

, T

0,W

, T

0,K4

, T

0,S4

полны по Крипке.

1) Класс всех фреймов является характеристическим для логики T

2) Класс всех рефлексивных фреймов является характеристическим для логики

0,W

3) Класс всех транзитивных фреймов является характеристическим для логики

0,K4

4) Класс всех рефлексивных и транзитивных фреймов является характеристи-

ческим для логики T

0,S4

Доказательство. По теоремам 13.4 и 13.12 достаточно показать, что фреймы со-

ответствующих канонических моделей Крипке принадлежат соответствующим клас-

сам фреймов.

Пункт 1) очевиден. Учитывая связь ¤ и временных связок G и H, доказательство

пунктов 2)-4) повторяет доказательство соответствующих пунктов теоремы полноты

для модальных логик. Теорема доказана.

Вопросы и задания.

1. Пусть M - временная модель Крипке и a - элемент из |M|. Тогда

а) a °

Gα ⇔ a °

¬F ¬α,

б) a °

Hα ⇔ a °

¬P ¬α,

в) a °

F α ⇔ a °

¬G¬α,

г) a °

P α ⇔ a °

¬H¬α.

2. Покажите, что

а) T

⊂ T

0,W

⊂ T

0,S4

б) T

⊂ T

0,K4

⊂ T

0,S4

в) T

0,K4

6⊆ T

0,W

, T

0,W

6⊂ T

0,K4

3. Покажите, что

а) G> ∈ T

, H> ∈ T

, F > 6∈ T

0,K4

, P > 6∈ T

0,K4

;

б) F > ∈ T

0,W

, P > ∈ T

0,W

;

в) F p → P p 6∈ T

, GF p → F p 6∈ T

0,K4

4. Укажите адекватные классы фреймов для временных логик T

, T

0,W

, T

0,K4

0,S4

и обоснуйте почему.

5. Сформулируйте теорему о канонической модели для временных логик и дока-

жите данное утверждение для случая временной формулы.

6. Почему каноническая модель Крипке временной логики является характери-

стической?

7. Укажите связь модальной логической связки ¤ и временных связок H, G?