A Dialectica-Like Interpretation of a Linear MSO on Infinite Words.

We devise a variant of Dialectica interpretation of intuitionistic linear logic for LMSO, a linear logic-based version MSO over infinite words. LMSO was known to be correct and complete w.r.t. Church's synthesis, thanks to an automata-based realizability model. Invoking Buchi-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 for all there exists-formula by only looking for proofs of either that formula or its linear negation.