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