Birkhoff's representation theorem is equivalent to the axiom of choice (Q1820782)

Birkhoff's Representation Theorem (BRT) states that every algebra is a subdirect product of subdirectly irreducible algebras. Let ZF\(^-\) be Zermelo-Fraenkel set theory without the axiom of foundation (AF) and without the axiom of choice (AC). Birkhoff's proof of (AC) \(\Rightarrow\) (BRT) can be carried out in ZF\(^-\). The author shows that the converse also is provable in \(ZF^-\). For this, he uses the result of H. Rubin and J. Rubin that, in ZF\(^-\), (AC) is implied by (AL 7): Every subalgebra is the intersection of all meet-irreducible subalgebras containing it as a subset. He shows that (BRT) \(\Rightarrow\) (AL 7) in ZF\(^-\). This is done with the help of the Congruence Lattice Representation Theorem: every algebraic lattice can be represented as the congruence lattice of an algebra. (It is shown how applications of (AC) can be eliminated from the usual proof of this theorem.) The author credits H. Andréka and I. Németi with pointing out to him that his original proof of (BRT) \(\Leftrightarrow\) (AC) in ZF\(^-+\)(AF) can be carried out in ZF\(^-\).