This posting is a continuation to an earlier one titled "[Can Foundation be captured in $\mathcal L\_{\omega\_1, \omega}$ ?](https://mathoverflow.net/questions/448486/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](https://mathoverflow.net/a/448488/95347) 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$](https://mathoverflow.net/questions/448369/does-adding-definability-axiom-expressed-in-infinitary-language-to-zf-let-all-m). This theory has all of its models being exactly the pointwise definable models of $\sf ZF$.[[Hamkins](https://mathoverflow.net/a/448434/95347)]


So, [it proves $\sf V=HOD$](https://mathoverflow.net/questions/448130/are-all-constructible-from-below-sets-parameter-free-definable/448132#448132), 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?
> 
> 
> 



Can Foundation be captured for some $\mathcal L_{\omega_1, \omega}$ theories?

> 
> **Lemma.** A model of ZF satisfies the “Foundation” axiom if and only if it is an $\omega$-model, i.e., iff it satisfies the simpler $\mathcal L\_{\omega\_1,\omega}$-sentence $\forall x\in\omega\,\bigvee\_{n\in\omega}x=n$.
> 
> 
> 


**Proof:**


Right-to-left: Working inside the model, given $x$ and $K$, define by recursion a partial function $f\colon\omega\to K$ such that $f(0)=x$ and if $f(n)$ is defined and intersects $K$, then $f(n+1)$ is the $\le$-least element of $f(n)\cap K$. If $f$ is total, then $\{f(n):n\in\omega\}$ contradicts the usual axiom of foundation of ZF. Thus, let $n\in\omega$ be minimal such that $f(n)$ is undefined. Assuming $n$ is standard, we have $\neg\exists v\_0,\dots,v\_n \cdots$ as in the axiom of “Foundation”.


Left-to-right: Define by recursion a function $f\colon\omega\to V$ such that $f(0)=0$ (say) and $f(n+1)=\{f(n)\}$. Let $K=\{f(n):n\in\omega\}$, and $x=f(n)$ for a fixed nonstandard $n\in\omega$. Then “Foundation” fails for $K$ and $x$.



> 
> **Corollary.** The following are equivalent (provably in ZF):
> 
> 
> 1. Your theory is consistent.
> 2. ZF (or ZFC) has an $\omega$-model.
> 3. The closure of ZF (or ZFC) under the $\omega$-rule is consistent.
> 
> 
> 


**Proof:** The equivalence of 2 and 3 holds for arbitrary countable FO theories by a well-known consequence of the omitting types theorem. Clearly, 1 implies 2 by the Lemma. On the other hand, if $M$ is an $\omega$-model of ZF, then $L^M$ is an $\omega$-model of ZF + V=L, and the set of parameter-free definable elements of $L^M$ is its elementary submodel, thus an $\omega$-model of ZF + Def.



> 
> **Corollary:** If the theory is consistent, then it has a non-well-founded model.
> 
> 
> 


**Proof:** Assume the theory has a model. If it is not well founded, we are done, thus we may assume there exists a well-founded model of ZF. It follows that there exists a least ordinal $\alpha$ such that $L\_\alpha$ is a model of ZF. Now, $L\_\alpha$ satisfies “the closure of ZF under the $\omega$-rule is consistent”, as the closure as computed in $L\_\alpha$ is included in the true closure. Thus, there exists $M\in L\_\alpha$ such that $L\_\alpha$ satisfies “$M$ is a point-wise definable $\omega$-model of ZF”. Since $L\_\alpha$ is itself a transitive model of ZF, $M$ really is a point-wise definable $\omega$-model of ZF, i.e., a model of your theory. But since $M\in L\_\alpha$, $M$ cannot be well founded by the minimality of $\alpha$.


