Positive first-order logic on words.

Prelegent(ci)

Denis Kuperberg

Afiliacja

ENS Lyon

Termin

16 grudnia 2020 14:15

Informacje na temat wydarzenia

online

Seminarium

Seminarium „Teoria automatów”

---

I will present FO+, a restriction of first-order logic where letters are required to appear positively, and the alphabet is partially ordered (for instance by inclusion order if letters are sets of atoms). Restricting predicates to appear positively is for instance very natural when considering logics with fixpoints. Here we will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, but can every FO-definable monotone language be defined in this way? On general structures, Lyndon's theorem gives such a syntax/semantics equivalence for monotone first-order formulas, but it is known to fail on finite structures. We will see that it also fails on finite words, giving a much simpler proof for the failure of Lyndon's theorem on finite structures. Finally we will look at whether FO+-definability is decidable for regular languages.

---