# Regularity in finitist models?

I understand there are various definitions of "finitist," so I'll be clear: by "finitist," I mean that any collection not finite is treated as a proper class. That is to say, such collections "exist" in the sense they can be discussed as a whole, but not in the sense that they might be manipulated as sets are. Every natural number exists, but the natural numbers do not; only definable reals exist, the notion of "definable real" eclipsed by that of "definition." Statements may be made about these definitions in general, so long as it's recognized that they comprise a proper class.

For simplicity's sake, let's restrict ourselves to the universe that makes use of the axioms of ZF bar infinity, plus the axiom of null set (to ensure the universe not be empty), and one of finiteness - let's say Tarski finiteness since it's easiest to break down. (If true for all sets, this implies choice, and therefrom Dedekind finiteness and bijection to a Von Neumann natural.)

So whereas I know this implies choice, my question is, what about regularity? My first instinct is that regularity is only made necessary by the notion of infinite sets, but when I sit down and try to work it out, I get nowhere. I can show that a set violating regularity would mean a cycle of membership, but that might not be impossible. Does anyone know if there's either a proof of regularity from the other axioms of this model, or a proof that they're independent? Any tidbits about other finitist models?

• Can you define what is a definable real, please? – Asaf Karagila Feb 27 '18 at 7:18
• Also, math.stackexchange.com/questions/282865/… may or may not have an answer to your question. – Asaf Karagila Feb 27 '18 at 7:20
• Do you know how to show that regularity is independent from the other axioms of ZFC? The usual idea to build a model where "sets" are certain directed graphs, as described here. If you take a model $M$ of your finitist set theory, and consider the class of finite accessible pointed directed graphs in $M$, you'll get a model of your finitist set theory and the negation of regularity (it's not hard to check that every finite accessible pointed directed graph satisfies the definition of Tarski-finiteness). – Alex Kruckman Feb 27 '18 at 14:48