I was having this doubt regarding how countability is defined within ZF set theory, in particular in relation with the Skolem-Löwenheim downward and upward theorems. I know 'countability' for a set is often defined as the existence of a bijection between its elements and $\mathbb{N}$, but how is this expressed in the language of ZF set theory? How does one speak of 'bijections,' for example? My concerns regarding this are also in relation to Skolem's paradox: I 'understand' that countability as seen from outside and from inside a model is distinct, and that countable models of ZF can exist (by DSL) due to them (in very informal words) being so 'poor' as to 'miss out' on some actually-existing bijections outside the model (this is the explanation van Dalen provides in his Logic and Structure).
Now, the concerns which make me seek the in-model notion of countability are the following: One can, given an appropriate language (say a language of identity $\mathscr{L}$ of type $\langle0; \ 0; \ 0\rangle$), define statements $\lambda_n$ and $\mu_n$ to effectively account for finite cardinality of a model and verify whether it possesses 'at least $n$ elements' or 'at most $n$ elements' respectively. One can also verify that any model of $\lbrace \lambda_n : n \in \mathbb{N} \rbrace$ is infinite. Now, I do not know whether this is possible, but, depending on how one defines 'countability' (and 'uncountability') within ZF, could one write a statement analogous to $\lambda_n$ and $\mu_n$ to mean (outside the model) 'has $\aleph_0$ elements'? If so, I suppose that, say, $\mathbb{N}$ could model such a statement, but here is where my concern arises: According to USL, if our statement $\varphi$ (of outside-model meaning 'has $\aleph_0$ elements') was expressed in a language of cardinality $\kappa$, then, if there exists some model $\mathfrak{A} \in \text{Mod}(\varphi)$ of cardinality $\lambda \ge \kappa$, there must exist models of $\varphi$ of any cardinality $\mu \gt \lambda$.
Now, as the language $\varphi$ (in case of existing) would be expressed in would have cardinality $\ge \aleph_0$, and $\mathbb{N}$ as a (likely) model of $\varphi$ has cardinality $\aleph_0$, would this not mean, then, that there exist models of cardinality $\gt \aleph_0$ that model 'has $\aleph_0$ elements'? I suppose some possible, limiting facts would be that (a) $\varphi$ might not be expressable in the language of ZF (in which case, how are countability and uncountability defined inside ZF?), or (b) the language $\varphi$ is expressable in has cardinality $\gt \aleph_0$ (in which case no model of actual $\aleph_0$ cardinality would have the appropriate type to model it, i.e., it would have no models).
I thank in advance any responses or help in clarifying my confussions surrounding this much interesting topic.