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.