A formula of the form $\forall \vec{p}\, \exists x \, \forall y\, (y \in x \leftrightarrow \phi(y,\vec{p}))$

is to be named a "*set-building*" formula.

Now, when $\vec{p}$ includes a predicate symbol, then its to be called a second order set-building formula. Otherwise, it is first order. Also, by *defining part* in a set-building formula, I mean $\phi(y,\vec{p})$ in the above expression.

By *atomic* formula in the first order language of set theory, I mean single identity or membership formula, i.e. of the form $x \in y$ or $x=y$. While in the second order language it'll include as well formulas $P(x_1,\ldots,x_n)$ for any predicate symbol $P$.

The size of a formula is taken here to mean the number of its atomic subformulas. If a subformula have more than one occurrence, then each occurrence is counted as if it is a distinct formula.

Working in ${\sf ZF}-{\sf Reg.}+ {\sf HF} \text{ exists}$:

**Principle:** Any first or second order set-building formula $\phi$ in the language of set theory whose defining part is of size $\leq 4$, that is satisfied by the set $\sf HF$ of all hereditarily finite sets, then it is satisfied by the whole world of sets $V$.

Now, clearly all set-building axioms of $\sf ZFC$ would be derived from the above rule. Second order Replacement can be written by set-building formula as:

$$\forall P \, \forall a \, \exists x \, \forall y \, (y \in x \leftrightarrow \exists z \in a ( P(z,y) \land \forall u \, (P(z,u) \to u=y)))$$

If we include function symbols in second order atomic formulas, i.e., consider $F(x) \in y; F(x)=y$ as second order atomic formulas, then one can even get a short formalization of Replacement as:

$$\forall F \, \forall a \, \exists x \, \forall y \, (y \in x \leftrightarrow \exists z \in a: F(z)= y )$$

Making all set-building rules of $\sf ZFC$ derivable using the above principle with defining parts of length $\leq 2$.

Now, the shortest expression of finiteness that I know of is the one written by Emil Jeřábek, which is: $$\neg\exists y\,(x\in y\land\forall a\in y\,\exists b\in y\,b\subsetneq a), $$ of size $6$.

if we increase the limit on the size of the defining part in the above principle to $5$ or even $6$. Does this give a clear inconsistency?

Even more daunting (but I think most likely inconsistent) is to say that every first or second order sentence of size $\leq 5$ true of the hereditarily finite set world, does generalize over the whole set world. All axioms of ${\sf ZFC}-{\sf Reg.}$ other than Infinity, are instances of these sentences.

The intuitive idea behind this principle is that very short expressions in the first or second order language of set theory that can define sets and hold over the whole hereditarily finite set world, then the reason for them holding over the entirety of that world has nothing to do with finiteness, it is because they are general set principles! The reason is that they are too short to express finiteness, and so they are reasoned not to be a property of it, so they can go beyond it, and so we can restrict our scope of infinite set world to those infinite sets who obey those rules, since they can in some sense be regarded as close to the strict finite set realm.