Пес Ебленский - Топосы в Логике

Пес Ебленский - Топосы в Логике

rex_weblen

[	website	\|	Наши рисуночки	]
[	userinfo	\|	ljr userinfo	]
[	archive	\|	journal archive	]

Links

[

Links:

update journal edit friends fif tiphareth recent comments

]

Топосы в Логике

[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

How to Be Polyamorous When You Have Trypophobia

(Link)

Many people are polyamorous – desiring or engaging in multiple relationships with more than one person. Ethical non-monogamy has been an extremely hot topic lately, with more and more people trying out dating multiple people with the consent of everyone involved for the first time, but that doesn’t mean it’s always a walk in the park. For example, what if you’re deeply afraid of seeing too many holes at once? Here’s how to be polyamorous even when you also have trypophobia:
https://reductress.com/post/how-to-be-polyamorous-when-you-have-trypophobia/

How to Be Polyamorous When You Have Trypophobia

Re: How to Be Polyamorous When You Have Trypophobia

Re: How to Be Polyamorous When You Have Trypophobia

Re: How to Be Polyamorous When You Have Trypophobia

Re: How to Be Polyamorous When You Have Trypophobia

Re: How to Be Polyamorous When You Have Trypophobia

Я насрал в твоё жаркое, дарагой!

Re: Я насрал в твоё жаркое, дарагой!

я твой футон топтал. ты ешь собачий рис гандон