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

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

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


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

Секвенции в биситусах (Н-В логика)

Пропозициональное исчисление Н-В логики представляет собой исчисление интуиционистской логики с двумя дополнительными связками —, г [Rauszer 1973].

Список аксиом Н-В логики состоит из всех формул вида:

Единственными правилами вывода являются modus ponens и (Г) _о_

-.га

N-категорным эквивалентом Н-В исчисления является HBN- категория, чье определение выглядит следующим образом:

Определение 1. HBN-категория является декартово бизамкну- той конечно биполной категорией предпорядка, снабженной двумя контравариантными функторами Л/,: С —> С и А/;: С —> С, такими, что:

  • 00
  • (iii) а—>b есть стрелка в С тогда и только тогда, когда а => Ь

= 1иа<=6 = 0 для любых двух объектов а,Ь из С. Декартова бизамкнутость означает здесь наличие одновременно декартовых замкнутости и козамкнутости и, следовательно, существование экспоненциала => и коэкспоненциала <=.

Словарь HBN-категорного перевода очевидным образом является объединением словарей Н- и BN-категорных переводов.

Секвенциальная формальная система GHB для пропозиционального исчисления Н-В логики, согласно [Rauszer 1973, с.25], состоит из множества аксиом вида а—их и множества следующих правил вывода:

Антецедент и сукцедент секвенций в вышеприведенных правилах не могут быть одновременно более чем одноэлементными. Например: в правиле (v->) если Д есть (непустая) секвенция, то Г есть пустая секвенция, а если Г есть (непустая) секвенция, то секвенция Д состоит не более чем из одной формулы.

Теперь мы определяем бипредтопологию на С как объединение предтопологии и копредтопологии, задающую, что для любого объекта р в С существуют одновременно Cov(p) и CoCov(p). Таким образом, мы определяем BiCov(p)=Cov{p)[uCoCov(p) и бипредтопо- логия на С является функцией, отображающей каждый С-объект р в BiCov(p). Следовательно, пара (C,BiCov(p)), в свою очередь, будет представлять собой биситус.

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

Доказательство. Легко видеть, что в свете замечания к определению 1 доказательство становится объединением доказательств дуальных теорем, доказанных ранее. ?

Для любой секвенции Г—> Д эквивалент отображения v в формулы определяется как

где aj,...,aw е Г,е Д . Соответственно, наше отображение fRH'. BiCovForm для бипокрытий должно определяться как

Отсюда проблема полноты рассматриваемого исчисления сводится к проблеме точности отображения/вн-

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