A constructive version of Birkhoff's theorem

A version of Birkhoff's theorem is proved by constructive, predicative, methods. The version we prove has two conditions more than the classical one. First, the class considered is assumed to contain a generic family, which is defined to be a set-indexed family of algebras such that if an identity is valid in every algebra of this family, it is valid in every algebra of the class. Secondly, the class is assumed to be closed under inductive limits. (C) 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.