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

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

Обзор

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

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

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

Внутренние языки: Это можно рассматривать как формализацию и обобщение доказательства погоня за диаграммой. Один определяет подходящий внутренний язык, называя соответствующие составляющие категории, а затем применяет категориальную семантику, чтобы превратить утверждения в логике над внутренним языком в соответствующие категориальные утверждения. Это было наиболее успешным в теории топы, где внутренний язык топоса вместе с семантикой интуиционистской логики высшего порядка в топосе позволяет рассуждать об объектах и морфизмах топоса, «как если бы они были множествами и функциями».^{[нужна цитата ]} Это было успешным при работе с топосами, имеющими «множества» со свойствами, несовместимыми с классической логикой. Ярким примером является Дана Скотт модель нетипизированное лямбда-исчисление в терминах объектов, которые втягиваются в собственное функциональное пространство. Другой пример - модель Моджи – Хайланда. система F внутренним полная подкатегория из эффективные топосы из Мартин Хайланд.
Термомодельные конструкции: Во многих случаях категориальная семантика логики обеспечивает основу для установления соответствия между теории в логике и экземплярах соответствующего вида категории. Классический пример - соответствие между теориями βη -эквациональная логика над просто типизированное лямбда-исчисление и Декартовы закрытые категории. Категории, возникающие из теорий через конструкции термодинамики, обычно можно охарактеризовать с точностью до эквивалентность подходящим универсальная собственность. Это позволило получить доказательства метатеоретический свойства некоторых логик с помощью соответствующего категориальная алгебра. Например, Фрейд дал доказательство существования и дизъюнктивных свойств интуиционистская логика Сюда.

Смотрите также

История теории топоса

Примечания

^ Ловер, квантификаторы и связки

дальнейшее чтение

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

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

внешняя ссылка

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

[1] Ловер, квантификаторы и связки

[1]