We devise a variant of Dialectica interpretation of intuitionistic linear logic for LMSO, a linear logic-based version of MSO over infinite words. LMSO was known to be correct and complete with respect to Church’s synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of MSO on infinite words, our interpretation provides us with a syntactic approach, without any further construction of automata on infinite words. Via Dialectica, as linear negation directly corresponds to switching players in games, we furthermore obtain a complete logic: either a closed formula or its linear negation is provable. This completely axiomatizes the theory of the realizability model of LMSO. Besides, this shows that in principle, one can solve Church’s synthesis for a given \forall\exists-formula by only looking for proofs of either that formula or its linear negation.