Working in $\mathcal L\_{\omega\_1, \omega}$, can Foundation be captured?


My idea is to formalize a theory where all of its models are the well founded pointwise definable models of $\sf ZFC$. I attempt to formalize it as:


$\textbf{Foundation: } \\\forall x: \neg [ \bigwedge\_{n \in \omega} (\exists v\_0,..,\exists v\_n: \bigwedge\_{i \in n} (v\_{i+1} \in v\_i) \land v\_0 \in x)] $


In English: for every set $x$ it is not the case that for every finite size there is a descending membership set from $x$ of that size.


This way all sets would be truly well founded.


So we add all axioms of $\sf ZF$ written as usual in $\mathcal L\_{\omega,\omega}$, and finally add the definability axiom written in $\mathcal L\_{\omega\_1, \omega}$, which is:


$\textbf{ Axiom of Definability: } \forall x D(x)$,


Where "$D$" is defined as:


$$Dx \iff \bigvee x= \{ y \mid \Phi \}$$


where $\Phi$ range over all formulas in $\mathcal L\_{\omega, \omega}$ in which only the symbol "$y$" occurs free, and the symbol "$y$" never occurs bound.



> 
> Are all models of this theory well founded!
> 
> 
> 


If that works, then we have all models of this theory countable, all pointwise definable, and all are well founded. And I think that all ought to be arithmetically sound.



> 
> But, do all models of this theory prove exactly the same $\mathcal L\_{\omega, \omega}$ set theoretic sentences.
> 
> 
> 


My point is that every set theoretic sentence in $\mathcal L\_{\omega, \omega}$ can be written arithmetically, then if this theory captures standard arithmetic, then it cannot prove opposing arithmetical sentences.



Can Foundation be captured in $\mathcal L(\omega_1,\omega)$?
Your Foundation axiom does not assert that there is no infinite descending sequence, but rather merely rules out sets at infinite set-theoretic rank. For example, if $x=\omega$, then we can find for every $n$ a descending $\in$ sequence of length $n$.


You can formulate well-foundedness in $L\_{\omega\_1,\omega\_1}$ by saying directly that there is no infinite $\in$-descending sequence. But this is not possible in $L\_{\omega\_1,\omega}$, by a result due to Morley.


