tiphareth: "Pink Floyd Ballet"

(Читать комментарии) - (Добавить комментарий)

	tiphareth 2022-05-01 14:07 (ссылка)
	на самом деле не теория множеств, а теория категорий теория множеств устарела (Ответить) (Уровень выше) (Ветвь дискуссии)

	sometimes 2022-05-01 17:13 (ссылка)
	множества же образуют категорию, довольно полезную? и постоянно приходится аккуратничать с универсумом и автореферентностью (Ответить) (Уровень выше) (Ветвь дискуссии)

	sometimes 2022-05-02 04:30 (ссылка)
	опять же, малые и локально малые категории (Ответить) (Уровень выше) (Ветвь дискуссии)

	(Анонимно) 2022-05-02 06:06 (ссылка)
	анус у карлика тоже может оказаться локально малым педофилы наверняка занимаются такими категориями (Ответить) (Уровень выше) (Ветвь дискуссии)

	sometimes 2022-05-02 15:33 (ссылка)
	Ухаживала за бывшими членами СС из внутреннего круга своего брата (Ответить) (Уровень выше) (Ветвь дискуссии)

	(Анонимно) 2022-05-02 19:42 (ссылка)
	славный малый тот брат, должно быть (Ответить) (Уровень выше)

bors
2022-05-02 00:47 (ссылка)

А есть вообще теория категорий как формальная система? Когда я в последний раз искал пару лет назад, не нашел законченной теории. Можно конечно построить её из терии множеств с каким-то универсумом, но это не интересно.

(Ответить) (Уровень выше) (Ветвь дискуссии)

	tiphareth 2022-05-02 05:00 (ссылка)
	нет, вроде бы были попытки в эту сторону, от вот этого деятеля https://en.wikipedia.org/wiki/William_Lawvere но дожимать никто не стал, хуле (Ответить) (Уровень выше)

sometimes
2022-05-02 05:05 (ссылка)

я тоже оскоромился этим вопросом, но к стыду своему постеснялся. как я понял, есть такие попытки, но я их не уважаю что-то абсолютно:

https://www.quora.com/How-do-you-feel-about-using-Category-Theory-to-replace-ZFC-set-theory
https://ncatlab.org/nlab/show/ETCS
https://arxiv.org/pdf/0810.1279.pdf

вот товарища Шульмана сейчас читаю, когда больше делать нехрена.

не уважаю вот почему: множества простые как пень, они лишены структуры. этим они сами по себе малоинтересны, но относительно удобны как строительный материал, потому что ничего на себе не тащат. грубо говоря, есть жалобы сумасшедшего человека Кравецкого, что надо выгнать машины Тьюринга из computer science, потому что они примитивные и на них никто ничего не программирует; а вот надо вместо них пихнуть, например, хотя бы python.

довод, что именно из-за трехкопеечной простоты и наглядной механической интерпретации машины Тьюринга (а не даже
RAM) так в ходу, в них без лишней возни можно управиться не только с проблемой останова, но и, например, с теоремой Кука-Левина (и прочими диагонально-подобными аргументами из теории вычислительной сложности), до него, увы, совершенно не доходит, потому что он упрямый пень.

категории, конечно, не пакость вроде python, а совсем наоборот, кодируют в себе важность морфизмов, а не элементов; но они все равно более громоздко устроены, и грабли автореферентности (которая приводит к противоречиям) в них, насколько я могу понять, в большей степени замаскированы. оговорки про то, что тут категория должна быть малая или локально малая, сплошь и рядом.

хотя когда пишут, что с типизированными объектами работать приятнее (или хотя бы честнее), это правда: когда говорят про число 3, например, плюют это элемент \mathbb{Z} или \mathbb{Q}, \mathbb{R}, \mathbb{C}, \mathbb{H}, \mathbb{O}, you name it, потому что \mathbb{Z} в них во все канонически вложено единственным образом (но при этом оно тоже разное - где коммутативное кольцо, где ассоциативное, а где просто алгебра с единицей - т.е. объекты разных категорий); но, например, c 1 + i уже не всё так хорошо; наверняка при запихивании во всякие системы формальной верификации с этим возникают неприятности.

в OCaml (и, кажется, standard ML), например, нет автоконвертации, и 3 как элемент целых и как элемент действительных это разные сущности.

(Ответить) (Уровень выше) (Ветвь дискуссии)

siblington
2022-05-02 08:25 (ссылка)

Все фигня, кроме графов. Множества - это уже перелет, а графы - в самый раз для описания чего угодно, втч математики. Например, числа это вершины графа, а математические операции с ними - ребра. Таким образом любая математика - это маршрут на графе. Примерно, то, что сейчас Вольфрам в массы несет.

(Ответить) (Уровень выше)

kaledin
2022-05-02 13:54 (ссылка)

Нет, потому что никого не ебет, мода прошла. Последние, кто пытался прописать основания как формальную систему, были Бурбаки; по результатам выяснилось, что (1) дело бессмысленное, ненужное и совершенно безблагодатное, и (2) они к тому же проспали тренд и в качестве основания взяли теорию множеств, хотя надо было теорию категорий. На этом осознании -- по словам Картье, который вообще-то врет как дышит, но здесь я ему верю -- проект "Бурбаки" кончился.

В теории, нужно бы в какой-то момент, но это будет сделано только если там найдутся интересные и нетривиальные явления; просто прописывать "чтоб было" никто не будет.

(Ответить) (Уровень выше) (Ветвь дискуссии)

tiphareth
2022-05-02 20:44 (ссылка)

основания, конечно, сомнительная кака, но
дело бурбаков очень полезное, ибо как учебники многие их книги до сих пор очень ок
"топологические векторые пространства" шедевр вообще

основные учебники бурбаков написаны в 1930-е, когда никаких категорий еще не было

(Ответить) (Уровень выше) (Ветвь дискуссии)

	kaledin 2022-05-02 20:49 (ссылка)
	>но дело бурбаков очень полезное Абсолютно! Но формальная система оказалась ненужной, по факту. Перестарались. (Ответить) (Уровень выше) (Ветвь дискуссии)

	sometimes 2022-05-03 15:53 (ссылка)
	Ну как ненужной, аккуратность же соблюдают с тех пор, когда с большими объектами работают. (Ответить) (Уровень выше) (Ветвь дискуссии)

kaledin
2022-05-03 20:56 (ссылка)

Аккуратность соблюдают со времен парадокса Рассела, когда никаких формальных систем не было.

Формальные системы это наследие идеи Гильберта все так прописать, чтоб комар носа не подточил -- которая, по-видимому, основана на его травматическом опыте боданя с Кронекером в юности, а так-то, ни для чего не нужна. Поскольку она к счастью еще и доказуемо неосуществима, можно про нее просто забыть и не заморачиваться.

Лично я избегаю даже универсов (по факту, даже они ни для чего содержательного не нужны).

(Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-05-04 10:25 (ссылка)

> Аккуратность соблюдают со времен парадокса Рассела, когда никаких формальных систем не было.

парадокс Рассела же как раз накопали в попытках её построения, нет? Russel, Whitehead и т.п.

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

аксиомой выбора, опять же, постоянно пользуются, все хотят максимальных идеалов (подмодулей; любых максимальных подобъектов вообще) потому что, а без Геделя и Коэна как-то стремновато было (она и правда вроде бы и очев. а вроде бы и не оч.).

континуум-гипотезой стараются не пользоваться, правда, хотя казалось бы
ну и вообще стараются понимать, использовалась по дороге AC или нет

(Ответить) (Уровень выше) (Ветвь дискуссии)

kaledin
2022-05-04 15:18 (ссылка)

>парадокс Рассела же как раз накопали в попытках её построения, нет?

Ровно наоборот.

Я б тебе процитировал вики, но там соотв. статьи все нахуй засраны философами и представляют собой идиотскую чушь ни о чем, процентов на 80. Но общая картинка понятна: парадоксы это примерно 1900, программа Гильберта это начало 1920х.

До 1900 таким занимался только Фреге, но он был идиотский идиот и фрик, это все знали.

(Ответить) (Уровень выше) (Ветвь дискуссии)

	sometimes 2022-05-04 18:30 (ссылка)
	> парадоксы это примерно 1900, программа Гильберта это начало 1920х а principia mathematica это 1910 (Ответить) (Уровень выше)

bors
2022-05-02 22:34 (ссылка)

Вот этого я не понимаю, кстати. Что там делать то? Аксиомы ZFC довольно понятны (не знаю, какие аксиомы у Бурбаки, но наверное, похожие), как из них получать стандартные конструкции понятно, а значит и подмножества через предикаты. Это ничего не гарантирует, но даёт некое ощущение как это может работать. Конечно, если сделать "основания математики" - это формально доказать тысячи теорем - то это и безблагодатно и недостижимо. Но почему нельзя предыдущее сделать через категории? Дать какие-то аксиомы и базовые конструкции? Но ничего такого элементарного я не нашел, значит там что-то не работает на фундаментальном уровне, наверное. Надо посмотреть ссылки что Миша и sometimes дали, когда время будет.

(Ответить) (Уровень выше) (Ветвь дискуссии)

kaledin
2022-05-02 22:54 (ссылка)

>Но почему нельзя предыдущее сделать через категории?

Можно, причем пятнадцатью разными способами. Просто не нужно.

Ловер же не просто так аксиоматизировал категорию множеств; там на выходе получилось хорошее понимание понятия топоса (которое открыл Гротендик конечно, но Ловер отчасти прояснил). Что-то похожее сделать с категорией категорий было бы полезно, но только если оно получится неожиданно хорошо (как в определении топоса, которое в итоге сводится к двум что ли аксиомам). Просто тупо выписывать набор аксиом дело совершенно безблагодатное, и не нужно вообще ни для чего, вроде бы.

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

Истроически, тот ж Ловер примерно тогда же -- середина 60-х, была например конфа в La Jolla, CA в 66 году, от которой есть том proceedings -- пытался и для категорий какую-то аксиоматику прописать, но без Гротендика ничего интересного не вышло, ну все и забили.

(Ответить) (Уровень выше) (Ветвь дискуссии)

bors
2022-05-04 14:03 (ссылка)

> формальные языки, которыми оперируют логики (и которые происходят из какой-то совершенно допотопной математики, типа до первой мировой войны

? Формальные языки происходят не из математики, а из математических доказательств. Их математика в целом не может быть понята - нельзя в одно запихнуть всё. Те немногие доказательства, что есть, в этой математике идут из её интепретации, через самореферентность. (Приложения может и используют какую-то интересную математику, но это другое). Это про начало века. Про форсинг и прочие науки я не знаю, но у меня есть интуиция, что там есть интересные и потенциально полезные (по крайней мере в анализе) идеи про переходы и пределы. Категорный язык инетерсен уже сейчас, конечно, но вы же понимаете, что интерес к формальным языкам происходит из-за их родства с доказательствами, которые в свою очередь являются более важной частью математики чем категории.

(Ответить) (Уровень выше) (Ветвь дискуссии)

kaledin
2022-05-04 15:34 (ссылка)

"Доказательство" это не математический обьект. Если мы интересуемся математикой -- а не философией, лингвистикой, или еще чем-то там -- то понятие "докательства" надо формализовать. То, как это сделано в логике, казалось внятным и актуальным 100 лет назад, а сейчас выглядит дико. Это уже на практике видно. Скажем, что такое "модель теории множеств" нормальный человек понять не в состоянии, там не замечаемые авторами априорные предположения и порочные круги на каждом шагу. Единственная известна мне внятная интерпретация это топос с некоторыми дополнительными свойствами. Да даже и на более фундаментальном уровне -- для Гильберта, базовым надежным уж точно существующим обьектом были положительные целые числа; с современной точки зрения, базовый обьект это категория конечных множеств, а число это так типа, обозначение для класса изоморфизма обьектов в ней.

Математика давно уже не наука про числа и формулы, и поэтому попытки обосновать ее через формулы особого интереса не вызывают. Какие-то полезные идеи в логике конечно есть, но их приходится буквально выцарапывать каждый раз. Почти как из физики.

(Ответить) (Уровень выше) (Ветвь дискуссии)

bors
2022-05-05 22:30 (ссылка)

>"Доказательство" это не математический обьект
да, но это не умаляет его важности для математики

Я не читал Ловера, я знаю как определять топос-точку без понятия множества (если он это делает), но если в результате получается категория с какими-то абстрактными объектами, типа множествами, но с хорошо определенными стрелками с понятными свойствами, то я согласен что это звучит хорошо и комфортно.

> для Гильберта, базовым надежным уж точно существующим обьектом были положительные целые числа; с современной точки зрения, базовый обьект это категория конечных множеств, а число это так типа, обозначение для класса изоморфизма обьектов в ней

ну типа и с бесконечными множествами люди как-то так думают. Есть стандартные конструкции, можно добавлять аксимоы существования недостижимых кардиналов: омега, всякие произведения и степени омеги, ординалы в какой-нибудь записи, с помощью предикатов определяются подмножества этих множеств. Конечно бывают счетные модели этого всего богатства, по понятным причинам, и в целом структура гораздо сложнее скелета категории конечных множеств, но картинка перед глазами какая-то такая, у меня по крайней мере.

(Ответить) (Уровень выше) (Ветвь дискуссии)

kaledin
2022-05-06 20:16 (ссылка)

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

Но придумал он это определение топоса, именно пытаясь аксиоматизировать множества.

(Ответить) (Уровень выше)

sometimes
2022-05-04 18:59 (ссылка)

Я не уверен, но по-моему вы с Дмитрием смешиваете две вещи - язык логики первого порядка (который кодирует в себе, действительно, процедуру верификации доказательства - с вариациями в виде интуиционизма, например; это та самая шняга с кванторами, птичками и стрелочками) и теории первого порядка - например, ZF (аксиоматика Пеано - другой пример), которая есть язык логики + ~~электрификация~~ аксиоматизация теории множеств Кантора, которую Гильберт называл раем потому, что из множеств, действительно, можно изготовить все математические объекты.

Так вот - первая про математические доказательства, а вторая - про множества, и это типа разные вещи.

(Ответить) (Уровень выше) (Ветвь дискуссии)

siblington
2022-05-05 08:31 (ссылка)

Вы все всё перепутали. Дело в том, что философы забыли сообщить математикам, что метафора здания, стоящего на твердом основании из аксиом и строгих определений, больше не обязательна. Поэтому математики обычно спокойно сидят крутят ручки своих арифмометров, но время от времени самого смышленого из них вдруг озаряет вопрос об основаниях. Они все вскакивают и начинают носиться кругами, как курица с оторванной головой, в поисках чего-то основательного. Ну и затихают постепенно на разных стадиях ничего - множествах, категориях, топосах-хуёпосах.
Философы математикам теперь не указ, а сами математики до смены метафоры на более адекватную никогда не допрут, так что этот перпетум мобиле ака цирк с конями будет продолжаться еще некоторое время. До самой ядерной войны, я думаю.

(Ответить) (Уровень выше)

	bors 2022-05-05 22:32 (ссылка)
	ну вы же сами написали, почему вторая про математические доказательства - потому что из неё можно изготовить все математические объекты, а они нужны для доказательств (Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-05-06 20:00 (ссылка)

~~you can call me Rachel~~ можно на ты, если комфортно. я имел в виду, что изготавливать все объекты можно и из чего-то другого, а вот сделать что-то со стрелочками и кванторами (и таким образом "пересесть с иглы формульного одобрения") я не очень понимаю, как: все равно остаются аксиомы и правила вывода. Они, конечно, могут иметь вид диаграмм и правил их преобразования, но по сути это те же формулы ведь (хотя, возможно, и более адекватные), e \circ f = g \circ h. Любую, наоборот, формулу можно записать как коммутативную диаграмму, но она довольно быстро станет impenetrable.

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

Почему-то ещё подумал (это к делу не относится, относится, однако, к логике) - в этой науке и самой по себе (в её существующей форме) есть весьма красивые вещи, не торчащие непосредственно наружу; помимо форсинга (который как раз прикладной), например, замечательные шкалы Крипке в интуиционизме и игры Эренфойхта. А вот как раз "доказательство теоремы о нулях через элиминацию кванторов" или теорема Тарского-Зайденберга выглядят, как помесь ежа с ужом; теория Хрущовского же слишком сложная для меня материя пока что, увы.

(Ответить) (Уровень выше) (Ветвь дискуссии)

bors
2022-05-07 13:52 (ссылка)

Мне видится так:

1) Язык первого порядка без множеств - это игрушечный пример формализации математических доказательств. Никто в теории групп не работает в аксиоматике теории групп. Для них это просто определние группы, а работают они со множествами/категориями. (Никто вообще в аксиоматике никакой не работает, но уж если пытаться формализовать, то как-то ближе к практике). С теорией чисел чуть менее однозначно, есть извращенцы, которые пытаются пользоваться только аксиомами Пеано (в своих целях), но нормальные люди так не делают. Все эти языки имеют какое-то теоритическое/математическое значение (как в теореме Тарского-Зайденберга), но они не аппроксимируют математические доказательства.

2) И наоборот, если есть базовое определение множества, то его можно элементарно формализовать (по определению "базовости"). Хоть, навреное, и не обязательно в языке первого порядка.

Поэтому для меня нет особой разницы между изучением мат. доказательств и ненаивной теорией множеств, хотя этот подход и забуксовал на данный момент.

Мне кажется, теория вероятностей может стать яснее, но я не знаю, занимаются ли этим люди сейчас.

(Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-05-09 07:27 (ссылка)

Я, кстати, погуглил, есть вполне к теорверу подход с т.з. giry monad, занятно

и есть какие-то статьи про statistical machine learning и bayesian reasoning в контексте теории категорий
не знаю, насколько густой и плодотворный, впрочем

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

аксиома фундирования причем слишком жесткая, говорят, что иметь множество, являющееся собственным элементом, бывает полезно, поэтому есть варианты затыкать эту дыру по-другому, называется non-well-founded set theory.

я, кстати, думал, что HoTT Воеводского тоже имеет отношение к этой теме, но там я совсем не разбирался.

(Ответить) (Уровень выше)

	sometimes 2022-05-09 07:40 (ссылка)
	P.S. а есть и теории, в которых есть множество всех множеств (что вроде бы выглядит естественным - мы можем его себе представить - так почему же его нет?), напр. https://en.wikipedia.org/wiki/New_Foundations (Ответить) (Уровень выше)

sometimes
2022-05-03 12:11 (ссылка)

Вот, кстати, типичная ошибка с перепутанными типами (анонимус захотел на Нептун, я стал смотреть, где там местечко покомфортнее):

https://www.jpl.nasa.gov/images/pia09927-neptunes-hot-south-pole

Scientists say Neptune's south pole is "hotter" than anywhere else on the planet by about 10 degrees Celsius (50 degrees Fahrenheit).

На самом деле на 18℉ - они перепутали аффинные градусы с векторными.
У физиков типам в какой-то степени соответствуют размерности, но не вполне - сами по себе целые и действительные и т.п. безразмерны.

(Ответить) (Уровень выше)

(Читать комментарии) -