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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

и определим

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

Eq(E);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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