Пес Ебленский [entries|archive|friends|userinfo] rex_weblen [ website | Наши рисуночки ] [ userinfo | ljr userinfo ] [ archive | journal archive ]

Links [ Links: | update journal edit friends fif tiphareth recent comments ]

Еще про топосы и логику [Sep. 27th, 2024|11:23 pm] [Tags | category theory, intuitionistic logic, logic, math, memuar, meta, news, planning, set theiry, sheaf theory, topos theory ] [ Current Mood | quixotic ] [ Current Music | THE MAD CAPSULE MARKET'S - Speak!!! ] Я хотел дальше сосредоточиться на Книге Белла. В некотором роде она представляет собой двойственное дополнение к Мак Лейну-Мурдяку. То есть, если в желтой книжке начинают с геометрических примеров, и постепенно мотивируя ими абстракции, приходят к логику, то Белл начинает с логики и постепенно приходит к все тем же пучкам. Основная идея Белла в том, что топосы являются моделями локальных теорий множеств, которые записываются на так называемых локальных языках. Что такое локальный язык кратко объяснить сложно, но он напоминает языки, используемые для теории типов. И я бы сказал, что это языки идеально подходящие для записи утверждений про топосы. Стиль Белла довольно сильно отличается от стиля Мак Лейна. Он очень педантичный с формальными доказательствами. Это может не всем понравиться. Тем не менее из-за обилия формализмов книга у Белла получилась куда более сжатой. И, кажется, что что делал Белл доказывает, что топосы — это не махание руками, а про операции с логическими формулами определенного вида. Я обратил внимание на то, что Белл уделяет в своей книге внимание модальным логикам. Строго говоря он рассматривает только определенный вид модальности, который я назвал бы равномерно ослабляющими идемпотентами. Про них можно думать как про модальности, ослабляющие значение правды. Например «иногда», «почти наверное»,«может быть»,«нельзя опровергнуть». Это не просто так, а потому что эти модальности полностью и однозначно соответствуют топологиям Ловера-Тирни. Поэтому получается, что вложения топосов моделириует теории множеств с такими модальностями. То есть такие теории множеств где можем сказать «элемент a принадлежит множеству В», а можем сказать « может быть, что элемент a принадлежит множеству B, а может не принадлежит, хуй его знает». Еще мне очень понравилось философское заключение у Белла (Белл был в значительной степени человеком с бэкгрундом в философской логике). Там он сравнивает теорию топосов с теорией относительности в физике. В его сравнении топосы (с объектом-натуральными числами) соответствуют разным инерциальным систем координат, а геометрические морфизмы заменам координат. И отсюда вытекает такая мотивация для интуиционистской логики, что типа правильно записанные законы физики выполняются во всех системах координат, то ностоящие математические законы должны выполняться во всех топосах, а это ровным счетом означает доказуемосость в инуиционалистской логике. Примерами утверждений, которые не выдерживают этот тест могут быть, например могут быть почти все утверждения про разные бесконечные кардиналы, потому что всегда можно найти такую «замену координат» где данный бесконечный кардинал будет счетным (обрушение кардиналов). Еще был приводит интересный пример с нестандартным анализом Робинсона. Там получается, что нестандартный анализ это функтор перехода от пучков над счетным бесконечным множеством к пучкам над компактификацией Стоуна-Чеха. Но к корректности этого утверждения нужно будет еще вернуться. Еще один мой должок — это теорема Жиру. Это теорема про то, когда категория является топосом Гротендика, то есть когда она эквивалентна пучкам на ситусе. У нее довольно громоздкая формулировка и длинное доказательство. Вот формклировка: категория является топосом Гротендика тогда и только тогда, когда выполняется шесть усовий, а именно 1) у категории есть все конечные пределы 2) у категории есть все копроизведения и они несвязны и устойчивы под пуллбэками 3) каждый эпиморфизм является ко-уравнителем 4) Каждое отношение эквивалентности задается морфизмами и допускает факторизацию 5) каждая точная вилка стабильно точна 6) Есть множество порождающих объектов. Поэтому, понятно, почему эту теорему Мак Лейн вынес в аппендикс. Правда ее можно упростить: элементарный топос является топососом Гротендика, когда у него есть порождающее множество и все копроизведения. В таком виде эта теорема мне больше нравится. У этой теоремы есть полезные следствие. Хотя бы ее можно использовать в другую сторону, чтобы пользоваться хорошими свойствами известного топоса Гротендика. Еще отсюда следует, что для топоса Гротендика можно выбрать не просто ситус, а ситус с уймой хороших свойств: конечноые пределы, экспоненцирование, счетные копределы, подобъекты и фактор-объекты. Что я планирую делать дальше? У меня есть кое-какие идеи, что дальше делать с топосами. Но я не уверен, что сейчас стоит писать про это здесь. В целом я устал от доказательств с коммутативными диаграммами, склеиванием пулбэков и сопряженными функторами. Но мне не перестало хотеться математики. Правда, теперь мне больше хочется чего-нибудь конкретного, типа водочки и картофанчика. P. S. Я добавил рубрикатор в верхнем посте. Или не рубрикатор, а типа оглавления блога, чтобы новым читателям было проще ориентироваться. Как вам? Пока там только математика, Берроуз, и некоторые относительно новые книжки. Но рубрикатор будет пополняться. Link 307 comments|Leave a comment

Геометрическая Логика [Sep. 22nd, 2024|07:10 pm] [Tags | category theory, intuitionistic logic, logic, math, memuar, sheaf theory, topos theory ] [ Current Mood | quixotic ] [ Current Music | Virgin Prunes - The Moon Looked,,, ] Значит так, геометрическая логика. Для того, чтобы мотивировать это понятие нужно вспомнить, что геометрические морфизму сохраняют не все формулы логики первого порядка, а только некоторые из них. Такие формулы называются геометрическими. Множество геометрических формул можно построить рекурсивно, используя атомарные формулы, операции конъюнкции, дизъюнкции, и квантор существования. Теории порождённые геометрическими формулами называются геометрическими. Например, любая алгебраическая теория является геометрическая. Но теория полей, которая не является алгебраической, будет геометрической. При этом нужно заметить, что в интуиционистской математике есть две разные формулировки теории полей, одна из которых будет геометрической, а другая нет. Во всяком случае, главное свойство геометрических теорий — это то, что геометрические морфизмы между топосами ограничиваются на функторы между моделями геометрических теорий в этих топосах. Потом Мак Лейн определяет категорию определимых объектов в топосе для модели М геометрической теории. Определимые объекты задаются символом типов X из соответствующего теории языка первого порядка с типами и геометрической формулой фи так, что все определимый объект имеет вид реализации для в модели M подмножества X, задаваемого формулой фи. Морфизмы в категории определимых объектов, это те морфизмы из исходного топоса, графики которых сами являются определяемыми объектами. Эта категория будет иметь все конечные пределы. Эта категория будет малой, если мы считаем, что исходный язык первого порядка с типами имеет исходное множество символов ограниченной кардинальности. Поэтому потом можно определить «определимый» топос, просто взяв пучки над топологией из эпиморфных семейств в категории определимых объектов. Эта топология будет под-канонической, то есть такой, что любой представимый функтор будет пучком. Следующая категория, еще более важна и одновременно с этим абстрактна. Это так называемая синтактическая категория. И она строится просто для геометрической теории. Ее объектами выступают классы эквивалентных геометрических формул, а морфизмами классы формул, которые задают графики. Это все определяется без отсылки к каким-либо топосам и моделям, но любая модель задает функтор реализации из синтактической категории в категорию определяемых объект. У синтаксической категории есть все хорошие свойства категории определяемых объектов. На синтаксической категории можно завести такую топологию Гротендика, что все функторы реализации будут сохранять покрытия. Так у нас получается синтаксический топос пучков над синтаксической категорией. Этот топос примечателен тем, что является классифицирующим для моделей соответствующей ему теории. Это на практики значит, что модели теории в топосе Т это то же самое, что непрерывные точные с лева функторы из синтаксической категории в данный топос T. Это довольно разумно, потому что, да, действительно модели как мы видели с самого начала, ведут себя как функторы. Этот результат сразу ведет к тому, что у каждой теории есть универсальная модель в таком вот синтактическом топосе. Тогда можно доказать, что если утверждение вида « Для любого x из X верно, что из фи от x следует пси от x&rauquo;, то это утверждение верно в любой модели. Комбинируя этот результат с теоремой Делиня, так как синтактический топос Когернетен, что если какое-то утверждение приведённого выше вида верно над категорией множеств SET, то оно верно в любой модели в любом топосе. Это очень мощный результат, потому что он показывает что истинность утверждений просто определенного синтактического вида, будет верна в любой интуиционистской логике. Мурдяк и Мак Лейн, получается, пишут что это результат один из самых значимых в теории топосов, потому что на нем они завершают свой учебник. Еще там есть аппендикс про теорему Жиро. Но этот результат про формулы относится к логике, и укрепляет впечатление, что основная забота теории топосов — это помогать логике. С точки зрении логики написан учебник Джона Лейн Белла. Вся геометрическая логика там вынесена в аппендикс, видимо, потому что дается без доказательств. В целом изложение там мне показалось довольно понятным. Может быть дело в том, что я устал от доказательств в стиле МакЛейна и Мурдяка. У меня остался вопрос как эта теория соотносится с форсингом в Топосах Гротендика. Напомню, что там элементы ситуса использовались как информация вынуждающая определенные утверждения быть верными. И в случае с синтакатическим топосом вполне естественно считать, что такая информация в явном виде состоит из классов формул. Интересно, можно ли утверждать, что любой топос Гротендика является синтактическим? Еще один вопрос, как устроена универсальная модель? Понятно, что это пучок над синтаксической категорией. То есть это функция которая сопоставляет классам формул множества. Мне кажется что это могли бы быть множества формул, которые «следуют» из любой в данном классе. Но отношение следования во внутренней логике топоса может быть более сложным, чем в обычной логике первого порядка. Еще одна тема, которой я не хочу заниматься, но которую надо упомянуть — это теория и практика Оливии Карамело "Топосы как мосты". И я так понял, ее идея в том, чтобы искать теории с общими классифицирующими топосами, и так находить скрытые связи в математике. Link 276 comments|Leave a comment

Топосы в Логике [Jun. 11th, 2024|11:20 pm] [Tags | category theory, general topology, intuitionistic logic, logic, math, memuar, set theory, sheaf theory, topos theory ] [ Current Mood | dorky ] [ Current Music | Echo And The Bunnymen - Crocodiles ] После долгого перерыва я вернулся к изучению теории топосов по книге Маклейна-Мурдяка. Следующая глава посвящена применяю топосов в логике. И мой финт, кажется, себя оправдал. Во-первых, знакомство с булево-значными моделями, действительно помогает лучше понять конструкции, связанные с форсингом в этой главе. А знакомство с локалями делает тривиальными, на мой взгляд, все алгебраические вопросы. При изучении булево-значных моделей я читал учебник Джона Лейна Белл. У него еще есть книга про топосы, обложку которой я привожу выше. Там упор на логику особенно сильный. А вот у Маклейна этот упор считается относительно слабым по сравнению, например, с Джонстоном. И, я хотел изначально перед тем как писать этот пост прочитать всего Белла. Но сейчас, я уже понимаю, что это — слишком много времени. А читать эти книги параллельно слишком тяжело. Поэтому я просто просмотрел Белла по диагонали. И может быть я вернусь к Беллу если мне захочется глубже погрузиться в категорную логику. Напомню, что в логической парадигме топосы рассматривают как математические вселенные, обладающее существенным подобием теории множеств. Маклэйн и Мурдяк начинают с этой темы. И разбирают, то как в топосах выражены разные более серьезные свойства теории множеств. Они используют многообразие топосов, чтобы доказать независимость гипотезы континуума и аксиомы выборы. Для гипотезы континуума используется структура знакомая по булево-значным моделям. Но язык доказательств совсем другой. А для аксиомы выбора используется конструкция знакомого нам Фрайда, когда пучки строятся на счетном ординале. То что было "частицами информации" в случае исходных доказательств теперь становиться пучками. Поэтому я предлагаю [довольно бессмысленный] лозунг "пучки = информация" для популяризации пучков. Дальше Маклэйн и Мурдяк для каждого топосы определяют особый язык, который называется языком Митчела-Бенабу. Это язык теории типов с кванторами, где в качестве типов выступают объекты исходного топосы. Тут подход мне показался довольно неформальным. Поэтому для тех, кто любит более формальный и педантичный подход к синтаксису, я рекомендую упомянутую выше книжку Белла про топосы. Там вместо языка Митчела-Бенабу авторы начинают с формального языка "локальной теории множеств". И моделями этой теории как-раз прекрасно должны выступать топосы. Когда язык есть, для него можно построить так называемую семантику Джояля-Крипке. На практике эта семантика очень похожа на форсинг, где в качестве информации используются объекты топоса (пучки) и морфизмы из этого объекта, которые символизируют подстановку значений в переменные логических формулах. При этом Крипке вообще не совсем категорщик, а скорее логиу и философ-аналитик в классическом смысле. И его интересовала создание семантики для интуционалистской логики (то есть логики без закона исключенного среднего). И его работа не касалась топосов. Но топосы могут реализовывать любую интуиционистскую логику. Поэтому в итоге получилось объединение имен Джоэля и Крипке. Для случая топоса Гротендика существует более простая семантика, которая просто называется семантикой пучков. Она тоже похожа на форсинг. Но там в качестве информации используются объекты ситуса на которых вычисляются пучки. Предлагаю придумать пример. Возьмем в качестве топоса совершенно классический пример пучков на евклидовом пространстве. Этот топос будет топосом Гротендика, а его ситус — открытые множества с включениями в качестве морфизмов. Тогда типы в соответствующем языке — это, например, непрерывные функции, гладкие функции, дифференциальные формы, тензоры и так далее. Разрешенные предикаты — это свойства которые всегда выполняются "локально", например гладкость. Вычисление предиката всегда выдает в качестве результата не 0 или 1, а открытое множество. В итоге имеем не-аристотелеву, не-булеву логику. В качестве предиката на гладких функций, можно например взять "является решением (не)линейного дифференциального уравнения". Такие дифференциальные уравнения задаются дифференциальными операторами, которые сами образуют пучок. В итоге, используя кванторы можно задавать на языке Митчела-Бенабу сложные объекты типа этих ваших пфаффианов. Условия форсинга в семантики Джояля-Крипке могут например выглядеть как "x ведет себя гладко в окрестности V". А для форсинга пучков просто как "наблюдаемая переменная находится в некой окрестности". Чем меньше окрестность, тем больше информации. Мне кажется, что даже тут, на простом примере, мы можем видеть потрясающую вещь, как теория топосов помогает установить связь между такими разными областями математики как дифференциальные уравнения и логика. Скажите, чего тут интересного? Понятно, что все условия связанные с гладкостью и дифференцированием могут быть записаны логически. Но тут мы видим связь с неклассической логикой, которая раньше не была очевидна. Также язык Митчела-Бенабу может быть использован для того, чтобы конструировать в топосе объекты из других разделов математики. Мне нравится в этом отношении думать про топос как завод, которому можно дать чертежи на формальном языке, и он собирает по ним кусок теории. Но логики топоса в общем случае интуциолналистская, поэтому безусловно верными оказываются только интуционалистсуки доказанные теоремы. Если топос булев, то есть его классификатор подпространств оказывается внутренней булевой алгеброй, то там можно собирать любые классические теории. То есть в этом плане булев топос как завод более полезен. Только после того, как я это осознал, я понял истинную важность инстуционалистской логики, как логики "заказов" для произвольного топоса. До этого я считал интуционализм каким-то барским капризом. Типа "не хочу закон исключенного третьего и все". В качестве примера такой конструкции Маклейн и Мурдяк собирают действительные числа в топосе пучков на топологическом пространстве, используя сечения Дедекинда. Удивительно, но в итоге получается просто пучок непрерывных действительно-значных функций. Кажется, это означает, что все утверждения верные для таких интуицоналистских действительных чисел должны быть верны для непрерывных функций в классической математике. Например, отсюда мы получаем, что даже такая простая теорема, что ограниченная монотонная последовательность имеет предел не верна в интуиционализме. Также на специальном ситусе из открытых подмножеств евклидовых пространств с непрерывными функциями в качестве морфизмов, конструируются интуиционистские действительные числа, на которых любая функция непрерывна. Это теорема Брауэра. Поэтому кажется, что для действительного анализа лучше подходят булевы топосы. И мы действительно уже видели булево-значный анализ, где действительные числа конструируются как измеримые функции, и как самосопряженные коммутирующие операторы на гильбертовом пространстве. Кажется все эти примеры братья из одного ларца. Касательно бессмысленного лозунга "Пучки — это информация." Мне кажется, что было бы правильно говорить, что информация это объекты ситуса. А пучки это "правильные способы интерпретации информации" или способы получения знаний. Причем правила задает структура ситуса. Знания выражаются в виде множеств возможных миров. Чем больше знаний, тем меньше множество. То есть в какой-то безумной интерпретации можно думать о непрерывных функция как возможных мирах. но я не додумал. В целом чистая логика и основания математики меня не так сильно интересуют сам по себе. А если интересуют, то как способ генерации примеров. Поэтому дольше с этой темой я задерживаться не хочу. Пойду разбирать Маклейна до конца. Link 63 comments|Leave a comment

Про Пучки [Sep. 8th, 2023|09:03 pm] [Tags | category theory, general topology, logic, math, memuar, sheaf theory, topology, topos theory ] [ Current Mood | sleepy ] [ Current Music | Conker's Bad Fur Day ] Я писал тут недавно, что перехожу к теории топосов. Как я уже писал в том посте я продвигаюсь вперед ужасно медленно. Но это объясняется неизвестным вам причинами. Как я писал я выбрал для себя учебник Saunders Mac Lane , Ieke Moerdijk; Sheaves in Geometry and Logic : A First Introduction to Topos Theory. В целом познание теории топосов широкой публикой осложняется тем, что существуют два дополняющих друг-друга определения топоса. Это топос Гротендика и элементарные топосы Лоури. Но если говорить популярно, то топосы это такие математические вселенные в которых возможны всевозможные конструкции. Так как определение топоса Гротендика опирается на концепт категории пучка, МакЛейн начинает свое изложение с понятия пучка над топологискими пространствами. И я пишу этот пост после освоения двух первых глав, перед переходам к настоящим, абстрактным топосам. Из пререквизотов, для освоения этого материала вам понадобятся только знание начал общей топологии и абстрактной алгебры. МакЛейн кратко излагает основы теории категорий в самом начале. Но мне это ведение не понадобилось, потому я его не читал и ничего сказать про его достаточность не могу. Во всяком случае тут теория категорий это основное топливо. Все понятия из математической логики тут вводятся в процессе изложения. Однако предварительное знакомство с ней все же будет полезно, а также знакомство с дифференциально геометрией, алгебраической топологией и комплексным анализом. Потому что тут очень много примеров, которые теоретически можно пропустить. Но если все же потратить время на все эти примеры, это сделает опыт чтения ярче. Обилие примеров это одна из черт стиля МакЛейна. Другой, я бы назвал то, что не закапывается слишком глубоко в детали. Поэтому не раз я чувствовал желания написать какой-нибудь фрагмент доказательства или нарисовать коммутативную диаграмму. Но меня такой стиль вполне устраивает. Чего тут нет, так это гомологий в пучках. Если вам интересна эта тема, то придется читать другие книги. Кстати, Джонстон, который мне показался слишком сложным, как мне кажется показался слишком сложным, возможно, касается этой темы. Первую главу сложно однозначно характеризовать однозначно. Но там тоже объясняются всякие предварительные понятия полезные для определения топосов. В целом, я уже знал большую их их часть, но тут более систематический подход с пулбэкам. Поэтому это мне было полезно. Тут, наверное, главное понятие это предпучки на категории. Предпучки это просто контравариантные функторы из малой категории в категорию множеств. Другое интересное понятие тут это классификатор подобъектов. Он позволяет описать множество подобъектов любого объекта как множество морфизмов в этот классификатор. В категории множеств этот классификатор это бинарная булева алгебра {0,1}. Но благодаря теории булево-злачных моделей мы знаем, как построить похожую би-полную категорию с классификатором — любой булевой алгеброй B. У МакЛейна есть интересная интерпретация сложных классификаторов как путей к истине. В в случае категории предпучков эти пути к истине образуют решета морфизмов в базовой категории. Меня задел момент, когда МакЛейн писал, что в классических алгебраических категориях не может классификатора подобъектов. Потому что такой классификатор должен содержать в себе изоморфную копию, любого объекта этой категории. Например, это могла бы быть группа, содержащая в себе все группы. И конечно, такого не бывает. Но с этой задачей могла бы справиться модель-монстр теории групп из теории моделей. Она, конечно, не была бы множеством. Но если придумать другое определение категорий и топосов, чтобы можно было использовать два типа объектов, например, группы-классы и группы-множества. Причем переделать все универсальны кванторы только по группам-множествам, а все экзистенциональные кванторы, и по группам множествам, и группам классов. И тогда модель-монстр можно использовать как классификатор подобъектов. И эти классические алгебраические категории тоже будут элементарные топосами. Грубо говоря, элементарные топосы это категории со всеми конечными пределами и копредалами, экспоненциальными объектами и классификатором подобъектов. Интересно, что в элементарном топосе множество подобъектов подобъектов образуют алгебру Гетинга. И сам классификатор подобъектов является объектом-алгеброй Гетинга в унивресальном смысле. Потому каждый элементарный топос обладает собственной внутренней, возможно неклассической, логикой. Вторая глава тут собственно про пучки. Но только про пучки на топологических пространствах. Пучки это предпучки на категории открытых множеств топологического пространства для которых выполняется лемма о склеивание. Конечно, эти пучки являются элементарными топосами. И их классификаторы подобъектов это открытые множества исходного подпространства. Поэтому опять же открытые множества образуют алгебру Гетинга. Любая алгебра Гетинга, а значит любая (не)классическая логика, может быть реализована как алгебра открытых множеств некоторого топологического пространства. Это должно быть пространство Стоуна, этой алгебры. Но мы тут забегаем вперед. У Манина мы еще видели пучки вычислимых функций на рекурсивно заданных множествах. Поэтому видов пучков должно быть намного больше че только топологические пространства. По моим ощущением, главная теорема этой главы, это результат про эквивалентность пучков и этальных пространств. Этальные пространства над X это топологические пространства снабженные локальным гомеоморфизмы снабженные локальным гомеоморфизмом в X. Это делает этальные пространства обобщениям накрытия из алгебраической топологии. Также как и накрытия они обладают некоторой связью с теорией Галуа, и позволяют переходить к т. н. этальным группам пространства. Но это тоже уже немного забегаю вперед. МакЛейн использует совершено потрясающую аналогию для разъяснения этой связи. Я чуть не упал со стула от смеха, когда это увидел. Он пишет, что про слои Этального пространства можно думать как про шашлык. И у накрытия это будет ровный и аккуратный шашлык из одинаковых кусочков. А у этального пространства на одном шампуре могут быть куски разного размера, и овощи. И почти что определение тут: Так вот, сегодня мы узнали, что бывают математические вселенные, которые состоят из шашлыка. Живите с этим. Link 13 comments|Leave a comment

navigation [ viewing | most recent entries ]