This comes in continuation to posting titled "Can Foundation be captured for some $\mathcal L_{\omega_1, \omega}$ theories?".

Here, an attempt at a stronger notion of Foundation, yet residing in the same language $\mathcal L_{\omega_1, \omega}$, is contemplated:

For any formula $\phi $; for any non-strict well ordering $R$ on the universe; define:

$[y=\min^R z:\phi(z)] \iff [\phi(y) \land \forall z (\phi(z) \to y \ R \ z)]$

It's clear that if $R$ exists, then we have:

$(\exists y: \phi ) \to (\exists y: y =\min^R z: \phi(z))$

Now $\sf ZF + Def$ proves $\sf V=HOD$ so it proves existence of a non-strict well ordering $\leqslant$ over the universe. Now we define:

$\textbf{Define: } y \in^\leqslant x \iff y= \min^\leqslant z: z \in x \\\textbf{Define: } y \in^\leqslant_\phi x \iff y= \min^\leqslant z: [z\in x \land \phi(z)]$

In English, $y \in^\leqslant x$ reads: $y$ is the minimal element of $x$, with respect to $\leqslant$; while $y \in^\leqslant_\phi x$ reads: $y$ is the minimal element of $x$ satisfying $\phi$, with respect to $\leqslant$.

$\textbf{Foundation scheme: }$if $\phi_0,\phi_1,\phi_2,..$ is a decidable set of formulas in $\mathcal L_{\omega_1,\omega}$, then: $ \\\bigwedge _{j \in \omega} \\ \forall x\!: \neg [\bigwedge_{n \in \omega} (\exists v_0,..,\exists v_n: \bigwedge_{i \in n}( v_{i+1} \in^\leqslant_{\phi_j} v_i) \land v_0 \in^\leqslant_{\phi_j} x)]$

Is $\sf ZF + Def + Foundation \ scheme$ consistent?

How does this Foundation schema compare (on top of ZF+Def) with the single Foundation axiom presented in the earlier posting linked above.