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

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

• Wouldn't the answer be no, given that we cannot express Dedekind-infinite 'property', i.e. that a set is infinite, in monadic logic? Commented Apr 23, 2015 at 12:52
• @prime4567: Can you prove that? All that is obvious is that the usual characterization of Dedekind-infiniteness is not expressible (since it quantifies over functions, not just subsets of the universe). Commented Apr 23, 2015 at 20:41
• @Asaf Karagila: it is indeed not obvious. It does follow from the result of Skolem that I refer to in my answer to the question. Commented Apr 23, 2015 at 21:01
• @Asaf Karagila Indeed, I was somewhat too quick there. The identity 'infinite(x) iff Dedekind-infinite(x)' apparently cannot be proven in ZF without the assumption of the axiom of choice. Commented Apr 23, 2015 at 22:09
• @prime4567: That is true, but somewhat irrelevant. I think we can assume the axiom of choice in the universe unless stated otherwise. Commented Apr 23, 2015 at 22:15

## 1 Answer

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.