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

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

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


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

Секвенции в полиситусах (классическая логика)

В случае секвенциальной формулировки классической логики начальные секвенции нашей соответствующей системы LK те же самые. Правила вывода имеют следующий вид:

Главная трудность заключается в том, что мы не имеем права интерпретировать секвенцию Г—»Д как покрытие некоторого С- объекта, ибо по правую сторону у нас также стоит список формул. Создается впечатление, что причина интерпретации секвенций как покрытий в Н-категориях связана с экспоненцированием, ибо из a—*beCov(b) мы заключаем, что a=>b—>beCov{b) и, следовательно, покрытия всегда замкнуты относительно <-,->и (для мы получаем это по определению). В случае интерпретации алгебры Брауэра в категориях предпорядка мы имеем дело с дуальным экспоненцированием, вследствие чего мы должны рассматривать ко- покрытия и коситусы. Более того, с точки зрения подобного подхода в случае НВ-апгебр мы имеем дело с двумя экспоненциалами одновременно и, как следствие, вынуждены рассматривать бипокрытия, образованные покрытиями и копокрытиями и соответственно нам требуется конструкция биситусов.

Рассматривая подобным образом булевы алгебры, мы приходим к заключению, что нам необходимо учитывать самодуальность классической логики [Ермолаева 1972].

Наш основной технический прием теперь заключается в использовании нашего словаря перевода в N-категорию.

Определение 1. Интерпретацией секвенции Г—>Д в С является {Cov(pj):е /} U {CoCov(q j): j е J), где р, принадлежит множеству переводов формул из Г, q, принадлежит множеству переводов формул и Д и С есть N-категория.

Мы обозначаем {Cov(p-): / е /} U {CoCov(q j): j е J) как

PCov(G,D) (полипокрытия), где G,D представляют собой списки переводов формул из Г,Д соответственно, и говорим, что (C,PCov) является полиситусом. Для получения максимальных полипокрытий мы требуем, чтобы наши копокрытия также были максимальными по отношению к N-функтору.

Теорема 1. Все аксиомы и правила вывода LK могут быть интерпретированы в полиситусе (C.PCov), где С есть N-категория.

Доказательство. Аксиома: по определениям покрытий и копо- крытий.

  • (ослабление —>): как в 2.4 (повторенное для всех покрытий из PCov(G,D)).
  • (-> ослабление): ввиду 1.2.(VII)-(VIII) и по З.З.(Ш).
  • (сокращение —>): как в 2.4 (повторенное для всех покрытий из PCov{G.D)).
  • (-> сокращение): ввиду того, что наши множества индексов в копокрытиях не являются мультимножествами и [а,а]—>а.
  • (перестановка —>): как в теореме 1 для интуиционистской логики (повторенное для всех покрытий из PCov{G,D)).
  • (—> перестановка): ввиду отсутствия упорядочения индексов в наших копокрытиях.
  • (сечение): ввиду транзитивности замкнутости наших покрытий и копокрытий.
  • (—>з): как в теореме 1 для интуиционистской логики. Здесь мы должны принять во внимание то, что лишь наши покрытия замкнуты относительно экспоненциала => (копокрытия замкнуты относительно коэкспоненциала <=).
  • (з—э): доказываем как в теореме 1 для интуиционистской логи- Г —> а Д,Е —> Д

ки правило - (соответствующим повторением) и

азД,Г,1->Д

затем доказываем (-> ослабление) для всех членов D, где D есть N- категорный перевод Д.

  • (—»vl),(—»v2): для Г—>а как в теореме 1 для интуиционистской логики и для копокрытий ввиду пункта (Ш) из определения копокрытий.
  • (v—>): как в теореме 1 для интуиционистской логики для а,Г—э<5, ДГ—эД (где <5еД) и ввиду (iii) из определения копокрытий.
  • (—>д): как в теореме 1 для интуиционистской логики для Г—>а, Г—>Ди по определению (-,-) для копокрытий.
  • (л-И),(л-»2): по (а,Ь) —> (Ь,а) и (а,Ь)—>а.
  • (—|—э): —эД мы интерпретируем как {1 -э р/: / е /} е CoCov(l)

где р,еD (D есть перевод Д). Для Г-э? (где 8eD) мы используем (ослабление —>) и для копокрытий наше доказательство дуально доказательству теоремы 1 для интуиционистской логики (используя [a,Na] = 1 и терминальность 1), принимая во внимание максимальность копокрытий.

(->-.): Для покрытий мы используем (ослабление -»), а для копокрытий доказательство дуально доказательству теоремы 1 для интуиционистской логики. ?

Каждая секвенция а^,...,ат —э р^,...,рп из LK имеет формульный эквивалент aj л... л ат —> Д| v... v Рп. Отсюда, как в слу

чае 2.7, путем использования 2.2.(Ш) и 3.5.(Ш) мы получаем отображение fc. PCov->Form, определенное как

PCov(G,D)h> J^[a- => Jj , где abb, принадлежат G,D соответ-

ie/ jeJ

ственно. Мы получаем полноту нашей интерпретации LK в полиси- тусах, используя наше отображение /с стандартным образом.

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