How is uncountability characterized in second order logic? How is uncountability characterized in second order logic?
Also, why is this characterization of uncountability "absolute" in the way that FOL's characterization of uncountability is not?
A very direct answer will be much appreciated.
Much thanks.
 A: There are slightly faster ways to define countability and uncountability in second-order logic, using more knowledge of the ambient set theory to avoid having to refer to axioms of arithmetic. In particular we can use the fact that "countable" is the smallest infinite cardinality.  
First, a set $X$ is infinite if there is a function from that set to itself that is injective but not surjective. That can be expressed as a formula $\operatorname{Inf}(X)$ in second-order logic with only the equality relation, by quantifying over functions. Now a set $X$ is countably infinite if if is infinite and for every infinite subset $Y$ of $X$ there is a bijection from $Y$ to $X$. This can also be expressed as a formula of second order logic. Finally, a set is uncountable if it is infinite and not countable.
A: The definition of uncountability is essentially the same as it is in first order logic: a set $X$ is uncountable if there is no surjective function $F$ from the natural numbers $\mathbb{N}$ onto $X$ (there are other ways of formulating uncountability, but they are equivalent to this definition).
Consequently in order to provide a formal definition in second order logic we must first define the following: the set of natural numbers $\mathbb{N}$; functions and their properties in second order logic; and finally the definition of uncountability.

Let's start with functions. Let $F$ be a unary function symbol, and let the domain of $F$ be given as
$$
\mathrm{dom}(F) = \left\{ x : \exists{y} (F(x) = y) \right\}
$$
while the range of $F$ is
$$
\mathrm{ran}(F) = \left\{ y : \exists{x} (F(x) = y) \right\}.
$$
These sets exist via the second order comprehension scheme.

Now we characterise the natural numbers $\mathbb{N}$ in second order logic. Given a function symbol $S$ for the successor function and a constant symbol $0$, the natural numbers is the set satisfying the following axioms. By a theorem of Dedekind, this suffices to characterise the natural numbers up to isomorphism.
$$
\forall{x}(0 \neq S(x)) \\
\forall{n}\forall{m} (S(n) = S(m) \rightarrow n = m) \\
\forall{P} ( P(0) \wedge \forall{n} (P(n) \rightarrow P(S(n))) \rightarrow \forall{n} (P(n)).
$$

Finally we are in a position to present a definition of uncountability in second order logic. A set $X$ is countable just in case it satisfies the following definition.
$$
\mathrm{countable}(X) =_{df} \exists{F} (\mathrm{dom}(F) = \mathbb{N} \wedge \mathrm{ran}(F) = X \wedge \forall{x \in X}\exists{y \in \mathbb{N}} (F(y) = x).
$$
The definition of uncountability is then just the negation of the countability condition.

The question of why this characterisation is 'absolute' in a way that the first order characterisation is not can be found in the Dedekind categoricity theorem cited above. Given the standard semantics for second order logic, all structures satisfying the second order Peano axioms are isomorphic—the theory is categorical.
Because of this, the Löwenheim–Skolem theorem is false for second order logic (with the standard semantics), so the kind of model-theoretic relativity you get in first order logic does not appear (at least to the same extent). We don't get models where the whole domain is countable (from the 'external' perspective), but the model itself thinks that there are uncountable sets just because certain functions don't exist.
