A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams - Theoretical Computer Science
Conference Papers Year : 2012

A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams

Abstract

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.
Fichier principal
Vignette du fichier
main.pdf (413.86 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-00692153 , version 1 (28-04-2012)

Licence

Identifiers

Cite

Colin Riba. A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.310-324, ⟨10.1007/978-3-642-33475-7_22⟩. ⟨hal-00692153⟩
589 View
174 Download

Altmetric

Share

More