ZFfin-formalization

Axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts on independence of an axiom from a system of axioms by defining appropriate models.