2
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ What do you mean by the "Define" axiom? Is it merely the empty set axiom, or something else? $\endgroup$
    – Yair Hayut
    Jun 9, 2023 at 8:56
  • 2
    $\begingroup$ @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. $\endgroup$ Jun 9, 2023 at 9:06
  • $\begingroup$ @YairHayut, Yes! I think you are right. I need to add an axiom against this. Thanks! $\endgroup$ Jun 9, 2023 at 11:33

1 Answer 1

8
$\begingroup$

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.

$\endgroup$
4
  • 4
    $\begingroup$ One very minor caveat: This theory also admits the empty model (since all its axioms are universals), unless you set up your logic to preclude the empty model entirely. $\endgroup$ Jun 9, 2023 at 8:05
  • $\begingroup$ @PeterLeFanuLumsdaine, yes the underlying logic does presume the existence of at least one object. $\endgroup$ Jun 9, 2023 at 11:29
  • $\begingroup$ 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$? $\endgroup$ Jun 12, 2023 at 15:10
  • $\begingroup$ @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. $\endgroup$ Jun 12, 2023 at 15:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.