Математическая логика
Категорная логика
Топос - это категория, которая ведёт себя как 'вселенная множеств', но с иной логикой. В разных топосах работают разные логики: в одном выполняется аксиома выбора, в другом нет; в одном - закон исключённого третьего, в другом нет. Это делает топосы мощным инструментом для изучения оснований математики.
- Proof assistants Coq и Lean 4: основаны на теории типов, соответствующей топосной логике через соответствие Карри-Говарда-Ламбека
- Синтетическая дифференциальная геометрия (SDG): в подходящем топосе существуют 'настоящие' бесконечно малые, и классическая дифференциальная геометрия строится аксиоматически
- Форсинг в теории множеств (Коэн): доказательство независимости CH использует топос, соответствующий форсинговому расширению ZFC
- Семантика программных языков: топосная семантика используется для моделирования параллельных и недетерминированных вычислений
Топосы и внутренняя логика
Лоувер и Тирни в 1970 году определили элементарный топос как категорию, обобщающую Set: декартово замкнутую с классификатором подобъектов Omega. Логика внутри топоса интуиционистская: закон исключённого третьего может не выполняться. Proof assistant Lean 4 и Coq основаны на типах, чья теоретическая основа - топосная и гомотопическая логика.
Почему внутренняя логика топоса интуиционистская, а не классическая?
Логика топоса определяется структурой Omega: в Set Omega = {T,F} (булева), логика классическая. В топосе пресвязок Omega - решётка Хейтинга, закон исключённого третьего не является теоремой.
Геометрические морфизмы и приложения
Геометрические морфизмы между топосами - морфизмы теорий. Каждый топос определяет свою логику; геометрический морфизм f: E -> F сохраняет геометрические формулы (с квантором существования и конечными конъюнкциями). Это обобщает отношение моделей в логике.
Связь с теорией типов: через соответствие Карри-Говарда-Ламбека, топосы соответствуют системам типов с зависимыми типами. Это основа proof assistant Coq (Calculus of Constructions) и Lean (основанного на CIC). Типы = объекты топоса, термины = морфизмы, доказательства = элементы типа.
Что такое классифицирующий топос для теории T?
Классифицирующий топос Set[T]: для любого топоса E модели теории T в E биективно соответствуют геометрическим морфизмам E -> Set[T]. Это унифицирует семантику теорий в категорном языке.
Итоги
- Топос - категория с конечными пределами, внутренними хомами и классификатором подобъектов Omega
- Omega образует алгебру Хейтинга: закон исключённого третьего может не выполняться, отсюда интуиционистская логика
- Внутренний язык топоса: суждения = морфизмы в топосе, теоремы = конструкции (соответствие Карри-Говарда-Ламбека)
- Топос пресвязок Set^{C^op}: объект = функтор C^op -> Set, Omega(c) = сивы на c (решётка Хейтинга)
- Геометрический морфизм f: E -> F - морфизм между топосами, сохраняющий геометрическую логику
- Классифицирующий топос Set[T]: модели T в E биективны геометрическим морфизмам E -> Set[T]