# Birkhoff's theorem (equational logic)

From HandWiki

__: Theorem in equational logic__

**Short description**There do not appear to be enough references currently present in this article to demonstrate notability. However, an editor has performed a search and claims that there are sufficient sources to indicate that this is a notable topic. (May 2020) (Learn how and when to remove this template message) |

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

- ↑ Baader, Franz; Nipkow, Tobias (March 1998). "Term Rewriting and All That" (in en). p. Th. 3.5.14, p. 55. https://www.cambridge.org/core/books/term-rewriting-and-all-that/71768055278D0DEF4FFC74722DE0D707.

Original source: https://en.wikipedia.org/wiki/Birkhoff's theorem (equational logic).
Read more |