Геометрическая логика

В математической логике геометрическая логика представляет собой бесконечное обобщение когерентной логики , ограничение логики первого порядка, предложенное Скулемом , которое доступно с точки зрения теории доказательств . Геометрическая логика способна выражать многие математические теории и тесно связана с теорией топоса .

Определения

Теория логики первого порядка является геометрической, если ее можно аксиоматизировать, используя только аксиомы вида $\bigwedge _{i\in I}\phi _{i,1}\vee \dots \vee \phi _{i,n_{i}}\implies \bigvee _{j\in J}\phi _{j,1}\vee \dots \vee \phi _{j,m_{j}}$где I и J — непересекающиеся наборы индексов формул, каждый из которых может быть бесконечным, а формулы φ — это либо атомы, либо отрицания атомов. Если все аксиомы конечны (т. е. для каждой аксиомы и I, и J конечны), теория когерентна.

Теорема

Каждая теория первого порядка имеет последовательное консервативное расширение.

Значение

Дайкхофф и Негри (2015) перечисляют восемь следствий приведенной выше теоремы, которые объясняют ее значение (без сносок и большинства ссылок):

1. В контексте секвенциального исчисления, такого как G3c, специальные связные выводы в виде аксиом могут быть преобразованы непосредственно в правила вывода, не затрагивая допустимость структурных правил (ослабление, сокращение и сокращение);
2. Аналогичным образом, последовательные теории — это «теории, выражаемые с помощью естественных правил дедукции в определенной простой форме, в которой только атомарные формулы играют решающую роль»;
3. Когерентные импликации образуют секвенции, дающие класс Гливенко. В этом случае результат, известный как теорема Барра первого порядка, утверждает, что если каждое I i: 0妻i可n является когерентной импликацией, а секвенция I 1, . . . , I n ⇒ I 0 классически доказуемо, то оно интуиционистски доказуемо;
4. Существует множество примеров когерентных/геометрических теорий: все алгебраические теории, такие как теория групп и теория колец, все по существу алгебраические теории, такие как теория категорий, теория полей, теория локальных колец, теория решеток, проективная геометрия, теория сепарабельно замкнутых локальных колец (также известная как «строго гензелевы локальные кольца») и бесконечная теория периодических абелевых групп;
5. Когерентные/геометрические теории сохраняются за счет отката вдоль геометрических морфизмов между топосами (Maclane & Moerdijk 1992, глава X);
6. Фильтрованные копределы в множестве моделей когерентной теории T также являются моделями T;
7. Специальные когерентные импликации ∀x. C ⊃ D обобщает предложения Хорна из логического программирования , где D должен быть атомом; по сути, они обобщают «пункты» дизъюнктивных логических программ, где D может быть дизъюнкцией атомов.
8. Эффективное доказательство теорем для последовательных теорий может быть относительно легко и ясно автоматизировано (с точки зрения разрешения). Как отметили Безем и др. ... отсутствие сколемизации (введения новых функциональных символов) не представляет собой реальной трудности, а отсутствие преобразования к клаузальной форме позволяет лучше сохранить структуру обычных математических аргументов.

Библиография

• Дайкхофф, Рой; Негри, Сара (2015), «Геометризация логики первого порядка» , Бюллетень символической логики , 21 (2): 123–163, doi : 10.1017/bsl.2015.7 , hdl : 10023/6818
• Джонстон, Питер (2002), Зарисовки слона: сборник теории топоса , Oxford University Press, ISBN  978-0-19-852496-0 , Zbl   1071.18002 (два тома, Oxford Logic Guides 43 и 44, 3-й том в стадии подготовки)
• Маклейн, Сондерс Мак; Мурдейк, Ике (1992), Пучки в геометрии и логике , Springer: Berlin, doi : 10.1007/978-1-4612-0927-0 , ISBN  978-1-4612-0927-0

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

• «Почему геометрическая теория называется «геометрической»?» . Обмен стеками . 15 ноября 2020 г.