Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

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

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

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

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

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

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

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

и правило

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

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

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

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

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

n(X,Y) = n(X)»n(Y),

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

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

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

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

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

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

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

Особый интерес представляла бы для нас системы типа SUL. В этом случае нам потребовалась бы связка Ш2, а затем пришлось бы расширить SL с помощью правила

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

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>