A transitive-closure specification over a vocabulary $L$ consists of a finite set of modes, an arity $k$, and first-order formulas over $L \cup \{\le\}$: a transition formula $\varphi_{m,n}(\bar x, \bar y)$ for each pair of modes and, for each mode $m$, a source formula $\sigma_m(\bar x)$ and a target formula $\tau_m(\bar x)$, with $\bar x$ and $\bar y$ tuples of $k$ variables. On a linearly ordered $L$-structure $A$ it defines a directed graph whose nodes are the pairs $(m, \bar a)$ of a mode and a $k$-tuple of elements, with an edge from $(m, \bar a)$ to $(n, \bar b)$ when $A \models \varphi_{m,n}(\bar a, \bar b)$. The specification accepts $A$ when some node satisfying its target formula is reachable, by a possibly empty path, from some node satisfying its source formula.

A decision problem $P$ over $L$ is FO(TC) definable when some specification accepts, for every nonempty finite $L$-structure $A$ and every linear order on $A$, exactly when $A$ is a yes-instance of $P$. This is the normal form of first-order logic with a transitive closure operator on ordered structures, a single positive application of the operator; the modes play the role of a bounded amount of extra state, which tuples of elements cannot carry on small universes.