Induction and foundation in the theory of hereditarily finite sets (Q1330312)

An intuitionistic theory of hereditarily finite sets is developed here. A set of axioms is offered, with justification, from which most of the basic results you would want about HF are proven. Alternative axiomatizations are suggested, some of which are equivalent to the primary one, others of which are not. In particular, there are no fewer than nine versions of induction identified. There are intuitions and motivations throughout the paper, especially analogies between various theories of arithmetic (both classical and intuitionistic) and corresponding set theories, some of which have yet to be explored at all.