tiphareth: "Pink Floyd Ballet"

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

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 (Ответить) (Уровень выше)

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