Résumé | It is well-known that every sentence of first-order logic over <, interpreted in finite words (FO[<]), is equivalent to a sentence in which only three variables are used. The fragment FO2[<] of sentences using only two variables, has been the subject of considerable study, and admits interesting characterizations in algebra and temporal logic.
In this talk, I will describe an extension of FO2[<] in which one allows a new binary relation that says, ‘there is an occurrence of the letter a between x and y’. In a sense, this is the simplest property that one can express that requires 3 variables.
I will present several logics, both first-order and temporal, that have the same expressive power; matching lower and upper bounds for the complexity of satisfiability for each of these formulations; and effective necessary and sufficient conditions, based on the syntactic monoid, for a property to be expressible in these logics. This algebraic analysis allows one to prove, among other things, that these new logics have strictly less expressive power than full first-order logic FO[<]. The proofs use a novel method for obtaining factorizations of words that may have independent interest.
This is joint work with Andreas Krebs, Kamal Lodaya, and Paritosh Pandya. The results are described in two papers presented at LICS 2016 and CSL 2018. A journal version, containing all the results and proofs (arXiv:1902.05905) will appear in Logical Methods in Computer Science. |