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

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

И по теореме дедукции получаем:

γ∈A

γ → ¬β.

Таким образом, формула

γ∈A

γ → ¬β доказуема в λ и, следовательно, вышеука-

занная эквивалентность выполняется: ¬β 6∈ T ⇔ < T ∪ {β}, ∅ > не совместно с λ.

Далее по лемме 8.9 теория < T ∪ { β}, ∅ > совместна с λ тогда и только тогда, ко-

гда существует полная интуиционистская теория, совместная с λ и расширяющая

< T ∪ {β}, ∅ >. Следовательно, ¬β 6∈ T тогда и только тогда, когда существует пол-

ная интуиционистская теория < H, L >, совместная с λ и расширяющая < T, F >.

По индуктивному предположению < T, F >6°

¬β. Таким образом, мы показали

¬β ∈ T ⇔< T, F >°

¬β.

Пусть α = β → γ. По лемме 8.14 β → γ 6∈ T тогда и только тогда, когда для

каждого конечного подмножества A из T формула

δ∈A

δ → (β → γ) не является

теоремой λ. Последнее условие эквивалентно условию

δ∈A

δ → (β → γ) 6∈ λ что

по доказанному в предыдущем пункте эквивалентно условию совместности теории

< A ∪ {β}, {γ} >, где A - конечное подмножество множества T . Следовательно, β →

γ 6∈ T тогда и только тогда, когда < T ∪ {β}, {γ} > совместно с λ. В силу леммы 8.9

последнее условие эквивалентно существованию полной интуиционистской теории,

совместной с λ и расширяющей теорию < T ∪ {β}, {γ} >. Таким образом, β → γ 6∈ T

тогда и только тогда, когда существует полная интуиционистская теория < H, L >

совместная с λ и расширяющая < T ∪ {β}, {γ} >. По индуктивному предположению

если существует такая теория < H, L >, то

< H, L >°

β, < H, L >6°

γ,

< T, F >≤< H, L >, < T, F >6°

β → γ.

Обратно, если < T, F >6°

β → γ, то для теории < H, L > указанные выше отноше-

ния выполняются и, следовательно, β → γ 6∈ T . Следовательно,

β → γ ∈ T ⇔< T, F >°

β → γ.

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

Определение 8.15. Пусть λ - суперинтуиционистская логика. Интуиционист-

ская модель Крипке M =< W, ≤, V > называется характеристической для λ, если

для любой формулы α выполняется:

α ∈ λ ⇔ M ° α.

Теорема 8.16. Каноническая интуиционистская модель Крипке M

произвольной

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

логики λ.

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

> → α и по лемме 8.14 для каждой

полной теории < T, F >, совместной с λ, α ∈ T . Отсюда по теореме о канонической

модели для суперинтуиционистской логики имеем, что < T, F >°

α и, следова-

тельно, M

° α. Обратно, пусть α 6∈ λ. Тогда по лемме 8.10 существует полная

интуиционистская теория < T, F >, совместная с λ, такая, что α ∈ F . Тогда α 6∈ T

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

< T, F >6°

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

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

1. Сформулируйте определение интуиционистского фрейма и интуиционистского

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

2. Каким образом определяется истинность формулы на элементе интуиционист-

ской модели?

3. Покажите, что для интуиционистской модели M =< W, ≤, V > и каждого

элемента a из W выполняется:

а) a °

¬p ⇔ a °

p → ⊥,

б) a °

p → ¬¬p,

в) a °

¬¬¬p → ¬p.

4. Покажите, что формула ¬¬p ∨ ¬p истинна на всех фреймах, соответствующих

логике KC.

5. Покажите, что формула (p → q) ∨ (q → p) истинна на всех фреймах, соответ-

ствующих логике LC.

6. Докажите, что для логик KC, LC выполняется следующее:

а) фрейм F адекватен логике KC тогда и только тогда, когда F принадлежит

классу всех частично упорядоченных множеств, удовлетворяющих условию:

∀x∀y∀z((x ≤ y&x ≤ z) ⇒ ∃t(y ≤ t&z ≤ t)),

б) фрейм F адекватен логике LC тогда и только тогда, когда F принадлежит

классу всех частично упорядоченных множеств, удовлетворяющих условию:

∀x∀y∀z((x ≤ y&x ≤ z) ⇒ (y ≤ z ∨ z ≤ y)).

7. Докажите следующие строгие включения: H ⊂ KC, KC ⊂ LC.

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

для модальных логик K, T, S4, S5 и суперинтуи-

ционистских логик H, KC, LC

Теорема 9.1. (теорема о полноте для модальных логик) Логики K, T , K4, S4, S5

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

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

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

логики T .

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

логики K4.

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

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

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

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

Доказательство. Пусть λ одна из модальных логик K, T , K4, S4, S5. Согласно

теореме об адекватности все указанные выше классы фреймов адекватны соответс-

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

вышеуказанной логики λ и каждой формулы α 6∈ λ найти λ-фрейм из соответствую-

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

что для любой нормальной модальной логики λ и любой аксиоматической системы

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

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

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

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

(λ(AS) = λ)

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

теоремы. Далее будем рассматривать канонические модели C

, C

по

названиям логик K, T , K4, S4, S5 соответственно.

1) Поскольку фрейм модели C

является фреймом, то C

∈ S и K полна по

Крипке.

2) Покажем, что модель C

имеет рефлексивный фрейм. Пусть T

- полная мо-

дальная теория из |C

|. Поскольку ¤α → α ∈ T , то по лемме о полной модальной

теории (пункт 1) имеем ¤α → α ∈ T

. Отсюда для любой формулы α если ¤α ∈ T

то по пункту 2) леммы о полной модальной теории имеем, что α ∈ T

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

отношение R

из C

является рефлексивным и, значит, логика T полна по Крипке и

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

3) Покажем, что каноническая модель C

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

, G

∈ |C

| и T

, H

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

. Рассмотрим произвольную

формулу α такую, что ¤α ∈ T

. Поскольку ¤ α → ¤¤α ∈ K4, то по пункту 1)

леммы о полной модальной теории ¤α → ¤¤α ∈ T

. Тогда по пункту 2) этой же

леммы из того, что ¤α ∈ T

следует ¤¤α ∈ T

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

, следует

¤α ∈ H

. Тогда α ∈ G

, так как H

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

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

транзитивно.

4) Используя пункты 2), 3) данного доказательства, нетрудно видеть, что кано-

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

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

5) Покажем, что каноническая модель C

имеет фрейм с отношением эквива-

лентности как отношением достижимости. В самом деле, C

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

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

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

Покажем, что отношение R

модели C

симметрично. Пусть T

, G

∈ |C

| и T

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

, T

>6∈ R

. Тогда существует формула α такая, что ¤α ∈

и α 6∈ T

. Поскольку T

- полная модальная теория, то ¬α ∈ T

. По теореме о

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

¤α

¬α.

Поскольку R

рефлексивно, то T

¦¬α. Применяя теорему о канонической моде-

ли, получаем ¦¬α ∈ T

. Так как ¦¬α → ¤ ¦ ¬α ∈ S5, то в силу пункта 1) леммы о

полной модальной теории имеем ¦¬α → ¤ ¦ ¬α ∈ T

. Отсюда так как ¦¬α ∈ T

, то

по пункту 2) леммы о полной модальной теории ¤ ¦ ¬α ∈ T

. По теореме о канониче-

ской модели T

¤ ¦ ¬α. Следовательно, поскольку T

, имеем G

¦¬α, что

противоречит G

¤α. Таким образом, G

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

симметрично.

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

Теорема о полноте даёт инструмент, с помощью которого можно распознавать

доказуемые формулы в нормальных модальных логиках.

Пример: Формула ¤p → ¤¤p не доказуема в логике T .

Действительно, пусть F =< 0, 1, 2, R >, где R задано следующим образом: 0R0,

1R1, 2R2, 0R1, 1R2. Из задания отношения R следует, что R рефлексивно. Далее,

пусть V (p ) = 0, 1. Тогда 0 °

¤p, 0 6°

¤¤p. Следовательно, 0 6°

¤p → ¤¤p, то

есть F 6° ¤ p → ¤¤p. Поскольку F ∈ Ref и Ref - характеристический класс для T ,

то 6`

¤p → ¤¤p.

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

ные логики обладают так называемым "свойством дизъюнкции". Нормальная мо-

дальная логика λ обладает свойством дизъюнкции, если и только если для любых

формул α и β выполняется: ¤α ∨ ¤β ∈ λ ⇔ (α ∈ λ) ∨ (β ∈ λ).

Теорема 9.2. Логики K, T , K4, S4 обладают свойством дизъюнкции.

Доказательство. Пусть λ - одна из логик, указанных в теореме. Предположим,

что α 6∈ λ и β 6∈ λ. Поскольку λ полна по Крипке, то существуют λ-фреймы F

:=<

, R

> и F

:=< W

, R

> и означивания V

и V

фреймов F

и F

соответственно

такие, что

(∃a

∈ W

)(a

6°

α),

(∃a

∈ W

)(a

6°

β).

Также можно полагать, что F

∩ F

= ∅.

Пусть

∪

∪{⊥}

⊥ 6∈

∪

∪{

⊥

, a >

∈

∪

}∪{

⊥, ⊥ >}, (∀p)(V

(p) = V

(p) ∪ V

(p)).

Индукцией по длине формулы δ нетрудно показать, что

(∀a ∈ F

)(a °

δ ⇔ a °

δ), i = 1, 2.

Если δ - пропозициональная переменная, то утверждение следует из определения

модели < F

, R

, V

>. Если a °

ϕ ∨ ψ, то a °

ϕ или a °

ψ. Пусть a °

ψ.

Тогда по индуктивному предположению a °

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

ϕ ∨ψ. Пусть

a °

ϕ ∨ ψ. Тогда a °

ϕ или a °

ψ. Предположим, что a °

ϕ. По индуктивному

предположению a °

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

ϕ ∨ ψ. Допустим, что a °

¬ϕ. Тогда

a 6°

ϕ и, по индуктивному предположению, a 6°

ϕ, то есть a °

¬ϕ. Обратно, если

a °

¬ϕ, то a 6°

ϕ и, по индуктивному предположению, a 6°

ϕ, то есть a °

¬ϕ.

Связки →, ¬ проверяются аналогично.

Рассмотрим случай a 6°

¤ϕ. Тогда существует b ∈ F

такое, что b 6°

ϕ и aR

b. По

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

ϕ и далее по определению отношения

получаем aR

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

¤ϕ. Предположим, что a 6°

¤ϕ. Тогда

существует b ∈ F

такое, что aR

b и b 6°

ϕ. Из задания фрейма < F

, R

> следует,

что b ∈ F

и aR

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

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

¤ϕ. Утверждение доказано.

Для фреймов F

, F

имеют место следующие соотношения:

, F

∈ S ⇒ F

∈ S,

, F

∈ R ef ⇒ F

∈ Ref,

, F

∈ T r ⇒ F

∈ T r

, F

∈ T R ⇒ F

∈ T R.

Первое утверждение очевидно. Второе следует из задания отношения R

, так

как ⊥R

⊥. Пусть R

, R

транзитивны. Предположим, что aR

b, bR

c. Тогда если

a = ⊥, то aR

c по заданию R

. Если a ∈ F

, i = 1, 2, то ввиду определения R

имеем b, c ∈ F

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

транзитивно, aR

c. Отсюда в силу

задания R

: aR

c. Значит, R

транзитивно и третье утверждение доказано. Последнее

утверждение следует непосредственно из двух предыдущих.

Вернёмся непосредственно к доказательству теоремы. Поскольку a

∈ W

и (a

6°

α), a

∈ W

и a

6°

β), то в силу вышедоказанного (a

6°

α) и (a

6°

β). По зада-

нию элемента ⊥ имеем, что ⊥R

, ⊥R

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

¤α и ⊥ 6°

¤β,

то есть ⊥ 6°

¤α ∨ ¤β. Значит, F

6° ¤α ∨ ¤β. Ввиду ранее доказанных соотноше-

ний для фреймов F

, F

имеем, что F

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

теореме о полноте для модальных логик (¤α ∨ ¤β) 6∈ λ. Теорема доказана.

Не все модальные логики обладают свойством дизъюнкции. Примером такой ло-

гики служит S5. Доказать это можно с помощью формулы ¤(¤p → ¤q) ∨ ¤(¤q →

¤p).

Перейдём к суперинтуиционистским логикам.

Теорема 9.3. Логики H, KC, LC полны по Крипке.

1) Класс F r

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

тическим для логики H.

2) Класс F r

всех частично упорядоченных множеств, удовлетворяющих ус-

ловию ∀x∀y∀z((x ≤ y&x ≤ z) ⇒ ∃t(y ≤ t&z ≤ t)), является характеристическим

для логики KC.

3) Класс F r

всех частично упорядоченных множеств, удовлетворяющих ус-

ловию ∀x∀y∀z((x ≤ y&x ≤ z) ⇒ (y ≤ z ∨ z ≤ y)), является характеристическим для

логики LC.

Доказательство. По теореме об адекватных фреймах суперинтуиционистских

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

, F r

адекватны соответственно логикам H, KC,

LC. В предыдущей лекции была доказана теорема о том, что каноническая интуи-

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

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

λ, где λ - произвольная суперинтуиционисткая логика. Таким образом, достаточно

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

сам фреймов.

Случай 1) очевиден.

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

ния из предыдущей лекции.

Лемма 9.4. Если < T, F > - полная теория, совместная с суперинтуиционистской

логикой λ, то

(i) (α ∧ β) ∈ T ⇔ (α ∈ T )&(β ∈ T ),

(ii) (α ∨ β) ∈ T ⇔ (α ∈ T ) ∨ (β ∈ T ).

Лемма 9.5. Пусть < T, F > - полная теория, совместная с суперинтуиционист-

ской логикой λ. Тогда для любой формулы α выполняется:

α ∈ T ⇔ ∃A[(A ⊆ T )&(||A|| < ω)&(`

δ∈A

δ → α)].

Лемма 9.6. Для любой интуиционистской теории < T, F >, совместной с супер-

интуиционистской логикой λ, существует полная теория < T

, F

>, расширяющая

< T, F > и совместная с λ.

Перейдём к доказательству пункта 2). Рассмотрим фрейм канонической модели

. Предположим, что < T, F >, < H, L >, < R, E > - теории из |M

| такие,

что < T, F >≤< H , L >, < T, F >≤< R, E >. Покажем, что теория < H ∪ R, ∅ >

совместна с логикой KC. В самом деле, в противном случае существуют некоторые

конечные подмножества A, B соответственно из H, R такие, что

α∈A

α ∧

β∈B

β → ⊥.

Используя теорему дедукции, получаем

α∈A

α,

β∈B

β `

⊥,

α∈A

α `

β∈B

β → ⊥,

α∈A

α `

¬(

β∈B

β).

Поскольку `

(¬

β∈B

β) ∨ (¬¬

β∈B

β), то по лемме 9.5

(¬

β∈B

β) ∨ (¬¬

β∈B

β) ∈ T.

Следовательно, по лемме 9.4 или (¬

β∈B

β) ∈ T или (¬¬

β∈B

β) ∈ T . Предполо-

жим, что выполняется первое включение, тогда, поскольку T ⊆ R, (¬

β∈B

β) ∈ R

и, следовательно, < R, E > несовместна с логикой KC, что противоречит условию.

Значит, (¬¬

β∈B

β) ∈ T ⊆ H. Так как

α∈A

α `

¬(

β∈B

β), то по лемме 9.5

¬(

β∈B

β) ∈ H и, следовательно, < H, L > несовместна с логикой KC. Таким

образом, теория < H ∪ R, ∅ > совместна с KC. Используя лемму 9.6, получаем,

что существует интуиционистская полная теория < T ∗, F ∗ >, расширяющая теорию

< H ∪ R, ∅ >. Тогда

< H, L >≤< T ∗, F ∗ >,

< R , E >≤< T ∗, F ∗ > .

3) Рассмотрим фрейм канонической интуиционистской модели M

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

что < T, F >, < H, L >, < R, E > - теории из |M

| такие, что < T, F >≤< H, L >,

< T, F >≤< R, E >. Предположим, что < H, L >6≤< R, E >, < R, E >6≤< H, L >.

Тогда существует формула α ∈ H такая, что α 6∈ R и существует формула β ∈ R

такая, что β 6∈ H. Однако `

(α → β) ∨ (β → α). Тогда по лемме 9.5 (α → β) ∨ (β →

α) ∈ T и по лемме 9.4 или (α → β) ∈ T или (β → α) ∈ T . Если (α → β) ∈ T ⊆ H, то

по лемме 9.5 и условию α ∈ H имеем, что β ∈ H, что противоречит предположению.

Аналогично, если (β → α) ∈ T ⊆ R, то по лемме 9.5 и условию β ∈ R имеем,

что α ∈ R и противоречие условию. Таким образом, или < H, L >≤< R, E > или

< R, E >≤< H, L >. Теорема доказана.

Суперинтуиционистская логика λ обладает свойством дизъюнкции, если и

только если для любых формул α и β выполняется следующее: α ∨ β ∈ λ ⇔ (α ∈

λ) ∨ (β ∈ λ).

Суперинтуиционистская логика λ замкнута снизу, если класс K всех фрей-

мов адекватных λ замкнут относительно операции ⊗ . Для любых фреймов F

:=<

, ≤

>, F

:=< W

, ≤

>, не имеющих общих элементов, фрейм F

⊗ F

имеет сле-

дующую структуру:

⊗ F

:=< |F

⊗ F

|, ≤>,

⊗ F

| := |F

| ∪ |F

| ∪ {⊥}, где ⊥ 6∈ |F

| ∪ |F

≤:=≤

∪ ≤

∪{⊥ ≤ a|a ∈ W

∪ W

} ∪ {⊥ ≤ ⊥}.

Для доказательства теоремы о дизъюнкции для суперинтуиционистских логик

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

Лемма 9.7. Пусть M :=< W, ≤, V > интуиционистская модель. Для произволь-

ной формулы α и каждого элемента a ∈ W выполняется:

∀a ∈ W ∀b ∈ W((a °

α)&(a ≤ b) ⇒ b °

α).

Теорема 9.8. Если суперинтуиционистская логика λ полна по Крипке и замкнута

снизу, то λ обладает свойством дизъюнкции.

Доказательство. Предположим, что α 6∈ λ и β 6∈ λ. Поскольку λ полна по

Крипке, то существуют λ-фреймы F

=< W

, ≤

>, F

=< W

, ≤

> и означивания

, V

, соответственно, фреймов F

, F

такие, что (∃a

∈ W

)(a

6°

α) и (∃a

∈

)(a

6°

β). Без ограничения общности можно считать, что фреймы F

и F

не

имеют общих элементов. Поскольку логика λ замкнута снизу, то фрейм F

⊗ F

является адекватным логике λ. Зададим означивание V на фрейме F

⊗F

следующим

образом: (∀p)(V (p) := V

(p) ∪ V

(p)).

Очевидно, что отношение °

на компонентах F

и F

совпадает с отношениями

, °

, соответственно. В частности, a

6°

α и a

6°

β. Поскольку ⊥ ≤ a

, ⊥ ≤ a

то по лемме 9.7 мы получаем, что ⊥ 6°

α и ⊥ 6°

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

(α ∨ β).

Так как F

⊗ F

является λ-фреймом, то по теореме полноты для суперинтуицио-

нистских логик (α ∨ β) 6∈ λ. Теорема доказана.

Из данной теоремы и теоремы полноты для суперинтуиционистских логик полу-

чаем

Следствие 9.9. Интуиционистская логика Гейтинга H обладает свойством дизъюн-

кции.

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

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

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

¦p → ¤ ¦ p

¤ ¦ p → ¦¤p

¦¤p → ¤ ¦ p

3. Покажите, что (¤(¤p → ¤q) ∨ ¤(¤q → ¤p)) ∈ S5.

4. Покажите, что выполняется следующее:

(i) (3¤p → ¤3p) ∈ S5,

(ii) (¤p → 3p) ∈ S5,

(iii) (p → 3p) ∈ S5.

5. Сформулируйте свойство дизъюнкции и теорему дизъюнкции для модальных

логик.

6. Какая модальная логика не обладает свойством дизъюнкции и почему?

7. Какие классы фреймов являются характеристическими для суперинтуицио-

нистских логик H, KC, LC?

8. Покажите, что классическое исчисление высказываний ИВ полно по Крипке и

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

зует ИВ.

9. Сформулируйте свойство дизъюнкции и теорему дизъюнкции для суперинтуи-

ционистских логик.

10. Покажите, что логики KC, LC не обладают свойством дизъюнкции.

10 Лекция 11. Метод фильтрации

Модальная логика λ называется разрешимой, если существует алгоритм, позволя-

ющий для любой формулы α установить, доказуема ли она в λ или нет. Определение

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

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

из некоторого характеристического класса. Но эти классы состоят из бесконечных

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

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

Это затруднение снимается нахождением более простых характеристических клас-

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

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

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

Леммоном.

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

логических систем, как финитная аппроксимируемость и разрешимость.

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

Определение 10.1. Пусть λ - алгебраическая логика и V ar(λ) = {A|A ² α, α ∈ λ} -

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

вы. Будем говорить, что λ финитно аппроксимируема, если для каждой формулы

α, не являющейся теоремой λ, существует конечная алгебра A из многообразия

V ar(λ) такая, что A 6 ² α.

Другими словами, логика λ называется финитно аппроксимируемоей, если для

любой формулы α, не доказуемой в λ, существует конечный фрейм F такой, что

F 6° α и F адекватен λ , то есть если существует класс конечных фреймов характе-

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

Теорема 10.2. (теорема Харропа) Если λ - финитно аппроксимируемая логика

с конечной аксиоматической системой AS (то есть с конечными множествами

аксиом и правил вывода), то λ разрешима.

Доказательство. Поскольку AS конечна, то можно построить эффективную

процедуру P

получения последовательности всех теорем λ. В тоже время λ финитно

аппроксимируема и, следовательно, можно задать эффективную процедуру P

−

ну-

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

формулы α начнём одновременно процедуры P

и P

−

. Тогда формулу α мы получим

либо на некотором шаге процедуры P

, либо на некотором шаге процедуры P

−

. В

первом случае α ∈ λ, во втором α 6∈ λ. Теорема доказана.

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

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

λ = {α|(∀F )(||F || < ω&F ° λ ⇒ F ° α)},

то есть λ полна относительно некоторого класса соответствующих конечных

фреймов.

Теорема 10.4. Модальная или суперинтуиционистская логика λ финитно аппро-

ксимируема тогда и только тогда, когда λ финитно аппроксимируема по Крипке.

Следствие 10.5. Любая модальная или суперинтуиционистская финитно аппро-

ксимируемая логика полна по Крипке.

Перейдём к методу фильтрации.

Пусть M :=< W, R, V > - модель Крипке (модальная или интуиционистская).

Пусть S - множество формул (модальных или интуиционистских, соответственно),

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

дение в формулы из S, содержатся в Dom(V ). Определим отношение эквивалентно-

сти ≡

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

a ≡

b ⇔ (∀α ∈ S)(a °

α ⇔ b °

α).

Разобьём множество W на классы эквивалентности относительно ≡

. Через [a]

≡

будем обозначать множество элементов W , эквивалентных a, а через W

≡

:= {[a]

≡

|a ∈

W } - фактор-множество W по эквивалентности ≡

(то есть множество всех классов

эквивалентности). Напомним, что V ar(S) - множество всех пропозициональных пе-

ременных, входящих в формулы из S.

Определение 10.6. Фильтрацией модели M по множеству S называется модель

Крипке M

:=< W

≡

, R

, V

> такая, что

(i) (∀p ∈ V ar(S))(V

(p) := {[a]

≡

|a °

p});

(ii) если M - модальная модель, то

(1) (∀x, y ∈ W )(xRy ⇒ [x]

≡

[y]

≡

(2) (∀x, y ∈ W )([x]

≡

[y]

≡

⇒ (¤α ∈ S)&x °

¤α ⇒ y °

α).

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

выполняется (1) и

(3) (∀x, y ∈ W )([x]

≡

[y]

≡

⇒ (α ∈ S)&x `

α ⇒ y °

α).

Ясно, что означивание V

определено корректно. Классы фильтраций всегда яв-

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

по S существует максимальная фильтрация: фильтрация с максимальным отно-

шением достижимости R

. Данное отношение получено из (2) для модального случая

и из (3) для интуиционистского случая заменой ⇒ на ⇔. Пересечение всех R

во всех

возможных фильтрациях на M по S задаёт минимальное отношение достижимости

, которое определяет на W

фильтрацию. Данная фильтрация называется ми-

нимальной. Нетрудно видеть, что R

может быть определено, как

< X, Y >∈ R

⇔ (X = [a]

≡

&Y = [b]

≡

&(aRb)).

Для канонических интуиционистских моделей минимальная и максимальная филь-

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

единственная фильтрация по заданному множеству S.

Лемма 10.7. (лемма о фильтрации) Пусть M

=< W

≡

, R

, V

> - фильтрация

модели M =< W, R, V > по множеству S. Тогда для любых a ∈ W и α ∈ S,

a °

α ⇔ [a]

≡

α.

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

модальной модели. Пусть α = p и p ∈ S. Если a °

p, то по определению V

[a]

≡

p. Если [a]

≡

p, то a ∈ V (p) и, следовательно, a °

Пусть α = β ∨ γ. Тогда a °

β или a °

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

[a]

≡

β или [a]

≡

γ. Следовательно, [a]

≡

β ∨ γ. Обратно, [a]

≡

β ∨ γ.

Тогда [a]

≡

β или [a]

≡

γ. Кроме того, ввиду замкнутости по подформуль-

ности, β ∈ S и γ ∈ S. Следовательно, по индуктивному предположению, a °

β или

a °

γ и, значит, a °

β ∨ γ.

Пусть α = ¬β. Если a °

¬β, то a 6°

β, β ∈ S ввиду закнутости S по под-

формульности, и по индуктивному предположению, [a]

≡

6°

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

[a]

≡

¬β. Обратно, [a]

≡

¬β. Тогда [a]

≡

6°

β, β ∈ S, и по индуктивному

предположению, a 6°

β, то есть a °

¬β.

Проверка логических связок ∧, → очевидна.

Рассмотрим α = ¤β. Поскольку множество S замкнуто по подформульности, то

β ∈ S. Предположим, что a °

¤β. Пусть [b]

≡

- произвольное множество такое, что

[a]

≡

[b]

≡

. Тогда из пункта 2) определения фильтрации следует, что b °

β и по

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

≡

β. Следовательно, [a]

≡

¤β. Обратно,

пусть [a]

≡

¤β и aRb. Тогда по пункту 1) из определения фильтрации следует,

что [a]

≡

[b]

≡

. Значит, [b]

≡

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

β.

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

¤β и модальный случай доказан.

В случае интуиционистской модели рассмотрение базы индукции и логических

связок ∧, ∨ очевидно и совпадает с доказательством для модальных логик. Пусть

α = β → γ. Отметим, что β, γ ∈ S ввиду замкнутости S по подформульности.

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

β → γ. Пусть [a]

≡

[b]

≡

и [b]

≡

β. По индуктивному

предположению b °

β. В силу пункта 3) определения фильтрации b °

β → γ. Тогда

b °

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

≡

γ. Следовательно, [a]

≡

β → γ. Обратно, пусть [a]

≡

β → γ. Рассмотрим произвольный элемент b такой,

что aRb и b °

β. По индуктивному предположению [b]

≡

β. Из пункта 1)

определения фильтрации получаем, что [a]

≡

[b]

≡

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

≡

γ и

индуктивное предположение влечёт b °

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

β → γ.

Индуктивный шаг для интуиционистской модели и формул вида ¬β сводится к

предыдущему ввиду эквивалентности ¬β ≡

β → ⊥. Лемма доказана.

Перейдём к применениям леммы о фильтрации.

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

C - каноническая модель для λ. Будем говорить, что λ обладает свойством филь-

трации тогда и только тогда, когда выполняется следующее. Для любого конечного

множества формул S, замкнутого по подформульности, и любого элемента a ∈ C,

существует фильтрация C

a,S

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

модели C, порождённой

элементом a, такая, что фрейм модели C

a,S

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

Теорема 10.9. Если логика λ обладает свойством фильтрации, то λ финитно ап-

проксимируема.

Доказательство. Пусть α 6∈ λ. Тогда α опровергается на канонической модели

Крипке C логики λ, так как в силу теоремы о канонической модели C характеризует

λ. Пусть Sub(α) - множество всех подформул формулы α. Пусть a - элемент модели

C, опровергающий α, и C

- открытая подмодель модели C, порождённая элементом

a. Тогда по свойству открытых подмоделей C

также опровергает α. Поскольку λ

обладает свойством фильтрации, то существует фильтрация C

a,Sub(α)

модели C

по

Sub(α) такая, что фрейм модели C

a,Sub(α)

является λ-фреймом. По определению мо-

дель C

a,Sub(α)

конечна. По лемме о фильтрации модель C

a,Sub(α)

также опровергает α.

Следовательно, λ финитно аппроксимируема по Крипке. И по теореме 10.4 логика λ

финитно аппроксимируема. Теорема доказана.