A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
Cécilia Pradic, Colin Riba · Lecture notes in computer science · 2019
Abstract We devise a variant of Dialectica interpretation of intuitionistic linear logic for "Equation missing", a linear logic-based version $$\mathsf {MSO}$$ over infinite words. "Equation missing" was known to be correct and complete w.r.t. Church’s synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of $$\mathsf {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 "Equation missing". 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.