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

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

Лемма 10.10. Модальные логики K, T , K4, S4, S5 обладают свойством фильтра-

ции.

Доказательство. Пусть λ ∈ {K, T, K4, S4, S5}. По теореме о канонической мо-

дели и теореме полноте для модальных логик фрейм канонической модели

логики

λ является λ-фреймом и

- модель,

- рефлексивная модель,

- транзитивная модель,

- рефлексивная и транзитивная модель,

имеет отношение эквивалентности как отношение достижимости.

Пусть S - конечное множество формул, замкнутое по подформульности.

Рассмотрим минимальную нормальную модальную логику K. Возьмём макси-

мальную фильрацию C

K,a,S

по S открытой подмодели C

K,a

модели C

, порождённой

произвольным элементом a. Ясно, что C

K,a,S

- конечная модель и её фрейм адекватен

K. Следовательно, K обладает свойством фильтрации.

Любая фильтрация произвольной рефлексивной модели должна быть рефлек-

сивной моделью. По теореме о полноте максимальная фильтрация C

T,a,S

по S про-

извольной открытой подмодели C

T,a

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

порождена конечным

T - фреймом и, следовательно, T имеет свойство фильтрации.

В случае если λ = K4, S4, то определим отношение R

между классами [w]

≡

эле-

ментов открытой подмодели C

λ,a

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

, порождённой элементом

a, следующим образом:

([w]

≡

[v]

≡

) ⇔ ∀¤α ∈ S(w °

¤α ⇒ v °

¤α ∧ α).

По теореме о полноте C

транзитивна. Поэтому R

удовлетворяет пунктам 1), 2) из

определения фильтрации и R

задаёт фильтрацию M модели C

λ,a

по S. Пусть λ =

K4. Докажем, что M транзитивна. Предположим, что [a]

≡

[b]

≡

и [b]

≡

[c]

≡

Пусть ¤α ∈ S и a °

¤α. По определению отношению R

имеем b °

¤α ∧ α и,

следовательно, b °

¤α и b °

α. Отсюда вновь по определению отношения R

получаем, что c °

¤α ∧ α. Таким образом, [a]

≡

[c]

≡

. Следовательно, фрейм

модели M является транзитивным и K4 обладает свойством фильтрации.

В случае λ = S4 транзитивность модели M доказывается аналогично преды-

дущему. Фильтрация рефлексивной модели является рефлексивной. В самом деле,

пусть ¤α ∈ S и a °

¤α. Отношение R модели C

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

тельно, aRa и a °

α. Тогда из определения отношения R

имеем [a]

≡

[a]

≡

и R

рефлексивно. Таким образом, M рефлексивно и S4 обладает свойством фильтрации.

Для логики S5 определим отношение R

между классами [w]

≡

элементов из

S5,a

(открытой подмодели канонической модели C

, порождённой элементом a)

следующим образом:

([w]

≡

[v]

≡

) ⇔ ∀¤α ∈ S(w °

¤α ⇒ v °

¤α).

По теореме о полноте C

имеет отношение эквивалентности как отношение достижи-

мости. Следовательно, R

удовлетворяет условиям 1), 2) определения фильтрации

и, значит, R

задаёт фильтрацию M модели C

S5,a

по S. Рефлексивность, транзи-

тивность и симметричность отношения R

следует непосредственно из его задания.

Значит, S5 обладает свойством фильтрации. Лемма доказана.

Из данной леммы, теоремы Харропа, теоремы 10.9 получаем

Следствие 10.11. Модальные логики K, T , K4, S4, S5 финитно аппроксимируемы

и разрешимы.

Лемма 10.12. Суперинтуиционистские логики H, KC, LC обладают свойством

фильтрации.

Доказательство. Пусть λ ∈ {H, KC, LC}. По теоремам о канонической модели

и полноте для суперинтуиционистских логик фрейм канонической модели C

для

логики λ является λ-фреймом и

- интуиционистская модель,

- интуиционистская модель, удовлетворяющая условию:

∀x∀y∀z((xRy)&(xRz) ⇒ ∃t((yRt)&(zRt))),

- интуиционистская модель, удовлетворяющая условию:

∀x∀y∀z((xRy)&(xRz) ⇒ ((yRz) ∨ (zRy))).

Пусть S - конечное множество формул, замкнутое по подформульности. Пусть a -

произвольный элемент канонической модели C

. Возьмём максимальную интуицио-

нистскую фильтрацию C

λ,a,S

по S открытой подмодели C

λ,a

канонической интуи-

ционистской модели Крипке C

для λ, порождённой элементом a. Ясно, что для

любой логики λ из {H, KC, LC} модель C

λ,a,S

является конечной интуиционистской

моделью.

Фрейм модели C

H,a,S

является H-фреймом и, следовательно, H обладает свой-

ством фильтрации.

Фрейм модели C

удовлетворяет условию

∀x∀y∀z((xRy)&(xRz) ⇒ ∃t((yRt)&(zRt))).

Отсюда в силу пункта 1) определения фильтрации фрейм модели C

KC,a,S

также удо-

влетворяет условию

∀x∀y∀z((xRy)&(xRz) ⇒ ∃t((yRt)&(zRt))).

И по теореме о полноте для суперинтуиционистских логик фрейм модели C

KC,a,S

является KC-фреймом. И логика KC обладает свойством фильтрации.

Модель C

удовлетворяет условию

∀x∀y∀z((xRy)&(xRz) ⇒ ((yRz) ∨ (zRy))).

Поэтому в силу пункта 1) определения фильтрации фрейм модели C

KC,a,s

удовлет-

воряет формуле

∀x∀y∀z((xRy)&(xRz) ⇒ ((yRz) ∨ (zRy))).

Примення теорему о полноте, получаем, что фрейм модели C

LC,a,S

является LC-

фреймом и логика LC обладает свойством фильтрации. Лемма доказана.

Из леммы 10.12, теоремы Харропа, теоремы 10.9 получаем

Следствие 10.13. Суперинтуиционистские логики H, KC, LC финитно аппро-

ксимируемы и разрешимы.

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

1. В чём заключается свойство финитной аппроксимируемости логики?

2. Укажите связь между финитно аппроксимируемыми логиками и логиками пол-

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

3. Сформулируйте и докажите теорему Харропа.

4. Дайте определение финитно аппроксимируемой по Крипке логики.

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

мируемости логики по Крипке.

6. Дайте определения фильтрации, а также максимальной и минимальной филь-

трации.

7. Сформулируйте лемму о фильтрации.

8. Приведите схему доказательства леммы о фильтрации.

9. Дайте определение логики, обладающей свойством фильтрации.

10. Какие модальные логики обладают свойством фильтрации?

11. Какие модальные логики являются финитно аппроксимируемыми и почему?

12. Какие модальные логики являются разрешимыми и почему?

13. Какие суперинтуиционистские логики обладают свойством фильтрации и по-

чему?

14. Какие суперинтуиционистские логики являются финитно аппроксимируемы-

ми и разрешиыми?

11 Лекция 12. Характеристические классы фреймов

для некоторых расширений модальных логик K,

T , K4, S4

Рассмотрим следующие расширения модальных логик K, T , K4, S4:

B := T ⊕ p → ¤3p,

D := K ⊕ ¤p → 3p,

K4.1 := K4 ⊕ ¤3p → 3¤p,

K4.2 := K4 ⊕ 3¤p → ¤3p,

K4.3 := K4 ⊕ ¤(¤p → q) ∨ ¤(¤q → p),

S4.1 := S4 ⊕ ¤3p → 3¤p,

S4.2 := S4 ⊕ 3¤p → ¤3p,

S4.3 := S4 ⊕ ¤(¤p → q) ∨ ¤(¤q → p).

Прежде, чем перейти к рассмотрению основных результатов данной лекции, на-

помним некоторые утверждения, доказанные в предыдущих лекциях.

Теорема 11.1. Для любой нормальной модальной логики λ и любой аксиоматиче-

ской системы AS для λ выполняется следующее: каноническая модель C

являет-

ся характеристической моделью Крипке для λ.

Лемма 11.2. Для каждого множества формул S, совместного с модальной ак-

сиоматической системой AS, существует полная модальная теория S

для AS,

содержащая множество S.

Лемма 11.3. (о полной модальной теории) Пусть 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)).

Теорема 11.4. (теореме о канонической модели) Для любой формулы α и любой

полной модальной теории T

в модели M

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

α ⇔ α ∈ T

Перейдём к теоремам полноты для логик, указанным в начале лекции.

Теорема 11.5. Логики B, D полны по Крипке.

1) Класс F r

всех рефлексивных фреймов, удовлетворяющих условию

∀x∀y(xRy ⇒ yRx),

является характеристическим для логики B.

2) Класс F r

всех фреймов, удовлетворяющих условию

∀x∃y(xRy),

является характеристическим для логики D.

Доказательство. 1) Пусть F - произвольный фрейм из класса Fr

. Фрейм F

адекватен логике B, так как, очевидно, формула p → ¤3 истинна на F . Пусть C

каноническая модель логики B. По теореме 11.1 C

является характеристической

для логики B. Поэтому для доказательства данного утверждения достаточно пока-

зать, что фрейм модели C

принадлежит классу фреймов F r

. По теореме о полноте

для модальных логик имеем, что фрейм модели C

является рефлексивным. Сле-

довательно, поскольку C

является подмоделью C

, то фрейм модели C

является

рефлексивным. Предположим, что T

, H

- полные модальные теории из C

и T

Пусть α - формула такая, что ¤α ∈ H

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

. Тогда по лем-

ме 11.3 (пункт 6) ¬α ∈ T

. Поскольку `

p → ¤3p, то в силу пункта 1) леммы 11.3

p → ¤3p ∈ T

и, следовательно, ¬α → ¤3¬α ∈ T

. Отсюда по пункту 2) леммы 11.3

получаем, что ¤3¬α ∈ T

и, следовательно, 3¬α ∈ H

. Учитывая 3 := ¬¤¬, по-

лучаем ¬¤α ∈ H

и ¤α ∈ H

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

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

и пункт 1) выполняется.

2) Не трудно видеть, что формула ¤p → 3p истинна на всех фреймах класса

F r

. По теореме 11.1 каноническая модель C

логики D является характеристиче-

ской для логики D. Покажем, что фрейм модели C

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

F r

. Пусть T

- полная модальная теория из C

. Формула ¤> доказуема в K и, сле-

довательно, доказуема в D. В силу пункта 1) леммы 11.3 и задания логики D имеем,

что ¤> → 3> ∈ T

. Отсюда по лемме refpmt2 (пункт 2) получаем, что 3> ∈ T

. То-

гда по теореме 11.4 (о канонической модели) имеем, что T

¤>. Тогда существует

некоторая теория H

∈ C

такая, что T

и H

>. Таким образом, T

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

Теорема 11.6. Логики K4.1, S4.1 полны по Крипке.

1) Класс F r

K4.1

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

∀x∃y(xRy&yRy&∀z(yRz ⇒ z = y)),

является характеристическим для логики K4.1.

2)Класс F r

S4.1

всех рефлексивных и транзитивных фреймов, удовлетворяющих

условию

∀x∃y(xRy&∀z(yRz ⇒ z = y)),

является характеристическим для логики S4.1.

Доказательство. 1) Докажем, что произвольный фрейм F из F r

K4.1

адекватен

логике K4.1. В силу теоремы об адекватных фреймах для модальных логик и зада-

ния логики K4.1 как K4 ⊕ ¤3p → 3¤p для этого достаточно показать истинность

формулы ¤3p → 3¤p на фрейме F . Предположим, что a °

¤3p, где a - произ-

вольный элемент фрейма F , V - означивание на фрейме F . Пусть b - произвольный

элемент фрейма F такой, что aRb, bRb, ∀c(bRc ⇒ c = b). Тогда в силу определения

логической связки ¤ и условия aRb имеем, что b °

3p. В силу задания элемента

b имеем, что b видит b и только b. Тогда, поскольку b °

3p, получаем b °

p и,

следовательно, b °

¤p. Значит, по определению логической связки 3 имеем, что

a °

3¤p и, следовательно, a °

¤3p → 3¤p. Таким образом, класс всех транзи-

тивных фреймов, удовлетворяющих условию

∀x∃y(xRy&yR y&∀z(yRz ⇒ z = y))

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

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

мов характеристический, достаточно показать, что каноническая модель C

K4.1

ло-

гики K4.1 имеет фрейм, принадлежащий соответствующий классу фреймов F r

K4.1

Модель K4.1 является подмоделью канонической модели C

логики K4. Отсюда в

силу теоремы полноты для модальных логик фрейм C

K4.1

является транзитивным.

По заданию логики K4.1 фреймы модели C

K4.1

обладают следующим свойством

(∀T

∈ C

K4.1

)(∃H

∈ C

K4.1

)(T

где T

, H

- полные модальные теории из C

K4.1

. В самом деле, иначе T

¤3> и

6°

3¤>. Откуда получаем, что T

6°

¤3> → 3¤> и по лемме 11.4 ¤3> →

3¤> 6∈ T

, что противоречит пункту 1) леммы 11.3.

Для каждой полной модальной теории T

из C

K4.1

зададим множество T

{¤α|¤α ∈ T

}. Тогда T

⊆ ¤T

, где ¤T

:= {α|¤α ∈ T

}. В самом деле, пусть

¤α ∈ T

. Тогда, поскольку формула ¤α → ¤¤α доказуема в K4, то по пункту 1)

леммы 11.3 ¤α → ¤¤α ∈ T

. Отсюда по пункту 2) леммы 11.3 имеем, что ¤¤α ∈ T

и, следовательно, ¤α ∈ ¤T

Зафиксируем полную модальную теорию T

из C

K4.1

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

множеств S, удовлетворяющих следующим условиям:

1) S состоит из конечных формул вида ¤γ,

2) множество S ∪ ¤T

совместно.

Отметим, что F не пусто. В самом деле, в силу вышесказанного для любого T

существует некоторая теория H

такая, что T

. Тогда ¤T

⊆ H

и, поскольку,

⊆ ¤T

, то F не пусто. Таким образом, T

принадлежит F, так как T

состоит из

формул вида ¤γ и совместно, как подмножество совместного множества. Применяя

лемму Цорна получаем, что в семействе F существует максимальное множество S

∗

Зафиксирауем такое S

∗

. Поскольку S

∗

∪ ¤T

совместно, то по лемме 11.2 существует

полная модальная теория H

, содержащая множество S

∗

∪ ¤T

. Используя выше-

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

: H

. Рассмотрим

множество C всех элементов E

∈ C

K4.1

таких, что H

. Как было показано ранее,

данное множество не пусто. Поскольку ¤T

⊆ H

, то T

. В силу транзитивно-

сти фрейма модели C

K4.1

получаем, что для каждого E

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

Покажем, что для каждого E

∈ C выполняется

= H

= S

∗

В силу включения T

⊆ ¤T

имеем S

∗

⊆ H

⊆ ¤H

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

∗

⊆ H

⊆ E

и S

∗

⊆ H

⊆ E

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

∗

⊂ E

. Тогда ¤T

∪E

⊆ E

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

¤T

∪ E

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

∗

. Таким образом,

= H

= S

∗

. Далее,

(∀E

∈ C)(∀α )(¤α ∈ E

⇒ α ∈ E

В самом деле, если ¤α ∈ E

, то по тождеству E

= H

= S

∗

имеем ¤α ∈

. Тогда из H

следует α ∈ E

. Покажем, что C состоит из единственного

рефлексивного элемента. В силу условий E

= H

= S

∗

и (∀E

∈ C)(∀α )( ¤α ∈ E

⇒

α ∈ E

), любая пара элементов E

, E

из множества C обладает свойством: E

и, следовательно, множество C является сгустком в C

K4.1

. Пусть α - формула

из E

, где E

∈ C и E

- фиксированный элемент из C. Тогда по теореме 11.4 E

и E

¤3α, так как ¤3α ∈ E

. Поскольку ¤3p → 3¤p аксиома логики K4.1 , то

по пунктам 1), 2) леммы 11.3 ¤3α → 3¤α и 3¤α ∈ E

. По теореме 11.4 E

3¤α.

Следовательно, существует E

такой, что E

и выполняется E

¤α. Однако

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

α и α ∈ E

. Таким образом, E

= E

и единтсвенный

элемент из C обладает указанными в теореме свойствами. Таким образом, фрейм

модели C

K4.1

принадлежит классу F r

K4.1

2) В данном случае модель S4.1 является подмоделью канонической модели C

логики S4. Отсюда в силу теоремы полноты для модальных логик фрейм C

S4.1

яв-

ляется рефлексивным и транзитивным. В остальном доказательство данного утвер-

ждения повторяет предыдущие рассуждения. Теорема доказана.

Теорема 11.7. Логики K4.2, S4.2 полны по Крипке.

1) Класс F r

K4.2

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

∀x, y, z((xR y)&(xRz) ⇒ ∃w((yR w)&(zRw))),

является характеристическим для логики K4.2.

2) Класс F r

S4.2

всех рефлексивных и транзитивных фреймов, удовлетворяющих

условию

∀x, y, z((xR y)&(xRz) ⇒ ∃w((yR w)&(zRw))),

является характеристическим для логики S4.2.

Доказательство. 1) Покажем, что класс фреймов F r

K4.2

адекватен логике K4.2.

Для этого достаточно показать, что формула 3¤p → ¤3p истинна на произволь-

ном фрейме F из класса F r

K4.2

. Пусть a - произвольный элемент фрейма F и a °

Diamond¤p. Тогда существует элемент b такой, что b °

¤p. Рассмотрим произволь-

ный элемент c такой, что aRc. В силу задания фрейма F существует элемент w такой,

что bRw и cRw. Следовательно, w °

p и c °

3p. Таким образом, в силу произволь-

ности выбора элемента c имеем, что a °

¤3p. Следовательно, a °

3¤p → ¤3p и,

класс фреймов F r

K4.2

адекватен логике K4.2.

Покажем, что фрейм канонической модели C

K4.2

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

F r

K4.2

. Модель C

K4.2

является подмоделью модели C

. Тогда по теореме о полноте

для модальных логик фрейм модели C

K4.2

является транзитивным. Пусть T

, E

, H

полные модальные теории такие, что T

, T

. Покажем, что ¤E

∪¤H

явля-

ется совместной, причем ¤E

:= {α|¤α ∈ E

} и ¤H

:= {α|¤α ∈ H

}. Предположим

противное. Тогда по пункту 3) леммы 11.3 существуют формулы α

, ..., α

∈ ¤E

, ..., β

∈ ¤H

такие, что `

K4.2

¬(α

∧ ... ∧ α

∧ β

∧ ... ∧ β

). Отсюда

K4.2

(α

∧ ... ∧ α

) → ¬(β

∧ ... ∧ β

Отсюда, поскольку α

, ..., α

∈ ¤E

и β

, ..., β

∈ ¤H

, то

K4.2

¤(α

∧ ... ∧ α

) → ¤¬(β

∧ ... ∧ β

Далее, учитывая ¤ := ¬3¬, получаем

K4.2

¤(α

∧ ... ∧ α

) → ¬3(β

∧ ... ∧ β

И по свойству логической связки ¤:

K4.2

(¤α

∧ ... ∧ ¤α

) → ¬3(β

∧ ... ∧ β

Отсюда по пункту 1) леммы 11.3 имеем

∧

...

∧

)

→ ¬

(

∧

...

∧

)

∈

. В силу

задания α

, ..., α

∈ ¤E

получаем, что ¤α

, ..., ¤α

∈ E

и, по пункту 3) леммы 11.3

имеем, что (¤α

∧ ... ∧ ¤α

) ∈ E

. Тогда по лемме 11.3 (пункт 2) получаем, что

¬3(β

∧ ... ∧ β

) ∈ E

Поскольку β

, ..., β

∈ ¤H

, то ¤β

, ..., ¤β

∈ H

и, используя свойства логической

связки ¤, получаем ¤(β

∧ ... ∧ β

) ∈ H

. По теореме о канонической модели имеем

¤(β

∧ ... ∧ β

). Так как T

, то T

3¤(β

∧ ... ∧ β

). Формула 3¤p →

¤3p является аксиомой логики K4.2, следовательно, по пункту 1) леммы 11.3 имеем

3¤(β

∧ ... ∧ β

) → ¤3(β

∧ ... ∧ β

) ∈ T

И по теореме 11.4

3¤(β

∧ ... ∧ β

) → ¤3(β

∧ ... ∧ β

Отсюда, учитывая ранее доказанное, по пункту 2) леммы 11.3 получаем

¤3(β

∧ ... ∧ β

Так как T

, то E

3(β

∧ ... ∧ β

) и по теореме 11.4 (о канонической модели)

3(β

∧ ... ∧ β

) ∈ E

, что противоречит ранее доказанному утверждению ¬3(β

∧ ... ∧

) ∈ E

Таким образом, ¤E

∪ ¤H

является совместной и по лемме 11.2 существует пол-

ная модальная теория M

, содержащая ¤E

∪ ¤H

. Тогда H

и E

. Сле-

довательно, фрейм модели C

K4.2

принадлежим классу F r

K4.2

. По теореме 11.1 кано-

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

K4.2

логики K4.2 является характеристической для логики K4.2.

Следовательно, утверждение 1) данной теоремы доказано.

2) В данном случае модель S4.2 является подмоделью канонической модели C

логики S4. Отсюда в силу теоремы полноты для модальных логик фрейм C

S4.2

яв-

ляется рефлексивным и транзитивным. В остальном доказательство данного утвер-

ждения повторяет предыдущие рассуждения. Теорема доказана.

Фрейм F называется связным, если (∀x, y ∈ F )((xRy) ∨ (yRx)). Фрейм F назы-

вается слабо связным, если (∀x, y, z ∈ F )(((xRy)&(xRz)) ⇒ ((yR z) ∨ (zRy))).

Теорема 11.8. Логики K4.3, S4.3 полны по Крипке.

1) Класс F r

K4.3

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

теристическим для логики K4.3.

2) Класс F r

S4.3

всех рефлексивных, транзитивных и слабо связных фреймов яв-

ляется характеристическим для логики S4.3.

Доказательство. 1) Докажем, что произвольный фрейм F из F r

K4.3

адекватен

логике K4.3. Для этого в силу задания логики K4.3 и теоремы об адекватных фрей-

мах модальных логик достаточно показать, что формула ¤(¤p → q) ∨ ¤(¤q → p)

истинна на F . Пусть a - произвольный элемент фрейма F , V - означивание на F .

Предположим, что существует элемент b такой, что aRb и b °

¤p, b 6°

q. Тогда

a °

¤(¤q → p). В самом деле, если aRc, то поскольку F слабо связный, cRb или

bRc. Если bRc, то c °

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

¤q → p. Предположим, что cRb.

Тогда, поскольку b 6°

q, то c 6°

¤q и, следовательно, c °

¤q → p. Так как c -

произвольный элемент такой, что aRc, то a °

¤(¤q → p). Следовательно, формула

¤(¤p → q) ∨ ¤(¤q → p) истинна на всех фоеймах из K4.3 и класс фреймов F r

K4.3

адекватен логике K4.3.

Покажем, что класс фреймов F r

K4.3

характеризует логику K4.3. Пусть C

K4.3

каноническая модель логики K4.3. По теореме 11.1 C

K4.3

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

ской для логики K4.3. Поэтому для доказательства данного утверждения достаточно

показать, что фрейм модели C

K4.3

принадлежит классу фреймов F r

K4.3

. По теореме

о полноте для модальных логик имеем, что фрейм модели C

является транзитив-

ным. Следовательно, поскольку C

K4.3

является подмоделью C

, то фрейм модели

K4.3

является транзитивным. Пусть T

, E

, H

- произвольные полные модальные

теории из C

K4.3

такие, что T

и T

. Тогда ¤T

⊆ E

и ¤T

⊆ H

. Пред-

положим, что < H

, E

>6∈ R

и < E

, H

>6∈ R

. Тогда существуют формулы α,

β такие, что ¤α ∈ H

, α 6∈ E

, ¤β ∈ E

, β 6∈ H

. Тогда по лемме 11.3 получа-

ем ¤α ∈ H

и ¬β ∈ H

, следовательно, ¤α ∧ ¬β ∈ H

. Тогда ¬(¬¤ ∨ β) ∈ H

¤α → β 6∈ H

. Аналогично рассуждая получаем ¤β → α 6∈ E

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

¤(¤α → β) 6∈ T

и ¤(¤β → α ) 6∈ T

. Отсюда ¬(¤(¤α → β)) ∧ ¬(¤(¤β → α)) ∈ T

¬((¤(¤α → β)) ∨ (¤(¤β → α))) ∈ T

. Отсюда (¤(¤α → β)) ∨ (¤(¤β → α)) 6∈ T

, но

данная формула является аксиомой логики K4.3, следовательно, в силу пункта 1)

леммы 11.3 получили противоречие. Таким образом, H

или E

и фрейм

модели C

K4.3

принадлежит классу F r

K4.3

Пункт 2) данной теоремы доказывается аналогично предыдущему пункту с учё-

том специфики строения фрейма модели C

S4.3

, а именно, фрейм модели C

S4.3

явля-

ется рефлексивным и транзитивным. Теорема доказана.

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

1. Какие классы фреймов являются характеристическими для модальных логик

B, D?

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

K4.1, S4.1?

3. Покажите, что ¤3p → 3¤p истинна на фрейме логики S4.1.

4. Покажите, что фрейм канонической модели Крипке C

S4.1

принадлежит классу

всех рефлексивных и транзитивных фреймов, удовлетворяющих условию

∀x∃y(xRy&∀z(yRz ⇒ z = y)).

5. Покажите, что класс всех рефлексивных, транзитивных, слабо связных фрей-

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

6. Укажите характеристический класс фреймов для логики S4.2, ответ обоснуйте

и покажите истинность формулы 3¤p → ¤3p на этом классе фреймов.

7. Покажите, какие справедливы включения для логик B, D, K4.1, S4.1, K4.2,

S4.2, K4.3, S4.3.

12 Лекция 13. Специальные модели Крипке для мо-

дальных логик.

В данной лекции рассмотрены n-характеристические модели Крипке, которые нашли

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

Введём необходимые определения.

Определение 12.1. Модель Крипке K

называется n-характеристической для нор-

мальной модальной логики λ, если означивание V из K

задано на переменных

, ..., p

, и для любой формулы α(p

, ..., p

), построенной на переменных p

, ..., p

выполняется следующее: α(p

, ..., p

) ∈ λ ⇔ K

° α(p

, ..., p

Пусть M =< W, R, V > - произвольная модель Крипке. Подмножество X ⊆

W называется формульным, если существует формула α такая, что X = {x|x ∈

W, x °

α}. Элемент a ∈ W называется формульным, если множество {a} фор-

мульно. Пусть S - новое означивание каких-то пропозициональных переменных на

фрейме < W, R > модели M. Означивание S называется формульным, если для

любой переменной p

∈ Dom(S) подмножество S(p

) формульно, то есть существует

формула α

такая, что S(p

) = V (α

Далее приведём определение p-морфизма и основное свойство такого отображе-

ния. Данное отображение широко используется при рассмотрении n-характеристических

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

Определение 12.2. Пусть f - отображение фрейма F

=< W

, R

> на фрейм

=< W

, R

>. Отображение f называется p-морфизмом, если:

1) (∀a, b ∈ W

)(aR

b ⇒ f(a)R

f(b)),

2) (∀a, b ∈ W

)(f(a)R

f(b) ⇒ (∃c ∈ W

)(aR

c&f(c) = f(b))).

Отображение f называется p-морфизмом модели M

=< W

, R

, V

> на мо-

дель M

=< W

, R

, V

>, если:

1) f является p-морфизмом фрейма < W

, R

> на фрейм < W

, R

2) Dom(V

) = Dom(V

3) (∀p ∈ D om(V

), ∀a ∈ W

)(a °

p ⇒ f(a) °

p).

Основное свойство p-морфизма состоит в сохранении истинности формул:

Теорема 12.3. Если f - p-морфизм модели M

=< W

, R

, V

> на M

=< W

, R

, V

то для любой формулы α, построенной из пропозициональных переменных Dom(V

)

выполняется:

∀a ∈ W

(a °

α ⇔ f(a) °

α).

Доказательство проведём индукцией по длине формулы α. Если α = p, то спра-

ведливость иеоремы следует из пункта 3) определения p-морфизма моделей Крипке.

В случае логических связок ∧, ∨, →, ¬ индуктивный шаг очевиден.

Пусть α = ¤β и a °

¤β. Предположим, что c ∈ W

и f(a)R

c. Поскольку

f является отображением "на", то существует b ∈ W

такой, что f(b) = c. Так как

f(a)R

f(b) и справедлив пункт 2) определения p-морфизма, то существует некоторый

элемент d ∈ W

такой, что aR

d и f(d) = f(b) = c. Поскольку a °

¤β, то d °

β и

по предположению индукции f(d) °

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

β и f(a) °

¤β.

Обратно, пусть f(a) °

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

b. Тогда по пункту 1) опре-

деления p-морфизма f (a)R

f(b) и, поскольку f(a) °

¤β, то f(b) °

β. Отсюда по

индуктивному предположению b °

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

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

Следствие 12.4. Если существует p-морфизм фрейма F

на фрейм F

, то λ(F

) ⊆

λ(F

Доказательство. Пусть α - формула из λ(F

) и V

- означивание переменных

формулы α на фрейме F

. Определим означивание V

данных переменных на фрейме

следующим образом V

(p) := f

−1

(p)). Тогда f является p-морфизмом модели

< F

, V

> на модель < F

, V

>. По лемме 12.3 < F

, V

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

α ∈ λ(F

). Следствие доказано.

Отметим, что допустимые правила вывода - это те правила вывода, добав-

ление которых к списку постулированных правил вывода не расширяет множества

доказуемых теорем исчисления. Для определения допустимости правил вывода су-

ществует следующий критерий:

Теорема 12.5. Пусть K

, n ∈ N, - последовательность n-характеристических

моделей модальной логики λ. Правило вывода r := α

, ..., α

/β допустимо в логике

λ тогда и только тогда, когда для каждого n ∈ N и любого формульно опреде-

лимого означивания S переменных правила r в K

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

S(α

) = K

,..., S(α

) = K

, то S(β) = K

, другими словами, если r истинно в K

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

Доказательство. Рассмотрим правило вывода r := α

, ..., α

/β с переменными

, ..., x

. Предположим, что r не допустимо в λ. Тогда существуют формулы γ

1 ≤ i ≤ k, такие, что для всех j, 1 ≤ j ≤ m, α

(γ

) ∈ λ&β(γ

) 6∈ λ. Предположим,

что число пропозициональных переменных, входящих в вышеуказанные формулы,

равно n. Модель K

является n-характеристической для λ, поэтому

∀j(K

(γ

))&K

6°

β(γ

Тогда означивание S(x

) := V (γ

) опровергает r в K

: ∀j(S(α

) = K

), S(β) 6= K

Обратно. Предположим, что существует n и формульно определимое означива-

ние W пропозициональных переменных x

, ..., x

во фрейме модели K

такое, что

W (α

) = K

, ..., W (α

) = K

, но W (β) 6= K

. Тогда из формульной определимости

означивания W следует, что существуют формулы γ

, ..., p

),...,γ

, ..., p

) такие,