| Еще про топосы и логику |
Sep. 27th, 2024|11:23 pm |
 
Я хотел дальше сосредоточиться на Книге Белла. В некотором роде она представляет собой двойственное дополнение к Мак Лейну-Мурдяку. То есть, если в желтой книжке начинают с геометрических примеров, и постепенно мотивируя ими абстракции, приходят к логику, то Белл начинает с логики и постепенно приходит к все тем же пучкам. Основная идея Белла в том, что топосы являются моделями локальных теорий множеств, которые записываются на так называемых локальных языках. Что такое локальный язык кратко объяснить сложно, но он напоминает языки, используемые для теории типов. И я бы сказал, что это языки идеально подходящие для записи утверждений про топосы. Стиль Белла довольно сильно отличается от стиля Мак Лейна. Он очень педантичный с формальными доказательствами. Это может не всем понравиться. Тем не менее из-за обилия формализмов книга у Белла получилась куда более сжатой. И, кажется, что что делал Белл доказывает, что топосы — это не махание руками, а про операции с логическими формулами определенного вида.
Я обратил внимание на то, что Белл уделяет в своей книге внимание модальным логикам. Строго говоря он рассматривает только определенный вид модальности, который я назвал бы равномерно ослабляющими идемпотентами. Про них можно думать как про модальности, ослабляющие значение правды. Например «иногда», «почти наверное»,«может быть»,«нельзя опровергнуть». Это не просто так, а потому что эти модальности полностью и однозначно соответствуют топологиям Ловера-Тирни. Поэтому получается, что вложения топосов моделириует теории множеств с такими модальностями. То есть такие теории множеств где можем сказать «элемент a принадлежит множеству В», а можем сказать « может быть, что элемент a принадлежит множеству B, а может не принадлежит, хуй его знает».
Еще мне очень понравилось философское заключение у Белла (Белл был в значительной степени человеком с бэкгрундом в философской логике). Там он сравнивает теорию топосов с теорией относительности в физике. В его сравнении топосы (с объектом-натуральными числами) соответствуют разным инерциальным систем координат, а геометрические морфизмы заменам координат. И отсюда вытекает такая мотивация для интуиционистской логики, что типа правильно записанные законы физики выполняются во всех системах координат, то ностоящие математические законы должны выполняться во всех топосах, а это ровным счетом означает доказуемосость в инуиционалистской логике. Примерами утверждений, которые не выдерживают этот тест могут быть, например могут быть почти все утверждения про разные бесконечные кардиналы, потому что всегда можно найти такую «замену координат» где данный бесконечный кардинал будет счетным (обрушение кардиналов). Еще был приводит интересный пример с нестандартным анализом Робинсона. Там получается, что нестандартный анализ это функтор перехода от пучков над счетным бесконечным множеством к пучкам над компактификацией Стоуна-Чеха. Но к корректности этого утверждения нужно будет еще вернуться.
Еще один мой должок — это теорема Жиру. Это теорема про то, когда категория является топосом Гротендика, то есть когда она эквивалентна пучкам на ситусе. У нее довольно громоздкая формулировка и длинное доказательство. Вот формклировка: категория является топосом Гротендика тогда и только тогда, когда выполняется шесть усовий, а именно 1) у категории есть все конечные пределы 2) у категории есть все копроизведения и они несвязны и устойчивы под пуллбэками 3) каждый эпиморфизм является ко-уравнителем 4) Каждое отношение эквивалентности задается морфизмами и допускает факторизацию 5) каждая точная вилка стабильно точна 6) Есть множество порождающих объектов. Поэтому, понятно, почему эту теорему Мак Лейн вынес в аппендикс. Правда ее можно упростить: элементарный топос является топососом Гротендика, когда у него есть порождающее множество и все копроизведения. В таком виде эта теорема мне больше нравится. У этой теоремы есть полезные следствие. Хотя бы ее можно использовать в другую сторону, чтобы пользоваться хорошими свойствами известного топоса Гротендика. Еще отсюда следует, что для топоса Гротендика можно выбрать не просто ситус, а ситус с уймой хороших свойств: конечноые пределы, экспоненцирование, счетные копределы, подобъекты и фактор-объекты.
Что я планирую делать дальше? У меня есть кое-какие идеи, что дальше делать с топосами. Но я не уверен, что сейчас стоит писать про это здесь. В целом я устал от доказательств с коммутативными диаграммами, склеиванием пулбэков и сопряженными функторами. Но мне не перестало хотеться математики. Правда, теперь мне больше хочется чего-нибудь конкретного, типа водочки и картофанчика.
P. S.
Я добавил рубрикатор в верхнем посте. Или не рубрикатор, а типа оглавления блога, чтобы новым читателям было проще ориентироваться. Как вам? Пока там только математика, Берроуз, и некоторые относительно новые книжки. Но рубрикатор будет пополняться. |
|