Title: An Algebraic Characterization of First-Order Definability
Author: A.J. Kfoury and M. Wymann-Boeni
Date: November 1993
Abstract:
We give a variable-free relational calculus which defines exactly
all first-order definable relations in a arbitrary structure.
We then show that, over an arbitrary class $\C$ of finite ordered
structures with signature $\{ \LE, R_1, \ldots, R_\alpha \}$,
the unary relations uniformly defined by this calculus over $\C$
are characterized by a another simplified variable-free calculus which we
call $\Q$. $\Q$ is the least set of formal expressions such that:
\begin{eqnarray*}
\Q &\supseteq&\ \{ \varnothing, R_1,\ldots, R_\alpha \}\ \cup\\
& &\ \{ (Q\PLUS x)\ |\ Q\in\Q, x\in\omega \cup \{\infty\} \}\ \cup
\ \{ (Q\MINUS x)\ |\ Q\in\Q, x\in\omega \cup \{\infty\} \}\ \cup \\
& &\ \{ (\NOT Q)\ |\ Q\in\Q\}\ \cup
\ \{ (Q_1\AND Q_2)\ |\ Q_1,Q_2\in\Q\}\ \cup
\ \{ (Q_1\OR Q_2)\ |\ Q_1,Q_2\in\Q\}\ .\
\end{eqnarray*}
where $\PLUS$ and $\MINUS$ are ``shift'' operators defined in Section 3.
\end{abstract}