# A conservativity result of intuitionistic set theory over arithmetic

In their 1985 paper "Arithmetic Transfinite Induction and Recursive Well-Orderings", Friedman and Ščedrov prove that the theory $\mathbf{ZFI}$ is conservative over $\mathbf{HA}^*$ (see here, Theorem 3.1). I am trying to understand the impact of this result for 'standard' intuitionistic set theory $\mathbf{IZF}$ (with this I mean the usual one-sorted first order theory based on intuitionistic logic).

The theory $\mathbf{ZFI}$ used in the above paper is formulated in a two-sorted language with the sorts being sets and natural numbers, the axioms are basically the standard axioms of Heyting arithmetic $\mathbf{HA}$ and intuitionistic set theory $\mathbf{IZF}$. The theory $\mathbf{HA}^*$ is obtained from usual Heyting arithmetic by adding an induction scheme for all primitive recursive binary relations on natural numbers.

My question is in what way this result transfers to normal intuitionistic set theory $\mathbf{IZF}$? For example, does it mean that the arithmetical statements that are provable in $\mathbf{IZF}$ are exactly those of $\mathbf{HA}^*$ when taking an arbitrary set theoretical coding for arithmetical statements?

In other papers of the authors I have seen one-sorted versions of what they call $\mathbf{ZFI}$ and those seem to be the same as $\mathbf{IZF}$, so is there even a difference between these two theories?

I am aware that these questions are quite vague as I haven't quite understood the result yet.

• If something in this area is hard to understand, I recommend starting with Michael Beeson's book instead. It may not have the particular results of this paper, but it's clear, comprehensive and well-organized for background and context. His summary of which set theories are conservative over HA is on p 321. – Matt F. May 1 '18 at 13:08