Finiteness axioms on fragments of intuitionistic set theory (Q2425348)

This paper solves some problems stated in the article ``Induction and foundation in the theory of hereditarily finite sets'' by \textit{F. Previale} [Arch. Math. Logic 33, 213--241 (1994; Zbl 0810.03048)]. Namely, it is shown that (i) in a suitable intuitionistic version \(\text{ZFC}^{\text{Int}}- \text{Inf}\) of Zermelo-Fraenkel set theory with the Axiom of Choice and deprived of the Axiom of Infinity, the statements \(V \subseteq \text{Fin}\) (every set is finite) and \(\text{Ord} \subseteq \text{Nat}\) (every ordinal is a natural number) are equivalent, and (ii) Previale's intuitionistic theory HS of hereditarily finite sets is equivalent to \(\text{ZFC}^{\text{Int}}- \text{Inf}+ V\subseteq \text{Fin}\) (and thus also to \(\text{ZFC}^{\text{Int}}- \text{Inf}+ \text{Ord}\subseteq \text{Nat}\)).