The modern theory of formal languages has progressed far beyond concepts such as regular expressions that the typical computer scientist is familiar with. One approach to language theory is based on the mathematical framework of profinite topologies; profinite words can be considered as limits of sequences of finite words, which converge according to a metric that denotes the size of the automaton needed to distinguish between two words.

The present paper investigates the logical description of profinite languages by a first-order logic with numerical predicates that constrain the length of a word and the symbols in it; for example, the sentence “exists x. a(x)” with unary predicate “a” is true for every word in which the symbol “a” occurs at some position. In particular, the authors investigate in which cases languages can be also characterized in a simpler form, namely by “ultrafilter equations” where an ultrafilter denotes a profinite language and a language satisfies an equation if it is denoted by both ultrafilters in the equation or by none. They show that every regular language that can be described by the first-order logic can be also described by a simple class of ultrafilter equations; this also gives rise to a new proof of decidability of the problem of whether a language is both regular and a Boolean algebra.

While the paper contains interesting results, its target readers are experts in the field. For a general motivation or examples, the reader should consult more accessible introductions to the profinite approach to language theory first.