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

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?

• What do you mean by the "Define" axiom? Is it merely the empty set axiom, or something else? Jun 9 at 8:56
• @YairHayut It’s not an axiom at all, but a definition of comprehension terms as a shorthand notation. It just explains what “$x=\{y\mid\dots\}$” means in the next two axioms. Jun 9 at 9:06
• @YairHayut, Yes! I think you are right. I need to add an axiom against this. Thanks! Jun 9 at 11:33

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.
• there is a problem about the $\sf HC$ since its cardinality is not determined in $\sf ZF$? So if all models are isomorphic then what is their cardinality? Is it $\omega_1$? Jun 12 at 15:10
• @ZuhairAl-Johar That doesn't affect this answer. Different models of $\mathsf{ZF(C)}$ disagree about the properties of $\mathsf{HC}$. However, this doesn't affect the fact that $\mathsf{ZF}$ proves "Every model of your theory is isomorphic to $\mathsf{HC}$." Think by analogy about how different models of $\mathsf{ZF}$ disagree over the properties of the real numbers, but the second-order theory of the reals is still $\mathsf{ZF}$-provably categorical. Jun 12 at 15:19