Is there a method converting implication into equality? I'm working with an algebra which has lattice structure amended with several other operations and axioms. I have couple of axioms which are expressed as implications, for example, conditional distributivity
$ H \wedge (x \vee y) = H \wedge (x \vee z) \vdash 
x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z) $
Is there a way to express it as a set of pure equational axioms? Specifically:

*

*Is there general universal algebra method?

*If not, is there a method for lattices?

*If not, is there a method for any other concrete algebra?

 A: Classes defined by implications of the type
$$p_1=q_1, \ldots, p_k=q_k \Rightarrow u=v,$$
where $p_i, q_i, u, v$ are terms of the relevant signature are called implicational classes, or quasi-varieties.
Every variety (or equational class) is a quasi-variety, in a trivial way.
Varieties are also characterized as classes of algebras closed under the formation of homomorphic images, subalgebras and direct products.
Quasi-varieties are those classes closed under the formation of subalgebras, direct products and ultraproducts.
I'll give you a more or less trivial example of a quasi-variety of lattices which is not a variety.
In view of the previous paragraph, it's enough to give an example of a class of algebras defined by an implication between equalities but not closed under the formation of homomorphic images.
Let $\mathcal K$ be the class of lattices satisfying the implication:
$$x \wedge (y \vee z) = x \wedge ((y \wedge (x \vee z)) \vee z)
\Rightarrow 
x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z).$$
Notice that the equality in the antecedent, i.e.,
$$x \wedge (y \vee z) = x \wedge ((y \wedge (x \vee z)) \vee z),$$
is the modular identity (satisfied by all those lattices which don't have a copy of the pentagon $\mathbf N_5$ as a sublattice), while the equality in the consequent is the distributive one, as it is well known.
Hence, the class $\mathcal K$ consists of those lattices which either are not modular, or are distributive.
On such example is the lattice $\mathbf L$ below.
Since elements $0, b, c, d, 1$ make a pentagon, it's not modular, and so it satisfies the implication.

Now, let $\theta = \Theta(c,d)$ be the least congruence relating $c$ and $d$.
It follows that
$$\theta = \{c,d\}^2 \cup \{(x,x):x\in L\},$$
whence, $\mathbf L/\theta$ (a homomorphic image of $\mathbf L$) is the following lattice:

This is a modular, but not distributive lattice, and so it doesn't satisfy the implication.
We conclude that the implication is not equivalent to a set of equalities.
Notice there are some examples of classes of algebras (including lattices) which are usually defined by implications but are equivalently definable by equalities.
A remarkable example is that of modular lattices, which are usually defined by the implication
$$x \leq z \Rightarrow x \vee (y \wedge z) = (x \vee y) \wedge z,$$
but can be defined by modular identity as stated above.
So there is no such method for lattices, in general, and consequently, neither there is for algebras in general.
About your last bullet point, there exist, indeed, varieties for which all sub-quasi-varieties are varieties too.
This is, for example, the case of $\mathcal M_{\omega}$, as proved in
Grätzer and Lakser, Algebra Universalis, 8 (1978) 135-135.
I don't know of any systematic way of telling whether or not a variety has this property.
