Ideas for unknown implications

Stream: Equational

[Pace Nielsen]

My student Parker Myers and I thought it would be fun to look at the list of unknown implications given here: https://github.com/amirlb/equational_theories/tree/unknown-implications

The first one on the list was Eqn9 => Eqn3. Here is a solution (showing that the implication holds) that we found, which may lead to some automated methods.

Eqn9 is x=x(xy) and Eqn3 is x=xx.

Assume by way of contradiction that Eqn9 holds but Eqn3 fails. Then there is some element 0 such that 0\neq 00. Taking x=y=0 in Eqn9, we get 0=0(00), or in other words 0=01. Next, taking x=0, y=1 in Eqn9 gives 0=0(0*1), or in other words 0=00, yielding the needed contradiction.

By the way, another open implication in the list was Eqn55 => Eqn3. This one is false, and a 3 element magma M (where M={0,1,2} and xy=y+1 mod 3) yields a counter-example. So I'm not sure if the unknown list has taken into account all of the small tables yet.

[Joachim Breitner]

Assume by way of contradiction that Eqn9 holds but Eqn3 fails. Then there is some element 0 such that 0\neq 00. Taking x=y=0 in Eqn9, we get 0=0(00), or in other words 0=01. Next, taking x=0, y=1 in Eqn9 gives 0=0(0*1), or in other words 0=00, yielding the needed contradiction.

Nice, but no need for a proof by contradiction, it can be phrased as two rewrites using Eqn9, simply by going x = x(x(xx)) = xx
(Often intuitive proofs by contradiction don’t need a contradiction and can be phrased simpler and more directly without.)

[Joachim Breitner]

The three element magma will be covered by automatic tools, at the latest tomorrow :-)

[Terence Tao]

By the way, I like this potential workflow in which progress can be modularized into a bunch of independent, but linked teams (we had a similar workflow for the Polymath8 gaps between primes project). Something like this:

• A "questions" team isolates interesting unresolved implications that are worth looking at (perhaps posted as Zulip threads, one for each implication (or cluster of implications)). This could involve using visualization tools or data analysis tools to isolate interesting portions of the implications graph.
• A "solver" team posts (to the aforementioned Zulip threads) human-readable solutions to implications produced by the "questions" team.
• An "abstraction" team abstracts out the metatheorems that the solutions produced from the "solver" team are special cases of (this could go in the blueprint, perhaps).
• A "formalizer" team proves the metatheorems from the abstraction team in Lean.
• A "run" team runs the metatheorems from the abstraction team against the unresolved implications to see which ones can get resolved, either as conjectures (of the formalizer team is not yet done with the metatheorem) or theorems. This would update the list of unresolved implications, thus looping back to the work of the questions team.

If there is enough interest, we could discuss actually trying to set up a structure like this. One particularly appealing feature of this structure for me personally is that each team could be led by a different group of people, in particular I myself would not need to be personally involved in each of these teams (or indeed in any of them, actually).

[Pace Nielsen]

@Joachim Breitner True. It is my understanding that one can always prove true implications between universal identities via rewrites. Contradiction is not, technically, needed.

My point was that perhaps instead of searching for rewrites, one could sometimes search through counter-example options, which may, in some cases, be faster than checking possible rewrites.

For example, another open implication on the list, studied by my student Katelyn Clark and me, is Eqn9 => Eqn100. This implication is also true, and thus will be provable with some clever substitutions (essentially repeating the substitutions you gave above to get x=x^2, and then plugging that in to Eqn9 to get Eqn 100). However, it is also easy to check it by the same argument as above, just checking options, after forcing Eqn100 to be false, and then trying to force Eqn9 to be true.

Here is another example, demonstrating this idea. Another open implication in the list is Eqn12 => Eqn4. Eqn4 is x=xy. Assuming this is false, then there are three cases to consider. (A) 0 0 = 1, (B) 0 1 = 1, or (C) 0 1 = 2 (for some distinct elements in the magma). Eqn12 is of the form x=x(yz).

First, consider Case A. Taking x=y=z=0 in Eqn 12, we get 0 1 = 0. Then taking x=y=0, z=1, we get 0 = 1, a contradiction.

Next, consider Case B. Taking x=y=0, z=1, we get 0 = 1, another contradiction.

Finally, consider Case C. [Indeed, we can do more, by assuming Cases A and B never occur, if we desire.] Taking x=y=0, z=1 in Eqn 12, we get 0 2 = 0. Then, taking x=y=0 and z=2 gives 1 = 2, another contradiction.

The point of all this is that this process of searching through cases can be automated, and may be easier than searching through possible rewrites.

[Terence Tao]

I've opened equational#185 to implement the first step of this strategy, which is to generate, for each X, a complete list of scenarios (up to relabeling) that would create a counterexample to EquationX. So, for instance, for X=4, one would list the scenarios 0 * 0 = 1, 0 * 1 = 1, and 0 * 1 = 2. The number of such scenarios may get excessive when EquationX is long with many variables, though; it may be that this strategy works best when the law in the equation is short or has very few variables.

[Amir Livne Bar-on]

How would this work for cases where a single cell in the multiplication table doesn't disprove a law? For example for x = x(xx) would a single counter-example look like 0 * (0 * 0) = 1 or like 0 * 0 = 1, 0 * 1 = 1?

[Leo Shine]

(Deleted)

[Leo Shine]

I may try it with equation 3053 next as it apparently has lots of unknown implications

[Terence Tao]

Amir Livne Bar-on said:

How would this work for cases where a single cell in the multiplication table doesn't disprove a law? For example for x = x(xx) would a single counter-example look like 0 * (0 * 0) = 1 or like 0 * 0 = 1, 0 * 1 = 1?

I guess it is safest to make the coarsest splitting, in this case 0 * (0 * 0) = 1. One can always split later into finer cases, in this case there would be three scenarios, 0 * 0 = 0; 0 * 0 - 1, 0 * 0 = 1, 0 * 1 = 1, and 0 * 0 = 2; 0 * 2 = 1, of which the first can be eliminated immediately, but I would imagine that for complex equations this splitting would create an undesirable combinatorial explosion.

[Pace Nielsen]

Using the newest list of unknown implications whose converse is proven I thought I'd try this method again.

At the end of the list is the open problem of whether Equation953, x = y ∘ ((z ∘ x) ∘ (z ∘ z)), implies Equation2, x = y. I'll show that it does (and hence 953, and also 954, 957, and perhaps some other related or reversed equations, are equivalent to 2).

Assume Equation 2 is false, so there are at least two elements 0 and 1. We break into two main cases.

Case 1: Suppose that 0 ∘ 0 = 0. Then taking x = z = 0 (in Equation 953) yields 0 = y ∘ 0. Then taking x = 1 and y = z = 0 yields 1 = 0.

Case 2: Suppose that 0 ∘ 0 = 1. There are three subcases.

Case 2a: 1 ∘ 1 = 0. Taking x = y = z = 0 yields 0 = 1.

Case 2b: 1 ∘ 1 = 1. Taking x = z = 0 and y = 1 yields 0 = 1.

Case 2c: 1 ∘ 1 = 2. First, taking x = z = 0 yields 0 = y ∘ 2. Then taking x = z = 1 yields 1 = y ∘ 0. Finally, taking x = 2, y = 0, and z = 1 yields 2 = 1.

[Terence Tao]

I wonder if this counterexample approach gives a new proof that 1689 implies 2. The current proof - due to Kisielewicz - is insanely long.

[Andrés Goens]

FWIW @Marcus Rossel found a very small (2 lines of Lean) proof of this, but using egg here

(I tried writing it out with calc and it's insanely longer than Kisielewicz's when spelled out)

[Andrés Goens]

not saying we should replace it, just thought it was an interesting data point in this context

[Terence Tao]

Opened equational#236 to formalize the 953->2 equivalence . I also wrote a slight rearrangement of the proof (with fewer case splittings) at https://teorth.github.io/equational_theories/blueprint/sect0003.html#953_equiv_2 which is perhaps more human-readable but less machine-findable. Hopefully the tooling to directly explore the known implication graph will come soon, so we can more easily identify implications that are worth directing human effort to complete.

[Pace Nielsen]

Terence Tao said:

I wonder if this counterexample approach gives a new proof that 1689 implies 2. The current proof - due to Kisielewicz - is insanely long.

My intuition leads me to believe that the two methods of proof in this context (i.e., substitution vs. case examination) are essentially rewrites of the same thing. However, in my experience, it is much more human understandable to discover the right case analysis than to find random-looking substitutions. So, I figured this would also hold for your question. It took a bit more work than in the other situations handled above, but it wasn't too difficult to find a human-discoverable proof of the implication (without any reference to other sources, such as Kisielewicz's paper). Here is a (mostly non-optimized) sketch. I'll write products using concatenation, for ease.

Step 1: First we'll show that 1689 in conjunction with xx=x yields x=y. Taking z=x in 1689, and simplifying using constancy of squaring yields x=(yx)x. By a change of variables, this means z=(xz)z. Thus Equation 1689 immediately simplifies to x=(yx)z. Taking y=x here, and simplifying using constancy of squaring, yields x=xz.

We now know that the semigroup is a left zero semigroup (i.e., the argument on the left of a product always wins). Thus 1689 transforms to x=y (since y is the left-most argument in the products on the right side of 1689).

Step 2: For the rest of the proof, we may fix distinct elements 0,1 such that 00=1, and try to derive a contradiction.

Case 2a: Suppose 10=0. Taking x=z=0 and y=1 in 1689 yields 0=1.

Case 2b: Suppose 10=1. Taking x=y=z=0 in 1689 yields 0=11. Then taking x=y=1 and z=0 yields 1=01. Switching the roles of 0 and 1 we reduce to Case 2a.

Case 2c: We must have 10=2. Taking x=y=z=0 yields 0=12. Taking x=z=0 and y=1 yields 0=22. (We now have 4 entries in our multiplication table permanently described.)

We are next going to consider the product 02.

Case 2ci: Suppose 02=0. We reduce to Case 2b by renaming 0-> 1 and 2-> 0.

Case 2cii: Suppose 02=2. We reduce to Case 2a under the same renaming.

Case 2ciii: Suppose 02=1. Taking x=y=0 and z=2 yields 0=2.

Case 2civ: We must have 02=3.

Taking x=z=2 and y=0 yields 2=33. Taking x=y=z=2 yields 2=03. (We now have six seven fixed entries.)

Finally taking x=0, y=1, and z=3 yields 0=2(23) while taking x=z=3 and y=0 yields 3=2(23), the final contradiction.

[Pace Nielsen]

Here is a (hopefully simple) question for you Lean experts out there. Would the case analysis above result in a shorter proof of 1689->2 than the current proof? [No need to actually type up such a proof, I'm just casually wondering what Lean experts would expect.]

[Terence Tao]

This paper by @Heather Macbeth is relevant here. The tradeoff between number of cases, and amount of "cleverness" in the argument, is different for human-readable proofs than machine-readable proofs. I think one could maybe make your new proof conceptually simpler, but longer in absolute length, in Lean by splitting quite maximally into cases, expanding out all potential specializations of the identity, and applying simplification and equality closure tactics. Whether this is a"better" proof than the existing options would be a matter of opinion.

I'm curious whether this particular implication 1689 -> 2 was also within reach of Vampire.

[Daniel Weber]

Vampire can prove it, yes:

@[equational_result]
theorem Equation1689_implies_Equation2 (G : Type*) [Magma G] (h : Equation1689 G) : Equation2 G := by
  by_contra nh
  simp only [not_forall] at nh
  obtain ⟨sK0, sK1, nh⟩ := nh
  have eq9 (X0 X1 X2 : G) : ((X1 ◇ X0) ◇ ((X0 ◇ X2) ◇ X2)) = X0 := mod_symm (h ..)
  have eq10 : sK0 ≠ sK1 := mod_symm nh
  have eq11 (X1 X2 X3 : G) : ((X1 ◇ X2) ◇ X2) = (X1 ◇ ((((X1 ◇ X2) ◇ X2) ◇ X3) ◇ X3)) := superpose eq9 eq9 -- superposition 9,9, 9 into 9, unify on (0).2 in 9 and (0).1.1 in 9
  have eq12 (X0 X1 X2 X3 : G) : (X0 ◇ X1) = ((X3 ◇ (X0 ◇ X1)) ◇ (X1 ◇ ((X1 ◇ X2) ◇ X2))) := superpose eq9 eq9 -- superposition 9,9, 9 into 9, unify on (0).2 in 9 and (0).1.2.1 in 9
  have eq15 (X0 X1 X2 : G) : ((X0 ◇ X1) ◇ X1) = (X0 ◇ (X1 ◇ ((X1 ◇ X2) ◇ X2))) := superpose eq9 eq11 -- superposition 11,9, 9 into 11, unify on (0).2 in 9 and (0).2.2.1 in 11
  have eq17 (X0 X1 X2 X3 : G) : ((X3 ◇ X0) ◇ (((X0 ◇ X1) ◇ X1) ◇ ((((X0 ◇ X1) ◇ X1) ◇ X2) ◇ X2))) = X0 := superpose eq11 eq9 -- superposition 9,11, 11 into 9, unify on (0).2 in 11 and (0).1.2.1 in 9
  have eq24 (X1 X2 X3 X4 : G) : (X2 ◇ ((X2 ◇ X3) ◇ X3)) = ((X1 ◇ X2) ◇ (((X2 ◇ X3) ◇ X3) ◇ ((((X2 ◇ X3) ◇ X3) ◇ X4) ◇ X4))) := superpose eq12 eq12 -- superposition 12,12, 12 into 12, unify on (0).2 in 12 and (0).2.1 in 12
  have eq26 (X0 X1 X2 X3 X4 : G) : (X3 ◇ X0) = ((X4 ◇ (X3 ◇ X0)) ◇ (X0 ◇ (((X0 ◇ X1) ◇ X1) ◇ ((((X0 ◇ X1) ◇ X1) ◇ X2) ◇ X2)))) := superpose eq11 eq12 -- superposition 12,11, 11 into 12, unify on (0).2 in 11 and (0).2.2.2.1 in 12
  have eq28 (X0 X1 X2 X3 X4 : G) : ((X1 ◇ X2) ◇ (X2 ◇ ((X2 ◇ X3) ◇ X3))) = ((X0 ◇ (X1 ◇ X2)) ◇ ((((X1 ◇ X2) ◇ (X2 ◇ ((X2 ◇ X3) ◇ X3))) ◇ X4) ◇ X4)) := superpose eq12 eq11 -- superposition 11,12, 12 into 11, unify on (0).2 in 12 and (0).1.1 in 11
  have eq32 (X2 X3 : G) : (X2 ◇ ((X2 ◇ X3) ◇ X3)) = X2 := superpose eq17 eq24 -- forward demodulation 24,17
  have eq37 (X0 X1 : G) : (X0 ◇ X1) = ((X0 ◇ X1) ◇ X1) := superpose eq32 eq15 -- backward demodulation 15,32
  have eq41 (X0 X1 X2 : G) : ((X1 ◇ X0) ◇ (X0 ◇ X2)) = X0 := superpose eq37 eq9 -- backward demodulation 9,37
  have eq42 (X1 X2 X3 : G) : (X1 ◇ X2) = (X1 ◇ (((X1 ◇ X2) ◇ X3) ◇ X3)) := superpose eq37 eq11 -- backward demodulation 11,37
  have eq44 (X1 X2 X3 : G) : (X1 ◇ X2) = (X1 ◇ ((X1 ◇ X2) ◇ X3)) := superpose eq37 eq42 -- forward demodulation 42,37
  have eq47 (X0 X1 X2 X3 X4 : G) : (X3 ◇ X0) = ((X4 ◇ (X3 ◇ X0)) ◇ (X0 ◇ (((X0 ◇ X1) ◇ X1) ◇ X2))) := superpose eq44 eq26 -- forward demodulation 26,44
  have eq48 (X0 X1 X2 X3 X4 : G) : (X3 ◇ X0) = ((X4 ◇ (X3 ◇ X0)) ◇ (X0 ◇ ((X0 ◇ X1) ◇ X2))) := superpose eq37 eq47 -- forward demodulation 47,37
  have eq49 (X0 X1 X3 X4 : G) : (X3 ◇ X0) = ((X4 ◇ (X3 ◇ X0)) ◇ (X0 ◇ X1)) := superpose eq44 eq48 -- forward demodulation 48,44
  have eq50 (X0 X1 X2 X3 X4 : G) : ((X1 ◇ X2) ◇ (X2 ◇ ((X2 ◇ X3) ◇ X3))) = ((X0 ◇ (X1 ◇ X2)) ◇ (((X1 ◇ X2) ◇ (X2 ◇ ((X2 ◇ X3) ◇ X3))) ◇ X4)) := superpose eq37 eq28 -- forward demodulation 28,37
  have eq51 (X0 X1 X2 X4 : G) : ((X0 ◇ (X1 ◇ X2)) ◇ (X2 ◇ X4)) = X2 := superpose eq41 eq50 -- forward demodulation 50,41
  have eq52 (X0 X3 : G) : (X3 ◇ X0) = X0 := superpose eq51 eq49 -- backward demodulation 49,51
  have eq57 (X0 X2 : G) : (X0 ◇ (X0 ◇ X2)) = X0 := superpose eq52 eq41 -- backward demodulation 41,52
  have eq61 (X0 X2 : G) : (X0 ◇ X2) = X0 := superpose eq52 eq57 -- forward demodulation 57,52
  have eq75 (X0 X1 : G) : X0 = X1 := superpose eq61 eq52 -- superposition 52,61, 61 into 52, unify on (0).2 in 61 and (0).1 in 52
  have eq77 (X0 : G) : sK0 ≠ X0 := superpose eq75 eq10 -- superposition 10,75, 75 into 10, unify on (0).2 in 75 and (0).2 in 10
  subsumption eq77 eq75

[Terence Tao]

Impressive. It seems to have taken a somewhat different path than the Kisielewicz proof. I recognize eq41 as the central groupoid law (Equation168). but don't know what conclusions to draw from that.