Xaositect,
да, я, в принципе, должен был понимать, что вы и так знаете, просто "задело за живое": сам долго не мог понять, как это так, что в математике, например, нет "множества всех слонов". А что делать, что мы хотим рассматривать "группу всех слонов" с бинарной операцией репродукции (хотя это будет не функция, так как каждой паре слонов будет далеко не один слоненок).
Странно, но меня именно этот факт и примерил, что "слонов" можно математически смоделировать с помощью чистых множеств, без атомов.
А интуиция страдает - это да.
А ETCS, как я понимаю, не столько для введения атомов (ведь есть и версия ZFC с атомами, хоть и в записанном виде не найти), cколько о формализации категорной интуиции. Например, чтобы изоморфизм не определялся теоретико-множественно, а был базовым объектом, а уже равенство было бы частным случаем изоморфизма.
Есть ещё SEAR Майкла Шулмана, но она не доделана или, по крайней мере, не записана полностью. И ETCS, и SEAR - это, так называемые structural set theories, которые интуитивны для категорщиков, не неинтуитивны для "простых смертных". Там, например, пусть и есть атомы, но нет множества даже конечного количества множеств, что тоже жутко неинтуитивно. Win some, lose some. Хотя, надо отдать должное, что-то в этом есть, потому что математики и не работают с реальными объектами, даже тот же анализ на вещественной прямой происходит не столько на реальной вещественной прямой, сколько линейно упорядоченном поле (ну и с возведением в степень), изоморфном ей.
А большая часть анализа
так и вообще формулируется для линейных отображений между определенными гильбертовыми пространствами.
-- 14.10.2017, 21:48 --Xaositect,
кстати, вот, о людях, которые
Цитата:
занимаются разными ETCS.
Почти все уже приняли тот факт, что нет в математике "единственно верных основний". Так что различные теории как множеств, так и типов, представляют не столько прагматичный интерес, сколько математико-логический.
В большинстве своем, люди, занимающиеся основаниями, не хотят, чтобы какие-то конкретные основания стали доминирующими, им просто это искренне интересно, и все.
Как и интересы коммутативных алгебраистов перестали ограничиваться нуждами алгебраических геометров, как и многих чистых специалистов в ПДУ не интересуют приложения в дифференциальной топологи, так и тут.
И это вовсе не плохо, а совершенно прекрасно. Плоха противположная ситуация, но о ней я уже много чего сказал, так что хватит с меня.