Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Навеяно комментом (Бурбаки 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 в смысле Уилларда.]

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

  • (без темы)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments