Геометрическая логика
-
Определение геометрической логики
- Геометрическая логика — это обобщение когерентной логики, ограниченное Сколемом.
- Она способна выразить множество математических теорий и связана с теорией топосов.
-
Аксиомы геометрической логики
- Теория логики первого порядка является геометрической, если аксиомы имеют форму, указанную в определении.
- Если все аксиомы конечны, теория является последовательной.
-
Теорема о последовательном консервативном продолжении
- Каждая теория первого порядка имеет последовательное консервативное продолжение.
-
Значимость теоремы
- Следствия теоремы позволяют преобразовывать специальные логические следствия в правила вывода без изменения структурных правил.
- Когерентные теории выражаются с помощью простых правил дедукции, где атомарные формулы играют ключевую роль.
- Последовательные следствия образуют классы Гливенко, и теорема Барра утверждает, что они доказуемы интуитивно.
- Множество алгебраических теорий, включая теорию групп и теорию колец, являются когерентными/геометрическими.
- Геометрические морфизмы между топосами сохраняют когерентные теории.
- Отфильтрованные ограничения в моделях когерентной теории также являются моделями.
- Особые когерентные следствия обобщают предложения Хорна из логического программирования.
-
Эффективное доказательство теорем
- Эффективное доказательство теорем для когерентных теорий возможно автоматизировать.
- Отсутствие сколемизации и клаузальной формы упрощает структуру математических аргументов.
-
Библиография
- Упомянуты два тома Оксфордских руководств по логике и третий том в стадии подготовки.
Полный текст статьи: