nLab Birkhoff's HSP theorem





(Birkhoff’s HSP theorem)

Given a language LL generated by a set of (single-sorted) finitary operations, and a class CC of structures for LL. Then CC is the class of models for a set of universally quantified equations between terms of LL (a Lawvere theory) if and only if

  1. (H) The class is closed under homomorphic images (see below),

  2. (S) The class is closed under subalgebras,

  3. (P) The class is closed under taking products.

See also at Lawvere theory – Characterization of examples


Here “closed under homomorphic images” means that if AA and BB are structures in the class, and ϕ:AB\phi \colon A \to B is a homomorphism between them, then also its image im(ϕ)Bim(\phi) \hookrightarrow B is an element of the class.


The first-order analogue of HSP (theorem ) is the characterization (see e.g. Chang and Keisler’s original text (Chang-Keisler 66) on continuous model theory) of elementary classes of structures of structures: they’re precisely those closed under elementary substructures, elementary embeddings, ultraproducts, and ultraroots (if an ultrapower of something is in your class, that something was in your class.)


  • Chang, Keisler Continuous Model Theory, Princeton University Press (1966) [ISBN: 9780691079295]

  • Michael Barr, HSP type theorems in the category of posets, in: Proc. 7th International Conf. Mathematical Foundation of Programming Language Semantics, Lecture Notes in Computer Science 598 (1992) 221–234 [doi:10.1007/3-540-55511-0_11, pdf]

  • Michael Barr, Functorial semantics and HSP type theorems, Algebra Universalis 31 (1994) 223–251 [doi:10.1007/BF01236519, pdf, pdf]

  • Michael Barr, HSP subcategories of Eilenberg-Moore algebras, Theory Appl. Categories 10 18 (2002), 461–468 [tac:10-18]

See also:

Last revised on November 4, 2023 at 09:11:31. See the history of this page for a list of all contributions to it.