An Algebraic Characterisation of First-Order Logic with Neighbour

TL;DR

This paper provides an algebraic framework for characterizing first-order logic with the neighbour relation on finite words using involution semigroups and introduces a new semidirect product called the locally hermitian product.

Contribution

It introduces the locally hermitian product of involution semigroups and establishes an algebraic characterization of FO with neighbour logic through this structure.

Findings

Characterization of FO with neighbour using locally hermitian products.

Establishment of an Eilenberg-type correspondence for involution varieties.

Identification of recognition conditions for languages definable in the logic.

Abstract

We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup. We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups.