Abstract

The paper contains an axiomatic treatment of the intuitionistic theory of hereditarily finite sets, based on an induction axiom-schema and a finite set of single axioms. The main feature of the principle of induction used (due to Givant and Tarski) is that it incorporates Foundation. On the analogy of what is done in Arithmetic, in the axiomatic system selected the transitive closure of the membership relation is taken as a primitive notion, so as to permit an immediate adaptation of the theory to cases of restricted induction (in particular primitive recursive induction). At the end of the paper several different forms of induction, which play an important role in the development of the theory, are compared. An alternative axiomatization of the theory, which is of intrinsic interest, is also discussed