"Взамен есть формальные теории, отвязанные от теоретико-множественного контекста."

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

"Она будет того же качества."
Это вы про "идиотскую хуйню"? Возникает вопрос, что, более или менее аналогичное - не идиотская хуйня и почему следует выбирать второе, а не первое.

> больше таких отвязанных теорий
Арифметика Пеано первопорядковая.

> Это вы про "идиотскую хуйню"?
Это про возможную противоречивость.

Вот тут большой список: https://en.wikipedia.org/wiki/List_of_first-order_theories

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

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

Но по сути это мало кого и беспокоит - сам язык множеств как ни крути полезен и нужен. То что ZFC взяли с потолка - ну и что же. Надо же как-то аксиоматизировать. Вот и аксиоматизировали как могли. Полезности самого языка это не отменяет. И сами основания, как они например описаны у Бурбаков, куда изящнее и проще всех HoTT и топосов вместе взятых.