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

• Определение геометрической логики

  • Геометрическая логика — это обобщение когерентной логики, ограниченное Сколемом. 
  • Она способна выразить множество математических теорий и связана с теорией топосов. 

• Аксиомы геометрической логики

  • Теория логики первого порядка является геометрической, если аксиомы имеют форму, указанную в определении. 
  • Если все аксиомы конечны, теория является последовательной. 

• Теорема о последовательном консервативном продолжении

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

• Значимость теоремы

  • Следствия теоремы позволяют преобразовывать специальные логические следствия в правила вывода без изменения структурных правил. 
  • Когерентные теории выражаются с помощью простых правил дедукции, где атомарные формулы играют ключевую роль. 
  • Последовательные следствия образуют классы Гливенко, и теорема Барра утверждает, что они доказуемы интуитивно. 
  • Множество алгебраических теорий, включая теорию групп и теорию колец, являются когерентными/геометрическими. 
  • Геометрические морфизмы между топосами сохраняют когерентные теории. 
  • Отфильтрованные ограничения в моделях когерентной теории также являются моделями. 
  • Особые когерентные следствия обобщают предложения Хорна из логического программирования. 

• Эффективное доказательство теорем

  • Эффективное доказательство теорем для когерентных теорий возможно автоматизировать. 
  • Отсутствие сколемизации и клаузальной формы упрощает структуру математических аргументов. 

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

  • Упомянуты два тома Оксфордских руководств по логике и третий том в стадии подготовки.