Infinite counterexamples

Stream: Equational

[Bruno Le Floch]

In various ATP explorations of whether an implication A⊨B holds (Higman-Neumann, conjunctions X∧Y, …), we search for a proof, and for finite counter-models. For Austin implications (that hold in finite magmas and fail for infinite magmas) neither side can succeed, regardless of computational power. Sometimes we can find proofs of finite implications by adding the property that injectivity ⇔ surjectivity for some specific functions (left/right multiplications, squaring, …). But to prove the non-implication for infinite magmas we need to construct infinite counterexamples. Are there any classes of infinite counterexamples that can be explored automatically? AFAIK, linear models cannot be interesting since they can always be reduced to large finite fields?

Concrete questions: how can I refute by an infinite magma construction the following implications that hold in finite magmas?

• (3 x=x◇x)∧(73 x = y ◇ (y ◇ (x ◇ y))) ⊨ (125 x = y ◇ ((y ◇ x) ◇ y)) ,
• (42323216 x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))) ⊨ (67953691 x = (y ◇ y) ◇ (y ◇ ((x ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))))

[Matthew Bolan]

One way to look for such techniques is to look at how we found counterexamples to implications true for finite magmas. An obvious standout is the greedy approach, as automated by Daniel Weber. Another is checking free magmas by finding a complete rewriting system. I think there also were some translation invariant models, which might be automatable given some ansatz, though I don't know if anyone has automated them for infinite magmas.

I doubt it will help with your implications, but infinite dimensional linear models can be interesting even when finite dimensional linear models are not, and this avoids any model theory tricks. For an example of this in the main project, there are linear counterexamples to the implication $1117 \to 2441$ (see #Equational > Outstanding equations, v1 @ 💬 ), even though this implication holds for finite magmas.

[Bruno Le Floch]

Thanks @Matthew Bolan. Indeed, infinite-dimensional linear models don't reduce to finite models, I hadn't realized that. Regarding Daniel Weber's code in equational_theories/Generated/Greedy/src/forcer.py, I managed to run it but haven't yet decoded what its output (like [Rule([[0, 1, 2], [0, 1, 3]], [2, 3]), Rule([[0, 1, 2], [0, 2, 3]], [3, 0, 1]), Rule([[0, 0, 1], [0, 1, 2]], [0, 2, 0])]) means. Maybe I can get away with using the whole pipeline all the way to Lean without understanding the intermediate steps precisely.

[Matthew Bolan]

@Bruno Le Floch If I recall correctly, Rule([[0, 1, 2], [0, 1, 3]], [2, 3]) means that if we have defined $0 \diamond 1 = 2$ and $0 \diamond 1 = 3$, then we must have $2 = 3$. Rule([[0, 1, 2], [0, 2, 3]], [3, 0, 1]) means that if we have already defined $0\diamond 1 = 2$ and $0 \diamond 2 = 3$, then we must have $3 \diamond 0 = 1$. Also its likely that this conversation should be moved to a separate thread.

[Notification Bot]

4 messages were moved here from #Equational > Thoughts and impressions thread by Bruno Le Floch.

[Bruno Le Floch]

For reference, #Equational > Equation 65 -> left cancellability @ 💬 is a good starting point to read up on Daniel Weber's greedy construction automation. I don't think there is any documentation.