Constructive Ackermann's interpretation

TL;DR

This paper develops a constructive analogue of Ackermann's observation, showing bi-interpretability between Heyting arithmetic and a finitary version of constructive set theory, with implications for models of these theories.

Contribution

It introduces a constructive analogue of Ackermann's observation, establishing bi-interpretability between Heyting arithmetic and finitary constructive set theory, and analyzes models based on hereditarily finite sets.

Findings

Heyting arithmetic is bi-interpretable with $ extsf{CZF}^{fin}$.

A model of $ extsf{CZF}^{fin}$ is constructed from hereditarily finite sets.

The model is not a model of finitary $ extsf{IZF}$.

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{CZF^{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{CZF^{fin}}$ but not a model of finitary $\mathsf{IZF}$.