Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Мечта о финитизме II: Аскетизм

Изначальная идея Гильберта по установлении математики на прочные основания состояла в том, чтобы выделить супернадёжную базовую теорию ("финитизм") и внутри неё доказать непротиворечивость всей остальной математики. (К сожалению, идея с доказательством непротиворечивости сильной системы из средствами более слабой, оказалась несостоятельна, но этот вопрос пока отставим в сторону.)

В прошлом посте я рассказал о том, что системой, позволяющей с комфортом и большой общностью работать с финитарными объектами, является недавно сформулированная OTT (Observable Type Theory). В такой системе вести метаматематические доказательства чрезвычайно удобно, однако на роль камменного фундамента она подходит едва ли: слишком уж большая и сложная теория. Тут нужна аскетичная теория.

В качестве таковой Торальф Сколем разработал примитивно-рекурсивную арифметику PRA. С тех пор, как Goodstein разработал для неё logic-free исчисление, она стала особенно притягательна в этом смысле. Язык PRA состоит из константы 0, неограниченного алфавита свободных переменных, и счётно-бесконечного числа символов примитивно-рекурсивных функций (по одному на каждую такую функцию). Утверждения в PRA имеют вид f(something1) = g(something2), где f и g примитивно-рекурсивные функции, а something1 и something2 изготавливаются из константы 0, свободных переменных и применения примитивно-рекурсивных функций. Переменные подразумеваются связанными квантором всеобщности. В качестве правил вывода используются 2 правила подстановки, одно правило воплощающее транзитивность равенства и одно правило для индукции. Аксиомы теории — в точности определения примитивно-рекурсивных функций. В общем, очень удобная и надёжная система, сложно себе представить, чтобы у неё где-то были уязвимости. С добавлением дополнительной аксиомы о допустимости трансфинитной индукции до ε0 в рамках этой системы можно доказать непротиворечивость арифметики Пеано, а если сделать индукцию до Г, то можно доказать и непротиворечивость OTT.

В целом очень удобно — добавляешь к PRA индукцию до определённого ординала и получаешь доказательство непротиворечивости теорий, сила которых не выше этого ординала. Сила теории это первый ординал, до которого изнутри теории “нельзя достать”. У всех теорий первого порядка (даже у страшно сильной теории множеств) сила является счётным ординалом. У всех более чем конечных теорий, сила не ниже ω. Если теория содержит более чем конечное число объектов, то до любого конечного ординала n мы можем достать, а ω — первый бесконечный ординал. Если внутри теории можно доказать тотальность умножения, то её сила уже не ниже ω2, если можно доказать тотальность степени, то ω3, если тетрации, то ω4 и так далее.

Некоторое неудобство PRA состоит в том, что у самой PRA довольно большая сила: ωω. Было бы удобнее взять в качестве базы теорию, имеющую минимальную возможную для теории с более чем конечным числом объектов силу ω. И тогда уже добавив к этой системе например допустимость индукции до ωω, доказать на её базе непротиворечивость PRA. Более того, известно, что такие системы способны в опредённом смысле осознавать собственную непротиворечивость.

Аскетичный финитизм AFIN должен быть системой силы ω, осознающей свою непротиворечивость, и такой, что доказательство непротиворечивости любой системы силы α получается добавлением к AFIN аксиомы о допустимости индукции до α. (Естественно, система с добавленной аксиомой уже не может осознавать собственную непротиворечивость.)

Отличным кандидатом на роль языка для такой системы является минимализированный язык диофантовых предикатов.

Мотивация Гильберта состояла в том, чтобы доказать непротиворечивость всей математики исходя из непогрешимого финитизма, этом не суждено сбыться, однако можно отдельно (а) создать непогрешимый финитизм и (б) доказывать непротиворечивость более сложных систем, исходя из непогрешимого финитизма и одной аксиомы инфинитарной аксиомы, общность которой позвояет оценивать, насколько далека та или иная система от конечности. Подробнее о том, почему мечте Гильберта несуждено было сбыться, можно прочитать в посте о теореме Гёделя.
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень 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.
  • 0 comments