Universal Horn class

Summary

A universal Horn class is the class of all structures of a signature that satisfy a given set of universal Horn sentences. Such a sentence is a universally quantified Horn clause built from first-order atomic formulas. Universal Horn classes are universal classes, and in addition they are closed under direct products of nonempty families. In an algebraic signature, the classes axiomatized by universal Horn sentences with a positive literal are exactly the quasivarieties.