Интуиционистская логика в N-категориях

Как известно, алгебра Гейтинга категорно представляет собой декартово замкнутую конечную кополную категорию предпорядка Н [Гольдблатт 1983]. Нетрудно превратить подобную категорию в N-категорию, если рассмотреть контравариантный функтор N: Н —> Н, такой, что:

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

Как и в случае N-категорий, нетрудно убедиться, что любая аксиома типа а => b = 1 может быть переписана как а —> Ь. Нетрудно, применяя подобное преобразование, получить Н-категорный эквивалент соответствующего списка интуиционистских аксиом.

Определение 1. Пусть Н и Н' будут две Н-категории (с функторами N и N' соответственно). Н-функтором F.H-* Н' будет называться функтор, для которого имеет место (для а, Ь, 1,0 в Н и для Г, 0' в НУ.

С помощью соответствующей модификации метода дедекиндовых сечений для N-категорий [Riscos Laita 1987, с.510] доказываются следующие два предложения (упражнение для читателя):

Предложение 1. Каждая Н-категория имеет полное расширение (полнота означает здесь наличие конечных копроизведений и произведений).

Предложение 2. Пусть А, В, С будут Н-категориями, причем В есть расширение, А и С полна. Любой Н-функтор F: А —" С может быть расширен до Н-функтора Н: В—> С.

С далее будет означать Н-категорию.

Пусть р будет объектом из С и обозначим как С_Г категорию.

с теми же самыми стрелками, что и в С. Если мы определим N_p. С,—>С_Г как NpX=[N_p, p], то легко видеть, что N_p будет представлять собой контравариантный функтор, откуда пара C_P, N_P становится Нкатегорией с р в качестве инициального объекта и теми же самыми произведениями, копроизведениями и экспоненциалами, что и в С. Подобные категории С_р являются очевидными обобщениями понятия принципиальных идеалов алгебры Гейтинга.

Пусть Е будет непустой совокупностью элементов С. Для п>2 рассмотрим.

и определим.

Доказательство следующих свойств очевидно.

Eq (E);

если Е = {р}, то (Е) = Е_р;

(?) = С тогда и только тогда, когда 0б (?) тогда и только тогда, когда существуют объектыр_и е Е_у такие, что (р_и = 0;

если /?,(рщ >€(?);

Если /?е (?), то Е_р с (Е).

Отметим, что наши (Е) являются просто Н-категорными переводами идеалов алгебры Гейтинга.

Отношение ~?, определенное как р ~е Я тогда и только тогда, когда (р => q_y q => р >е (?), есть отношение эквивалентности, по которому можно образовать фактор-множество 01(E). Если мы определим в С/₍?>, что.

||дг|| —> |lv|| есть стрелка тогда и только тогда, когда л:=> у е (?),.

то С/₍?) становится категорией предпорядка. Если мы определим N_e: 01(E) -" 01(E) как N_ex = ||Afe||, то N_E будет контравариантным функтором, так что пара (CI (E), N_e) становится Н-категорией с ||0|| в качестве инициального объекта, ||1|| в качестве терминального объекта, произведениями (IWUWDf⁼ 1К*цУ>||, копроизведениями [ММ]е = [ху] И IMI =>Е у = II* => >>||. Справедливо следующее предложение:

Предложение 3. F: С—>С/(Е), определенный с помощью Fx = x_y есть Н-функтор.

Определение 2. (Е) является максимальным, если не существует такого Е 'с: С, что (Е) с (Е *) с С.

Максимальность эквивалентна С/(Я>= {||0|| -> ||1||>.

Определение 3. Н-категорная интерпретация логики высказываний есть пара (С,(?)), описывающая множество высказываний, содержащее доказуемые высказывания.

Определение 4. Пусть В будет нетривиальной Н-категорией. Боценка есть Н-функтор V С-+В. Элемент ре С называется истинным при У, если Vp = 1. (C.(Zr)) семантически непротиворечива, если существует оценка V, такая, что реЕ влечет Vp= 1.

При этих условиях легко доказать, что Vp = 1 для всех /?€(?), и также, что применение ||V||: С/_(?) V, задаваемого как || V|| ||р|| = Vp_y

определяет Н-функтор.

Определение 5. Модель (С,(?)), есть Б-оценка V, такая, что Vp= 1 для всех реЕ.

Говоря кратко: модель теории есть структура, в которой аксиомы теории являются значимыми. Тогда (С,(?)) является семантически непротиворечивой тогда и только тогда, когда (С,(Е)) имеет модель, и легко доказать, что (С,(?)) семантически непротиворечива тогда и только тогда, когда (Е) является собственным.

Определение 6. (С,(?)) семантически полна, если выполняется следующее условие: ре (Е) тогда и только тогда, когда р истинно во всех моделях (С,(?)).

Как и в случае классической логики, легко можно показать, что (С,(Е)) является семантически полной.