Категорическая логика
Категориальная логика — это раздел математики , в котором инструменты и концепции теории категорий применяются для изучения математической логики . Он также известен своими связями с теоретической информатикой . [1] В широком смысле категориальная логика представляет как синтаксис, так и семантику категорией а также интерпретацию функтором , . Категориальная структура обеспечивает богатую концептуальную основу для логических и теоретико-типических конструкций. В этом смысле предмет известен примерно с 1970 года.
Обзор [ править ]
В категориальном подходе к логике есть три важные темы:
- Категориальная семантика
- Категориальная логика вводит понятие структуры, оцениваемой в категории C, с классическим теоретико-модельным понятием структуры, возникающим в частном случае, когда C является категорией множеств и функций . Это понятие оказалось полезным, когда теоретико-множественному понятию модели не хватает общности и/или оно неудобно. Моделирование РЭГ Сили различных непредикативных теорий, таких как Система F , является примером полезности категориальной семантики.
- Было обнаружено, что связки предкатегорической логики более четко понимаются с использованием понятия сопряженного функтора , а кванторы также лучше всего понимаются с использованием сопряженных функторов. [2]
- Внутренние языки
- Это можно рассматривать как формализацию и обобщение доказательства путем поиска диаграмм . Определяется подходящий внутренний язык, называющий соответствующие составляющие категории, а затем применяется категориальная семантика для преобразования утверждений логики внутреннего языка в соответствующие категориальные утверждения. Это было наиболее успешным в теории топосов , где внутренний язык топоса вместе с семантикой интуиционистской логики высшего порядка в топосе позволяет рассуждать об объектах и морфизмах топоса, как если бы они были множествами и функциями. . [3] Это позволило успешно работать с топосами, имеющими «множества» со свойствами, несовместимыми с классической логикой . Ярким примером является Даны Скотт модель нетипизированного лямбда-исчисления в терминах объектов, которые втягиваются в свое собственное функциональное пространство . Другой является модель Моджи -Хайланда системы F по внутренней полной подкатегории эффективного топоса Мартина Хайланда .
- Конструкции терм-модели
- Во многих случаях категориальная семантика логики обеспечивает основу для установления соответствия между теориями логики и экземплярами соответствующего вида категории. Классическим примером является соответствие между теориями βη - эквациональной логики над просто типизированным лямбда-исчислением и декартовыми замкнутыми категориями . Категории, возникающие из теорий посредством конструкций термин-моделей, обычно могут быть охарактеризованы с точностью до эквивалентности подходящим универсальным свойством . Это позволило доказать метатеоретические свойства некоторых логик с помощью соответствующей категориальной алгебры . Например, Фрейд доказал свойства дизъюнкции и существования интуиционистской логики . таким образом
См. также [ править ]
Примечания [ править ]
- ^ Гоген, Джозеф; Моссаковски, Тилль; де Пайва, Валерия; Рабе, Флориан; Шредер, Лутц (2007). «Институциональный взгляд на категориальную логику». Международный журнал программного обеспечения и информатики . 1 (1): 129–152. CiteSeerX 10.1.1.126.2361 .
- ^ Ловер 1971 , Кванторы и пучки
- ^ Алуффи, Паоло (15 июля 2009 г.). «Алгебра: Глава 0» . Американское математическое общество . дои : 10.1090/gsm/104 . Проверено 11 мая 2024 г.
Ссылки [ править ]
- Книги
- Абрамский, Самсон; Габбай, Дов (2001). Логические и алгебраические методы . Справочник по логике в информатике. Том. 5. Издательство Оксфордского университета. ISBN 0-19-853781-6 .
- Габбай, DM; Канамори, А.; Вудс, Дж., ред. (2012). Наборы и расширения в двадцатом веке . Справочник по истории логики. Том. 6. Северная Голландия. ISBN 978-0-444-51621-3 .
- Кент, Аллен; Уильямс, Джеймс Г. (1990). Энциклопедия компьютерных наук и технологий . Марсель Деккер. ISBN 0-8247-2272-8 .
- Барр, М .; Уэллс, К. (1996). Теория категорий для информатики (2-е изд.). Прентис Холл. ISBN 978-0-13-323809-9 .
- Ламбек, Дж. ; Скотт, Пи Джей (1988). Введение в категориальную логику высшего порядка . Кембриджские исследования в области высшей математики. Том. 7. Издательство Кембриджского университета. ISBN 978-0-521-35653-4 .
- Ловере, ФРВ ; Роузбру, Р. (2003). Наборы по математике . Издательство Кембриджского университета. ISBN 978-0-521-01060-3 .
- Ловере, ФРВ; Шануэль, SH (2009). Концептуальная математика: первое введение в категории (2-е изд.). Издательство Кембриджского университета. ISBN 978-1-139-64396-2 .
Основополагающие статьи
- Ловере, ФРВ (ноябрь 1963 г.). «Функториальная семантика алгебраических теорий» . Труды Национальной академии наук . 50 (5): 869–872. Бибкод : 1963PNAS...50..869L . дои : 10.1073/pnas.50.5.869 . JSTOR 71935 . ПМК 221940 . ПМИД 16591125 .
- - (декабрь 1964 г.). «Элементарная теория категории множеств» . Труды Национальной академии наук . 52 (6): 1506–11. Бибкод : 1964PNAS...52.1506L . дои : 10.1073/pnas.52.6.1506 . JSTOR 72513 . ПМК 300477 . ПМИД 16591243 .
- — (1971). «Кванторы и пучки». Материалы Международного конгресса математиков, Ницца, 1–10 сентября 1970 г. Паб. Под руководством Оргкомитета Конгресса . Готье-Виллар. стр. 1506–11. OCLC 217031451 . Збл 0261.18010 .
Дальнейшее чтение [ править ]
- Маккай, Майкл ; Рейес, Гонсало Э. (1977). Категорическая логика первого порядка . Конспект лекций по математике. Том. 611. Спрингер. дои : 10.1007/BFb0066201 . ISBN 978-3-540-08439-6 .
- Ламбек, Дж.; Скотт, Пи Джей (1988). Введение в категориальную логику высшего порядка . Кембриджские исследования в области высшей математики. Том. 7. Издательство Кембриджского университета. ISBN 978-0-521-35653-4 . Довольно доступное введение, но несколько устаревшее. Категориальный подход к логикам высшего порядка над полиморфными и зависимыми типами получил развитие в значительной степени после публикации этой книги.
- Джейкобс, Барт (1999). Категориальная логика и теория типов . Исследования по логике и основам математики. Том. 141. Северная Голландия, Эльзевир. ISBN 0-444-50170-3 . Обширная монография, написанная ученым-компьютерщиком; он охватывает логику как первого, так и высшего порядка, а также полиморфные и зависимые типы. Основное внимание уделяется расслоенной категории как универсальному инструменту категориальной логики, который необходим при работе с полиморфными и зависимыми типами.
- Белл, Джон Лейн (2001). «Развитие категорической логики» . В Габбае, DM; Гентнер, Франц (ред.). Справочник по философской логике . Том. 12 (2-е изд.). Спрингер. стр. 279–361. ISBN 978-1-4020-3091-8 . Версия доступна онлайн на домашней странице Джона Белла.
- Маркиз Жан-Пьер; Рейес, Гонсало Э. «История категорической логики 1963–1977» . Габбай, Канамори и Вудс, 2012 г. стр. 100-1 689–800.
Предварительная версия .
Внешние ссылки [ править ]
- Аводи, Стив (9 июля 2022 г.). «Категорическая логика» . конспекты лекций .
- Лурье, Джейкоб . «Категорическая логика (278х)» . конспекты лекций .
- ^ Алуффи, Паоло (2009). Алгебра: Глава 0 (1-е изд.). Американское математическое общество. стр. 18–20. ISBN 978-1-4704-1168-8 .