Intuitionistic fixed point theories over Heyting arithmetic
Toshiyasu Arai · arXiv (Cornell University) · 2010
In this paper we show that an intuitionistic theory for fixed points is conservative over the Heyting arithmetic with respect to a certain class of formulas. This extends partly the result of mine. The proof is inspired by the quick cut-elimination due to G. Mints.