A second-order transitive-closure specification over a vocabulary $L$ consists of a block of relation variables and three first-order sentences over $L \cup \{\le\}$: a transition sentence over two copies of the block, and a source and a target sentence over one copy. On a linearly ordered $L$-structure it defines a directed graph whose nodes, the states, are the assignments of relations to the block, with an edge from one state to another when the transition sentence holds with the first copy of the block read as the current state and the second as the next. The specification accepts the structure when some state satisfying the target sentence is reachable, by a possibly empty path, from some state satisfying the source sentence.

A decision problem $P$ over $L$ is SO(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$. A state holds polynomially many bits and a path may be exponentially long: this is the logic SO(TC), which captures polynomial space on ordered structures, in the normal form of a single application of the operator.