A generic characterization of generalized unary temporal logic and two-variable first-order logic

TL;DR

This paper provides a unified algebraic and logical framework for various two-variable first-order logics and unary temporal logics, generalizing known characterizations and establishing decidability results for their classes.

Contribution

It introduces a generic operator to characterize classes of languages associated with different variants of two-variable first-order logic and unary temporal logic, extending known results.

Findings

Provides a generic algebraic characterization of $FO^2(I_C)$ classes.

Shows that decidability of separation in class $C$ implies decidability of membership in $FO^2(I_C)$.

Establishes equivalence between $FO^2(I_C)$ and a variant of unary temporal logic $TL(C)$.

Abstract

We investigate an operator on classes of languages. For each class $C$, it outputs a new class $FO^2(I_C)$ associated with a variant of two-variable first-order logic equipped with a signature$I_C$ built from $C$. For $C = \{\emptyset, A^*\}$, we get the variant $FO^2(<)$ equipped with the linear order. For $C = \{\emptyset, \{\varepsilon\},A^+, A^*\}$, we get the variant $FO^2(<,+1)$, which also includes the successor. If $C$ consists of all Boolean combinations of languages $A^*aA^*$ where $a$ is a letter, we get the variant $FO^2(<,Bet)$, which also includes "between relations". We prove a generic algebraic characterization of the classes $FO^2(I_C)$. It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if $C$ has decidable separation (plus mild properties), then $FO^2(I_C)$ has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class $C$, we consider a variant $TL(C)$ of unary temporal logic whose future/past modalities depend on $C$ and such that $TL(C) = FO^2(I_C)$. Finally, we also characterize $FL(C)$ and $PL(C)$, the pure-future and pure-past restrictions of $TL(C)$. These characterizations as well imply that if \Cs is a class with decidable separation, then $FL(C)$ and $PL(C)$ have decidable membership.