HORN-SAT is PTIME-complete under first-order reductions. It is SO-Horn definable, by a Horn program that computes unit propagation and assembles the unbounded body of an input clause along the order; and every SO-Horn definable problem reduces to it by an ordered first-order reduction that emits one propositional Horn clause per clause of the program and per valuation of its first-order variables. This is the polynomial-time counterpart of the Cook–Levin theorem.