| Геометрическая Логика |
Sep. 22nd, 2024|07:10 pm |
 
Значит так, геометрическая логика. Для того, чтобы мотивировать это понятие нужно вспомнить, что геометрические морфизму сохраняют не все формулы логики первого порядка, а только некоторые из них. Такие формулы называются геометрическими. Множество геометрических формул можно построить рекурсивно, используя атомарные формулы, операции конъюнкции, дизъюнкции, и квантор существования. Теории порождённые геометрическими формулами называются геометрическими. Например, любая алгебраическая теория является геометрическая. Но теория полей, которая не является алгебраической, будет геометрической. При этом нужно заметить, что в интуиционистской математике есть две разные формулировки теории полей, одна из которых будет геометрической, а другая нет. Во всяком случае, главное свойство геометрических теорий — это то, что геометрические морфизмы между топосами ограничиваются на функторы между моделями геометрических теорий в этих топосах.
Потом Мак Лейн определяет категорию определимых объектов в топосе для модели М геометрической теории. Определимые объекты задаются символом типов X из соответствующего теории языка первого порядка с типами и геометрической формулой фи так, что все определимый объект имеет вид реализации для в модели M подмножества X, задаваемого формулой фи. Морфизмы в категории определимых объектов, это те морфизмы из исходного топоса, графики которых сами являются определяемыми объектами. Эта категория будет иметь все конечные пределы. Эта категория будет малой, если мы считаем, что исходный язык первого порядка с типами имеет исходное множество символов ограниченной кардинальности. Поэтому потом можно определить «определимый» топос, просто взяв пучки над топологией из эпиморфных семейств в категории определимых объектов. Эта топология будет под-канонической, то есть такой, что любой представимый функтор будет пучком.
Следующая категория, еще более важна и одновременно с этим абстрактна. Это так называемая синтактическая категория. И она строится просто для геометрической теории. Ее объектами выступают классы эквивалентных геометрических формул, а морфизмами классы формул, которые задают графики. Это все определяется без отсылки к каким-либо топосам и моделям, но любая модель задает функтор реализации из синтактической категории в категорию определяемых объект. У синтаксической категории есть все хорошие свойства категории определяемых объектов. На синтаксической категории можно завести такую топологию Гротендика, что все функторы реализации будут сохранять покрытия. Так у нас получается синтаксический топос пучков над синтаксической категорией. Этот топос примечателен тем, что является классифицирующим для моделей соответствующей ему теории. Это на практики значит, что модели теории в топосе Т это то же самое, что непрерывные точные с лева функторы из синтаксической категории в данный топос T. Это довольно разумно, потому что, да, действительно модели как мы видели с самого начала, ведут себя как функторы. Этот результат сразу ведет к тому, что у каждой теории есть универсальная модель в таком вот синтактическом топосе. Тогда можно доказать, что если утверждение вида « Для любого x из X верно, что из фи от x следует пси от x&rauquo;, то это утверждение верно в любой модели. Комбинируя этот результат с теоремой Делиня, так как синтактический топос Когернетен, что если какое-то утверждение приведённого выше вида верно над категорией множеств SET, то оно верно в любой модели в любом топосе. Это очень мощный результат, потому что он показывает что истинность утверждений просто определенного синтактического вида, будет верна в любой интуиционистской логике.
Мурдяк и Мак Лейн, получается, пишут что это результат один из самых значимых в теории топосов, потому что на нем они завершают свой учебник. Еще там есть аппендикс про теорему Жиро. Но этот результат про формулы относится к логике, и укрепляет впечатление, что основная забота теории топосов — это помогать логике. С точки зрении логики написан учебник Джона Лейн Белла. Вся геометрическая логика там вынесена в аппендикс, видимо, потому что дается без доказательств. В целом изложение там мне показалось довольно понятным. Может быть дело в том, что я устал от доказательств в стиле МакЛейна и Мурдяка.
У меня остался вопрос как эта теория соотносится с форсингом в Топосах Гротендика. Напомню, что там элементы ситуса использовались как информация вынуждающая определенные утверждения быть верными. И в случае с синтакатическим топосом вполне естественно считать, что такая информация в явном виде состоит из классов формул. Интересно, можно ли утверждать, что любой топос Гротендика является синтактическим? Еще один вопрос, как устроена универсальная модель? Понятно, что это пучок над синтаксической категорией. То есть это функция которая сопоставляет классам формул множества. Мне кажется что это могли бы быть множества формул, которые «следуют» из любой в данном классе. Но отношение следования во внутренней логике топоса может быть более сложным, чем в обычной логике первого порядка.
Еще одна тема, которой я не хочу заниматься, но которую надо упомянуть — это теория и практика Оливии Карамело "Топосы как мосты". И я так понял, ее идея в том, чтобы искать теории с общими классифицирующими топосами, и так находить скрытые связи в математике. |
|