BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Positive first-order logic on words and graphs - D
enis Kuperberg (ENS Lyon)
DTSTART:20231124T110000Z
DTEND:20231124T115000Z
UID:TALK5347AT
URL:/talk/index/5347
DESCRIPTION:*Zoom details*\n\n* Link: https://bham-ac-uk.zoom.
us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IU
T09\n* Meeting ID: 818 7333 5084\n* Passcode: 217\
n\n*Abstract*\n\nWe will investigate the gap betwe
en syntactically and semantically positive first-o
rder logic formulas.\nA formula is syntactically p
ositive if it does not contain negated predicates\
, while it is semantically positive when the class
of structures it defines is monotone\, i.e. close
d under making the predicates true on more tuples.
\nStarting with finite words\, I will present the
logic FO+\, where letter predicates are required t
o appear positively. The words considered here are
on a "powerset alphabet": predicates a(x) and b(x
) can be true simultaneously on the same position
x of the word. We will ask a syntax versus semanti
cs question: FO+-definable languages are monotone
in the letters\, but can every FO-definable monoto
ne language be expressed in FO+ ? On general struc
tures\, Lyndon's theorem gives a positive answer t
o this question\, but it is known to fail on finit
e structures. We will see that it already fails on
finite words\, by giving a simple counter-example
language. This gives a new proof for the failure
of Lyndon's theorem on finite structures\, that is
much more elementary than previous proofs.\nWe wi
ll also study the problem on finite graphs: if a c
lass of finite graphs is FO-definable and closed u
nder edge addition\, can it be defined with a nega
tion-free formula ? To our knowledge this was an o
pen question\, which we can answer negatively via
a suitable encoding of our counter-example languag
e.\nFinally\, if time permits\, we will go back to
regular languages of finite words and see that FO
+-definability is surprisingly undecidable in this
framework.\n\nThis talk is based on work publishe
d in LICS 2021\, together with a full version incl
uding graphs that was recently published in LMCS 2
023.
LOCATION:LG23\, Computer Science // Zoom
CONTACT:George Kaye
END:VEVENT
END:VCALENDAR