Constructing a database of finite counterexamples

Stream: Equational

[Fox Room]

Okay, so, we obviously don't have a finite counterexample for all non-implications, but an interesting data-investigation tool along the lines of the equation explorer would be some kind of database of what pairs of equations have finite counterexamples, along with providing explicitly the finite counterexample. I'm interested in such a database (potentially integrated with the equation explorer) in the hope of completing more of these (admittedly necessarily very large number of) statements.

I would like to contribute towards this goal but unfortunately there's not much I can do other than rather naive approaches of looking for particularly powerful counter-implications. For instance, I could pick out an equation, then look for the non-implied equations that are highest on the implication graph and plug them into Mace4 to try to produce a counterexample for everything in that implication chain. Does anyone have any partial data to put forth, or an idea on how to turn any data into a database?

[Bruno Le Floch]

We know exactly which implications have finite counterexamples: this is (the complement of) the finite implication graph. The script extra_implications can be used to list all implications. Running lake exe extract_implications --finite-only --closure > /tmp/implications.txt in the top directory of the project gives a 22 million line file, with nonimplications written as ¬ (Equation1 → Equation2). Without --closure the file is only half a million lines and is mostly the reduced graph, but it might not be complete (github.com/teorth/equational_theories#1245).

[Vlad Tsyrklevich]

Okay, so, we obviously don't have a finite counterexample for all non-implications

I'm not sure I understand this, for all non-implications with a finite counter-example (except for the one unknown) we do have an explicit counter-example. It is not directly shown in the equation explorer, but you can find it by looking at 'Show proof'

[Vlad Tsyrklevich]

I just re-read this comment and noticed that I should have specified that for this to work you should be on the Display the finite graph view of the explorer

[Fox Room]

Oh, huh?
Hold on

[Fox Room]

Hm, I can't figure out how to find them.
I just get a list of implications. I know we know which HAVE a finite counterexample but I can't actually find the counterexamples! If these are actually accessible, how do I get to them?

[Matthew Bolan]

You click on show proof, and the steps in the proof will link you to where they are proven. One of these (the anti-implication arrow in particular) will be the counterexample.

[Fox Room]

I just get a long string of numbers that are definitely not encoding a magma's multiplication table.

[Fox Room]

I may just not know how to read what I'm looking at, but it seems to me to just be equation numbers.

[Matthew Bolan]

Well, the different files are laid out differently, but my guess is that you are looking at an implication falsified by a 2x2 magma, in which case if you scroll to the top of the file you'll find the corresponding magma.

[Fox Room]

I can't find a single one laid out in that manner.

[Matthew Bolan]

Which two laws are you currently looking at

[Fox Room]

I just looked at commutativity (43) does not imply associativity (4512) but as I said, nothing I've randomly clicked on has any magma I can recognize as such. This one at least has a polynomial which presumably can be translated into a magma in some manner I'm not familiar with.

[Matthew Bolan]

Yes, this is saying that $(\mathbb Z / 3 \mathbb Z, \diamond)$ where $x \diamond y := x^2 + y^2 + 2x + 2y + xy \pmod 3$ is a counterexample.

[Fox Room]

oh, okay, that's easy enough to construct. Oh, and I've just figured out what you meant by the 2x2 ones.

[Fox Room]

So it seems like the data is, in fact, there, but it'd still be worthwhile to explicitly construct the magma in question in each case since this involves some nontrivial algebraic work

[Fox Room]

I envisioned it directly linking to the magma in finite magma explorer, actually

[Matthew Bolan]

It would be worth it to have everything in the same format, currently there are maybe 4/5 different formats. The finite magma explorer sounds nice.

[Fox Room]

I am tempted to just start manually collating a list, but considering I know there's about six million nonimplications there's no real point doing that.

[Matthew Bolan]

Well, most of those are falsified by the same magmas. I don't expect you'll need more than a few thousand individual magmas.

[Fox Room]

Oh, yeah, true, like I noted already. I should just look for those "heavy-hitting" counterexamples.

[Vlad Tsyrklevich]

It’ll probably just be the smallest ones given that they’re the most likely to both satisfy and not satisfy many laws at once

[Kevin Buzzard]

What's the smallest number of finite magmas which you need to falsify every false implication? :-)

[Kevin Buzzard]

The smallest "separating set" for the 4000-or-so equations?

[Alex Meiburg]

At most 1414: there are 1415 equations, up to equivalence relation, and you can separate each equation from an arbitrary number of non-implications with a single finite magma. (Take the counter examples that A-/->B1, A-/->B2, etc. and take their direct product. This still obeys A and does not obey any of the Bi.)

[Fox Room]

That's cheating though, since you still have to find the factors
Also that seems like a basic fact I really should know but didn't. Proof?

[Alex Meiburg]

I don't know what you mean by cheating. It would be very easy to construct these 1414 counterexamples from what is already in the equational_theories repo.

[Alex Meiburg]

For each A, take each Bi that it doesn't imply; there is some counterexample in the repo that shows A -/-> Bi. Then take the direct product of these.

[Alex Meiburg]

(This could even be verified efficiently in Lean: not by providing the explicit multiplication table, but by describing abstractly "these k-tuples that operate coordinate-wise according to these tables", and then studying that.)

[Fox Room]

Alex Meiburg said:

I don't know what you mean by cheating. It would be very easy to construct these 1414 counterexamples from what is already in the equational_theories repo.

Well I suppose it depends on your motivation for considering the "smallest separating set", but my motivation for considering 'heavy hitting counterexamples' was for ease of information and having to explicitly calculate less, so if you have to calculate two factors it doesn't really matter if they can be combined into a single model. But it's true that it does technically make the list of counterexamples smaller, so if that's all you cared about then sure.

[Fox Room]

In any case, I assume it's a well known result, but it isn't obvious to me as a non-mathematician that a product magma preserves all 1415 equations, that's what I meant by proof.

[Alex Meiburg]

I agree that it's not a construction that gives small, or illuminating, proofs. I was just thinking about Kevin Buzzard's question. :)

The fact is not hard to prove: if M1 and M2 satisfy an equation E, then their direct product also satisfies E. This is because everything (the magma operation, and the definition of equality) goes compnent-wise.

And, conversely, if M1 does not satisfy an equation E, then (regardless of whether M2 does or not) the direct product of M1 and M2 doesn't satisfy E either. Simply take any assignment of values x, y, z from M1 that fail to obey E, and an arbitrary element t from M2, and check the equation on the pairs (x,t), (y,t), (z,t). If the equation held, then it would also hold on the first coordinate, which we know it doesn't.

(This requires M2 to be non-empty; obviously if it is empty, then the direct product is empty, and it obeys all equations.)

[Fox Room]

Oh, right, duh, because we're talking specifically about equational laws so there's no first order existential quantification nonsense. Yes, that is actually somewhat obvious, I'm just slow.