nLab Birkhoff's HSP theorem

This is about Birkhoff’s variety or HSP theorem in universal algebra, related to equational logic?. While it is sometimes referred to simply as Birkhoff’s theorem beware of other well know Birkhoff's theorems.

Statement

Theorem

(Birkhoff’s HSP theorem)

Given a language $L$ generated by a set of (single-sorted) finitary operations, and a class $C$ of structures for $L$. Then $C$ is the class of models for a set of universally quantified equations between terms of $L$ (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.

In a more classical wording/terminology it is phrased as

(Birkhoff’s variety theorem) A class of algebras of the same signature is a variety of algebras iff it is closed under homomorphic images, subalgebras and arbitrary (small) products.

See also at Lawvere theory – Characterization of examples

Remark

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

Remark

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.)

References

The original reference is

• Garrett Birkhoff, On the structure of abstract algebras, Proc. Cambridge Philos. Soc. 31 (4): 433–454 (1935) doi pdf

There is a textbook treatment in the monograph

• 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]

• Robert Goldblatt, What is the coalgebraic analogue of Birkhoff’s variety theorem?, Theoretical Computer Science 266:1–2 (2001) 853–886 doi

Some Birkhoff’s variety-style theorems in a categorical setup for equational logic play role in

• G. Roşu, Complete categorical deduction for satisfaction as injectivity, In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science 4060, Springer 2006 doi
• G. Roşu, Axiomatizability in inclusive equational logics, Mathematical Structures in Computer Science 12:5 (2002) 541–563 doi

See also:

• Wikipedia, Birkhoff's theorem

category: algebra, logic