Исключение вырезов для исчисления с помощью nats или другого индуктивного типа данных?

Кто-нибудь направляет меня к статье, подробно описывающей теорему исключения среза для пропозициональной интуиционистской логики, включая индуктивный тип данных, такой как натуральные числа (списки или деревья тоже подойдут)? Примером системы, которая меня интересует, является T Годеля, который имеет типы, заданные грамматикой . Меня не очень интересуют квантификаторы натуральных чисел или предикаты, индексируемые натуральными числами.$A ::= \mathbb{N} \;\;|\;\; A \to A'$

Я знаю, как доказать бета-нормализацию для версии этих систем с естественным выводом, используя аргумент логических отношений (или связанные методы, такие как NbE), но хотел бы знать, существуют ли стандартные ссылки о том, как адаптировать эти методы для последовательных исчислений.

Причина, по которой я спрашиваю, состоит в том, что я изучаю добавление операторов фиксированной точки для защищенной рекурсии в язык. Денотационная идея довольно старая - интерпретировать типы как ультраметрические пространства и фиксированные точки с помощью теоремы Банаха - но чисто синтаксические методы, которые я знаю для доказательства исключения среза, похоже, не очень хорошо адаптируются.

Как насчет работы Ульриха Бергера? Например, Сильная нормализация для прикладного лямбда-исчисления . Часть «рекурсивно определенные константы» дает вам индуктивные типы, более или менее. И не стоит откладывать слово «нетипизированный», он получает результаты и для типизированных систем.

Вы можете взглянуть на McDowell и Miller's Cut-Elmination для логики с определениями и индукцией , в которой показано, как адаптировать метод Таита к интуитивистскому последовательному исчислению первого порядка с индуктивно определенным предикатом натуральных чисел.