ω-Models of finite set theory

Finite set theory, here denoted ZFfin, is the theory obtained by replacing the axiom of infinity by its negation in the usual axiomatization of ZF (Zermelo-Fraenkel set theory). An ω-model of ZFfin is a model in which every set has at most finitely many elements (as viewed externally). Mancini and Zambella (2001) employed the Bernays-Rieger method of permutations to construct a recursive ω-model of ZFfin that is nonstandard (i.e., not isomorphic to the hereditarily finite sets Vω). In this paper we initiate the metamathematical investigation of ω-models of ZFfin. In particular, we present a new method for building ω-models of ZFfin that leads to a perspicuous construction of recursive nonstandard ω-model of ZFfin without the use of permutations. Furthermore, we show that every recursive model of ZFfin is an ω-model