(CT) Следствие T:
T → (∀Q)(Q → ◊Q)
Правило необходимости:
(∀Q)(⊢Q → □Q)
Определение 1:
B = (∀P)(P → □◊P)
A1 (предположение 1):
T
D1 (Modus Ponens, A1, CT):
(∀Q)(Q → ◊Q)
A2 (предположение 2):
~(∀P)(P → □◊P)
1 (Существенное значение, A2):
~(∀P)(~PV□◊P)
2 (Изменение квантификатора, 1):
(∃P)~(~PV□◊P)
3 (Закон Де Моргана, 2):
(∃П)(~~П&~□◊П)
4 (двойное отрицание, 3):
(∃P)(P&~□◊P)
5 (Экзистенциальное воплощение, 4):
П&~□◊П
6 (Упрощение, 5):
P
7 (универсальная реализация, D1):
P → ◊P
8 (Модус Поненс, 7, 6):
◊P
9 (Правило необходимости, 8):
□◊P
10 (Упрощение, 5):
~□◊P
11 (Союз, 9, 10):
□◊П&~□◊П
Предполагаемое косвенное доказательство AIP (A2 — 11):
(∀P)(P → □◊P)
Д2 (Замена, АИП, Защита 1):
B
Предполагаемое условное доказательство ACP (A1-D2):
T → B
Вывод:
T → B
Почему S4 подразумевает S5:
Предпосылка 1:
T → B
Определение 1:
S4 = (Т&(К&4))
Определение 2:
S5 = (S4 и B)
A1 (предположение 1):
S4
D1 (Замена, Защита 1, A1):
Т&(К&4)
D2 (упрощение, D1):
T
Д3 (Модус Поненс, Д2, П1):
B
D4 (Соединение, A1, D3):
S4&B
Д5 (Замена, Д4, Защита 2):
S5
Предполагаемое условное доказательство (A1-D9):
S4 → S5
Вывод:
S4 → S5
