From Sets to Points: Simplifying MSO Interpretations via Reparameterizations

We study the conditions under which monadic second-order (MSO) interpretations can be simplified by replacing representations of elements as tuples of arbitrary sets with representations as tuples of finite sets or points. Using reparameterizations of MSO formulas, we prove that for formulas with free finite-set variables, it is decidable whether a point reparameterization exists, and that such a reparameterization can be effectively constructed over countable chains. Moreover, over countable Dedekind-complete labeled chains, a formula with free arbitrary set variables admits a finite-set reparameterization if and only if it has at most countably many satisfying assignments. These results yield effective simplification procedures for MSO interpretations over broad classes of countable linear orders.