Is there a monadic second-order (MSO) theory, or even formula, T over some signature $\Sigma$, such that for every structure M for $\Sigma$, M satisfies T if and only if M is finite?
(Note that this question is different from a previous question that asked whether there is an MSO theory/formula that is only satisfied by an infinite model. The difference is that the latter formula may be satisfied by some infinite structures but not by other infinite structures of the same signature. Hence, such a formula does not characterize infiniteness. I am asking whether there is a theory/formula that is satisfied by all finite structures of some signature and by no infinite structure of that signature.)
The answer is NO.
Over the empty signature (and over the signature with =) every MSO sentence is equivalent to a boolean combination of sentences of the form "the domain has at least n elements". As this can be expressed in first-order logic with equality (FOL=), MSO over the empty signature is not stronger than FOL=, which cannot characterize finiteness.
In Addition, no signature $\Sigma$ can help MSO in characterizing finiteness: Consider the class S of structures that interpret all relations of $\Sigma$ as False and all functions of $\Sigma$ as the identity to the first parameter of the function. Then, S has structures of all cardinalities, and MSO cannot characterize the finite among them, since with respect to S, every MSO sentence over $\Sigma$ is equivalent to an MSO sentence over the empty signature.