BOOLEAN: Prove Theorem 5.8 (Sheffer stroke axiom)

[teorth]

The bare outline of a proof is sketched at https://teorth.github.io/equational_theories/blueprint/sect0004.html#sheffer , but one should refer to the paper https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf for more details. That proof is also computer assisted.

One should also locate the equation number for this equation (in principle this just requires running the generate_eqs_list.py script with EQ_SIZE = 6).

When done, mark the statement and proof of Theorem 5.8 with a \leanok, as well as a \lean{} tag.

[jjtowery]

claim

[jjtowery]

I'd like to give this a try starting tomorrow, but for now I ran generate_eqs_list.py with EQ_SIZE = 6 and it doesn't seem to have generated the equation in question: https://i.imgur.com/P98JAzp.png Is figuring out the number of the equation harder than just running the script? Is it a bug? Or did I just mess up?

[teorth]

Ah, there were some parentheses missing, the law should be x = (y ◇ ((x ◇ y) ◇ y)) ◇ (x ◇ (z ◇ y)). Can you find it now? I will fix the blueprint.

[jjtowery]

The equation number is 345169.

[teorth]

Great! If you are planning to update the blueprint in any event (e.g., to expand upon the sketch of proof currently given), you can certainly add the equation number there, and also add it to Equations.lean as part of your formalization.

[jjtowery]

I am going to temporarily shelf this until after midterms. My progress so far can be seen here: https://github.com/jjtowery/equational_theories/blob/main/equational_theories/Sheffer.lean and in these Vampire-generated proofs: https://github.com/jjtowery/equational_theories/blob/main/equational_theories/Generated/VampireProven/Sheffer.lean.

First with Sheffer_Equation345169 I show that the Sheffer stroke defined as (a ⊓ b)ᶜ satisfies the 345169. Then I show that 345169 implies the Sheffer axioms with Equation345169_implies_Axiom1, Equation345169_implies_Axiom2, and Equation345169_implies_Axiom3.

Vampire was easily able to do Equation345169_implies_Axiom1 and Equation345169_implies_Axiom2, but Equation345169_implies_Axiom3 it was not very happy with. I tried to goad it into doing Axiom3 by giving it some extra assumptions that I could then prove, but I ended up having to give it so much to do the calculation that it wasn't making it easier at all. I ended up going through the proof given in the paper until I got to something Vampire could do, with lots of Vampire sub-proofs along the way. Probably suboptimal, and I'm not sure how to get Vampire to do something nice like in the paper. Maybe someone more experienced could help.

I believe this is technically sufficient, but I'd like to properly 'close' off by showing a BooleanAlgebra structure from an operation that satisfies the Sheffer axioms with each operation defined in terms of NAND. This is probably unnecessary, but I'd like to try. Going off of how le_trans has been, this will probably need auto-generated proofs too.

This has been super fun to think about, I've learned a ton and have enjoyed it a lot. I will get back to this if no one else does.

[jjtowery]

disclaim

[teorth]

Thanks for all the work on this statement! Hopefully either you, or some other volunteer, will pick it up again later, but it is not time sensitive, and of course your midterms take priority. Glad you enjoyed the experience!

[codyroux]

This looks fun, though it looks like the hard work is already done by @jjtowery. I'll try to finish it up, should be standard stuff (the McCune &al paper refers to Sheffer's original paper!)

Not sure how to correctly make sure @jjtowery gets the credit, maybe fork and then let them PR?

[codyroux]

claim

[teorth]

You could add comments in the Lean code and in the commits indicating that @jjtowery 's code was used as a starting point.

[jjtowery]

Oh hey! I was thinking of starting this back up either tonight or tomorrow but if you'd like to finish it off, please do! I look forward to seeing what your solution is because this final part of building a BooleanAlgebra instance seemed a bit more involved than what was in Sheffer's paper.

[codyroux]

I mean I don't have a solution! I can easily leave it in your hands. It's just that this feels like pretty classic stuff: the Shaffer paper builds the "algebraic" version of what people traditionally call boolean algebra (e.g. here).

Then people separately define a <= b by a = a /\ b and prove that this is an order with the desired properties, in particular transitivity which should follow from a <= b <= c <==> a = a /\ b = a /\ b /\ c etc.

Not trivial stuff, but "textbook", though I can't say I have anything at home that details this. Probably any lattice theory textbook covers this.

I doubt I will have this finished by tomorrow though, so honestly if you wanna take a crack at this with the above hint, no worries.

[codyroux]

Ok I did the first half, that just leaves reducing the "equational presentation" of Boolean algebras (that I called "Boolean rings") to the 3 Shaffer laws.

https://github.com/codyroux/equational_theories/blob/codyroux/boolean-ring/equational_theories/BooleanRing.lean

I'll do that tomorrow, I think, unless @jjtowery wants to deliver the killing blow there.

This is actually quite fun! With the calc and conv tactics, you can almost exactly follow the paper proofs. Indeed it's much less tedious than doing this on paper, since there's no worry that you're getting it wrong.

[codyroux]

Almost done! The Sheffer laws imply that the magma is a boolean ring (I'm still not happy with the name) and a boolean ring is always a boolean algebra.

Now all that needs to be done is to tie it all together. I'll do that tonight, being careful to note the hard work of @jjtowery (I think over half by volume?).

I didn't use Vampire but I'm regretting it a bit. The paper proofs are quite nice though so no cleverness was required.

[codyroux]

Oh btw: the theorem is only true the magma is non-empty, of course (but Lean cares about these things).

[teorth]

Perhaps you can update the blueprint to indicate this. This is the sort of thing that having the formalization helps with. One could imagine a very subtle error in some long argument if nobody bothered to mention that non-emptiness had to be verified at some point in order to interpret this law as a Sheffer stroke.

[codyroux]

I'll do that later, perhaps, it's really the same thing as specifying that a group should have at least 1 element, I guess. Curiously, people often like boolean algebras to have at least 2 elements, (which Sheffer notes) but Mathlib does not.

[codyroux]

propose PR #708

[codyroux]

Hope I didn't bork the merge...