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

Докажите следующие теоремы модального исчисления высказываний (S4):

Задание 14. □ 𝑝 ⇒⋄𝑞 ⇒ (□⋄𝑝 ⇒ ¬(⋄¬𝑝 ⇒ □¬𝑞)⇒⋄□¬𝑝)
каждый шаг распиши максимально подробно

Основной особенностью модальных исчислений является прямая зависимость от их мо
делей. Поэтому в зависимости от свойств шкал Крипке выделяется несколько модальных
пропозициональных исчислений.
Минимальная логика K
Аксиомы:– Аксиомыпропозиционального исчисления– (AK): □(A ⊃ B) ⊃(□A⊃□B)(аксиомаКрипке,основная модальная аксиома)
Правила вывода:– MP:A,A⊃B ⊢B– □:A⊢□A– Подстановка Sub: A ⊢ [a/x]A
Такой минимальнойлогикесоответствует любая произвольная шкала Крипке.. Добавле
ние каждого из свойств регулируется следующей аксиомой:– (R□): □p ⊃ p(рефлексивность)– (T□): □p ⊃ □□p(транизитивность)– (S□): p ⊃ □♢p(симметричность)
52
Добавляя каждую такую аксиому к минимальному исчислению будем получать новое
исчисление. Среди возможных вариантов выделяют следующие 3:– Исчисление S3: AK +R□– Исчисление S4: AK +R□+T□– Исчисление S5: AK +R□+T□+S□
Замечание. Заметим,чтовопределенииминимальногоисчисленияK указано,чтооновклю
чает в себя аксиомыпропозициональногоисчисления, нонеуказано, какого конкретно. По
умолчанию, будем считать, что имеется ввиду исчисление P2. В то же время, можно взять в
качестве базового исчисления интуиционистское Pi и получитьмодальнуюинтуиционист
скую логику.
Также, в зависимости от выбранного базового исчисления, имеют место и доказанные
в этих исчислениях теоремы — для P2 это теорема дедукции, теорема о подстановочности
эквивалентности и именные теоремы.
5.4. Теоремы модального пропозиционального исчисления
Замечание. Учитывая, что имеется несколько модальных исчислений, при доказательстве
необходимо указывать, в рамках какого исчисления была доказана та или иная формула.
Т 5.1. (I♢): p ⊃ ♢p
Доказательство. В данном выводе используется аксиома R□, значит данная теоремы вы
полнима в исчислении S3, то есть на любых рефлексивных шкалах Крипке.

1. ⊢p⊃q⊃(q ⊃p)
2. ⊢□p⊃p⊃(p⊃
   C¬′
   □p) [□p/p,p/q]1
3. ⊢□p⊃p
4. ⊢□p⊃p
5. ⊢p⊃
6. ⊢p⊃
   □p
   □p
7. ⊢p⊃♢p
   Т 5.2. (I□
   ♢): □p ⊃ ♢p
   R□
   [p/p]3
   MP(4,2)
   ES(≡¬,5)
   Def♢(6)
   ■
   Доказательство. Данная теорема устанавливает связь между модальностями аналогичную
   связимеждукванторами.Втожевремя,длядоказательстваэтойтеоремынеобходимоиметь
   аксиому R□. Это означает, что только в рефлексивных шкалах возможна связь такого рода.
8. ⊢q ⊃s⊃(p⊃q⊃(p⊃s))
   B
9. ⊢p⊃♢p⊃(□p⊃p⊃(□p⊃♢p)) [□p/p,p/q,♢p/s]1
10. ⊢□p⊃p⊃(□p⊃♢p)
    MP(I♢,2)
11. ⊢□p⊃♢p
    MP(R□,3)
    ■
    Определение 5.7. В модальной логике, наряду с материальными связками ⊃ и ≡, вводятся
    также строгие связки ⇒ и ⇔, которые определяются следующим образом:
    53
    – p⇒q:=□(p⊃q)– p⇔q:=□(p≡q)
    Т 5.3. (K□): p ⇒ (q ⇒ p)
    Доказательство.
    Т 5.4. ⊢ □p ⊃ p ≡p⊃♢p
12. p ⊢q ⊃p
    MP(K)
13. q ⊃p⊢□(q ⊃p) [q⊃p/p]□
14. p ⊢□(q ⊃p)
15. ⊢p⊃□(q ⊃p)
16. ⊢□(p ⊃□(q ⊃p))
17. ⊢p⇒(q ⇒p)
    Доказательство. Необходимость:
18. ⊢(p ⊃q) ⊃(q ⊃p)
19. ⊢(
    MP(2,1)
    TD(3)
    □(4)
    Def⇒
    C¬′
    ♢p ⊃p) ⊃(p⊃♢p) p/q,♢p/p
20. ⊢(□p ⊃p)⊃(p⊃♢p)
    Def□
21. □p⊃p⊢□p⊃p
22. □p⊃p⊢p⊃♢p
    Доказательство. Достаточность:
23. ⊢(p ⊃q) ⊃(q ⊃p)
24. ⊢(p ⊃
    Sub
    MP(4,2)
    C¬′
    □p) ⊃ (□p ⊃p) □p/q
25. ⊢(p ⊃♢p) ⊃(□p⊃p) Def♢(1)
26. p ⊃♢p⊢p⊃♢p
    Sub
27. p ⊃♢p⊢□p⊃p
    Т 5.5. ⊢ □(p∧q) ≡ (□p∧□q)
    Доказательство. Необходимость:
28. ⊢□(p ⊃q)⊃□p⊃□q
29. ⊢□(p∧q ⊃q)⊃□(p∧q)⊃□q
30. ⊢□(p∧q ⊃q)
31. □(p∧q) ⊢ □q
    MP(4,2)
    p ∧ q/p
    TD(MP(3,2))
32. ⊢□(p∧q ⊃p)⊃□(p∧q)⊃□p p∧q/p,p/q
33. ⊢□(p∧q ⊃p)
34. □(p∧q) ⊢ □p
35. □(p∧q) ⊢ □p∧□q
    TD(MP(6,5))
    And(7,4)
    ■
    ■
    ■
    AK
    □(∧R)
    □(∧L)
    54
    ■
    Доказательство. Достаточность:
    AK

⊢ □(p ⊃q) ⊃□p⊃□q
⊢ □(p ⊃(q ⊃p∧q)) ⊃□p⊃□(q ⊃p∧q)
⊢ □(p ⊃(q ⊃p∧q))
⊢ □p⊃□(q ⊃p∧q)
□p ⊢□(q ⊃p∧q)
⊢ □(q ⊃p∧q)⊃□q ⊃□(p∧q)
⊢ □p⊃(□q ⊃□(p∧q))
⊢ p ⊃(q ⊃r)⊃(p∧q ⊃r)
q ⊃ p∧q/q
□(And)
MP(3,2)
MP(4)
q/p, p ∧ q/q
TD(MP(4,6))
т. о соединении посылок
⊢ (□p ⊃(□q ⊃□(p∧q))) ⊃ □p∧□q ⊃□(p∧q) [□p/p,□q/q,□(p∧q)/r]
10. ⊢ □p∧□q ⊃□(p∧q)
MP(9,7)