John Mayberry published what he calls a *Euclidean set theory* in his book The *Foundations of Mathematics in the Theory of Sets*. It is ZF with the axiom of infinity replaced by an axiom saying "the whole is always larger than the part." In other words every set is asserted to be Dedekind finite: no proper subset of $S$ is in bijection with $S$.

The hereditarily finite sets of ZF form a model of this set theory. But, besides that this set theory obviously does not give a set which models arithmetic, it has no minimal definable infinite sequence of sets. Every definable infinite sequence of sets has definable subsequences that also contain (the interpretant of) 0 and are closed under (the interpretation of) successor.

Is there a known description of which theories of arithmetic are interpretable in this set theory? Of course I mean a description in more conventional terms than just saying "the ones interpretable here."

For that matter, this theory obviously implies the theory ZF-inf which is just ZF with the negation of the usual ZF axiom of infinity. See Non-standard models of finite set theory

But is there a known more specific relation between these set theories?

These questions seem not to be answered in the book, but left as open questions (p. 387).