Шестая. 
Интерпретация секвенций в ситусах

Предтопологии в категориях предпорядка

В предыдущем разделе была описана интерпретация классической логики в N-категориях. Последние представляют собой категории предпорядка, снабженные контравариангными функторами, выполняющими функцию отрицания. Идя по этому пути, мы можем рассматривать алгебру Гейтинга как категорию предпорядка, снабженную контравариантным функтором, отображающим каждый элемент алгебры в его интуиционистское отрицание. При этом мы очевидным образом можем без особых затруднений переформулировать все свойства алгебры Гейтинга в подобных Nкатегориях.

Более интересно то обстоятельство, что в полученных Nкатегориях мы можем естественным образом интерпретировать секвенциальную формулировку интуиционистской логики. Главная идея такого подхода может быть пояснена чисто алгебраически, с помощью понятия предтопологии. Для алгебры Гейтинга Н предтопология на Н представляет собой функцию, сопоставляющую каждому элементу р совокупность Cov (p) множеств элементов (покрытий), таких, что:

• (i) peCov (p);
• (ii) если {р/. Pj

  и iel) eCov (p) и для любого iel имеет место {р'у p’j^Pi иу’еД} eCov (p), то {pf. p‘j

  и iel и j eJ,} eCov{p)

• (iii) если r, qe Cov (p,) то r a qe Cov (p), и наоборот.

Легко видеть, что мы можем отождествить список формул Г некоторой секвенции Г—" а с элементами предтопологии на Н. Тогда правило сечения из секвенциальной формулировки, например, может рассматриваться как следствие условия (ii) нашего определения. Но более элегантно подобная интерпретация выглядит в Nкатегориях, поскольку там покрытия будут представлять собой совокупности множеств стрелок {р, —> р: iel}

Преимущество подобной интерпретации становится более очевидным, если мы рассмотрим случаи алгебры Брауэра и НВалгебры. Согласно предложенному подходу, чтобы интерпретировать соответствующую логику в алгебре Брауэра, мы должны использовать дуальную конструкцию копредтопологии и копокрытия. Далее, подобная предтопология в случае НВ-алгебры превращается в бипредтопологию с некоторыми элементами в качестве общего «центра» покрытий и копокрытий, и если рассматривать бипокрытия лишь как совокупности множеств, то легко можно упустить из виду эти «центры».

В случае классической логики ситуация еще более усложняется, поскольку в классических секвенциях списки формул фигурируют в обеих частях секвенции. Соответственно мы приходим к заключению, что наша предтопология здесь превращается в полипредтопологию и мы должны рассматривать полипокрытия, когда каждый элемент является членом покрытия и копокрытия одновременно. Интуитивный смысл сказанного может быть пояснен с помощью следующего рисунка:

Поскольку в теоретико-категорной формулировке (в отличие от алгебраической) понятие предтопологии входит составной частью в определение ситуса (см. [Гольдблатт 1983, с. 386]), то мы получаем еще один аргумент в пользу N-категорного подхода.

Наконец, мы можем перенести эти конструкции в любые декартово замкнутые категории ввиду имеющейся возможности перейти от категорий предпорядка к так называемым категориям путей. Это позволяет нам избежать обвинения в слишком узком традиционном рассмотрении категорий.