# Birkhoff's theorem (equational logic)

Short description: Theorem in equational logic

In logic, Birkhoff's theorem in equational logic states that an equality t = u is a semantic consequence of a set of equalities E, if and only if t = u can be proven from the set of equalities.[1] It is named after Garrett Birkhoff.

## References

1. Baader, Franz; Nipkow, Tobias (March 1998). "Term Rewriting and All That" (in en). p. Th. 3.5.14, p. 55.