Великость

На прошлой мюнхенской матшколе мы в разговоре как-то задумались о термине “мощность множества” в русском языке, ведь он чертовски неудачный, потому что основной смысл этого слова — та мощность, которая измеряется в ваттах и лошадиных силах, и она к величине множеств никакого отношения не имеет. По-немецки эта мощность называется «Leistung», а то, что горе-переводчики перевели мощностью в работах Георга Кантора называется «Mächtigkeit», и это термин выдуманный Кантором, производный от слова «Mächtig» в смысле крупный, громадный.

Переводчику не следовало стесняться изобретать новые слова, и тоже нужно было исходить из прилагательного синонимичного слову «размер», но отражающего гигантичность этого размера. Крупность, громадность или, лучше всего, великость. Великость лучше всего подходит благодаря существованию термина равновеликий.

Дело в том, что понятие великости (давайте теперь называть её так) множества вводится Кантором именно через равновеликость:
Кантор говорит, давайте называть множества равновеликими, если их элементы можно поставить во взаимно-однозначное соответствие. Потом доказывает что классы равновеликости конечных множеств классифицируются натуральными числами. А потом говорит, а давайте обобщим натуральные числа до более общей линейной* шкалы «великостей» множеств, элементы которой суть классы эквивалентности множеств по равновеликости.

Такая missed opportunity, эх.

Впрочем, таких в математике пруд пруди. Например, ещё Феликс Клейн пишет, что “группа“ есть абстрактное воплощение типа симметрии, а “действие группы“ на тот или иной математический объект (многочлен, многогранник, замощение, пространство) это конкретное воплощение симметрии. Так почему же в слове “группа” нет ни буквы о симметрии?

Аналитические топосы

Как известно, огромную часть математики можно формализовать, пользуясь лишь конструктивными методами, не выходя за рамки аксиомы зависимого выбора DC и пользуясь только множествами конечной, счётно-бесконечной и континуальной мощности, причём последние всегда являются вполне-сепарабельными топологическими пространствами. Сюда входит общая топология в рамках эффективных пространств Суслина, весь вещественный (и вообще весь метрический) анализ, солидная часть функционального анализа, оперирующая сепарабельными банаховыми пространствами.

Однако как только мы опускаем требование сепарабельности (т.е. выходим в мир множеств более чем континуальной мощности), нам резко требуется жёстко неконструктивный гаджет: аксиома о том, что каждый фильтр достраивается до ультрафильтра (она же Boolean prime ideal theorem, она же теорема о представимости Стоуна, она же теорема о представимости непротиворечивых теорий).

Без него не работают в несепарабельном случае такие центральные инструменты функционального анализа и общей топологии, как теорема Хана-Банаха, компактификация Стоуна-Чеха, теорема Тихонова для Хаусдорфовых пространств. Конечно же их сепарабельно-ограниченные варианты работают без неё (причём сепарабельная теорема Хана-Банаха даже DC не требует, она эквивалентна WKL), но так работать несколько неудобно.

С другой стороны, теорема Хана-Банаха влечёт существование неизмеримых множеств и парадокс Банаха- Тарского, то есть BPI это люто-неконструктивный принцип. Каждый выбирает по себе.

Но главный вывод из этого всего в том, что Proof Assistant'ы стало быть не могут ограничиваться модальностью, имеющими вычислительную интерпретацию. В смысле, в рамках Proof Assistait'ов не то чтобы несложно, но обозримым образом можно реализовать вычислимым образом не только классическую модальность (где верен закон исключённого третьего) через кодирование двойным отрицанием, но и классическую модальность с зависимым выбором (через открытую рекурсию, вполне вычислимый принцип). А вот модальность, в которой была бы верна BPI, так не сделаешь, BPI (как и общую аксиому выбора) можно только постулировать.

Вот проанализируешь это и сразу понимаешь, зачем Воеводский занялся своими B-системами и вовсю трудится, пытаясь создать общий фреймворк для теорий типов и инструментарий для доказательства скопом, что их синтаксические модели инициальны в категориях всех их моделей — только этот результат позволит показать, что постулировать штуки типа BPI и AC действительно _можно_, без риска получить кукиш на выходе.

Тривиализация присущая малым размерностям

Существует приличное количество результатов, верных для вещественной плоскости, и неверных в более высоких размерностях. Так например только в двухмерье верно, что равносоставленные фигуры равновелики, и что всякая простая замкнутая кривая делит плоскость на две несвязные области: “внутреннюю” область, гомеоморфной стандартному диску, и “внешнюю”, гомеоморфную плоскости с выколотой точкой.

Можно ли как-то вычленить, какое именно свойство топологического двумерья ответственно за такую регулярность?