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

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

p, q

p ∧ q

p → q, q → r

p → r

p → q

¬q → ¬p

p → q

(q → r ) → (p → r)

В логике Гейтинга справедливы следующие эквивалентности:

1. p ≡ p ∧ p, 2. p ∨ p ≡ p,

3. (p ∧ q) ∧ r ≡ p ∧ (q ∧ r), 4. (p ∨ q) ∨ r ≡ p ∨ (q ∨ r),

5. p ∧ q ≡ q ∧ p, 6. p ∨ q ≡ q ∨ p ,

7. p ∧ (p ∨ q) ≡ p, 8. p ∨ (p ∧ q) ≡ p,

9. p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r), 10. p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r),

11. ((p ∨ q) → r) ≡ ((p → r) ∧ (q → r)),

12. p → (q ∧ r) ≡ (p → q) ∧ (p → r),

13. ((p → q) → q) → q ≡ p → q,

14. (p → q) ≡ [((p → q) → p) → q],

15. ¬¬¬p ≡ ¬p,

16. ¬(p ∨ q) ≡ ¬p ∧ ¬q

В логике Гейтинга следующие формулы доказуемы:

1. ¬¬(p ∨ ¬p)

2. (p → ¬q) → (q → ¬p)

3. (¬p ∨ ¬q) → ¬(p ∧ q)

4. ¬(p ∧ ¬p)

5. (p ∨ q) → ¬(¬p ∧ ¬q)

6. (p ∧ q) → ¬(¬p ∨ ¬q)

7. (p → q) → ¬(p ∧ ¬q)

Расширения логики Гейтинга с тем же набором логических связок, полученные за

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

ведём примеры наиболее известных суперинтуиционистских логик.

1. F or

= Li + {p} ' множество всех формул,

2. CP C = Li + {p ∨ ¬p}

классическое исчисление высказываний,

3. KC = Li + {¬p ∨ ¬¬ p } логика,

4. LC = Li + {(q → p) ∨ (p → q)} линейная логика,

5. KP = Li + {(¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r))}

логика ,

6. SL = Li + {((¬¬p → p) → (¬p ∨ p)) → (¬p → ¬¬p)}

логика,

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

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

sc = 2(2p → q) ∨ 2(2q → p)

grz = 2(2(p → 2p) → p) → p

sym = p → 23p

klmn

= 3

p → 2

tra

i=0

p → 2

n+1

den

= 2

n+1

p → 2

euc = 32p → 2p

ga = 32p → 23p

dir = 3(2p ∧ q) → 2(3p ∨ q)

con = 2(p ∧ 2p → q) ∨ 2(q ∧ 2q → p)

i=0

→

(3(p

∧ (p

∨ 3p

))

= 32p

→ p

, bd

n+1

= 3(2p

n+1

∧ ¬bd

) → p

n+1

al t

= 2p

∨ 2(p

→ p

) ∨ · · · ∨ 2(p

∧ · · · ∧ p

→ p

n+1

)

l a = 2(2p → p) → 2p

——————————————————————-

1. D = K ⊕ 2p → 3p

2. T = K ⊕ 2p → p

3. KB = K ⊕ p → 23p

4. K4 = K ⊕ 2p → 22p

5. K5 = K ⊕ 32p → 2p

6. Alt

= K ⊕ 2p

∨ 2(p

→ p

) ∨ · · · ∨ 2(p

∧ · · · ∧ p

→ p

n+1

)

7. D4 = K4 ⊕ 3>

8. S4 = K4 ⊕ 2p → p

9. GL = K4 ⊕ 2(2p → p) → 2p

10. F or = K4 ⊕ p

11. Grz = K ⊕ 2(2(p → 2p) → p) → p

12. K4.1 = K4 ⊕ 23p → 32p

13. K4.2 = K4 ⊕ 3(p ∧ 2q) → 2(p ∨ 3q)

14. K4.3 = K4 ⊕ 2(2

p → q) ∨ 2(2

q → p)

15. S4.1 = S4 ⊕ 23p → 32p

16. S4.2 = S4 ⊕ 32p → 23p

17. S4.3 = S4 ⊕ 2(2p → q) ∨ 2(2q → p)

18. T riv = K4 ⊕ 2p ↔ p

19. V erum = K4 ⊕ 2p

20. S5 = S4 ⊕ p → 23p

21. K4B = K4 ⊕ p → 23p

22. A

∗

= GL ⊕ 22p → 2(2

p → q) ∨ 2(2

q → p)

23. K4Z = K4 ⊕ 2(2p → p) → (32p → 2p)

24. Dum = S4 ⊕ 2(2(p → 2p) → p) → (32p → p)

25. D4G

= D4 ⊕ 2(2

p ∨ 2

¬p) → 2p ∨ 2¬p

26. K4H = K4 ⊕ p → 2(3p → p)

27. K4Alt

= K4 ⊕ 2p

∨ 2(p

→ p

) ∨ · · · ∨ 2(p

∧ · · · ∧ p

→ p

n+1

)

28. K4BW

= K4 ⊕

i=0

→

(3(p

∧ (p

∨ 3p

))

29. K4BD

= K4 ⊕ bd

30. K4

n,m

= K4 ⊕ 2

p → 2

p, 1 6 m < n.

Временные логики

Язык временной логики содержит логические связки ∧, ∨, →, ¬, 2

, 2

. Опреде-

ление формулы даётся аналогично другим модальным логикам. Символы 2

, 2

будем читать "всегда будет", "всегда было". В качестве аксиом минимальной вре-

менной логики возьмём аксиомы классического исчисления высказываний и доба-

вим аксиомы для логических связок "всегда будет", "всегда было". Кроме правила

modus ponens, возьмём два правила, соответствующих связкам 2

и 2

. Минималь-

ную временную логику будем обозначать символом T

. Приведём схемы аксиом и

правила вывода логики T

A1 (X → (Y → X)),

A2 ((X → (Y → Z)) → ((X → Y ) → (X → Z))),

A3 ((X ∧ Y ) → X),

A4 ((X ∧ Y ) → Y ),

A5 ((X → Y ) → ((X → Z) → (X → (Y ∧ Z)))),

A6 (X → (X ∨ Y )),

A7 (Y → (X ∨ Y )),

A8 ((X → Z) → ((Y → Z) → ((X ∨ Y ) → Z))),

A9 (X → Y ) → ((X → ¬Y ) → ¬X),

A10 ¬¬X → X,

KF 2

(X → Y ) → (2

X → 2

Y ),

KP 2

(X → Y ) → (2

X → 2

Y ),

KFP X → 2

KPF X → 2

Правила вывода логики T

X, X → Y

Поскольку логика T

содержит все аксиомы и правила вывода классической ло-

гики, то все формулы, доказуемые в классической логике, доказуемы и в T

. Ана-

логичное утверждение справедливо и для формул в языке логики K: если α ∈ K

и α

, α” - формулы, полученные из формулы α заменой связки 2 на 2

или 2

соответственно, то α

∈ T

и α” ∈ T

В частности справедливы эквивалентности:

1) 2

(p ∧ q) ≡ 2

p ∧ 2

2) 3

(p ∨ q) ≡ 3

p ∨ 3

3) 2

(p ∧ q) ≡ 2

p ∧ 2

4) 3

(p ∨ q) ≡ 3

p ∨ 3

Здесь формула 3

p является сокращением для ¬2

¬p и, соответственно, 3

является сокращением для ¬2

¬p.

Докажем теорему дедукции для логики T

. Формулы вида

. . . 2

α будем называть модальностями и обозначать Mα, где

M = 2

. . . 2

Теорема 7.1. Если Γ, α ` β, то существуют такие модальности

, . . . , M

, что Γ ` M

α ∧ · · · ∧ M

α → β

Пусть ϕ

, . . . , ϕ

вывод формулы β из гипотез Γ, α. Индукцией по индексу i до-

кажем

Лемма 7.2. Для любого i существуют такие модальности M

, . . . , M

, что Γ `

α ∧ · · · ∧ M

α → ϕ

I. Если i = 1, то ϕ

либо аксиома, либо принадлежит Γ, либо совпадает с α.

Все рассуждения, проведённые при доказательстве теоремы дедукции в Lp остаются

справедливыми и, следовательно, Γ ` α → ϕ

II. Пусть лемма справедлива для всех i < k. Докажем её для индекса k. Для

формулы ϕ

возможны следующие утверждения: 1) ϕ

является аксиомой, 2) ϕ

приналежит Γ, 3) ϕ

совпадает с α, 4) ϕ

получена из предыдущих формул по пра-

вилу modus ponens, 5) ϕ

получена из предыдущей формулы по одному из правил

В случаях 1)-3) остаются справедливыми все построения из логики Lp.

В случае 4) ϕ

является следствием формул ϕ

и ϕ

→ ϕ

, для которых спра-

ведливо предположение индукции: существуют модальности M

, . . . , M

и N

, . . . , N

такие, что Γ ` M

α ∧ · · · ∧ M

α → ϕ

и Γ ` N

α ∧ · · · ∧ N

α → ( ϕ

→ ϕ

). Обозначим

для сокращения записей α

= M

α ∧ · · · ∧ M

α, α

= N

α ∧ · · · ∧ N

α. Построим

следующий квазивывод из гипотез Γ:

1. α

→ ϕ

выводимая из Γ формула,

2. α

∧ α

→ α

аксиома A3,

3. α

∧ α

→ ϕ

из 1, 2 по правилу сечения,

4. α

→ (ϕ

→ ϕ

) выводимая из Γ формула,

5. α

∧ α

→ α

аксиома A4,

6. α

∧ α

→ (ϕ

→ ϕ

) из 4, 5 по правилу сечения,

7. (α

∧ α

→ (ϕ

→ ϕ

)) → ((α

∧ α

→ ϕ

) → (α

∧ α

→ ϕ

))

аксиома A5,

8. (α

∧ α

→ ϕ

) → (α

∧ α

→ ϕ

)

из 6, 7 по правилу m.p.,

9. α

∧ α

→ ϕ

из 3, 8 по правилу m.p.,

Рассмотрим последний 5) случай: ϕ

получена из предыдущей формулы ϕ

по

одному из правил

, т.е. ϕ

= 2

, где T ∈ {F, P }. По предположению

индукции Γ ` M

α ∧ · · · ∧ M

α → ϕ

. Следовательно Γ ` 2

α ∧ · · · ∧ M

α → ϕ

Формула 2

α ∧ · · · ∧ M

α → ϕ

) → (2

α ∧ · · · ∧ M

α) → 2

) является

аксиомой T

. В силу правила modus ponens имеем Γ ` 2

α ∧ · · · ∧ M

α) → 2

Так как 2(M

α ∧ · · · ∧ M

α) ≡ (2

α ∧ · · · ∧ 2

α), то окончательно получаем

Γ ` 2

α ∧ · · · ∧ 2

αα → 2

Лемма доказана. Заключение теоремы дедукции для T

получим если положим в

лемме i = n, т.е. ϕ

является последней формулой в выводе ϕ

, . . . , ϕ

и совпадает с

β.

Приведём другие примеры временных логик, являющихся расширениями логики

. Положим T

= T

+ {2

X → X, 2

X → X}, T

= T

+ {2

X → 2

X, 2

X →

X}, T

= T

+ {2

X → 2

X, 2

X → 2

X}. Нетрудно видеть, что

приведённые примеры логик являются аналогами мономодальных логик T , K4 и S4,

соответственно. Теорема дедукции может быть переформулирована с учётом свойств

модальных связок каждой из приведённых логик.

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

1. Сформулируйте теорему дедукции для логики T

2. Как изменится формулировка теоремы дедукции в расширении T

, содержащем

аксиомы рефлексивности для обеих модальностей?

3. Сформулируйте теорему дедукции для расширения логики T

, содержащего акси-

омы транзитивности для обеих модальных связок.

4. Во всякой ли временной логике эквивалентны формулы 2

α и 2

α?

5. Будет ли доказуемым в логике Гейтинга правило

p→q

¬q→¬p

8 Лекция 9. Семантика Крипке для суперинтуицио-

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

В данной лекции будет рассмотрена семантика Крипке применительно к суперин-

туиционистским логикам.

Суперинтуиционистским фреймом называется частично упорядоченное мно-

жество < W, ≤>, то есть отношение ≤ является рефлексивным, транзитивным, ан-

тисимметричным:

1) ∀x ∈ W (x ≤ x),

2) ∀x∀y∀z ∈ W(x ≤ &y ≤ z ⇒ x ≤ z),

3) ∀x∀y ∈ W (x ≤ y&y ≤ x ⇒ x = y).

Будем говорить "a видит b"или "b достижим из a", если a ≤ b, a, b ∈ W .

Означиванием называется отображение V , удовлетворяющее следующим свой-

ствам:

1) V : P → 2

, то есть ∀p ∈ P (V (p) ⊆ W ),

2) (∀a∀b ∈ W )(∀p ∈ P)(a ≤ b ⇒ (a ∈ V (p) ⇒ b ∈ V (p))).

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

где < W, ≤> - частично упорядоченное множество и V - интуиционистское означи-

вание множества P пропозициональных переменных на < W, ≤>.

Истинность формул на элементе a интуиционистской модели M =< W, ≤

, V > определяется следующим образом:

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

p) ⇔ (a ∈ V (p))),

(∀a ∈ W )(a °

(α ∧ β) ⇔ (a °

α)&(a °

β)),

(∀a ∈ W )(a °

(α ∨ β) ⇔ (a °

α) ∨ (a °

β)),

(∀a ∈ W )(a °

(¬α) ⇔ (∀b ∈ W )(a ≤ b ⇒ b 6°

α)),

(∀a ∈ W )(a °

(α → β) ⇔ (∀b ∈ W )(a ≤ b ⇒ (b °

α ⇒ b °

β)).

Формула α истинна на интуиционистской модели M =< W, ≤, V > (обоз-

начение M ° α), если она истинна на каждом элементе a из W при означивании

V . Формула α истинна на фрейме F =< W, ≤> (обозначение F ° α), если она

истинна на каждом элементе a из W при любом означивании V таком, что Dom(V )

включает в себя все переменные формулы α. Для логики λ фрейм F называется

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

α. Класс фреймов Ω называется адекватным для логики λ, если Ω состоит из

множества λ-фреймов.

Легко видеть, что Ω адекватен λ, тогда и только тогда, когда

λ ⊆ λ(Ω) := {α|α ∈ F or

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

Класс фреймов Ω называется характеристическим для суперинтуиционистской

логики λ, если λ = λ(Ω). Если существует класс характеристических фреймов для

суперинтуиционистской логики λ, то λ называется полной по Крипке.

Интуиционистская модель Крипке обладает важным свойством стабильности ис-

тинности формулы: если формула α истинна на элементе a заданной интуиционистс-

кой модели и a видит b, то α истинна на b. Покажем это в следующей лемме.

Лемма 8.1. Пусть M =< W, ≤, V > - интуиционистская модель. Тогда для любой

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

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

α)&(a ≤ b) ⇒ b °

α).

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

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

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

Пусть α = β → γ. Предположим, что a °

β → γ и a ≤ b. Если b ≤ c ∈ W , то a ≤ c

и, по определению истинности логической связки →, если a °

β, то c °

γ. Отсюда

если b °

β, то c °

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

β → γ.

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

¬β, то (∀b ∈ W )(a ≤ b ⇒ b 6°

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

b ≤ c, то c 6°

β, так как a ≤ c. Значит, b °

¬β. Лемма доказана.

Введём следующие классы фреймов:

F r

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

F r

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

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

F r

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

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

Теорема 8.2. (об адекватных фреймах суперинтуиционистских логик)

1)Класс фреймов F r

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

2) Класс фреймов F r

адекватен логике KC := H ⊕ {¬¬p ∨ ¬p}.

3) Класс фреймов F r

адекватен логике LC := {(p → q) ∨ (q → p)}.

Доказательство. Для доказательства теоремы достаточно доказать следующие

два пункта: а) правило вывода modus ponens сохраняет истинность формул в про-

извольной интуиционистской модели Крипке, б) все аксиомы заданных логик спра-

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

Лемма 8.3. Если все аксиомы суперинтуиционистской логики λ истинны на фрей-

ме F и правило вывода modus ponens сохраняет истинность формул в произволь-

ной интуиционистской модели Крипке, построенной на фрейме F , то все теоремы

истинны на F .

Доказательство. В самом деле, произвольная теорема α заданной логики λ вы-

водима из схем аксиом данной логики. Пусть S - вывод теоремы α. Рассмотрим

некоторое означивание V всех пропозициональных переменных из α. Зададим оз-

начивание V на всех переменных из S таким образом, что при означивании V все

переменные, не входящие в α, принимают значение "ложь"во всём фрейме F . Все

схемы аксиом β, встречающиеся в S, истинны во фрейме F при означивании V . Пусть

β - результат подстановки в некоторую аксиому γ логики λ, где γ = γ(p

), β = γ(δ

Зададим означивание V

переменных p

во фрейме F следующим образом: означива-

ние V

ставит в соответствие каждой переменной p

множество V (δ

) всех элементов

из F , на которых δ

истинна при означивании V . По лемме 8.1 означивание V

яв-

ляется интуиционистским. Кроме того, истинностные значения γ при V

совпадают

с истинностными значениями γ(δ

) при V . Поскольку γ выполняется на F при лю-

бом означивании, то формула γ(δ

), эквивалентная β, истинна на F при означивании

V . Таким образом, все схемы аксиом β из S истинны на фрейме F при означива-

нии V . По условию правило вывода modus ponens сохраняет истинность формул в

произвольной интуиционистской модели Крипке, построенной на фрейме F . Отсюда

индукцией по количеству вхождений формул в S, несложно доказать, что α истинна

на фрейме F при означивании V . Лемма доказана.

Покажем справедливость пункта а). В самом деле,

Лемма 8.4. Пусть M - интуиционистская модель Крипке с означиванием V .

Пусть L(M) := {α|α ∈ F or

, M ° α}. Множество L(M) замкнуто относительно

правила вывода modus ponens: x, x → y/y.

Доказательство. Предположим, что формулы α и α → β истинны в модели M

с означиванием V . Пусть a ∈ |M|. Тогда по предположению a °

α и a °

α → β.

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

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

Рассмотрим пункт б). 1) Покажем, что все аксиомы логики H выполняются на

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

Пусть F =< W, ≤> - частично упорядоченное множество и V - означивание на

F . Логика H имеет следующие аксиомы:

(A1) (p → (q → p)),

(A2) (p → (q → r)) → ((p → q) → (p → r)),

(A3) p → (p ∨ q),

(A4) q → (p ∨ q),

(A5) (p → r ) → ((q → r) → ((p ∨ q) → r)),

(A6) (p ∧ q) → p,

(A7) (p ∧ q) → q,

(A8) (p → q) → ((p → r) → (p → (q ∧ r))),

(A9) (p → q) → ((p → ¬q) → ¬p),

(A10) p → (¬p → ¬q).

Рассмотрим (A1). Нужно доказать, что (∀a ∈ W ) a °

(p → (q → p)). Предполо-

жим, что a ≤ b и b °

p. Далее если b ≤ c, то в силу леммы 8.1 c °

p. Поэтому

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

c °

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

p → (q → p).

Покажем, что формула (A2) истинна на любом элементе из W при означивании

V . В самом деле, пусть a ≤ b и b °

(p → (q → r)). Предположим, что b ≤ c и

c °

(p → q), c ≤ d и d °

p. Тогда, поскольку b ≤ d, то d °

q и d °

(q → r).

Отсюда следует, что d °

Истинность аксиом (A3), (A4) очевидна.

Покажем истинность аксиомы (A5) на произвольном элементе a из W . Предпо-

ложим, что a ≤ b ∈ W , b °

(p → r). Пусть b ≤ c и c °

(q → r). Предположим, что

c ≤ d и d °

(p ∨ q). Тогда d °

p или d °

q. Если d °

p, то, поскольку b ≤ d,

имеем d °

r. Если d °

q, то, поскольку c ≤ d, имеем d °

r. Таким образом, (A5)

истинна на фрейме F при означивании V .

Истинность аксиом (A6), (A7) следует непосредственно из определения интуицио-

нистского означивания и леммы 8.1.

Рассмотрим аксиому (A8). Пусть a - произвольный элемент фрейма F . Предпо-

ложим, что a ≤ b и b °

(p → q), b ≤ c и c °

(p → r). Пусть c ≤ d и d °

p. Тогда,

поскольку b ≤ d, c ≤ d, то d °

q и d °

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

q ∧ r.

Проверим формулу (A9). Пусть a - произвольный элемент из W и a ≤ b, b °

(p → q) Предположим, что b ≤ c и c °

(p → ¬q). Тогда для каждого d такого, что

b ≤ d, выполняется d °

p ⇒ d °

q и d °

p ⇒ d °

¬q. Следовательно, для всех

таких d справедливо d 6°

p и, значит, b °

¬p.

Покажем, что формула (A10) истинна на произвольном элементе a фрейма F .

Пусть a ≤ b и b °

p. По лемме 8.1 для всех c ∈ W таких, что b ≤ c выполняется c °

p. Следовательно, для всех c таких, что b ≤ c, выполняется c 6°

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

c °

(¬p → q).

Таким образом, класс фреймов F r

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

2) Для доказательства пункта 2) данной теоремы достаточно доказать, что фор-

мула (¬¬p∨¬p) истинна на всех фреймах из F r

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

F r

и V - означивание на F . Предположим, что a ∈ W и a 6°

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

существует b ∈ W такой, что a ≤ b и b °

p. Пусть c - произвольный элемент из

W такой, что a ≤ c. Поскольку F ∈ F r

, то существует элемент d ∈ W такой, что

b ≤ d и c ≤ d. Tак как b °

p, то d °

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

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

для всех c таких, что a ≤ c, выполняется c 6°

¬p. Значит, a °

¬¬p.

3) Достаточно доказать, что формула (p → q) ∨ (q → p) истинна на всех фреймах

из F r

. Пусть F ∈ F r

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

что a 6°

(p → q). Тогда существует элемент b такой, что a ≤ b, b °

p и b 6°

Предположим, что c - произвольный элемент из W такой, что a ≤ c и c °

q. Так как

F ∈ F r

, то b ≤ c или c ≤ b. Если c ≤ b, то по лемме 8.1 b °

q, что противоречит

заданию элемента b: b 6°

q. Следовательно, b ≤ c и c °

p. Значит, a °

(q → p).

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

Определение 8.5. Интуиционистской теорией называется пара < T, F >, где T ,

F - множества формул в языке интуиционистской пропозициональной логики.

Определение 8.6. Теория < T, F > называется совместной с некоторой супер-

интуиционистской логикой λ, если не существует конечных подмножеств A, B

соответственно множеств T , F таких, что

∈A

→

∈B

Определение 8.7. Интуиционистская теория < T, F > называется полной, если

T ∪ F = F or

, то есть каждая формула является элементом множества T ∪ F .

Будем говорить, что пара < H, L > расширяет пару < T, F >, если T ⊆ H, F ⊆ L.

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

(< T, F >≤< H, L >) ⇔ ((T ⊆ H)&(L ⊆ F )).

Лемма 8.8. Пусть < T, F > - интуиционистская теория, совместная с некоторой

суперинтуиционистской логикой. Для любой формулы α или теория < T ∪{α}, F >

или теория < T, F ∪ { α} > совместна с λ.

Доказательство. Предположим, что обе теории, указанные в условии леммы, не

совместны с λ. Тогда существуют конечные множества формул A

, A

, B

такие,

что A

⊆ T , A

⊆ T , B

⊆ F , B

⊆ F и

∈A

∧ α →

∈B

∈A

→

∈B

∨ α.

Отсюда, используя соответствующие выводы в интуиционистской логике H, по-

лучаем:

∈A

∧

∈A

∧ α →

∈B

∨

∈B

∈A

∧

∈A

→

∈B

∨

∈B

∨ α.

Тогда в силу соответствующих выводов в H, получаем:

∈A

∧

∈A

→

∈B

∨

∈B

и, следовательно, пара < T, F > не совместна с λ, полученное противоречие доказы-

вает лемму.

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

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

, F

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

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

Доказательство. Зададим процедуру присоединения формул α

к теории <

T, F > следующим образом. Пусть < T

, F

>:=< T, F >. Предположим, что теория

< T

i−1

, F

i−1

> построена на (i − 1) шаге. Рассмотрим i-ый шаг. Согласно лемме 8.8

на i-ом шаге формулу α

можно добавить к T

i−1

или к F

i−1

таким образом, что одна

из полученных теорий будет совместима. Данную теорию обозначим < T

, F

>. Объ-

единение всех теорий < T

, F

> задаёт совместную теорию < H, L >, так как 1) на

i-ом шаге теория < T

, F

> совместна по выбору, и 2) данная теория является рас-

ширением всех теорий, построенных ранее. Таким образом, теория < H, L > полна,

совместна и расширяет теорию < T, F >. Лемма доказана.

Лемма 8.10. Если суперинтуиционистская логика λ совместна (то есть ⊥ 6∈ λ)

и формула α не является теоремой λ, то существует полная интуиционистская

теория < T, F >, совместная с λ, такая, что α ∈ F .

Доказательство. Теория < ∅, {α} > совместна с λ. В самом деле, предположим,

что или < ∅, ∅ > не совместна или > → α ∈ λ. Если < ∅, ∅ > не совместна, то > →

⊥ ∈ λ и, следовательно, ⊥ ∈ λ, откуда следует, что λ не совместна. Если > → α ∈ λ,

то α ∈ λ. По лемме 8.9 существует полная совместная с λ мнтуиционистская теория

< T, F >, расширяющая теорию < ∅, {α} >. Лемма доказана.

Определение 8.11. Для любой совместной суперинтуиционистской логики λ ка-

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

=< W

, ≤, V >, где означи-

вание V всех пропозициональных переменных из P на W

определено следующим

образом:

(∀p ∈ P )(∀ < T, F >∈ W

)((< T, F >∈ V (p)) ⇔ (p ∈ T )).

Использование канонических моделей отражено в следующей теореме.

Теорема 8.12. (о канонической модели для интуиционисткой логики) Пусть λ -

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

теории < T, F > из W

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

< T, F >°

α ⇔ α ∈ T.

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

справедливость теоремы вытекает из опрделения означивания V . Индуктивный шаг

для логических связок ∧, ∨ выполняется в силу следующего утверждения

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

ской логикой λ, то

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

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

Доказательство. 1) Пусть α ∧ β ∈ T и α 6∈ T . Так как теория < T, F > пол-

ная, то α ∈ F . Поскольку `

α ∧ β → α, то теория < T, F > не совместна с H и,

следовательно, с λ. Оюратно, пусть α ∈ T и β ∈ T . Предположим, что α ∧ β 6∈ T .

Поскольку рассматриваемая теория полна, то α ∧ β ∈ F . Однако `

(α ∧ β) → (α ∧ β)

и, следовательно, < T, F > не совместна. Таким образом, α ∧ β ∈ T .

2) Пусть (α ∨ β) ∈ T . Предположим, что α 6∈ T и β 6∈ T . Тогда α ∈ F и β ∈ F .

Однако `

(α ∨ β) → (α ∨ β) и, следовательно, < T, F > не совместна. Значит,

α ∈ T или β ∈ T . Обратно, пусть α ∈ T и α ∨ β 6∈ T . Тогда α ∨ β ∈ F . Поскольку

α → (α ∨ β), то < T, F > не совместна, что противоречит условию леммы. Лемма

доказана.

Прежде, чем перейти к логическим связкам ¬, → докажем следующую лемму.

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

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

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

δ∈A

δ → α)).

Доказательство. Если α ∈ T , то возьмём A = {a} и лемма доказана, так как

α → α. Обратно, пусть α 6∈ T . Тогда, поскольку < T, F > - полная теория, α ∈ F .

Поскольку < T, F > совместна, то для каждого конечного подмножества A из T :

δ∈A

δ → α. Лемма доказана.

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

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

γ∈A

γ → ¬β не доказуема в λ. Формула

γ∈A

γ → ¬β не доказуема в λ тогда и только тогда, когда для каждого конечного

подмножества A из T теория < A ∪ {β}, ∅ > совместна с λ. Покажем это. Пусть

формула

γ∈A

γ → ¬β доказуема в λ, то есть `

γ∈A

γ → ¬ β. Тогда

γ∈A

γ ∧ β → ¬β.

Поскольку формула (p ∧ q) → q является аксиомой H, то

γ∈A

γ ∧ β → β.

Применяя эквивалентности ИВ, получаем, что

γ∈A

γ ∧ β → ⊥.

Таким образом, < A ∪ {β}, ∅ > не совместна с λ. Обратно, пусть < A ∪ {β}, ∅ > не

совместна с λ. Тогда

γ∈A

γ ∧ β → ⊥.

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

γ∈A

γ, β `

⊥,

γ∈A

γ `

β → ⊥.

В интуиционистской логике формула ¬x эквивалентна формуле x → ⊥, где ⊥ := ¬>.

Поэтому

γ∈A

γ `

¬β.