Категориальная логика

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

В категориальном подходе к логике есть три важных темы:

Категориальная семантика

Категориальная логика вводит понятие структуры, оцениваемой в категории C с классическим теоретико-модельным понятием структуры, появляющимся в частном случае, когда C - это категория множеств и функций. Это понятие оказалось полезным, когда теоретико-множественное понятие модели лишено общности и / или неудобно. Моделирование различных импредикативных теорий, таких как система F, является примером полезности категориальной семантики.

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

Внутренние языки

Это можно рассматривать как формализацию и обобщение доказательства с помощью поиска диаграмм. Один определяет подходящий внутренний язык, называя соответствующие составляющие категории, а затем применяет категориальную семантику, чтобы превратить утверждения в логике над внутренним языком в соответствующие категориальные утверждения. Это было наиболее успешным в теории топосов, где внутренний язык топоса вместе с семантикой интуиционистской логики высшего порядка в топосе позволяет рассуждать об объектах и ​​морфизмах топоса » как если бы они были наборами и функциями ». Это было успешным при работе с топосами, имеющими «множества» со свойствами, несовместимыми с классической логикой. Ярким примером является модель Даны Скотт нетипизированного лямбда-исчисления в терминах объектов, которые втягиваются в свое собственное функциональное пространство. Другой пример - модель Моджи – Хайланда системы F посредством внутренней полной подкатегории эффективных топос Martin Hyland.

построений терм-модели.

Во многих случаях категориальная семантика логики обеспечивает основу для установления соответствия между теориями в логике и экземплярами соответствующего вида категории. Классическим примером является соответствие между теориями βη -эквациональной логики над просто типизированным лямбда-исчислением и декартовыми замкнутыми категориями. Категории, возникающие из теорий через конструкции терм-модели, обычно могут быть охарактеризованы с точностью до эквивалентности подходящим универсальным свойством. Это позволило доказать метатеоретические свойства некоторых логик с помощью соответствующей категориальной алгебры. Например, Фрейд таким образом дал доказательство существования и дизъюнктивных свойств интуиционистской логики.

• История теории топосов

• Философский портал

Книги

• Абрамский, Самсон; Габбай, Дов (2001). Справочник по логике в компьютерных науках: логические и алгебраические методы. Оксфорд: Издательство Оксфордского университета. ISBN 0-19-853781-6. CS1 maint: ref = harv (ссылка )

• Габбай, Дов (2012). Справочник по истории Логика: множества и расширения в двадцатом веке. Oxford: Elsevier. ISBN 978-0-444-51621-3. CS1 maint: ref = harv (ссылка )

• Кент, Аллен; Уильямс, Джеймс Г. (1990). Энциклопедия компьютерных наук и технологий. Нью-Йорк: Marcel Dekker Inc. ISBN 0-8247-2272-8. CS1 maint: ref = harv (link )

• Barr, M. and Wells, C. (1990), Category Theory for Computing Science. Хемел Хемпстед, Великобритания.
• Ламбек, Дж. и (1986), Введение в категориальную логику высшего порядка. Издательство Кембриджского университета, Кембридж, Великобритания.
• Ловер, FW и ( 2003), Sets for Mathematics. Cambridge University Press, Cambridge, UK.
• Lawvere, FW (2000), и Schanuel, SH, Conceptual Mathematics: A First Introduction to Categories. Кембриджский университет Press, Кембридж, Великобритания, 1997 г. Перепечатано с исправлениями, 2000 г.

Seminal pa чел.

• Ловер, Ф.В., Функториальная семантика алгебраических теорий. In Proceedings of the National Academy of Sciences 50, No. 5 (ноябрь 1963), 869-872.
• Лавер, Ф.В., Элементарная теория категории множеств. In Proceedings of the National Academy of Sciences 52, No. 6 (December 1964), 1506-1511.
• Lawvere, F.W., Quantifiers and Sheaves. In Proceedings of the International Congress on Mathematics (Nice 1970), Gauthier-Villars (1971) 329-334.

• Майкл Маккай и Гонсало Э. Рейес, 1977, категориальная логика первого порядка, Springer -Verlag.
• Ламбек, Дж. и Скотт, П.Дж., 1986. Введение в Категориальную логику высшего порядка. Довольно доступное введение, но несколько устаревшее. Категориальный подход к логикам высшего порядка над полиморфными и зависимыми типами был разработан в значительной степени после публикации этой книги.
• Jacobs, Bart (1999). Категориальная логика и теория типов. Исследования по логике и основам математики 141. Северная Голландия, Эльзевир. ISBN 0-444-50170-3.Подробная монография, написанная ученым-компьютерщиком; он охватывает логики как первого, так и более высокого порядка, а также полиморфные и зависимые типы. Основное внимание уделяется расслоенной категории как универсальному инструменту категориальной логики, который необходим при работе с полиморфными и зависимыми типами.

• Джон Лейн Белл (2005) Развитие категориальной логики. Справочник по философской логике, том 12. Springer. Версия доступна в Интернете на домашней странице Джона Белла.
• Жан-Пьер Маркиз и Гонсало Э. Рейес (2012). История категориальной логики 1963–1977. Справочник по истории логики: множества и расширения в двадцатом веке, том 6, Д. М. Габбей, А. Канамори и Дж. Вудс, ред., Северная Голландия, стр. 689–800. Предварительная версия доступна по адресу [1].

• Категориальная логика конспекты лекций Стива Води
• Категориальная логика (278x) конспекты лекций Джейкоб Лурье