Is this theory of well founded countable sets formalized in infinitary logic, complete and categorical?

Question

Working in $\mathcal L_{\omega_1, \omega_1}$, add symbol $=$ with its axioms; add symbol $\in$ and axiomatize:

$\textbf{Extensionality: } \forall x \forall y : \forall z (z \in x \leftrightarrow z \in y) \to x=y$

$\textbf{Foundation: } (\forall v_n)_{n \in \omega} \, \exists x: \bigvee_{n \in \omega} (x=v_n) \land \bigwedge_{n \in \omega} (v_n \not \in x)$

$\textbf{Define: } x=\{y \mid \phi\} \equiv_{def} \forall y \, (y \in x \leftrightarrow \phi)$

$\textbf{Construction: } \\(\forall v_n)_{n \in \omega} \, \exists x : x=\{y \mid \bigvee_{n \in \omega} ( y=v_n)\}$

$ \textbf{Countability: } \\ \forall x \, (\exists v_n)_{n \in \omega} : x=\{y \mid y \neq v_0 \land \bigvee_{n \in \omega} ( y=v_n)\} $

$\textbf {Empty set: } \exists x \forall y: y \not \in x$.

Is this theory Complete?

Is this theory Categorical?

Answer 1

Yes, this is categorical and hence complete (with respect to any satisfactory notion of proof, that is). Specifically, I claim that any model $M$ of your theory is isomorphic to $\mathsf{HC}$, the set of hereditarily countable sets.

First, given $M$ we can construct recursively an embedding $i:\mathsf{HC}\rightarrow M$. (Note that this uses the "construction" axiom.) So we just need to show that $i$ is surjective. I think the cleanest way to do this is to note that the image of $i$ is $\mathcal{L}_{\omega_1,\omega_1}$-definable in $M$, as "$a\in im(i)$ iff there is a well-founded countably-branching tree such that, when we recursively label the nodes of $T$ by the sets of labels of their children, the root gets labelled with $a$." (In fact, since $M$ correctly computes well-foundedness and countability this is a first-order definition in $M$, but that doesn't matter.) Now every element of $M\setminus im(i)$ must consist only of elements of $M\setminus im(i)$, but this contradicts well-foundedness.

Note that the ability to characterize well-foudnedness makes $\mathcal{L}_{\omega_1,\omega_1}$ diverge wildly from the standard model-theoretic constraints we are used to for first-order logic or even $\mathcal{L}_{\omega_1,\omega}$. That said, the situation shouldn't be overstated: see S. Friedman's Model theory for $\mathcal{L}_{\infty\omega_1}$ for a discussion of what sort of "local" compactness phenomena (analogous to Barwise compactness) can still occur.