Uniformisation of Regular Relations in First-Order Logic with Two Variables

A uniformisation of a binary relation is a functional relation contained in it, with the same domain. The uniformisation problem asks whether such a uniformisation can be defined in a given formalism.

We solve this problem in the context of regular relations over finite words, for the fragment FO 2 [<] of First-Order Logic with two variables: we provide an algorithm that decides if a given regular relation over finite words admits a uniformisation definable in FO 2 [<].

The paper provides a new representation of languages definable in FO 2 [<], which can be used for the decidability of other problems involving this formalism, e.g. the problem of separability of two regular languages by a language definable in FO 2 [<].