A groupoid is a set together with a binary operation defined on this set. If s = t is a pair of terms constructed by variables of an alphabet X and one binary operation symbol then s = t is called identity in the groupoid (A; ¦ ^A) if for all evaluations of variables occurring in s, t by elements from A the resulting propositions are true. So identities are expressions in a first order language where quatification is allowed only with "for all" over variables.

A class of all groupoids satisfying a given set of equations is called variety.

Examples:

The derivation concept for identities if based on the well-known five derivation rules. The derivation concept is complete and consistent.

If we substitute for the binary operation symbol in an identity any binary term then we obtain an expression in the second order language which is called HYPERIDENTITY. The model classes of sets of hyperidentities are called solid varieties. They are varieties of second order. The derivation concept of those expressions contains one more derivation rele, the so-called hypersubstitution rele. As a consequence, derivations run more quickly. This hyperequational logic is also complete and consistent. The general theory is applied to concrete varieties of groupoids. We determine solid (or more general M-solid) varieties of groupcids and give examples how the new derivation concept works.