Аннотация:
Логика Гёделя–Лёба — яркий представитель логик доказательств. Она описывает те факты, которые арифметика Пеано может вывести о самой себе. В этом докладе будут рассмотрены её свойства и ограничения. Также будет рассказано о её применении к языкам программирования в виде защищенной рекурсии (guarded recursion).