A Horn clause over a vocabulary $L$, a block of second-order relation variables and $k$ first-order variables $\bar x$ is an implication $\gamma(\bar x) \wedge \alpha_1 \wedge \dots \wedge \alpha_m \to \eta$, where the guard $\gamma$ is an arbitrary first-order formula over $L$, the body atoms $\alpha_i$ are atoms in the relation variables, and the head $\eta$ is such an atom or $\bot$, the clause being then a goal clause. A Horn program is a finite list of such clauses, and an assignment of relations to the block satisfies it on a structure when every clause holds at every valuation of $\bar x$.

A decision problem $P$ over $L$ is SO-Horn definable when there are a block, a number $k$ and a Horn program over $L \cup \{\le\}$ such that, for every nonempty finite $L$-structure $A$ and every linear order on $A$, $A$ is a yes-instance of $P$ if and only if some assignment satisfies the program on $A$ with that order. This is the fragment SO-Horn of Grädel, existential second-order logic whose first-order kernel is universal and Horn in the second-order atoms.