Если " A истинно" без допущений вида " B истинно", то " A допустимо".
Это категорическое суждение усваивается как унарная связка ◻ A (читай "обязательно A ") со следующими правилами введения и исключения:
| Действительный ─────── ◻ I ◻ Истинный | ◻ Истинный ──────── ◻ E Истинный |
Обратите внимание, что посылка "Действительная" не имеет определяющих правил; вместо этого вместо нее используется категорическое определение действительности. Этот режим становится понятнее в локализованной форме, когда гипотезы являются явными. Мы пишем " Ω ; Γ ⊢ A true ", где Γ , как и раньше, содержит истинные гипотезы, а Ω содержит действительные гипотезы. Справа есть только одно суждение " Истинное"; достоверность здесь не нужна, поскольку " Ω ⊢ Действительное" по определению совпадает с " Ω ; ⋅ ⊢ Истинным". Вводная и исключающая формы тогда:
| Ω; ⋅ ⊢ π : Истинное ──────────────────── ◻ Я Ω; ⋅ ⊢ поле π : ◻ Истинное | Ω;Γ ⊢ π : ◻ Истинное ────────────────────── ◻ E Ω;Γ ⊢ распаковать π : истинное |
Модальные гипотезы имеют свою собственную версию правила гипотезы и теоремы подстановки.
| ─────────────────────────────── допустимо- hyp Ω , u : (действительный) ; Γ ⊢ u : истинный |
Теорема о модальной подстановке
Если Ω ; ⋅ ⊢ π 1 : истинно и Ω , u : ( допустимо) ; Γ ⊢ π 2 : C истинно , тогда Ω ; Γ ⊢ [ π 1 / u ] 2 : C истинно .
Эта структура разделения суждений на отдельные наборы гипотез, также известная как многозональные или полиадические контексты, является очень мощной и расширяемой; она применялась для многих различных модальных логик, а также для линейных и других субструктурных логик , чтобы привести несколько примеров. Однако относительно небольшое количество систем модальной логики может быть формализовано непосредственно в естественной дедукции. Дать теоретико-доказательные характеристики этих систем, расширения, такие как маркировка или системы глубокого вывода.
Добавление меток к формулам позволяет гораздо точнее контролировать условия, при которых применяются правила, позволяя применять более гибкие методы аналитических таблиц , как это было сделано в случае дедукции с метками . Метки также позволяют именовать миры в семантике Крипке; Симпсон (1993) представляет влиятельную технику преобразования фреймовых условий модальной логики в семантике Крипке в правила вывода в формализации естественной дедукции гибридной логики . Stouppa (2004) рассматривает применение многих теорий доказательства, таких как гиперследности Аврона и Поттинджера и логика отображения Белнапа к таким модальным логикам, как S 5 и B .
Сравнение с другими основополагающими подходами