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.
Best Answer
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.