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

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

Обзор

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

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

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

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

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

Эти три темы связаны. Категориальная семантика логики состоит в описании категории структурированных категорий, которая связана с категорией теорий в этой логике посредством присоединения, где два функтора в присоединении задают внутренний язык структурированной категории, с одной стороны, и термин-модель теории, с другой.

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

Примечания

^ Гоген, Джозеф; Моссаковски, Тилл; де Пайва, Валерия; Рабе, Флориан; Шредер, Лутц (2007). «Институциональный взгляд на категорическую логику». Международный журнал программного обеспечения и информатики . 1 (1): 129–152. CiteSeerX 10.1.1.126.2361 .
^ Ловер 1971, Квантификаторы и пучки
^ Алуффи 2009

Ссылки

Книги

Абрамский, Самсон; Габбай, Дов (2001). Логические и алгебраические методы . Справочник по логике в информатике. Том 5. Oxford University Press. ISBN 0-19-853781-6.
Алуффи, Паоло (2009). Алгебра: Глава 0 (1-е изд.). Американское математическое общество. стр. 18–20. ISBN 978-1-4704-1168-8.
Габбей, Д.М.; Канамори, А.; Вудс, Дж., ред. (2012). Множества и расширения в двадцатом веке. Справочник по истории логики. Том 6. Северная Голландия. ISBN 978-0-444-51621-3.

Кент, Аллен; Уильямс, Джеймс Г. (1990). Энциклопедия компьютерных наук и технологий . Марсель Деккер. ISBN 0-8247-2272-8.
Барр, М.; Уэллс , К. (1996). Теория категорий для вычислительной науки (2-е изд.). Prentice Hall. ISBN 978-0-13-323809-9.
Ламбек, Дж.; Скотт, П.Дж. (1988). Введение в категориальную логику высшего порядка. Кембриджские исследования в области высшей математики. Том 7. Cambridge University Press. ISBN 978-0-521-35653-4.
Lawvere, FW ; Rosebrugh, R. (2003). Наборы для математики. Cambridge University Press. ISBN 978-0-521-01060-3.
Lawvere, FW; Schanuel, SH (2009). Концептуальная математика: первое введение в категории (2-е изд.). Cambridge University Press. ISBN 978-1-139-64396-2.

Основополагающие статьи

Lawvere, FW (ноябрь 1963 г.). «Функториальная семантика алгебраических теорий». Труды Национальной академии наук . 50 (5): 869–872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . JSTOR 71935. PMC 221940 . PMID 16591125.
— (декабрь 1964 г.). «Элементарная теория категории множеств». Труды Национальной академии наук . 52 (6): 1506–11. Bibcode :1964PNAS...52.1506L. doi : 10.1073/pnas.52.6.1506 . JSTOR 72513. PMC 300477 . PMID 16591243.
— (1971). «Кванторы и пучки». Акты: Du Congres International Des Mathematiciens, Ницца, 1–10 сентября 1970 г. Паб. Sous La Direction Du Comite D'organisation Du Congres . Готье-Виллар. стр. 1506–11. OCLC 217031451. Збл 0261.18010.

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

Маккай, Майкл ; Рейес, Гонсало Э. (1977). Категорическая логика первого порядка. Lecture Notes in Mathematics. Vol. 611. Springer. doi :10.1007/BFb0066201. ISBN 978-3-540-08439-6.
Ламбек, Дж.; Скотт, П.Дж. (1988). Введение в категориальную логику высшего порядка. Кембриджские исследования в области высшей математики. Том 7. Cambridge University Press. ISBN 978-0-521-35653-4.Достаточно доступное введение, но несколько устаревшее. Категориальный подход к логикам высшего порядка над полиморфными и зависимыми типами был в значительной степени разработан после публикации этой книги.
Якобс, Барт (1999). Категориальная логика и теория типов. Исследования по логике и основаниям математики. Том 141. Северная Голландия, Elsevier. ISBN 0-444-50170-3.Всеобъемлющая монография, написанная ученым-компьютерщиком; она охватывает как логику первого порядка, так и логику высшего порядка, а также полиморфные и зависимые типы. Основное внимание уделяется волокнистой категории как универсальному инструменту в категориальной логике, необходимому при работе с полиморфными и зависимыми типами.
Белл, Джон Лейн (2001). «Развитие категорической логики». В Gabbay, DM; Guenthner, Franz (ред.). Handbook of Philosophical Logic . Том 12 (2-е изд.). Springer. С. 279–361. ISBN 978-1-4020-3091-8.Версия доступна онлайн на домашней странице Джона Белла.
Маркиз Жан-Пьер; Рейес, Гонсало Э. «История категорической логики 1963–1977». Габбай, Канамори и Вудс, 2012 г. стр. 689–800.
Предварительная версия.
Аводей, Стив (12 июля 2024 г.). «Категориальная логика». конспект лекций .
Лурье, Якоб . «Категорическая логика (278x)». конспект лекций .