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

Conference item

Abstract:: We devise a variant of Dialectica interpretation of intuitionistic linear logic for Open image in new window, a linear logic-based version MSO over infinite words. Open image in new window 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 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 Open image in new window. Besides, this shows that in principle, one can solve Church’s synthesis for a given ∀∃ -formula by only looking for proofs of either that formula or its linear negation.

Files:: Pradic-Riba2019_Chapter_ADialectica-LikeInterpretation.pdf

(Preview, Version of record, pdf, 1.4MB, Terms of use)

Copyright holder:: Pradic et al
Notes:: © The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

If you are the owner of this record, you can report an update to it here: Report update to this record