Are magma law implications not semidecidable?

Stream: Equational

[Franklin Pezzuti Dyer]

This question is just out of curiosity, and I wonder if anyone knows of any references addressing it.

For context: we know that for any (computably enumerable) magma M, deciding whether an equational law L holds in M is semidecidable, because listing all combinations of possible values for the free variables will eventually yield a counterexample to L when one exists. Deciding whether a law L holds over a finite magma M is decidable by enumeration, and hence deciding whether an implication L1 -> L2 holds over finite magmas is semidecidable because enumerating all finite magmas is guaranteed to yield a counterexample to L1 -> L2 when one exists.

My question is: is L1 -> L2 semidecidable in general? My intuition is that the answer is negative, and that it is just plain undecidable, because this project has seen pairs of laws crop up that are equivalent over finite magmas but not over arbitrary magmas. But this does not amount to a proof that magma law implications fail to be semidecidable, and I'm wondering if anyone knows of a reference (or a simple argument I'm missing) that proves/disproves this.

[Daniel Weber]

Can't you just search for a proof, and by the completeness theorem if the implication is true you'll find it?

[Franklin Pezzuti Dyer]

Ha, I guess that is the simple argument I was missing!