Generating non-implications for laws

Stream: Equational

[Andrés Goens]

I've been slowly chipping away at lifting all equational results to laws so we can apply duality to prove the closure of things. Equational#459 for example generates an implication of (syntactic) laws for every implication of equations, and that works well! We only generate a law implication where we had the equation implication, since we have transitivity (and as @Joachim Breitner pointed out, duality should work the same essentially, we just compute it when we need it).

The problem is that for anti-implications (of which there is roughly 2x as many), things are not as clear. We have this whole system of facts, so that we get one counterexample providing multiple non-implications. I wonder if it's worth creating an anti-implication theorem for laws for each of these?

For a random example, Refutation29 shows that for that concrete example, Equations 3894, 4098, 4284, 4423 and 4497 hold, whereas Equations[3253, 3456, 3660, 3661, 3685, 3687, 3721, 3725, 3865, 3867, 3881, 3887, 3915, 3928, 4070, 4073, 4084, 4131, 4269, 4273, 4275, 4276, 4283, 4290, 4291, 4293, 4314, 4320, 4321, 4396, 4398, 4405, 4433, 4435, 4442, 4445, 4473, 4479, 4480, 4583, 4591, 4598, 4599, 4605, 4606, 4608, 4631, 4635, 4636, 4647, 4656 don't hold. That's 5 * 51 = 255 anti-implications. So one theorem on Equations would become 255 theorems on Laws!

We obviously also don't need all anti-implications because of transitivity (backwards), but I don't know if we want to split these sweeping counterexamples (as individual ¬ LawN.implies LawM theorems) ?Or do we want to encode the whole batch of non-implications as laws (using propositional logic), defering the "splitting up" to the computation of the transitive closure again for laws? Maybe someone here has a better idea what we should do?

[Andrés Goens]

e.g. if we have a magma that shows laws $L_1, L_2$ but not $L_3, L_4$ we could translate it to an implication like ¬(L₁ ∨ L₂ → L₃ ∨ L₄) but then we'd need to extend the implication definition on laws to express these disjunctions (and multiple laws), which I guess could be useful in the future? (there's also already satisfiesSet so it shouldn't be too difficult)

[Terence Tao]

One could do something like ∀ L L', L ∈ { L₁, L₂ } → L' ∈ { L₃, L₄ } → ¬(L→ L') perhaps?