This posting is a continuation to an earlier one titled "Can Foundation be captured in $\mathcal L_{\omega_1, \omega}$ ?"

It appears that capturing foundation is problematic at every $\mathcal L_{\alpha, \omega}$ and even at $\mathcal L_{ \infty, \omega}$. [see this and comments below it]

However, can there be particular cases where this fails? I mean where we can capture Foundation for some particular $\mathcal L_{\omega_1, \omega}$ theory.

I'm specifically referring to the theory $\sf ZF + Def$. This theory has all of its models being exactly the pointwise definable models of $\sf ZF$.[Hamkins]

So, it proves $\sf V=HOD$, and accordingly there is a finitary formula $\phi$ in two free variables that defines a binary relation $\leqslant$ that well orders the universe. Now can we use this feature to capture Foundation?

$\textbf{Define: } x \in^{\leqslant} y \iff x \in y \land \forall m \in y \, ( x \leqslant m )$

That is, $x$ is the element of $y$ of the least order according to $\leqslant$.

Now, we define:

$ \textbf{Define: } y \in^\leqslant_K x \iff y \in^\leqslant x \cap K $

Where, as usual: $ x \cap K =\{y \mid y \in x \land y \in K\}$

$\textbf{Foundation: } \forall K \forall x:\\ \neg [ \bigwedge_{n \in \omega} (\exists v_0,..,\exists v_n: \bigwedge_{i \in n} (v_{i+1} \in^\leqslant_K v_i) \land v_0 \in^\leqslant_K x)] $

Now, the idea is that if there exists a nonempty set $K$ such that every element of $K$ has an element of it that is an element of $K$, then there would exist $x \in K$ that violates Foundation.

Would that succeed in capturing Foundation, thereby rendering all models of the resulting theory well founded?