%0 Conference Proceedings
%T A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams
%+ Laboratoire de l'Informatique du Parallélisme (LIP)
%+ Preuves et Langages (PLUME)
%A Riba, Colin
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 7th International Conference on Theoretical Computer Science (TCS)
%C Amsterdam, Netherlands
%Y Jos C. M. Baeten
%Y Tom Ball
%Y Frank S. Boer
%I Springer
%3 Theoretical Computer Science
%V LNCS-7604
%P 310-324
%8 2012-09-26
%D 2012
%R 10.1007/978-3-642-33475-7_22
%Z Computer Science [cs]
%Z Computer Science [cs]/Logic in Computer Science [cs.LO]Conference papers
%X We discuss the completeness of an axiomatization of Monadic Second- Order Logic (MSO) on infinite words (or streams). By using model-theoretic tools, we give an alternative proof of D. Siefkes' result that a fragment with full comprehension and induction of second-order Peano's arithmetic is com- plete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman- Vaught Theorems and the Ehrenfeucht-Fra ̈ıss ́e method for Henkin models of second-order arithmetic. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan fac- torizations similar to those for standard infinite words. We also discuss a Ramsey's theorem for MSO-definable colorings, and show that in linearly ordered Henkin models, Ramsey's theorem for additive MSO-definable col- orings implies Ramsey's theorem for all MSO-definable colorings.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://hal.science/hal-00692153/document
%2 https://hal.science/hal-00692153/file/main.pdf
%L hal-00692153
%U https://hal.science/hal-00692153
%~ ENS-LYON
%~ CNRS
%~ INRIA
%~ UNIV-LYON1
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG
%~ IFIP-TC2
%~ IFIP-TCS
%~ IFIP-WG2-2
%~ IFIP-LNCS-7604
%~ INRIA-AUT
%~ UDL
%~ UNIV-LYON