Birkhoff's theorem

Birkhoff's theorem answers a foundational question: which classes of algebras are exactly the ones you can pin down with equations? The surprising and beautiful answer is that you never need to look at the equations themselves — a class is equational if and only if it is closed under three completely concrete construction operations. This converts a logical property (definability by identities) into a structural one (closure), and is the cornerstone of universal algebra.

Precisely, write H for the operation of forming homomorphic images, S for subalgebras and P for (arbitrary, including infinite) direct products of a class of algebras. Birkhoff's HSP theorem (G. Birkhoff, 1935) states: a class K of algebras of a fixed signature is a variety — that is, K = Mod(E) for some set of identities E — if and only if K is closed under H, S and P. Equivalently, the smallest variety containing a class K equals HSP(K), the result of applying these three operations in that order.

One direction is routine: any equational class is obviously closed under H, S and P, since identities are preserved by quotients, subalgebras and products. The hard direction builds, from a class closed under HSP, a defining set of identities, using free algebras: the relevant identities are read off from the free algebra of the class on countably many generators. The theorem fails if one drops products or allows relations, which is why it is a theorem specifically about equational logic.