Навеяно комментом (Бурбаки 2.0)

66george: А если он дотянет снизу до лямбда-два, будет ли это выдающимся вкладом в науку?

Сетцер уже внёс выдающихся вклад в науку, тем что определил ординал iMLTT with induction-recursion — мощного исчисления построений с внутренней моделью себя, и потом спутся десятилетие смог даже построить его предикативно снизу в рамках системы explicit mathematics.

Теперь причёсывать надо. Нужно как-то соотнести explicit mathematics с усиленными теориями множеств Крипке-Платека (по которым много продвинулся Ратьен) или (предпочтительно) сильными предикативными исчислениями построений (HoTT = iMLTT + аксиома унивалентности + высшие индуктивные типы). Причесать тут важнее, чем продвинуться, потому что зоопарк уже напоминает зоопарк элементарных частиц, в физике семидесятых.

На роль безопасного ядра для математики претендуют
- Классическая арифметика второго порядка Z2 и её пять подсистем для reverse mathematics.

- Отличная (но недоделанная) HoTT, замечательная тем, что агностична в смысле интуиционизма и конструктивности, и очень хорошо совместима с классической математикой: она не содержит, но совместима как с Законом Исключённого Третьего, так и с Аксиомой Выбора.
-- Вариант с аксиомой выбора включает в себя всю классическую математику (в виде ZFC) и эквиконсистентен ZFC с гипотезой о каком-то большом кардинале. Особенно удобно, что аксиомы о больших кардиналах прямо трансформируются в аксиомы о больших вселенных, так что можно получить надсистему классической математики с любыми желаемыми крупнокардинальными дополнениями.
-- Вариант с исключённым третьим имеет (судя по всему) внутренную realizability-интерпретацию в интуиционистском варианте с открытой рекурсией, и эквиконсистентен Z2.
-- интуиционистский вариант (даже с открытой рекурсией) имеет (судя по всему) прямую вычислительную интерпретацию.
Однако, HoTT недоделана: её нужно доделать открытой рекурсией и высшей индукцией-рекурсией (насколько я понимаю, сейчас ещё никто точно не знает как), чтобы у неё была внутренняя модель себя и realizability model для Z2. Наконец нужно выделить в HoTT подсистемы соответствующие ослабленным вариантам Z2 из Reverse mathematics.

- Прикольная explicit mathematics (тоже градуированная по силе для reverse mathematics), и превосходящая HoTT (в его текущем недоделанном состоянии по крайней мере) тем, что имеет внутреннюю модель и пригодна для описания более крутых ординалов, да и вообще очень прямая и прозрачная. [EM с HoTT должна помирить внутренная модель вычислений внутри HoTT (возможно, directed types в той или иной форме).]

- наконец есть никому непонятная Ludics, но прорывная как термоядерная бомба. [Есть соображение, что обобщение HoTT под названием Opetopic Type Theory это шаг в направлении такого великого объединения, но это ещё очень далёкие горизонты.]

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

В идеале, нужно будет сделать линейный вариант системы*, непротиворечивый по построению + внутреннюю нотацию для рекурсивных ординалов, устроенную так, постулат о фундированности того или иного рекурсивного ординала можно напрямую использовать, как инструмент дедукции. Тогда доказательства, требующие бОльшей дедуктивной силы, можно будет выписывать кондиционально относительно гипотезы о фундированности потребного ординала/существования потребного большого кардинала.

[* В ещё более идеальном варианте он должен представлять из себя естественную self-justifying system в смысле Уилларда.]

Потом останется только переписать Бурбаков с компьютерной верификацией всех доказательств, и открыть новую эру в математике. ;-)