Хотелось бы не теорию множеств улучшить, а логику первого порядка. Не "теорию всего", а язык.
Кому хотелось бы? Логикам? Или остальным математикам?
Дело в том, что нет совершенно,
совершенно ничего плохого в изолированности отдельных областей математики. Более того, почти все области (но не подобласти) математики изолированы друг от друга, это объективная реальность, и убежать от этого не получится, выделим ли мы в категорию "core mathematics", как Вербицкий, области, наиболее популярные в двадцатом веке области, а все остальные объявим "нематематикой", придумаем ли какую-нибудь иную глупость - все равно ничего не получится. Это объективная реальность, и с ней надо жить. Специалистам в комбинаторике и в ПДУ не нужны абстрактные гомологические методы (алгебраический анализ не считаем, потому что он хоть и интересен, но интересен сам по себе, приложений к классической теории ПДУ пока мало имеет), а гомологическим алгебраистам, напритив, не нужно знать множество аналитических оценок (которым их, к слову, в отличие от аналитиков по отношению к алгебре и теории категорий, часто сильно-пресильно заучивают на математических факультетах, привет советской традиции).
Но пытаться продать, как на рынке, "впарить" идеи, релевантные в вашей области остальным математикам, да ещё и при этом смотреть свысока на тех, кто покупать это не хочет, мол, "ничего вы не понимаете", уже некрасиво, да и просто бессмысленно.
Конкретно Воеводского в этом обвинить сложно, потому что у него были довольно приземленные цели - сделать proof assistant, а идеологическая "правильность" HoTT была на втором плане (вас, естественно, тоже не обвиняю, потому что ничего о вас не знаю; просто именно ваше высказывание сподвигло на написание поста).
Но вот весь этот шум вокруг HoTT сейчас создает ситуацию с толпой сектантов, у которых бы "все взять и переписать", а кто не хочет, тот просто ничего не понимает.
Тут ранее говорилось о ncatlab. Так вот, тот сайт в том числе и содержит немало тех логиков, которым недостаточно заниматься интересными для них логическими и/или концептуальными вопросами, они ещё и хотят, чтобы все остальные математики начали внезапно вместе с ними "молиться" на эту модную HoTT и остальные похожие проекты (например, теорию топосов и переформулировку дифференциальной геометрии на её языке).
Что интересно, в
-категориях самая ключевая фигура - это Jacob Lurie. Вот только и он не понимает причину всего этого, как сейчас выражаются в соцсетях, "хайпа" вокруг HoTT, фраза создателя ncatlab (Urs Schreiber) о том, как плохо и некрасиво, что алгебраические топологи не понимают ценности HoTT, смутила и его (Лури).
Впрочем, и на ncatlab
-категории уже не "котируются", там в почете
-категории и
-категории (скоро будут, наверное,
-категории для произвольного ординала
, такая тема уже была где-то на mathoverflow; любопытно, впрочем).
Наверное, чтобы быть объективным, надо сказать, что в такие рамки этих специалистов ставит математическое сообщество, которое то и дело пестрит любителями позадавать вопросы: "А зачем вы это делаете? А какой толк от этого? А как это поможет мне решать дифференциальные уравнения/доказывать утверждения про алгебраические кривые? Может быть, вам заняться чем-нибудь другим?"
Причем это распространено и среди великих людей, что ни в коем случае не умалает их математических достоинств.
Таким грешили, в том числе, по рассказам, Гельфанд и Бернштейн. У первого (опять же, по рассказам) вся теория гомотопий сводилась к гладким многообразиям (а та, что не сводилась, была не нужна, как очевидно), а второй с похожим снобизмом относился к гомологической алгебре. Арнольд переплюнул и их, когда заявил, что "математика - часть физики" (подразумевая, что остальная математика не очень-то и не нужна, это можно было бы называть "вырыванием из контекта", если бы не остальные его мысли про "преступных бурбакизаторов").
В Америке сейчас это тоже очень развито (в плохом смысле), и долгое время они и Гротендика не уважали в широких круга, что-то типа "да у него единственным примеров является его же одна большая теория".
Кстати, кто знает историю математики, уточните, пожалуйста, не привело ли подобное поведение со стороны широкой математической общественности к, мягко говоря, большим проблемам в жизни у таких великих математиков, как Лобачевский и Кантор?