How would you express, in ZFC, that the number of countable models of Th($\mathbb{N}$), up to isomorphism, is at most $2^{\aleph_0}$? Intuitively, it is clear to me why, up to isomorphism, there are at most $2^{\aleph_0}$ non-isomorphic models of Th($\mathbb{N}$): I can choose as "representative" of any countable model $\mathfrak{A}$ of Th($\mathbb{N}$) a model $\mathfrak{N}$ such that its universe is $\mathbb{N}$ and such thath $\mathfrak{A}$ and $\mathfrak{N}$ are isomorphic, using the bijection between |$\mathfrak{A}$| and $\mathbb{N}$. We can then observe, by easy cardinality considerations, that the number of countable models of Th($\mathbb{N}$) that have as universe $\mathbb{N}$ is, at most, $2^{\aleph_0}$.
Well, now, if I want to formalize in ZFC this argument, how should I proceed? In particular, how can I just express in ZFC something like " up to isomorphism, there are at most $2^{\aleph_0}$ countable models of Th($\mathbb{N}$)", wich is the claim of the theorem ? What we are saying is that, up to isomophism, the cardinality of the set of countable models of Th($\mathbb{N}$) is at most $2^{\aleph_0}$. But I cannot get (1) how to express "up to isomorphism" and (2) how to refer to the object "the set of countable models of Th($\mathbb{N}$)", because that's a proper class. Clearly, (1) e (2) are linked, and I think that the solution is to find the right expression in ZFC and resolve them togheter.
The best thing that I could find is this:
ZFC $\vdash$ [$\forall\mathfrak{A}$ $\forall\mathfrak{B}$[($\mathfrak{A}\ and\ \mathfrak{B}\ are\ isomorphic\ models\ of\ Th(\mathbb{N})$)$\rightarrow\ \mathfrak{A}=\mathfrak{B} $]]
$\rightarrow \exists A(A$ is the set of countable models of $Th(\mathbb{N})$ and $|A|\ \leq 2^{\aleph_0})$
Any improvements or suggestions?
 A: Here is one way to express this in the language of set theory: There is a set $X$ of cardinality $2^{\aleph_0}$ such that for every $\mathfrak{A}$, if $\mathfrak{A}$ is a countable model of $\mathrm{Th}(\mathbb{N})$, then there exists $\mathfrak{B}\in X$ such that $A\cong \mathfrak{B}$.
Of course, this is a natural language abbreviation for the sentence in question. If it's not clear to you how to write this in the first-order syntax, I can expand on it.
Why does this formalize the natural language statement "there are at most $2^{\aleph_0}$ non-isomorphic countable models of $\mathrm{Th}(\mathbb{N})$"? Well, letting $C$ be the class of countable models of $\mathrm{Th}(\mathbb{N})$, we can pick a well-ordering of $X$ anad define a class function $F\colon C\to X$ by mapping $\mathfrak{A}$ to the least $\mathfrak{B}\in X$ such that $\mathfrak{A}\cong \mathfrak{B}$. Then $F$ respects isomorphism, so it descends to an injective function $C/{\cong} \hookrightarrow X$, demonstrating that $|C/{\cong}|\leq 2^{\aleph_0}$.
From this formulation, it's even clear how to go about proving the statement: just let $X$ be the set of all structures in the language of arithmetic with domain $\omega$.
The language of ZFC doesn't allow us to talk directly about classes (and in particular, we can't quantify over class functions), so we have to do this kind of translation of statements about classes into equivalent formulations just about sets in order to formalize them.

The sentence you wrote has lots of problems:

$$[\forall\mathfrak{A}\, \forall\mathfrak{B}\, [(\mathfrak{A}\text{ and } \mathfrak{B}\text{ are isomorphic models of }\mathrm{Th}(\mathbb{N}))\rightarrow \mathfrak{A}=\mathfrak{B}]]\rightarrow \\\exists A\,(A \text{ is the set of countable models of }\mathrm{Th}(\mathbb{N})\text{ and }|A| \leq 2^{\aleph_0}).$$

Both the antecedent and the consequent of the implication are false:

*

*ZFC proves that there exist $\mathfrak{A}$ and $\mathfrak{B}$ models of $\mathrm{Th}(\mathbb{N})$ such that $\mathfrak{A}\neq \mathfrak{B}$.

*ZFC proves that the class of countable models of $\mathrm{Th}(\mathbb{N})$ is a proper class, so there does not exist a set $A$ which is the set of all countable models of $\mathrm{Th}(\mathbb{N})$, much less one of size $\leq 2^{\aleph_0}$.

So ZFC does prove the sentence you wrote down (by propositional logic - the statement is vacuously true). But this theorem is basically meaningless.
A: Let me add a very minor result which provides a methodological coda to Alex Kruckman's answer.
There is a natural theory I'll call "$\mathsf{NBG}^{hyper}$" (basically a boring repackaging of $\mathsf{NBG}$) which, unlike $\mathsf{ZFC}$ itself, can very straightforwardly talk about collections of classes and so within which "$T$ has continuum-many isomorphism types of countable models" can be expressed naively, as "There is a hyperclass bijection between the set $\mathbb{R}$ and the hyperclass of isomorphism classes of countable models of $T$." Let's call this statement $\star_T$.
This much is boring. Things get interesting, though, when we look at how $\mathsf{NBG}^{hyper}$ interfaces with $\mathsf{ZFC}$. There are two key points:

*

*$\mathsf{NBG}^{hyper}$ is a conservative extension of $\mathsf{ZFC}$ (in the stronger, model-theoretic sense, even!).


*$\mathsf{NBG}^{hyper}$ proves the following: "For every theory $T$ we have $\star_T\leftrightarrow \mathbb{A}_T$," where $\mathbb{A}_T$ is the "sets-only" formulation of "$T$ has continuum-many countable models" given in Alex's answer.
Together this says that our extra-theoretic decision to construe $\mathbb{A}_T$ as a faithful "$\mathsf{ZFC}$-ification" of the a-priori-hyperclass-referencing statement "$T$ has continuum-many countable models" is actually justified - in a precise sense it will never lead us to false conclusions. While probably not very illuminating in this specific case, I think that understanding this sort of analysis will increase one's confidence in our reflexive implementations of various ideas in set theory.
(Finally, we note that in particular it's easy to prove $\mathbb{A}_{Th(\mathbb{N})}$ inside $\mathsf{ZFC}$ per Alex's answer.)
