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

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

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


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

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

Рассмотрим теперь секвенциальную формулировку LJ интуиционистской логики согласно [Такеути 1978]. Начальные секвенции Ы имеют вид а —> а для любой пропозициональной переменной а. Правила вывода имеют следующий вид:

Для интерпретации в терминах Н-категорий данного списка правил нам потребуется ввести некоторые новые понятия. Пусть, как и раньше, С будет Н-категорией.

Определение 1. Предтопология на С есть функция, сопоставляющая каждому С-объекту р совокупность Cov(p) множеств С- стрелок с концом вр (покрытий), таких, что:

  • (i) 1 peCov(p)
  • (ii) если [р, —> р: iel} и для любого iel мы имеем {p'j->pi: jeJi} еСо>(р,), то {p'j -> р;. iel & jeJi) eCovfp);
  • (iii) если q-+peCov(p), то (r,q)->peCov(p), и наоборот ((-,->-замкнутость).

Нетрудно проверить, что наша предтопология будет предтопо- логией Гротендика и, более того, пара (C,Cov) есть ситус.

Теперь наша главная идея заключается в отождествлении секвенций с покрытиями. Поэтому мы переводим любую произвольную секвенцию Г-эа как Cov(a), где а является Н-категорным переводом формулы а.

Единственной проблемой является существование N-функтора в наших Н-категориях, поскольку мы должны описать взаимодействие N-функтора и покрытий в ситусе (С,Соу). Поэтому мы налагаем на предтопологию еще одно ограничение:

(iv) каждое Cov(p) максимально по отношению к N-функтору, т.е. либо aeCov(p), либо NaeCovip), но не одновременно.

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

Доказательство. Аксиома: следует из l(i).

  • (ослабление —>): по l(iii) и в силу произвольности наших множеств индексов. Фактически это просто означает добавление произвольного члена с—у а в Cov(a).
  • (—^ослабление): Г —> мы интерпретируем как Cov(O) = {а, —у 0: iel}, где а, есть интерпретация формул из Г. 1 есть инициальный объект, поэтому мы имеем о, —у 0 —у а и по 1 (ii) любое Cov(0) порождает Cov(a).
  • (сокращение): так как наше множество индексов / не является мультимножеством и ввиду того, что а = {ала) в Н-категориях.
  • (перестановка): ввиду неупорядоченности множества индексов, (сечение): является следствием 1 (ii).
  • (—эо): следует из того, что в Н-категориях существует стрелка Ь-у а => Ь.
  • (з->): по (о,Ь) —» 6 и l(ii)-(iii) мы получаем, что Cov(a) с Cov{c) (где а,с являются переводами а,у соответственно). Затем по => b, b => с)—у а => с и по l(ii)-(iii) мы получаем а=> Ь-у Cov(c). (—»vl),(—>v2): по а -у [а,Ь] и [а,Ь] —> [6,а].
  • (v->): используя диаграмму определения [-,-].
  • (л->1),(л->2): по (а,Ь) -> {Ь,а) и (а,Ь) -У а.
  • (—>л): по определению произведений в С мы имеем

и, следовательно, Cov(a) и Cov(b) будут Cov((a,b)) с (а,Ь)-Уа и (a,b)-yb соответственно.

(—!—»): Так как (a,Na) = 0 и 0 является инициальным С- объектом, то мы имеем 0 -у aeCov(a) и (a,Na) -у aeCov(a). Затем из диаграммы

легко можно видеть, что по 1(H) мы получаем Na —» OeCov(O) и (о,- —? 0: /e/}eCov(0) и множество / индексов здесь то же, что и для Cov(a). Следовательно, мы получили интерпретацию нижних секвенций, используя 1 (iv).

(—>—i): вновь мы используем (a,Na) = 0 и (a,Na) —> Na. Ввиду ((a,Na),ai) —? (a,Na) мы из {{a,Na),a,) —> (a,Na) —> Na и no l(iii) получаем {я,-> Na: iel)eCov(Na). Затем мы используем l(iv).B

Обычно каждая секвенция ai, ... , ат -> р имеет формульный эквивалент опл ... латз р. Наше свойство 1(Ш) дает нам, фактически, одно-однозначное отображение fH: Cov —> Form, где Form есть множество переводов формул, определенное для каждого покрытия как Cov(a) ?— (л;-) => а. Однако существуют некоторые неклас-

ie/

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

Тем не менее, в нашем случае существование подобных эквивалентов делает наши последующие шаги тривиальными, и мы получаем теорему полноты путем использования fH стандартным образом.

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