О приложениях интуиционистской теории множеств Крипке–Платека с праэлементами

В этом докладе я расскажу об интуиционистской теории множеств Крипке-Платека с праэлементами ($\mathrm{KPU}^i$) и двух её приложениях. Основное концептуальное наблюдение здесь состоит в том, что, с одной стороны, как и в случае классической теории $\mathrm{KPU}$, эта теория позволяет развить теорию обобщенной вычислимости, основанной на понятии Σ-определимости и имеющей многие привычные свойства обычной вычислимости. С другой стороны, $\mathrm{KPU}^i$ обладает большим разнообразием моделей, чем $\mathrm{KPU}$, и тем самым может быть увязана с большим разнообразием альтернативных понятий вычислимости.

Одно приложение связано с построением понятия функционалов конечных порядков над интерпретациями. Второе приложение связано с разработкой удобного формализма для построения β-доказательств. Для второго приложения требуется развитие определенного варианта семантики реализуемости и её использование для доказательства аналога теоремы Бухгольца об интуиционистских теориях неподвижных точек строго позитивных операторов.