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 shortest parameter free formula in that language that can define '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: $\forall x_1,..,x_n\ \exists x \ [x=\{y|set(y) \wedge \phi(y,x_1,..,x_n)\}] $
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 [\exists o (o \in K \wedge \neg \exists m (m \in o)) \wedge \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 \forall b (a \in K \wedge b \in K \to \exists c (c \in K \wedge \forall d (d \in c\leftrightarrow d \in a \lor d \in b ))) \\ \to A \in K]$$

In English: $A$ is finite if and only if it is an element of every class $K$ that contains the empty set among its elements, 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 this axiomatic theory whose language is first order logic with membership and equality using the customary four logical connectives.

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

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

Where "x is hereditarily finite" is defined as the transitive closure class of x being finite [Another definition is that x is finite and every element of the transitive closure of x is finite also].

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 shorter than any formula defining finiteness, in which only symbols $``y,x"$ occur free, and those only occur free, then:

$\forall x [x \in HF \to \forall y (\phi(y,x) \to y \in HF)] \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 than three atomic subformulas, so the principle would be written as:

8'. The principle of ternary Transfer from the pure finite world: if $\phi(y,x)$ is a formula having no more than three occurrences of atomic formulas in it, in which only symbols $``y,x"$ occur free, and those only occur free, then:

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

THEN this would still be enough to interpret the whole of $ZC$! Moreover I think that the theory with this ternary version of the transfer principle can be proven to be consistent relative to $ZFC$.

Replacement is not interpretable by the above two principles. 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 shorter than any formula defining finiteness, in which only symbols $``y,x"$ occur free, and those only occur free, then:

$\forall x [x \in HF \to \forall y \subseteq HF (\phi(y,x) \to y \in HF)] \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 any formula defining finiteness.

$\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) \wedge \\ \forall b (b \in B \to \exists m (m \in F \wedge b \in 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 some line properties, so for a property $P$ in that line, we stipulate that:

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$, and also we stipulate parallel axioms sufficient to define the property $P$, also axioms asserting the element-hood of all hereditarily $P$ classes, and the existence of a set of all hereditarily $P$ sets. Of course this can only be done for some selected line of properties.

is that possible or it is involved with clear inconsistencies? and what would be the general qualification of such property $P$?

After-note: I have shorter definitions of finiteness and of subnumerousity, than the ones given here, those are:

Define: class $B$ is subnumerous to class $A$ if and only if:

$$\exists F \large{(} \normalsize \forall b [b \in B \to \exists a \exists f (a \in A \wedge f \in F \wedge b \in f \wedge a \in f \wedge \forall x (x \in f \to x=a \lor x=b))] \wedge \forall a [a \in A \to \exists z \forall m (m \in F \wedge a \in m \to m=z)] \large {)}$$

I think this can be further shortened to:

$$ \exists F [\forall b (b \in B \to \exists a (a \in A \wedge \exists f (f \in F \wedge a \in f \wedge b \in f \wedge \forall h (h \in F \wedge a \in h \to h=f))))]$$

Define: class $a$ is said to be $finite$ iff: \begin{align} \forall k [&\exists m (m \in k)\\ &\land \forall x \forall y (x \in a \lor y \in k \to \forall z (\forall n (n \in z \to n=x \lor n \in y ) \to z \in k)) \\ & \to a \in k] \end{align}