Модальный аналог двухуровневой теоремы дедукции

Рассмотрим теперь язык ПР, получаемый путем добавления унарного пропозиционального оператора ?. Мы строим язык ПР² точно так же, как язык Р² был построен на основании Р. Предположим, что у нас есть система DS в языке DP, которая представляет собой расширение S за счет некоторых стрелок и операций с ?, и добавим к системе DS^L в DP², полученной из OS так же, как S^L была получена из S, следующее правило:

Постараемся выяснить, каковы будут последствия этого шага для стрелок и операций QS. Допустим, что теперь DS представляет собой DNL, a DS^l есть DNL, т. е. мы имеем слабейшую из наших логик со слабейшей металогикой. Мы получаем следующий вывод в? NL^nl + (?):

Назовем эту секвенцию (пес), поскольку она утверждает, что в ONL мы должны иметь операции на стрелках, соответствующие гёделевскому правилу введения необходимости.

Кроме этого в DNL^nl + (?) имеется следующее правило сечения:

из которого с помощью (U)4, сечения с (иЛ"Т1- ЗВ) —> (ТЬ ПА з QS), затем сечения с (Ть А з В) —> (Ah В) и применяя (?)4 и сечение со стрелками Т, получаем 0 —> (П (А эй) К (ЗА з DS)). Таким образом, в LINL имеется следующая стрелка d_{A B}: С (А з В Ь ПА =з ОВ, и частичная одноместная операция на стрелках:

Нетрудно показать, что стрелка d_{A B} и операция пес могут быть заменены в на следующие стрелки:

и правило.

Легко также получить, что в DNL у нас имеется стрелка? (В<=А) — П5 <= ПА.

Покажем теперь, что DNL может быть аксиоматизирована путем расширения NL в ПР за счет операции пес и следующих стрелок:

при условии, что в В_квс, В°_АВС либо А, либо В, либо С имеет вид? D, и в С_{А В} либо А, либо В

имеет вид QD. Таким образом, мы получаем расширение S4-THna системы NL.

Пусть ?NL^nl получается из GNL так же как и NL^nl была получена из NL, т. е. мы допускаем в? NL^nl стрелки 1/, (°), i/, правило сечения и (-)'i,(-)V Таким образом, мы не принимаем (?). Теперь рассмотрим перевод п из ШР² в ОР: п (АВ) =? (А з В), и (0) = Т,.

n (X, Y) = n (X)"n (Y),

и(X -> (А — В)) = и (Я)н (А з В).

Этот перевод отличается от предыдущего перевода за счет добавления префикса О к переводам стрелок по левую сторону от —к Следующий модальный аналог предложения 5 доказывается тем же способом, что и предложение 5.

Предложение 8. (p: X —> / доказуема в DNL^nl тогда и только тогда, когда п (Х —> f) есть стрелка в GNL.

Как следствие, мы получаем аналог предложения 6 в виде Предложение 9. Система HNL^nl замкнута относительно правила (?).

Доказательство. Мы имеем:

• (1) (Th- А) X —> (SiС) в DNL^nl тогда и только тогда, когда 0(Т з А)"п (Х)ЬBz>Cb DNL,
• (2) тогда и только тогда, когда п (Х) — (Ш/4"В) з С в UNL,
• (3) тогда и только тогда, когда X —> (ПА"В- С) в? NL^nl. ?

Таким образом, мы приходим к заключению, что модальные постулаты GNL^nl необходимы и достаточны, чтобы DNL^nl была замкнута относительно (?).

Особый интерес представляла бы для нас системы типа S^UL. В этом случае нам потребовалась бы связка Ш², а затем пришлось бы расширить S^L с помощью правила.

что привело бы к получению модальной логики на уровне S^L, а не на уровне S, который бы не подвергся изменениям. Роль D² в DNL^nl фактически выполнял оператор пес, преобразующий стрелку / Т I- А в стрелку nec (/): Т I- 04, однако его действие было детерминировано оператором? на формулах. В общем же случае, рассматривая D²/ как необходимое доказательство, в отличие от просто доказательства f, А В, можно было бы рассуждать о необходимых выводах, свойства которых определялись бы лишь заданными постулатами. С использованием же дополнительной метасвязку импликации => можно было бы говорить о полученных модальных логиках на метастрелках как о некоторых стратегиях доказательства.