# Can Foundation be captured in $\mathcal L(\omega_1,\omega)$?

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.

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.
• More generally, well-foundedness is not expressible in $L_{\infty,\omega}$. Jun 9, 2023 at 9:02
• The problem of $L_{∞,ω}$ was asked by Mostowski, Lopez-Escobar solved it by first finding that the Hanf number of $L_{κ,ω}$ is less or equal to $\beth_{(2^{κ})^+}$, then assume $φ∈L_{κ^+,ω}$ express well-ordering (we can assume it is a single sentence, if we require a theory $T⊆L_{λ,ω}$ we can just take $κ=\max(|T|,λ)$ and let $φ$ be the conjunction of $T$) then they construct a (quite complicated) sentence $ψ∈L_{κ^+,ω}$ such that ordinals $(α,∈;...)$ does not satisfy $ψ$ if $α>\beth_{2^{2^{2^{κ}}}}$ but there exists $α≥\beth_{(2^{κ^+})^+}$ that satisfy this sentece
• @JoelDavidHamkins Perhaps another way to see this through Hanf numbers is by building indiscernibles. Morley's Omitting Types Theorem (which I recently learned is due to Chang in the uncountable case) says that if $\phi \in L_{\kappa, \omega}$ has models of size (cofinal in) $\beth_{(2^\kappa)^+}$, then it has arbitrarily large models. The proof goes by building a blueprint $\Phi$ that builds model $EM_\tau(T, \Phi)$ of $\phi$ with $I$ as indiscernibles. You can modify this to build the indiscernibles in whatever definable set you like (or more) as long as the definable set... Jun 13, 2023 at 19:18
• ...is sufficiently big. So take your hopefuly definition $\phi$, and we may as well make the well-ordered bit some predicate $(P, <)$. If $\phi$ has models were $(P, <)$ has size (cofinal in) the Hanf number, build a blueprint $\phi$ so the indiscernibles are in $P$. This will contradict the well-orderedness by, e.g., plugging in an I with lots of automorphisms. Jun 13, 2023 at 19:58