Погружение модального $\lambda$-исчисления в логику доказательств

Система логики доказательств LP, введенная автором, восходит к доказуемостному исчислению Гёделя, известному также под именем модальной логики S4, которому была посвящена монография П. С. Новикова “Конструктивная математическая логика с точки зрения классической” LP дает точный математический ответ на вопрос о доказуемостной семантике S4, поставленный Гёделем. В настоящей работе проводится сравнение выразительной силы LP, типового $\lambda$-исчисления и модального $\lambda$-исчисления. Показано, что малый (а именно хорновский) фрагмент LP достаточен для естественного погружения типового $\lambda$-исчисления. Показано, что сама LP моделирует модальное $\lambda$-исчисление.