Is there any formula of monadic second-order logic that is only satisfied by an infinite set?

Question

Is there any formula, of monadic second-order logic, that is only satisfied by an infinite set?

Answer 1

Skolem proved a quantifier elimination result for Peirce's "Calculus of Classes". See this article in the Stanford Encyclopaedia of Philosophy for some references. This calculus amounts to the first-order theory over the signature $(\subseteq; \emptyset, -, \cup, \cap)$ of type $(2; 0, 1, 2, 2)$ whose intended interpretation is the set of subsets of some universe with $\subseteq$ being the subset relation,with $\emptyset$ denoting the empty set and with $-$, $\cup$ and $\cap$ denoting complementation, union and intersection.

Skolem's result shows that every sentence is equivalent to a propositional combination of sentences $L_n$ ($n = 1, 2, \ldots)$, where $L_n$ means "the universe has at least $n$ elements". Monadic second order logic can be reduced to the theory of the Calculus of Classes by mapping sets to themselves and by treating elements as singleton sets, noting that singleton sets are the atoms for the subset relation. A satisfiable propositional combination of the sentences $L_n$ is satisfiable in a finite universe, hence a satisfiable sentence of the form $\exists x.\phi$ is satisfiable with a witness for $x$ that is finite.