Gentzen-style axiomatizations in equational logic

The notion of a Gentzen-style axiomatization of equational theories is presented. In the standard deductive systems for equational logic axioms take the form of equations and the inference rules can be viewed as quasi-equations. In the deductive systems for quasi-equational logic the axioms, which are quasi-equations, can be viewed as sequents and the inference rules as Gentzen-style rules. It is conjectured that every finite algebra has a finite Gentzen-style axiomatization for its quasi-identities. We verify this conjecture for a class of algebras that includes all finite algebras without proper subalgebras and all finite simple algebras that are embeddable into the free algebra of their variety.Dedicated to the memory of Alan DayPresented by J. Sichler.Supported by an Iowa State University Research Assistantship.Supported by National Science Foundation Grant #DMS 8005870.