In "Mathematical Logic" second edition written by H-D Ebbinghaus, J.Flum and W.Thomas, in chapter 9 "Extensions of First-Order Logic", page 140, in the prooof of theorem 1.5 (The Lowenheim-Skolem theorem does not hold for $\mathfrak{L}_{II}$, there's a sentence saying "To define $\varphi_{unc}$ we use an $L_{II}^{\emptyset}$-formula $\psi_{fin}(X)$, similar to $\varphi_{fin}$, with just one free unary relation variable $X$, for which $(\mathfrak{A},\gamma)\models\psi_{fin}(X)$ iff $\gamma(X)$ is finite."
Right after that sentence there's a note saying "We leave it to the reader to write down such a formula.".
Does anyone know how to write down such a formula? I have no clue.
Let $S$ be a symbol set, that is, a set of relation symbols, function symbols and constants. The alphabet of $L_{II}^S$ contains, in addition to the symbols of $L^S$, for each $n\geq1$ countably many $n$-ary relation variables $V_0^n,V_1^n,V_2^n,...$.
To denote relation variables we use letters $X,Y,...$, where we indicate the arity by superscripts, if necessary. We define the set $L_{II}^S$ of second-order $S$-formulas to be the set generated by the rules of the calculus for first-order furnulas extended by the following two rules:
1. if $X$ is an $n$-ary relation variable and $t_1,\ldots,t_n$ are $S$-terms, then $Xt_1 \ldots t_n$ is an $S$-formula.
2. If $\varphi$ is an $S$-formula and $X$ is a relation variable, then $\exists X\varphi$ is an $S$-formula.
In order to be clearer, my question is part of the following proof of the follwoing theorem:
"Theorem: The Lowenheim-Skolem theorem does not hold for $\mathfrak{L}_{II}$.
proof: We give a setence $\varphi \in L^\emptyset_{II}$ such that for all structures $\mathfrak{A}$, $\mathfrak{A}\models \varphi_{unc}$ iff $A$ is uncountable.
Then $\varphi_{unc}$ is satisfiable but it has no model that is at most countable.
To define $\varphi_{unc}$ we use an $L^\emptyset_{II}$-formula $\psi_{fin}(X)$, similar to $\varphi_{fin}$, with just one free unary relation variable $X$, for which
$(\mathfrak{A},\gamma)\models \psi_{fin}(X)$ iff $\gamma (X)$ is finite.
(We leave it to the reader to write down such a formula.)"
To say that the domain is uncountable, you can say:
Any full model that satisfies that sentence must have an uncountable domain. The key point is that if the domain were countable, then there would be bijections between all infinite subsets of the domain - and then, since the model is a full model, these bijections would all be in the model.
So all that remains is to write the quoted phrase as a sentence of second order logic. The only symbol that has to be in the signature is $=$, actually; no other non-logical vocabulary is needed.
If the version of second-order logic you are using allows for directly quantifying over functions, as well as subsets, then the sentence is relatively straightforward to write.
If the logic only allows for quantifying over finitary relations, then you have to use a binary relation instead of a function, and include in the sentence an additional clause to make the binary relation be the graph of a function.
This method can be extend quite a bit. For example, you can write a sentence so that any full model has cardinality at least $\aleph_2$, or $\aleph_8$, etc. You can also write a sentence so that any full model has cardinality at least $\aleph_\omega$, with a little more work.
By taking the negations of these sentences, you can find sentences whose only full models are countably infinite, or have cardinality exactly $\aleph_7$, etc. This is all related to the Lowenheim number of full second-order logic, which is enormous.