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).