Logo Utrecht University

TULIPS – The Utrecht Logic in Progress Series

Upcoming Talks


Monadic Second Order Logic as a Model Companion

I will talk about a connection between monadic second order logic and more traditional first order model theory, which has emerged in my recent joint work with Ghilardi [1,2].
Monadic second order (MSO) logic, when interpreted in discrete structures, is closely related to certain formal models of computation. For example, the MSO-definable sets of finite colored linear orders (“words”) are exactly the regular languages from automata theory. MSO logic and its connection to automata has also been studied on many more structures, including omega-indexed words and binary trees.
In more traditional model theory, one typically studies first order logic as a generalization of certain constructions in mathematics. A fundamental insight there was that the theory of algebraically closed fields can be generalized to a purely logical notion of “existentially closed model”. The syntactic counterpart of this notion is called the “model companion” of a first order theory.
We prove that MSO logic, both on omega-words [1] and on binary trees [2], can be viewed as the model companion of a finitely axiomatized universal first order theory. In each case, this universal theory is closely connected to well-known modal fix-point logics on such structures.
[1] S. Ghilardi and S. J. van Gool, A model-theoretic characterization of monadic second-order logic on infinite words, Journal of Symbolic Logic, vol. 82, no. 1, 62-76 (2017). https://arxiv.org/pdf/1503.08936.pdf
[2] S. Ghilardi and S. J. van Gool, Monadic second order logic as the model companion of temporal logic, Proc. LICS 2016, 417-426 (2016). https://arxiv.org/pdf/1605.01003.pdf

Time: 16:00 – 17:30

Location: Room 302, Drift 25