Choice-Free Proof of Mal'cev's Theorem on Quasivarieties
Mal'cev's theorem characterizes quasivarieties of first-order structures as exactly the classes containing a unit and closed under isomorphisms, substructures, and reduced products. This gives a proof of that characterization, and of its extension to arbitrary basic Horn formulas, entirely within Zermelo-Fraenkel set theory without the axiom of choice, replacing choice with the collection principle and yielding a new free-algebra-free proof of Birkhoff's HSP theorem.
2501.00766
A quasivariety is a class of first-order structures axiomatized by quasi-identities (strict basic Horn formulas). Mal'cev's 1966 theorem characterizes quasivarieties purely structurally: a class is a…