Revisiting the conservativity of fixpoints over intuitionistic arithmetic

Mattias Granberg Olsson, Graham E. Leigh

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $\widehat{\mathrm{ID}}{}_1^{\mathrm{i}}$, over Heyting arithm…