How do these two principles of Foundation written in $\mathcal L_{\omega_1,\omega}$ compare?

Question

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.

Answer 1

Your axiom schema is equivalent to being an $\omega$-model.

Working inside an $\omega$-model, any counter example to your schema will be counter example of the axiom of foundation of ZFC, as you can use $\le$ and the given $\phi$ of the counter-example to construct the counter-example sequence, this sequence is of infinite length externally, but the model has the same finite numbers, so it is infinite internally as well.

Now assume the model is not an $\omega$-model, let $\phi(x)$ be $x=x$ and $X$ be a $k$-nested singleton where $k$ is some non standard natural, then $X, \phi$ will be a counter example to the schema as the sequence defined as $x_{i+1}=\min_\le\{x\in x_i\}, x_0=X$ won't stop in any standard step.