Can these short set-building expressions of the finite set world extend to the infinite set world?

Question

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.

Answer 1

There is a counter-example:

let $\phi(y)$ be the formula: $$\forall a \, (a \in y \to \forall b \, ( \forall z \, (z \in b \to z=a) \to b \in y)) $$, the set-building formula with this formula as its defining part, would define a set in $\sf HF$ which is $\{\varnothing\}$, but of course cannot be generalized to $V$. So, we need the size of the defining part to be $\leq 3$. However, this won't affect deriving the set-building rules of $\sf ZF-Reg.$ since its enough to have defining parts of size $\leq 2$

As regards the second question, the sentence: $$\forall a \neg \exists x \, :a \in x \land \forall y \in x \forall z (\forall u \in z(u=y) \to z \in x) $$, is true of $\sf HF$, but not true of $V$. So, we need to reduce the size of sentences to be $\leq 4$. However, this won't be enough to derive all axioms of $\sf ZF-Reg-Infinity$. A possible salvage is to allow formula sizes of $\leq 5$ but provided that the first order atomic formulas not exceeding $3$, this way we get to capture Separation as: $$\forall A \forall P \exists x: \forall y \, (y \in A \land P(y) \to y \in x) \land \forall y \, (y \in x \to P(y))$$, and the rest of axioms to be written in implicational form.

Of note, with these restrictions it appears that we can use $V_\omega$ instead of $\sf HF$ and thus maintain an approach that is consistent with Foundation, we need the defining parts of be of size $\leq 2$, and for sentences we need them to be of size $\leq 5$ but with the first order part of size $\leq 3$.

This renders this approach very narrow, that it can barely justify $\sf ZFC$. But, nevertheless, if it succeeds, then it speaks of a possible origin of familiarity of those axioms, thereby unravelling their natural genre, it shows that the roots of that lies in familiarity with rules of the strict finite set realm.