Constructive Ackermann's interpretation

Abstract

The main goal of this paper is to formulate a constructive analogue of Ackermann's observation about finite set theory and arithmetic. We will see that Heyting arithmetic is bi-interpretable with $\mathsf{CZ}{\mathsf{F}}^{\mathsf{fin}}$, the finitary version of $\mathsf{CZF}$. We also examine bi-interpretability between subtheories of finitary $\mathsf{CZF}$ and Heyting arithmetic based on the modification of Fleischmann's hierarchy of formulas, and the set of hereditarily finite sets over $\mathsf{CZF}$, which turns out to be a model of $\mathsf{CZ}{\mathsf{F}}^{\mathsf{fin}}$ but not a model of finitary $\mathsf{IZF}$.

arXiv comment16 pages