george66По структуре очень напоминает теорию типов, которая была изложена в "Principia Mathematica", там парадокс лжеца нельзя было сформулировать, потому что утверждения уровня
могли содержать только ссылки на утверждения уровня
, ну и для каждого уровня, формально, нужно было формулировать все определения и утверждения занаво, потому что эта "лесенка" вынесена на метаязык. Ну только это не избавляет от тех же проблем, категорию всех категорий нельзя рассмотреть, ровно как и нельзя рассмотреть "категорию всех множеств на всех уровнях". Унивёрсумы Гротендика это, всё же, нечто другое.
Anton_PeplovMetacategory это не формальный язык, а модель определенной теории первого порядка. ETAC позволяет рассуждать о категориях ровно столько, сколько формальные выводы из аксиом групп позволяют рассуждать о группах. То есть всё хорошо до тех пор, пока нам не нужен какой-то механизм образования групп/категорий и механизм насыщения групп/категорий доп. структурами. К тому же это никак не решает проблему 2-категорий всех категорий, о ней на ETAC говорить нельзя. Про
ETCC доказано, что она не обладает достаточной выразительной силой, чтобы охарактеризовать метакатегорию всех категорий.
ETCS это вообще аксиоматизация топоса
(снова, я, конечно за то, чтобы говорить что множество - это объект категории
, а категория - это множество (которое объект категории
), но это, видимо, не то, что вы ищите). Всё это в приведённой ссылке есть, почитайте, там помимо строгих конструкций есть довольно популярные объяснения.