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

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

4 Лекция 4. Немодальные расширения позитивной

логики.

4.1 Расширение логики Lp с помощью константы ⊥

В данной лекции рассмотрим некоторые немодальные расширения логики Lp. В

первую очередь рассмотрим расширение Lp, полученное добавлением одной только

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

чать Lj

⊥

и называть минимальной логикой, или логикой Иоганссона. Константу ⊥

будем называть "абсурдом". Нетрудно дать определение формулы в языке, содер-

жащем логические связки ∧, ∨, →, ⊥. Множество формул в этом языке будем обо-

значать F or

⊥

. Поскольку алфавит расширился, то и множество формул будет шире,

появляются формулы с константой ⊥, т.е. F or

⊂ F or

⊥

Нетрудно видеть, что Lp ⊂ Lj

⊥

и любая формула, полученная из формулы, при-

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

F or

⊥

, будет принадлежать Lj

⊥

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

Теорема 4.1. Любая формула логики Lj

⊥

может быть получена из подходящей

формулы логики Lp с помощью подстановки константы ⊥ вместо некоторой про-

позициональной переменной.

Пусть ϕ

, . . . , ϕ

некоторое доказательство в логике Lj

⊥

. Дадим индуктивное

определение mp-веса формулы ϕ

в доказательстве ϕ

, . . . , ϕ

1. Аксиома имеет нулевой mp-вес.

2. Если mp-вес формулы α → β равен i и mp-вес формулы α равен j, то mp-вес

формулы β равен max(i, j) + 1.

Пусть q - пропозициональная переменная, которая не встречается в доказатель-

стве ϕ

, . . . , ϕ

. В последовательности формул ϕ

, . . . , ϕ

все вхождения константы

⊥ заменим на переменную q. Далее индукцией по mp-весу формул покажем, что

полученная в результате последовательность ϕ

, . . . , ϕ

является доказательством в

логике Lp.

I. Пусть mp-вес формулы ϕ

равен нулю, т.е. ϕ

получена из некоторой аксиомы

A1-A8 подстановкой подстановкой формул φ

, . . . , φ

вместо переменных p

, . . . , p

Поскольку ни одна из аксиом A1-A8 не содержит константы ⊥, то все вхождения кон-

станты ⊥ будут находиться в формулах φ

, . . . , φ

, из которых после указанной заме-

ны мы получим формулы φ

, . . . , φ

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

является результатом подста-

новки в соответствующую аксиому формул φ

, . . . , φ

вместо переменных p

, . . . , p

т.е. тоже является аксиомой.

II. Пусть формула ϕ

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

→ ϕ

и ϕ

по пра-

вилу modus ponens. Тогда mp-вес формул ϕ

→ ϕ

и ϕ

меньше веса формулы ϕ

и следовательно каждая из формул ϕ

→ ϕ

и ϕ

либо аксиома, либо по предпо-

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

, . . . , ϕ

по правилу modus ponens. Следовательно и формула ϕ

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

формул ϕ

→ ϕ

и ϕ

последовательности ϕ

, . . . , ϕ

по правилу modus ponens. То

есть ϕ

, . . . , ϕ

доказательство в Lp.

Очевидно, что при обратной замене переменной q на константу ⊥ из последова-

тельности ϕ

, . . . , ϕ

мы получим последовательность ϕ

, . . . , ϕ

. Что и требовалось

доказать. ¥

Следствие 4.2. Формула ⊥ не принадлежит логике Lj

⊥

, в частности логика Lj

⊥

не тривиальна.

Предположим противное ⊥ ∈ Lj

⊥

. Тогда в силу теоремы 4.1 формула ⊥ может

быть получена из некоторой формулы ϕ логики Lp подстановкой константы ⊥ вме-

сто пропозициональной переменной. Но это означает, что ϕ совпадает с пропозицио-

нальной переменной. Но это невозможно, поскольку Lp содержится в классическом

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

переменной не доказуема.

4.2 Расширение логики Lp с помощью связки ¬

Далее рассмотрим расширение Lj

логики Lp, которое получается добавлением к

языку логики Lp связки ¬ и аксиом вида:

A9. (X → Y ) → ((X → ¬Y ) → ¬X)

Докажем некоторые секвенции и эквивалентности логики Lj

1. p → q гипотеза,

2. ¬q гипотеза,

3. ¬q → (p → ¬q) аксиома A1,

4. p → ¬q m.p. 2,3

5. (p → q) → ((p → ¬q) → ¬p) аксиома A9,

6. (p → ¬q) → ¬p m.p. 1,5

7. ¬p m.p. 4,6

Следовательно p → q, ¬q ` ¬p. Применив к последнему утверждению теорему

дедукции, получим p → q, ` ¬q → ¬p. Таким образом, правило

p→q

¬q→¬p

доказуемо

в Lj

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

контрапозиции.

Приведём доказательство секвенции p ` ¬¬p.

1. p гипотеза,

2. p → (q → p) аксиома A1,

3. q → p m.p. 1,2,

4. ¬p → ¬q из 3 по правилу контрапозиции,

5. p → (¬q → p) аксиома A1,

6. ¬q → p m.p. 1,5,

7. ¬p → ¬¬q из 6 по правилу контрапозиции,

8. (¬p → ¬q) → ((¬p → ¬¬q) → (¬¬p))

аксиома A8,

9. (¬p → ¬¬q) → (¬¬p) m.p. 4,8,

10. ¬¬p m.p. 7,9.

Применяя к секвенции p ` ¬¬p теорему дедукции, приходим к ` p → ¬¬p . То есть

формула p → ¬¬p принадлежит логике Lj

. Подставляя в эту формулу вместо пере-

менной p формулу ¬p, получим новую доказуемую формулу логики Lj

: ¬p → ¬¬¬p.

Применяя к формуле p → ¬¬p правило контрапозиции, получим доказуемую форму-

лу ¬¬¬p → ¬p. Таким образом справедлива эквивалентность ¬¬¬p ≡ ¬p. Отметим,

что в логике Lj

формула ¬¬p → p не доказуема, в чём мы сможем убедиться лишь

построив соответствующую семантику нашего исчисления. То есть ¬¬p 6≡ p.

1. p гипотеза,

2. p → ((q → q) → p) аксиома A1,

3. (q → q) → p из 1, 2 по правилу m.p.,

4. ¬p гипотеза,

5. ¬p → ((q → q) → ¬p) аксиома A1,

6. (q → q) → ¬p из 4, 5 по правилу m.p.,

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

аксиома A9,

8. ((q → q) → ¬p) → ¬(q → q) из 3, 7 по правилу m.p.,

9. ¬(q → q) из 6, 8 по правилу m.p..

В силу приведённого вывода p, ¬p ` ¬ (q → q). Применяя теорему дедукции,

получаем ¬p ` p → ¬(q → q). Покажем, что справедливо и обратное утверждение

p → ¬(q → q) ` ¬p.

1. (q → q) → (p → (q → q)) аксиома A1,

2. q → q доказуемая в Lp формула,

3. p → (q → q) из 1, 2 по правилу m.p.,

4. p → ¬(q → q) гипотеза,

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

аксиома A9,

6. (p → ¬(q → q)) → ¬p из 3, 5 по правилу m.p..

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

Таким образом справедлива формальная эквивалентность ¬ p ≡ p → ¬(q → q).

Далее докажем эквивалентность ¬(p ∨ q) ≡ ¬p ∧ ¬q.

1. p → (p ∨ q) аксиома A6,

2. ¬(p ∨ q) → ¬p из 1 по правилу контрапозиции,

3. q → (p ∨ q) аксиома A7,

4. ¬(p ∨ q) → ¬q из 3 по правилу контрапозиции,

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

аксиома A5,

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

из 2, 5 по правилу m.p..

7. ¬(p ∨ q) → ¬p ∧ ¬q из 4, 6 по правилу m.p..

Для доказательства обратной импликации достаточно доказать утверждение ¬p, ¬q `

¬(p∨q), которое в силу доказанных ранее эквивалентностей эквивалентно утвержде-

нию p → ¬(r → r), q → ¬(r → r) ` ¬(p ∨ q).

1. p → ¬(r → r) гипотеза,

2. q → ¬(r → r) гипотеза,

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

аксиома A5,

4. (q → ¬(r → r)) → ((p ∨ q) → ¬(r → r))

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

5. (p ∨ q) → ¬(r → r) из 2, 4 по правилу m.p..

6. ¬¬(r → r) → ¬(p ∨ q) из 5 по правилу контрапозиции,

7. (r → r) → ¬¬(r → r) доказуемая в Lp

формула,

8. (r → r) → ¬(p ∨ q) из 7, 6 по правилу сечения,

9. (r → r) доказуемая в Lp формула,

10. ¬(p ∨ q) из 8, 9 по правилу m.p..

Лемма 4.3. Следующие формулы доказуемы в Lj

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.

1. p → (p ∨ ¬p) аксиома A6,

2. ¬(p ∨ ¬p) → ¬p из 1 по правилу контрапозиции,

3. ¬p → (p ∨ ¬p) аксиома A7,

4. ¬(p ∨ ¬p) → ¬¬p из 3 по правилу контрапозиции,

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

аксиома A9,

6. (¬(p ∨ ¬p) → ¬¬p) → ¬¬(p ∨ ¬p) из 2, 5 по правилу m.p..

7. ¬¬(p ∨ ¬p из 4, 6 по правилу m.p..

Для доказательства формулы 2 достаточно доказать секвенцию p → ¬q, q ` ¬p).

1. q гипотеза,

2. q → (p → q) аксиома A1,

3. p → q из 1, 2 по правилу m.p..

4. p → ¬q гипотеза,

5. (p → q) → ((p → ¬q) → ¬p) аксиома A9,

6. (p → ¬q) → ¬p из 3, 5 по правилу m.p.,

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

Докажем формулу 3.

1. (p ∧ q) → p аксиома A3,

2. ¬p → ¬(p ∧ q) из 1 по правилу контрапозиции,

3. (p ∧ q) → q аксиома A4,

4. ¬q → ¬(p ∧ q) из 3 по правилу контрапозиции,

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

аксиома A8,

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

из 2, 5 по правилу m.p.,

7. (¬p ∨ ¬q) → ¬(p ∧ q) из 4, 6 по правилу m.p..

Докажем формулу 4.

1. (p ∧ ¬p) → p аксиома A3,

2. (p ∧ ¬p) → ¬p аксиома A4,

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

аксиома A9,

4. ((p ∧ ¬p) → ¬p) → ¬(p ∧ ¬p) из 1, 3 по правилу m.p.,

5. ¬(p ∧ ¬p) из 2, 4 по правилу m.p..

Докажем формулу 5.

1. (¬p ∧ ¬q) → ¬p аксиома A3,

2. ¬¬p → ¬(¬p ∧ ¬q) из 1 по правилу контрапозиции,

3. (¬p ∧ ¬q) → ¬q аксиома A4,

4. ¬¬q → ¬(¬p ∧ ¬q) из 2 по правилу контрапозиции,

5. p → ¬¬p доказуемая формула логики Lj

6. p → ¬(¬p ∧ ¬q) из 5, 2 по правилу сечения,

7. q → ¬¬q доказуемая формула логики Lj

8. q → ¬(¬p ∧ ¬q) из 7, 4 по правилу сечения,

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

аксиома A8,

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

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

11. (p ∨ q) → ¬(¬p ∧ ¬q) из 8, 10 по правилу m.p..

Докажем формулу 6.

1. (p ∧ q) → p аксиома A3,

2. ¬p → ¬(p ∧ q) из 1 по правилу контрапозиции,

3. (p ∧ q) → q аксиома A4,

4. ¬q → ¬(p ∧ q) из 3 по правилу контрапозиции,

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

аксиома A8,

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

из 2, 5 по правилу m.p.,

7. (¬p ∨ ¬q) → ¬(p ∧ q) из 4, 6 по правилу m.p.,

8. ¬¬(p ∧ q) → ¬(¬p ∨ ¬q) из 7 по правилу контрапозиции,

9. (p ∧ q) → ¬¬(p ∧ q) доказуемая формула логики Lj

10. (p ∧ q) → ¬(¬p ∨ ¬q) из 9, 8 по правилу сечения.

Для доказательства формулы 7 достаточно доказать секвенцию p → q ` ¬(p∧¬q).

1. (p ∧ ¬q) → p аксиома A3,

2. p → q гипотеза,

3. (p ∧ ¬q) → q из 1, 2 по правилу сечения,

4. (p ∧ ¬q) → ¬q аксиома A4,

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

аксиома A9,

6. ((p ∧ ¬q) → ¬q) → ¬(p ∧ ¬q) из 3, 5 по правилу m.p.,

7. ¬(p ∧ ¬q) из 4, 6 по правилу m.p..

4.3 Трансляции

Далее дадим определения некоторых отображений множества формул в одном языке

во множество формул в другом языке, которые будем называть трансляциями.

Трансляция θ : F or

→ F or

⊥

действует следующим образом: формула θ(ϕ) полу-

чается из формулы ϕ заменой всех её подформул вида ¬ψ на подформулы ψ → ⊥.

Отметим что для любой формулы из F or

, т.е. не содержащей отрицаний, θ(ϕ) = ϕ.

Кроме того, отображение θ взаимнооднозначно и θ(F or

) является собственным под-

множеством множества F or

⊥

. Взаимнооднозначность отображения θ докажем индук-

цией по длине формулы. Для пропозициональных переменных утверждение верно,

поскольку θ(p

) = p

. Предположим утверждение верно для формул более коротких,

чем ϕ. Если формула ϕ имеет вид ϕ = ϕ

∗ϕ

, где ∗ ∈ {∧, ∨, →}, то θ(ϕ) = θ(ϕ

)∗θ(ϕ

Предположим θ(ϕ) = θ(ϕ

). То есть θ(ϕ

) = θ(ϕ

) ∗ θ(ϕ

) и следовательно ϕ

= ϕ

∗ ϕ

θ(ϕ

) = θ(ϕ

), θ(ϕ

) = θ(ϕ

). В силу предположения индукции ϕ

= varphi

, т.е. ϕ

= varphi. Пусть ϕ = ¬ϕ

. В этом случае θ(ϕ) = θ(ϕ

) → ⊥.

Если θ(ϕ

) = θ(ϕ) = θ(ϕ

) → ⊥, то в силу предположения индукции θ(ϕ

) имеет

единственный прообраз и ϕ

= ¬ϕ

= ϕ. Что и требовалось доказать. Поскольку

формулы вида ψ ∨ ⊥, ψ ∧ ⊥ не являются образами никаких формул из F or

, то

трансляция θ не является отображением на F or

⊥

Зафиксируем некоторую пропозициональную переменную, например p

. Транс-

ляция ρ : F or

⊥

→ F or

действует следующим образом: формула ρ(ϕ) получается из

формулы ϕ заменой всех входящих в неё констант ⊥ на подформулы ¬(p

→ p

). От-

метим что для любой формулы из F or

, т.е. не содержащей константы ⊥, θ(ϕ) = ϕ.

Отображение ρ также является взаимнооднозначным, для того чтобы восстановить

прообраз формулы ρ(ϕ) достаточно все вхождения формулы ¬(p

→ p

) заменить на

формулу ⊥. Также ρ(F or

⊥

) 6= F or

так как, например, формулы вида ¬(ϕ ∨ ψ) не

имеют прообразов в F or

⊥

Лемма 4.4. a) Если T ∪{ϕ} ⊆ F or

и T `

ϕ, то θ(T ) `

⊥

θ(ϕ). b) Если T ∪{ϕ} ⊆

F or

и T `

ϕ, то ρ(T ) `

⊥

ρ(ϕ).

Доказательство. а) Предположим ϕ

, . . . , ϕ

- вывод формулы ϕ в логике Lj

Покажем, что θ(ϕ

), . . . , θ(ϕ

) - вывод формулы θ(ϕ) в логике Lj

⊥

. Если ϕ

получена

из одной из аксиом A1-A8 логики Lj

подстановкой формул ψ

, то θ(ϕ

) получена

из той же аксиомы подстановкой формул θ(ψ

) и следовательно является аксиомой

логики Lj

⊥

. Трансляция θ аксиомы A9 даёт формулу (p → q) → ((p → (q → ⊥)) →

(p → ⊥)), эквивалентную аксиоме A2 в логике Lj

⊥

. Таким образом трансляция θ

аксиомы Lj

отображает в аксиомы Lj

⊥

. Предположим α → β и α - доказуемые

формулы логики Lj

и уже доказано, что θ(α → β) и θ(α) - формулы, выводимые

в Lj

⊥

из гипотез θ(T ). Так как θ(α → β) = θ(α) → θ(β), то формула θ(β) является

следствием формул θ(α → β) и θ(α) по правилу modus ponens и поэтому также

выводима в логике Lj

⊥

из гипотез θ(T ).

b) Предположим ϕ

, . . . , ϕ

- вывод формулы ϕ в логике Lj

⊥

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

ρ(ϕ

), . . . , ρ(ϕ

) - вывод формулы ρ(ϕ) в логике Lj

. Если ϕ

получена из одной

из аксиом A1-A8 логики Lj

⊥

подстановкой формул ψ

, то ρ(ϕ

) получена из той же

аксиомы подстановкой формул ρ(ψ

) и следовательно является аксиомой логики Lj

Таким образом трансляция ρ аксиомы Lj

⊥

отображает в аксиомы Lj

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

α → β и α - доказуемые формулы логики Lj

⊥

и уже доказано, что ρ(α → β) и ρ(α)

- формулы, выводимые в Lj

из гипотез ρ(T ). Так как ρ(α → β) = ρ(α) → ρ(β),

то формула ρ(β) является следствием формул ρ(α → β) и ρ(α) по правилу modus

ponens и поэтому также выводима в логике Lj

⊥

из гипотез ρ(T ).

Лемма 4.5. a) ρθ(ϕ) ≡ ϕ,

b) θρ(ϕ) ≡ ϕ.

Доказательство. а) Докажем вначале эквивалентность ¬ϕ ≡ ϕ → ¬(p

→ p

1. ϕ гипотеза,

2. ϕ → ((p

→ p

) → ϕ аксиома A1,

3. (p

→ p

) → ϕ из 1, 2 по правилу m.p.,

4. ¬ϕ гипотеза,

5. ¬ϕ → ((p

→ p

) → ¬ϕ аксиома A1,

6. (p

→ p

) → ¬ϕ из 4, 5 по правилу m.p.,

7. ((p

→ p

) → ϕ) → ((( p

→ p

) → ¬ϕ) → ¬ (p

→ p

))

аксиома A9,

8. ((p

→ p

) → ¬ϕ) → ¬ (p

→ p

)

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

9. ¬(p

→ p

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

Мы доказали секвенцию ¬ϕ, ϕ ` ¬(p

→ p

). Применив теорему дедукции, полу-

чим ¬ϕ ` ϕ → ¬(p

→ p

). Докажем обратное утверждение ϕ → ¬(p

→ p

) ` ¬ϕ.

1. p

→ p

теорема Lp,

2. (p

→ p

) → ¬¬(p

→ p

) теорема Lp

3. ¬¬(p

→ p

) из 1, 2 по правилу m.p.,

4. ϕ → ¬(p

→ p

) гипотеза,

5. ¬¬(p

→ p

) → ¬ϕ из 4 по правилу контрапозиции,

6. ¬ϕ из 3, 5 по правилу m.p..

Утверждение а) верно для пропозициональных переменных. Далее проведём до-

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

, ψ

с помощью одной из связок ∧, ∨, →, т.е. ϕ = ψ

∗ ψ

, где ∗ ∈ {∧, ∨, →}, и для

более коротких формул утверждение а) верно. Тогда ϕ = ψ

∗ ψ

≡ ρθ(ψ

) ∗ ρθ(ψ

) =

ρθ(ψ

∗ ψ

) = ρθ(ϕ). Пусть теперь ϕ = ¬ψ. В силу доказанного ϕ ≡ ψ → ¬ (p

→ p

) ≡

ρθ(ψ) → ¬(p

→ p

) = ρθ(¬ψ), что и требовалось доказать.

Утверждение b) также докажем индукцией по длине формулы. Утверждение b)

верно для пропозициональных переменных. Нетрудно видеть, что в Lj

⊥

справедлива

эквивалентность ⊥ ≡ ((p

→ p

) → ⊥. В силу индуктивного предположения θρ(ψ

∗

) = θρ(ψ

) ∗ θρ(ψ

) ≡ ψ

∗ ψ

Из лемм 4.2 и 4.5 вытекает

Следствие 4.6. Логика Lj

не тривиальна.

Теорема 4.7. Трансляции θ и ρ обладают следующими свойствами:

a) для любого подмножества T ⊆ F or

и для любой формулы ϕ ∈ F or

T `

ϕ ⇐⇒ θ(T ) `

⊥

θ(ϕ),

b) для любого подмножества T ⊆ F or

⊥

и для любой формулы ϕ ∈ F or

⊥

T `

⊥

ϕ ⇐⇒ ρ(T ) `

ρ(ϕ),

Достаточность в обоих утверждениях доказана в лемме 4.4. Необходимость до-

кажем от противного. В силу теоремы дедукции утверждения достаточно доказать

для T = ∅, т.е. только для доказуемых формул. Предположим существует формула

ϕ ∈ F or

недоказуемая в Lj

, но трансляция θ(ϕ) которой доказуема в Lj

⊥

. Соглас-

но пункту b) леммы 4.4 формула ρθ(ϕ) доказуема в Lj

, что противоречит пункту

b) леммы 4.5. Аналогично доказывается второй пункт теоремы.

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

1. Если трансляция формулы α из F or

является аксиомой Lj

⊥

, то будет ли α

аксиомой Lj

2. Если формула ψ ∈ F or

⊥

получена по правилу modus ponens из формул, явля-

ющихся трансляциями, то является ли ψ трансляцией?

3. Если формула ψ ∈ F or

⊥

полученная по правилу modus ponens из аксиом α, β

логики Lj

⊥

, является трансляцией, то являются ли α, β трансляциями аксиом логики

5 Лекция 5. Свойства некоторых расширений логи-

ки Lp

Определим ряд расширений логики Lp.

1. Li = Lj

⊥

+ {⊥ → p} ' интуиционистская логика,

2. Ln = Lj

⊥

+ {⊥} минимальная негативная логика,

3. Lk

= Lp + {((p → q) → p) → p}

классическая позитивная логика,

4. Lk = Li + {p ∨ (p → q)} классическая логика,

5. Le = Lj + {p ∨ (p → q)} логика классической опровержимости,

6. Lmn = Ln + {p ∨ (p → q)} максимальная негативная логика,

Классическая позитивная логика Lk

Далее символом P будем обозначать аксиому ((p → q) → p) → p, а символом E -

аксиому p ∨ (p → q).

Лемма 5.1. В логике Lp + E справедливы эквивалентности:

1) ((p ∧ q) → r) ≡ ((p → r) ∨ (q → r)),

2) (p → q) → r ≡ r ∨ p ∧ (q → r),

3) p → (q ∨ r) ≡ (p → q) ∨ (p → r).

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

уже доказанные секвенции и эквивалентности.

1. p → r ` (p → r) ∨ (q → r) в силу аксиомы A6,

2. p → r, (p ∧ q) → r ` (p → r) ∨ (q → r) следует из 1,

3. p → r ` ((p ∧ q) → r) → ((p → r) ∨ (q → r))

по теореме дедукции из 2,

4. p, q, (p ∧ q) → r ` r

по правилу объединения посылок и правилу m.p.,

5. p, (p ∧ q) → r ` q → r по теореме дедукции из 4,

6. p, (p ∧ q) → r ` (p → r) ∨ (q → r) по m.p. из 5 и A7,

7. p ` ((p ∧ q) → r) → ((p → r) ∨ (q → r)) по теореме дедукции из 6,

8. ` p ∨ (p → r) аксиома E,

9. p → r, (p ∧ q) → r ` (p → r) ∨ (q → r) по аксиоме вида A6,

10. p → r ` ((p ∧ q) → r) → ((p → r) ∨ (q → r))

по теореме дедукции из 9,

11. ` ((p ∧ q) → r) → ((p → r) ∨ (q → r)) по m.p. из 7, 8, 10 и A8,

1. p ∧ q ` p по m.p. из A3,

2. p ∧ q ` q по m.p. из A4,

3. p → r, p ∧ q ` r по m.p. в силу 1,

4. q → r, p ∧ q ` r по m.p. в силу 2,

5. p → r ` (p ∧ q) → r по теореме дедукции из 3,

6. q → r ` (p ∧ q) → r по теореме дедукции из 4,

7. ` (p → r) → ((p ∧ q) → r ) по теореме дедукции из 5,

8. ` (q → r) → ((p ∧ q) → r) по теореме дедукции из 6,

9. ` [(p → r) → ((p ∧ q) → r )] →

[[(q → r ) → ((p ∧ q) → r)] → [((p → r) ∨ (q → r)) → ((p ∧ q) → r)]]

аксиома A8,

10. [(q → r ) → ((p ∧ q) → r)] → [((p → r) ∨ (q → r)) → ((p ∧ q) → r)]

из 7,9 по m.p.

11. [((p → r) ∨ (q → r)) → ((p ∧ q) → r)]

из 8,10 по m.p.

` (p → (q → r)) ≡ ((p ∧ q) → r) ≡ ((p → r) ∨ (q → r))

1. r → ((p → q) → r) аксиома A1,

2. p ∧ (q → r), (p → q) ` r доказуемая секвенция,

3. p ∧ (q → r) ` (p → q) → r из 2 по теореме дедукции,

4. ` (p ∧ (q → r)) → ((p → q) → r) из 3 по теореме дедукции,

5. ` [r → ((p → q) → r)] →

[[(p ∧ (q → r)) → ((p → q) → r)] → [(r ∨ p ∧ (q → r)) → ((p → q) → r)]]

аксиома A8

6. ` (r ∨ p ∧ (q → r)) → ((p → q) → r) по правилу m.p. из 1, 4, 5

Для доказательства обратной импликации докажем ряд секвенций.

1. q → (p → q) аксиома A1,

2. q гипотеза,

3. p → q по m.p. из 1, 2,

4. ((p → q) → r) гипотеза,

5. r из 3, 4 по m.p..

Итак, доказана секвенция ((p → q) → r), q ` r. Применяя к ней теорему дедукции,

получим секвенцию ((p → q) → r) ` q → r.

1. r гипотеза,

2. r → q ∨ r аксиома A7,

3. q ∨ r по m.p. из 1, 2,

4. q ∨ r → p гипотеза,

5. p по m.p. из 3, 4.

Мы доказали секвенцию r, q ∨ r → p ` p. Применяя теорему дедукции, получим

q ∨ r → p ` r → p. Докажем секвенцию ((p → q) → r), q ∨ r → p ` p.

1. ((p → q) → r) гипотеза,

2. q ∨ r → p гипотеза,

3. r → p из 2 в силу доказанной ранее секвенции,

4. ((p → q) → p) по правилу сечения из 1,3,

5. p → p доказанная формула,

6. (p → p) → [((p → q) → p) → ((p ∨ (p → q)) → p)]

аксиома A8,

7. ((p → q) → p) → ((p ∨ (p → q)) → p)

из 5, 6 по m.p.,

8. (p ∨ (p → q)) → p из 4, 7 по m.p.,

9. p ∨ (p → q) аксиома E,

10. p из 8, 9 по m.p..

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

1. ((p → q) → r), q ∨ r → p ` p доказано ранее,

2. (p → q) → r ` q → r доказано ранее,

3. ((p → q) → r), q ∨ r → p ` p ∧ (q → r)

из 1, 2 по правилу объединения посылок,

4. ((p → q) → r), q ∨ r → p ` r ∨ p ∧ (q → r)

из 3 согласно аксиоме A7,

5. q, ((p → q) → r) ` r доказано ранее,

6. q, ((p → q) → r) ` r ∨ p ∧ (q → r) из 5 в силу А6,

7. q ` ((p → q) → r) → r ∨ p ∧ (q → r) из 6 по теореме дедукции,

8. r ` r ∨ p ∧ (q → r) в силу A6,

9. r, (p → q) → r ` r ∨ p ∧ (q → r) в силу п.8,

10. r ` ((p → q) → r) → r ∨ p ∧ (q → r) из 9 по теореме дедукции,

11. q ∨ r → p ` ((p → q) → r) → r ∨ p ∧ (q → r)

по теореме дедукции из п.4,

Для сокращения записей введём обозначение X = ((p → q) → r) → r ∨ p ∧ (q → r)

и продолжим доказательство.

12. ` q → X по теореме дедукции из п.7,

13. ` r → X по теореме дедукции из п.10,

14. ` (q → X) → ((r → X) → (q ∨ r → X))

аксиома A8,

15. ` (q ∨ r → X) из 12, 13, 14 по m.p.,

16. q ∨ r → p ` X п.11,

17. ` (q ∨ r → p) → X по теореме дедукции из п.16,

18. ` (q ∨ r → X) → [((q ∨ r → p) → X) → (((q ∨ r) ∨ (q ∨ r → p)) → X)]

аксиома A8,

19. (((q ∨ r) ∨ (q ∨ r → p)) → X)

по m.p. из 15, 17, 18,

20. ((q ∨ r) ∨ (q ∨ r → p)), аксиома E,

21. ` X из 19, 20 по m.p..

3) Секвенция (p → q) ∨ (p → r) ` p → (q ∨ r) была ранее доказана в Lp. Для

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

квенцией p → (q ∨ r) ` p → ((p → q) ∨ (p → r)).