Equational theories of profinite structures

TL;DR

This paper develops a general framework for constructing profinite structures and characterizes lattices of recognizable sets using profinite equations, extending previous results from finite words to relational structures.

Contribution

It introduces a broad method for profinite structures and proves a key theorem linking recognisable sets and profinite equations, generalizing earlier finite-word results.

Findings

Lattices of recognisable sets are definable by profinite equations.

The framework applies to finite relational structures and first-order logic.

Provides a characterization of lattices of first-order formulas.

Abstract

In this paper we consider a general way of constructing profinite struc- tures based on a given framework - a countable family of objects and a countable family of recognisers (e.g. formulas). The main theorem states: A subset of a family of recognisable sets is a lattice if and only if it is definable by a family of profinite equations. This result extends Theorem 5.2 from [GGEP08] expressed only for finite words and morphisms to finite monoids. One of the applications of our theorem is the situation where objects are finite relational structures and recognisers are first order sentences. In that setting a simple characterisation of lattices of first order formulas arise.