Heyting algebra
Heyting algebras generalize Boolean algebras in the sense that a Heyting algebra satisfying "a" ∨ ¬"a" = 1 (excluded middle), equivalently ¬¬"a" = "a" (double negation elimination), is a Boolean algebra. Those elements of a Heyting algebra "H" of the form ¬"a" comprise a Boolean lattice, but in general this is not a subalgebra of "H" (see below).