Informally the idea of this question is about whether the rules of set theory can be derived as a transfer of some rules from the hereditarily finite set realm, and whether this transfer principle itself can be coined for notions other than the "finite" notion?

The principle I want to negotiate is: "if $\phi$ is a property that is definable by a formula in the language of set theory that is strictly shorter than the least formula in that language that can express 'finiteness', then if $\phi$ is CLOSED on the the hereditarily finite set world, then it can be generalized over the whole realm of sets.

The crude informal idea is that if a property that cannot mention finiteness generalizes over the whole hereditarily finite set realm, then it can go beyond it.

To formally capture that, I'll work up in a class theory, so we define "set" as an element of a class, the language of the theory is mono-sorted first order logic with identity and membership, we stipulate axioms of:

1. Extensionality: as in ZF
2. Class comprehension schema: as in Morse-Kelley
3. The empty class is a set
4. Singletons: $\forall x [ set(x) \to set(\{x\})]$
5. Boolean Union: $\forall x,y [set(x) \wedge set(y) \to set (x \cup y)]$

Define: $ fin(A) \iff \forall K ([\forall x (x \in A \to \exists y (y \in K \wedge x \in y \wedge \forall z (z \in y \to z=x))) \wedge \\ \forall a,b (a \in K \wedge b \in K \to \exists c (c \in K \wedge \forall d (d \in a \lor d \in b\to d \in c))) ] \to A \in K)$

In English: $A$ is finite if and only if it is an element of every class $K$ that is closed under Boolean union and that has the singletons of all elements of $A$ among its elements.

"I think this is along the shortest way to define "finite set" in the first order language of set theory, only taking 79 symbols"

Perhaps the above formula can be shortened further, or perhaps there is another shorter formulation of "x is a finite set" in the language of set theory, however for the sake of presentation here we'll take 79 to be the length of the shortest formula defining finiteness.

6. $ \forall x (x \text{ is hereditarily finite } \to set(x))$

Where "x is hereditarily finite" is defined as x being finite and every element of the transitive closure of x being finite.

We shall denote the class of all sets by $V$, and the class of all hereditarily fintie sets by $HF$

7. $HF \in V$

8. The principle of Transfer from the pure finite world: if $\phi(y,x)$ is a formula composed of less than 79 individual symbols, in which only symbols $``y,x"$ occur free, and those only occur free, then:

$\forall x [HF(x) \to \forall y (\phi(y,x) \to HF(y))] \to \forall x \in V [ \forall y (\phi(y,x) \to y \in V)]$

Now it is clear that all axioms of Union, Power and Separation over sets are derivable from the above transfer principle, and so $ZC$ is interpretable here. Actaully if we restrict $\phi$ to have no more that three atomic subformulas, we can still interpret the whole of $ZC$. Replacement is not interpretable by this principle. Yet, a minor modification of this principle might succeed in proving replacement over sets, this can be done by changing the closure property to involve only subsets of $HF$, what I call as "proximity closure over HF", so to restate that:

8'.The principle of Transfer from proximity of the pure finite world: if $\phi(y,x)$ is a formula composed of less than 79 individual symbols, in which only symbols $``y,x"$ occur free, and those only occur free, then:

$\forall x [HF(x) \to \forall y \subseteq HF (\phi(y,x) \to HF(y))] \to \forall x \in V [ \forall y (\phi(y,x) \to y \in V)]$

That replacement is provable can be shown from examining the following formula whose length is shorter than 79:

$\exists F [\forall m (m \in F \to \exists a,b (a \in A \wedge b \in B \wedge a \in m \wedge b \in m)) \wedge \\ \forall m,n (m \in F \wedge n \in F \wedge \exists k(k \in m \wedge k \in n) \to n=m)]$

Now if $A$ is hereditarily finite and $B$ is a subset of $HF$ that fulfills the above formula, then $B$ is hereditarily finite, this mean that the property defined by the above formula is "proximity closed over the hereditarily finite world"

I don't have any proof of consistency of these principles, but if there is no clear inconsistency of those relative to $ZF$ or $MK$ or some extension of those, then could it be possible to think of extending that principle to properties other than "x is finite"? so we generalize it to any property $P$, that is:

any predicate $Q$ that is closed over the pure $P$ world, would generalize over the whole set world,

or even stronger:

any predicate $Q$ that is proximity closed over the pure $P$ world, would generalize over the whole set world

Of course in both cases $Q$ must be expressible by a formula strictly shorter than the shortest expression defining property $P$.

is that possible or it is involved with clear inconsistencies?