The biggest axiom in the world

In math the rules of a game are called axioms.  What's the longest axiom that people have ever thought about?

I'm not sure, but I have a candidate.  A lattice is a set with two operations called ∨ and ∧, obeying the 6 equations listed below.  But a while back people wondered: can you give an equivalent definition of a lattice using just one equation?   It's a pointless puzzle, as far as I can tell, but some people enjoy such challenges. 

And in 1970 someone solved it: yes, you can!   But the equation they found was incredibly long.

Before I go into details, I should say a bit about lattices.  The concept of a lattice is far from pointless - there are lattices all over the place! 

For example, suppose you take integers, or real numbers.  Let x ∨ y be the maximum of x and y: the bigger one.  Let x ∧ y be the minimum of x and y: the smaller one.  Then it's easy to check that the 6 axioms listed here hold.

Or, suppose you take statements.  Let p ∨ q be the statement "p or q", and let p ∧ q be the statement "p and q".  Then the 6 axioms here hold! 

For example, consider the axiom p ∧ (p ∨ q) = p.  If you say "it's raining, and it's also raining or snowing", that means the same thing as "it's raining" - which is why people don't usually say this. 

The two examples I just gave obey other axioms, too.  They're both distributive lattices, meaning they obey this rule:

p ∧ (q ∨ r) = (p ∧ q) ∨ (p ∧ r)

and the rule with ∧ and ∨ switched:

p ∨ (q ∧ r) = (p ∨ q) ∧ (p ∨ r)

But nondistributive lattices are also important.  For example, in quantum logic, "or" and "and" don't obey these distributive laws! 

Anyway, back to the main story.  In 1970, Ralph McKenzie proved that you can write down a single equation that is equivalent to the 6 lattice axioms.  But it was an equation containing 34 variables and roughly 300,000 symbols!  It was too long for him to actually bother writing it down.  Instead, he proved that you could, if you wanted to.

Later this work was improved.  In 1977, Ranganathan Padmanabhan found an equation in 7 variables with 243 symbols that did the job.  In 1996 he teamed up with William McCune and found an equation with the same number of variables and only 79 symbols that defined lattices.  And so on...

The best result I know is by McCune, Padmanbhan and Robert Veroff.  In 2003 they discovered that this equation does the job:

(((y∨x)∧x)∨(((z∧(x∨x))∨(u∧x))∧v))∧(w∨((s∨x)∧(x∨t)))  =  x

They also found another equation, equally long, that also works.

Puzzle: what's the easiest way to get another equation, equally long, that also defines lattices?

That is not the one they found - that would be too easy!

How did they find these equations?  They checked about a half a trillion possible axioms using a computer, and ruled out all but 100,000 candidates by showing that certain non-lattices obey those axioms.  Then they used a computer program called OTTER to go through the remaining candidates and search for proofs that they are equivalent to the usual axioms of a lattice. 

Not all these proof searches ended in success or failure... some took too long.  So, there could still exist a single equation, shorter than the ones they found, that defines the concept of lattice.

Here is their paper:

• William McCune, Ranganathan Padmanabhan, Robert Veroff, Yet another single law for lattices,

By the way:

When I said "it's a pointless puzzle, as far as I can tell", that's not supposed to be an insult.  I simply mean that I don't see how to connect this puzzle - "is there a single equation that does the job?" - to themes in mathematics that I consider important.  It's always possible to learn more and change ones mind about these things.

The puzzle becomes a bit more interesting when you learn that you can't find a single equation that defines distributive lattices: you need 2.  And it's even more interesting when you learn that among "varieties of lattices", none can be defined with just a single equation except plain old lattices and the one-element lattices (which are defined by the equation x = y).

By contrast, "varieties of semigroups where every element is idempotent" can always be defined using just a single equation.  This was rather shocking to me.

However, I still don't see any point to reducing the number of equations to the bare minimum!  In practice, it's better to have a larger number of comprehensible axioms rather than a single  complicated one.  So, this whole subject feels like a "sport" to me: a game of "can you do it?"

#spnetwork arXiv:math/0307284 #lattice #variety

Shared publiclyView activity