Using Mathematica to Understand the Computer Proof of the Robbins Conjecture

Branden Fitelson

fitelson@students.wisc.edu



Department of Philosophy
University of Wisconsin–Madison
600 North Park Street
Madison, WI  53706
 


December 14, 1997

Introduction1

In October 1996, Bill McCune et al at Argonne National Laboratory made national headlines (see Kolata (1996) and Peterson (1997)) with their computer proof of the long-standing Robbins conjecture.  The Robbins conjecture had stumped some of the world's best mathematicians for over 60 years.  Amazingly, the Argonne team's automated theorem-proving program EQP took only 8 days to find a proof of it.  Unfortunately, the proof found by EQP is quite complex and difficult to follow.  Some of the steps of the EQP proof require highly complex and unintuitive substitution strategies.  As a result, it is nearly impossible to reconstruct or verify the computer proof of the Robbins conjecture entirely by hand.  This is where the unique symbolic capabilities of Mathematica 3 come in handy.  With the help of Mathematica, it is relatively easy to work out and explain each step of the dense EQP proof in detail.  In this paper, I use Mathematica to provide a detailed, step-by-step reconstruction of the highly complex EQP proof of the Robbins conjecture.

Preliminaries: Boolean Algebra—Definition and Notation

The first strictly axiomatic definitions of Boolean algebra were surveyed by E.V. Huntington (1904)((.)^2)  Huntington (1904) presents four axiomatizations of Boolean algebra.  The first Huntington axiomatization, which is closest to Boole's original system (Kneale and Kneale 1962, page 423), and which is often taken as definitive of Boolean algebra (Stoll 1963, page 249), is as follows
 
Definition.  A Boolean algebra is a 6-tuple ⟨B, ⊕, ⊗, (OverBar[•]), 0, 1⟩, where B is a set, ⊕ is a binary relation (usually called union, join, or disjunction) in B, ⊗ is a binary relation in B (usually called intersection, meet, or conjunction), (OverBar[•]) is a function from B into B (usually called complementation or negation), 0 and 1 are distinct elements of B, and the following five conditions are satisfied

(i)  The operations ⊕ and ⊗ are associative: for all a, b, c ∈ B

a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c        and        a ⊗ (b ⊗ c) = (a ⊗ b) ⊗ c

(ii)  The operations ⊕ and ⊗ are commutative: for all a, b ∈ B

a ⊕ b = b ⊕ a        and        a ⊗ b = b ⊗ a

(iii)  Each of the operations ⊕ and ⊗ distributes over the other: for all a, b, c ∈ B

a ⊕ (b ⊗ c) = (a ⊕ b) ⊗ (a ⊕ c)        and        a ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)

(iv)  For all a ∈ B,

a ⊕ 0 = a        and       a ⊗ 1 = a

(v)  For each a ∈ B, there exists an element (OverBar[a]) ∈ B such that

a ⊕ (OverBar[a]) = 1        and       a ⊗ (OverBar[a]) = 0

In the context of Boolean logic, for instance, ⊕ is disjunction (typically denoted by ⋁), ⊗ is conjunction (typically denoted by ⋀), and (OverBar[•]) is negation (typically denoted by ¬).  Moreover, in Boolean logic, the elements 0 and 1 denote contradiction (e.g., p ⋀ ¬ p) and tautology (e.g., p ⋁ ¬ p), respectively.  With these terminological preliminaries out of the way, we are ready to begin our brief sketch of the history of the Robbins conjecture.

A Brief History of the Robbins Conjecture

Almost thirty years after his seminal 1904 paper, Huntington (1933a and 1933b) discovered the following greatly simplified three axiom basis for Boolean algebra, which only requires the single binary relation ⊕((.)^3)

	x ⊕y=y ⊕x					[Commutativity of ⊕]
	(x ⊕y) ⊕z=x ⊕(y ⊕z)			[Associativity of ⊕]
	(OverBar[(OverBar[x]) ⊕y])⊕(OverBar[(OverBar[x]) ⊕(OverBar[y])]) =x 				[Huntington equation]

Shortly thereafter, Herbert Robbins conjectured that if the Huntington equation were replaced with the following equation, which, in any Boolean algebra, is equivalent to the Huntington equation (see the Appendix for a one-line Mathematica proof of this equivalence) 

	(OverBar[(OverBar[x ⊕y])⊕(OverBar[x ⊕(OverBar[y])])]) =x				[Robbins equation]

then the resulting axiomatization would also be characteristic of Boolean algebra.  This is the Robbins conjecture.  Robbins and Huntington could not find a proof of (or a counterexample to) the Robbins conjecture.  The problem was later studied intensively by Tarski and his students (Tarski et al 1971, problem 1.1).

Algebras satisfying commutativity, associativity, and the Robbins equation are known as Robbins algebras.  It is easy to show that every Boolean algebra is a Robbins algebra (see the Appendix for an elegant Mathematica proof of this), so the interesting question is "Are all Robbins algebras Boolean?".  In other words, can the Huntington equation be derived from commutativity, associativity, and the Robbins equation? 

Until the late 1970's, very little progress was made toward resolving the Robbins conjecture.  In 1979, S. Winker at Argonne National Laboratory began looking for Boolean conditions that are sufficient to make any Robbins algebra Boolean.  With the help of Argonne's automated theorem-provers, many such sufficient Boolean conditions were found.  For instance, the double negation condition

	(OverBar[(OverBar[x])]) = x						[Double negation]

can easily be shown to make any Robbins algebra Boolean (see the Appendix for a Mathematica proof).  Unfortunately, these first Boolean conditions found by Winker proved to be too strong, in the sense that they were almost as difficult to deduce from the Robbins axioms as the Huntington equation itself!  As a result, these early Winker conditions (e.g., double negation) were not very useful for resolving the Robbins conjecture.  So, Winker set out to find logically weaker sufficient conditions.  Ultimately, Winker (1992) was able to show  that  the surprisingly weak condition

	(∃C) (∃D) (OverBar[C ⊕D])=(OverBar[C])			[Winker condition]

also suffices, with proofs by hand using insight from theorem-prover searches.

Since then, the problem has received continued attention from mathematicians and computer scientists, but until October 1996, no significant mathematical progress on the problem was made.

The Computer Proof of the Robbins Conjecture

The proof that solves the Robbins problem was found on October 10, 1996, by Bill McCune et al at Argonne, using their mechanical theorem-prover EQP\(TraditionalForm\`\(.\^4\)\)   EQP is similar in many ways to the more well known Argonne theorem-prover Otter\(TraditionalForm\`\(.\^5\)\)  EQP proved that every Robbins algebra satisfies the Winker condition, by refuting the following pair of assumptions 

	\(\(\(x⊕y\)\&_⊕\(x⊕y\&_\)\&_
                  \)\&_\  = x\)				[Robbins equation]
	(OverBar[x ⊕y])≠(OverBar[x]) 					[Denial of the Winker condition]

It follows immediately from this and Winker's work that all Robbins algebras are Boolean (i.e., that the Robbins conjecture is true).  The successful proof search took about 8 days on an RS/6000 computer and used about 30 megabytes of memory.

Unfortunately, the 16-line proof object generated by EQP is very cryptic and complex.  Moreover, EQP does not provide any information about how each line in the proof object follows from previous lines.  This makes verifying the EQP proof object quite a daunting task for a mere human.  Below, I will illustrate how Mathematica can be used to make human verification and explanation of the EQP proof object more tractable.

The EQP Proof Object: EQP Notation vs Mathematica 3 Notation

The main problem with the EQP proof object is that it uses the one-dimensional notation "n(x)" instead of Boole's two-dimensional notation "\(TraditionalForm\`x\&_\)" for denoting the complementation (or negation) operator\(TraditionalForm\`\(.\^6\)\)  This makes it almost impossible to keep track of the highly complex and deeply nested syntactical patterns that occur in the computer proof of the Robbins conjecture.  By allowing us to work directly with Boole's more visually perspicuous 2-D notation, Mathematica 3 makes it much easier for us to see what is going on in the EQP proof.   

Below, I have included the entire 16-line EQP proof object, first in EQP notation, then in Mathematica 3 notation.  Notice how difficult it is to comprehend (or even parse!) the lines written in EQP notation, as compared to Mathematica 3 notation (especially, the extremely complex line 15).  And, notice how little EQP tells us about how each line can be derived from previous lines.  The bracketed lists of line numbers after each line tell us which previous lines in the proof were used in the derivation of the present line.  EQP tells us nothing about how these derivations were performed (i.e., which substitutions were made in which lines, etc.).  These "hints" are very sketchy.  But, as I will demonstrate below, these sketchy "hints" provide sufficient information for us (with a lot of help from Mathematica) to reconstruct a detailed proof.

The EQP Proof Object in EQP Notation\(TraditionalForm\`\^7\)

1. n(n(x⊕y)⊕n(y⊕n(x)))==y        [Assumption: the Robbins equation]
			
2. n(y⊕n(y⊕n(x)⊕n(x⊕y)))==n(x⊕y)        [1]
			
3.  n(y⊕n(x⊕y⊕n(y⊕n(x))))==n(y⊕n(x))        [1]

4.  n(n(y⊕n(x))⊕n(x⊕y⊕y⊕n(y⊕n(x))))==y	        [1, 3]

5.  n(n(y⊕z)⊕n(z⊕n(y⊕n(x))⊕n(x⊕y⊕y⊕n(y⊕n(x)))))==z        [1, 4]

6.  n(y⊕n(x⊕y⊕y⊕n(y⊕n(x))⊕n(y⊕n(x))))==n(y⊕n(x))        [1, 4]

7.  n(n(y⊕n(x))⊕n(x⊕y⊕y⊕y⊕n(y⊕n(x))⊕n(y⊕n(x))))==y        [1, 6]

8.  n(z⊕n(z⊕n(y⊕z)⊕n(y⊕n(x))⊕n(x⊕y⊕y⊕n(y⊕n(x)))))==n(y⊕z)        [1, 5]

9.  n(n(u⊕n(y⊕z))⊕n(u⊕z⊕n(z⊕n(y⊕z)⊕n(y⊕n(x))⊕n(x⊕y⊕y⊕n(y⊕n(x))))))==u        [1, 8]

10.  n(x⊕n(x⊕x⊕x⊕n(x⊕n(x))))==n(x⊕n(x))        [1, 2, 9]

11.  n(n(y⊕n(x⊕n(x)))⊕n(x⊕y⊕n(x⊕x⊕x⊕n(x⊕n(x)))))==y        [1, 10]

12.  n(n(x⊕n(x))⊕n(x⊕x⊕x⊕x⊕n(x⊕n(x))))==x        [1, 10]

13.  n(x⊕n(x⊕x⊕x⊕x⊕n(x⊕n(x))⊕n(x⊕n(x))))==n(x⊕n(x))        [1, 12]

14.  n(n(y⊕n(x⊕n(x)))⊕n(x⊕y⊕n(x⊕x⊕x⊕x⊕n(x⊕n(x))⊕n(x⊕n(x)))))==y	        [1, 13]

15.  n(x⊕n(x⊕n(x⊕x⊕x⊕n(x⊕n(x)))⊕n(x⊕x⊕x⊕x⊕n(x⊕n(x))⊕n(x⊕n(x)))))==
	n(x⊕x⊕x⊕x⊕n(x⊕n(x))⊕n(x⊕n(x)))        [7, 11]

16.  n(x⊕x⊕x⊕x⊕n(x⊕n(x))⊕n(x⊕n(x)))==n(x⊕x⊕x⊕n(x⊕n(x)))        [4, 14, 15]

The EQP Proof Object in Mathematica 3 Notation

1.    (OverBar[(OverBar[x ⊕y]) ⊕(OverBar[y ⊕(OverBar[x])])])==y        [Assumption:  the Robbins Equation]
			
2.  (OverBar[y ⊕(OverBar[y ⊕ (OverBar[x]) ⊕ (OverBar[x ⊕y])])])==(OverBar[x ⊕y])        [1]
			
3.  (OverBar[y ⊕(OverBar[x ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])==(OverBar[y ⊕(OverBar[x])])        [1]

4.  (OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])==y       [1, 3]

5.  (OverBar[(OverBar[y ⊕z]) ⊕(OverBar[z ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])])==z        [1, 4]

6.  (OverBar[y ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[y ⊕(OverBar[x])])])])==(OverBar[y ⊕(OverBar[x])])        [1, 4]

7.  (OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[y ⊕(OverBar[x])])])])==y        [1, 6]

8.  (OverBar[z ⊕(OverBar[z ⊕(OverBar[y ⊕z]) ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])])==(OverBar[y ⊕z])        [1, 5]

9.  (OverBar[(OverBar[u ⊕(OverBar[y ⊕z])]) ⊕(OverBar[ u ⊕z ⊕(OverBar[z ⊕(OverBar[y ⊕z]) ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])])])==u        [1, 8]

10.  (OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])==(OverBar[x ⊕(OverBar[x])])        [1, 2, 9]

11.  (OverBar[(OverBar[y ⊕(OverBar[x ⊕(OverBar[x])])]) ⊕(OverBar[x ⊕y ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])])==y        [1, 10]

12.  (OverBar[(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])==x        [1, 10]

13.  (OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])])==(OverBar[x ⊕(OverBar[x])])        [1, 12]

14.  (OverBar[(OverBar[y ⊕(OverBar[x ⊕(OverBar[x])])]) ⊕(OverBar[x ⊕y ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])])])==y        [1, 13]

15. (OverBar[x ⊕(OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])]) ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])])])==(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])]) 
													[7, 11]

16.  (OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])==(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])        [4, 14, 15]

Using Mathematica to Decipher the EQP Proof Object

Encoding The Robbins Axioms in Mathematica 3

Encoding the Commutativity and Associativity of ⊕

We can tell Mathematica to assume only that ⊕ is commutative (viz., Orderless) and associative (viz., Flat), as follows\(TraditionalForm\`\(.\^8\)\)

Attributes[CirclePlus] = {Orderless, Flat};

In my reconstruction of the EQP proof, I will just let Mathematica automatically make use of the commutativity and associativity of ⊕.  I will not explicitly announce which steps depend on these two basic properties of ⊕.  This will allow us to focus our attention on the more interesting and important logical role played by the Robbins equation itself\(TraditionalForm\`\(.\^9\)\)

Encoding the Robbins Equation—Two Handy Mathematica Constructs

The two-place function RobbinsExpand allows us to logically expand x (in terms of any y) in accordance with the Robbins equation.  In other words, for any x and y, RobbinsExpand[x,y] =  (OverBar[(OverBar[x⊕y])⊕(OverBar[x⊕(OverBar[y])])])  = x.  Thus, RobbinsExpand[x,y] allows us to create arbitrary Robbins-equivalents of any formula x.  The one-place function RobbinsSimplify automatically simplifies Mathematica expressions containing instances of the Robbins pattern.

RobbinsExpand[x_,y_]=(OverBar[(OverBar[x⊕y])⊕(OverBar[x⊕(OverBar[y])])]);RobbinsSimplify[expr_]:=expr//.(OverBar[(OverBar[x__⊕y__])⊕(OverBar[x__⊕(OverBar[y__])])]):>x;

Here is a simple example that illustrates how RobbinsExpand and RobbinsSimplify allow us to expand/simplify Mathematica expressions in accordance with the Robbins equation.

RobbinsExpand[a,b]⊕ RobbinsExpand[b,a]

% // RobbinsSimplify

Now that we have encoded commutativity, associativity and the Robbins equation in Mathematica 3, we are ready to tackle the EQP proof of the Winker Condition, line-by-line.

Deciphering the EQP Proof of the Winker Condition Line–By–Line

Line 1 of the EQP Proof—The Robbins Equation

Line 1 of the EQP proof is just the Robbins equation, as discussed above

ProofLine[1]=(OverBar[(OverBar[x⊕y])⊕(OverBar[y⊕(OverBar[x])])])==y

Line 2 of the EQP Proof—The first (of many) cryptic substitution strategies

Line 2 of the EQP proof is

ProofLine[2]=(OverBar[y⊕(OverBar[y⊕(OverBar[x])⊕(OverBar[x⊕y])])])==(OverBar[x⊕y])

Line 2 of the proof says that  (OverBar[x⊕y]) = (OverBar[y⊕(OverBar[y⊕(OverBar[x])⊕(OverBar[x⊕y])])]).  All we are told by EQP is that line 2 follows (somehow) from the Robbins equation (i.e., line 1).  The only way to go from the Robbins equation to line 2 is by creating a Robbins–equivalent of (OverBar[x⊕y]) using RobbinsExpand[(OverBar[x⊕y]),y], for some y.  The question is which y is such that RobbinsExpand[(OverBar[x⊕y]),y] yields the desired formula (OverBar[y⊕(OverBar[y⊕(OverBar[x])⊕(OverBar[x⊕y])])])?  

As with any good proof-theoretic question of this kind, the answer involves a neat trick.  In this case, the relevant trick is very difficult to figure out (or even see) without Mathematica's help.  Mathematica enabled me to  experiment with many candidate formulas in a very short period of time (a task that would be nearly impossible to undertake with pencil and paper).  After trying several substitution strategies, I discovered the following crucial Robbins-equivalent of (OverBar[x⊕y])

RobbinsExpand[(OverBar[x⊕y]),(OverBar[x])⊕y]

The two-dimensional Mathematica notation makes it relatively easy to see that the expression RobbinsExpand[(OverBar[x⊕y]),(OverBar[x])⊕y] contains two distinct instances of the Robbins pattern.  By definition, the entire expression is an instance of the Robbins pattern (equivalent to (OverBar[x⊕y])).  But, so is the sub-expression (OverBar[(OverBar[x⊕y])⊕(OverBar[y⊕(OverBar[x])])]), which is equivalent to y.  Using RobbinsSimplify, we can automatically simplify this sub-expression, yielding the desired result.

RobbinsExpand[(OverBar[x⊕y]),(OverBar[x])⊕y]//RobbinsSimplify

In other words, the left hand side of line 2 can be obtained by logically expanding (OverBar[x ⊕y]) in terms of (OverBar[x]) ⊕y, in accordance with the Robbins equation, and then simplifying the resulting expression which contains an instance of the Robbins pattern.  All of this can be done (and verified) automatically with the following single line of Mathematica code.

ProofLine[2]== (RobbinsExpand[(OverBar[x⊕y]),(OverBar[x])⊕y]== (OverBar[x ⊕y]))//RobbinsSimplify

Line 3 of the EQP Proof

Line 3 of the EQP proof is

ProofLine[3]=(OverBar[y⊕(OverBar[x⊕y⊕(OverBar[y⊕(OverBar[x])])])])==(OverBar[y⊕(OverBar[x])])

Seeing how line 3 follows from line 1 (i.e., the Robbins equation) involves a trick very similar to the trick described above in connection with our deciphering of line 2.  Here, the trick is to logically expand (OverBar[y⊕(OverBar[x])]) in terms of y⊕x, in accordance with the Robbins equation, and then simplify the resulting expression which contains an instance of the Robbins pattern.  Once again, this can be done (and verified) automatically with the following single line of Mathematica code.

ProofLine[3]==(RobbinsExpand[(OverBar[y⊕(OverBar[x])]),y⊕x]==(OverBar[y⊕(OverBar[x])]))//RobbinsSimplify

Equivalently, we can use RobbinsSimplify alone to see that line 3 is the following substitution instance of line 1

ProofLine[3]==(ProofLine[1]/.{x->y⊕x,y->(OverBar[y⊕(OverBar[x])])})//RobbinsSimplify

The function Line3Expand allows us to rewrite expressions of the form (OverBar[y ⊕(OverBar[x])]) in the more complex, line 3-equivalent  form (OverBar[y ⊕(OverBar[x ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])]).   Line3Expand will come in handy in our proof of line 4, below.

Line3Expand[(OverBar[y__⊕(OverBar[x__])])]:=(OverBar[y⊕(OverBar[x⊕y⊕(OverBar[y⊕(OverBar[x])])])]);

Line 4 of the EQP Proof

Line 4 of the EQP proof is

ProofLine[4] = (OverBar[(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])])==y

The EQP proof object says only that line 4 follows from from lines 1 and 3.  With our functions RobbinsExpand, RobbinsSimplify, and Line3Expand, we can automatically verify that line 4 is equivalent to

ProofLine[4]==(Line3Expand[RobbinsExpand[y,x]]==y)//RobbinsSimplify

The trick here is to recognize that the left-hand side of line 1 (i.e., (OverBar[(OverBar[x ⊕y]) ⊕(OverBar[y ⊕(OverBar[x])])])) is itself an instance of the right-hand side of line 3 (i.e., (OverBar[𝕪 ⊕(OverBar[𝕩])]), where 𝕪=(OverBar[y ⊕(OverBar[x])]), and 𝕩=x ⊕y).  This allows us to rewrite (OverBar[(OverBar[x ⊕y]) ⊕(OverBar[y ⊕(OverBar[x])])])=y equivalently as (OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[(OverBar[x ⊕y]) ⊕(OverBar[y ⊕(OverBar[x])])])])])=y, in accordance with line 3.  Finally, the Robbins equation allows us to simplify (OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[(OverBar[x ⊕y]) ⊕(OverBar[y ⊕(OverBar[x])])])])])=y down to the desired identity (OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])=y (we did this automatically using RobbinsSimplify).

Line 5 of the EQP Proof

Line 5 of the EQP proof is

ProofLine[5] = (OverBar[(OverBar[y⊕z])⊕(OverBar[z⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])])])==z

The EQP proof object says only that line 5 can be obtained via some substitution strategy involving lines 1 and 4.  To see the appropriate substitutions, let 𝕒 = (OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])]).  Then, ProofLine[5] becomes

(ProofLine[5])'=ProofLine[5]//.{(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])->𝕒}

From line 4, we know that y=(OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])=(OverBar[𝕒]).  Substituting (OverBar[𝕒]) for y in (ProofLine[5])' yields

((ProofLine[5])')'=(ProofLine[5])'//.{y->(OverBar[𝕒])}

And, ((ProofLine[5])')' is an obvious instance of line 1 (i.e., the Robbins equation).

Line 6 of the EQP Proof

Line 6 of the EQP proof is

ProofLine[6] =(OverBar[y⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[y⊕(OverBar[x])])])])==(OverBar[y⊕(OverBar[x])])

The EQP proof object says only that line 6 can be obtained via some substitution strategy involving lines 1 and 4.  To see the relevant substitutions, let 𝕓 = x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])]).  Then, ProofLine[6] becomes

(ProofLine[6])'=ProofLine[6]//.{x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])->𝕓}

From line 4, we know that y=(OverBar[(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])=(OverBar[(OverBar[𝕓])⊕(OverBar[y⊕(OverBar[x])])]).  Substituting (OverBar[(OverBar[𝕓]) ⊕(OverBar[y ⊕(OverBar[x])])]) for the first instance of y in (ProofLine[6])' yields

((ProofLine[6])')'=(OverBar[(OverBar[(OverBar[𝕓])⊕(OverBar[y⊕(OverBar[x])])])⊕(OverBar[𝕓⊕(OverBar[y⊕(OverBar[x])])])])==(OverBar[y⊕(OverBar[x])])

And, ((ProofLine[6])')' is a substitution instance of line 1, as the test below confirms.

((ProofLine[6])')'//RobbinsSimplify

Line 7 of the EQP Proof

Line 7 of the EQP proof is

ProofLine[7] = (OverBar[(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[y⊕(OverBar[x])])])])==y

The EQP proof object says only that line 7 follows from lines 1 and 6.  To see how, let 𝕔=x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[y ⊕(OverBar[x])]).  Then, line 7 becomes

(ProofLine[7])'=ProofLine[7]//.{x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[y⊕(OverBar[x])])->𝕔}

From line 6, we know that (OverBar[y ⊕(OverBar[x])])=(OverBar[y ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[y ⊕(OverBar[x])])])])=(OverBar[y ⊕(OverBar[𝕔])]).  Substituting (OverBar[y ⊕(OverBar[𝕔])]) for (OverBar[y ⊕(OverBar[x])])  in (ProofLine[7])' yields

((ProofLine[7])')'=(ProofLine[7])'//.{(OverBar[y⊕(OverBar[x])])->(OverBar[y⊕(OverBar[𝕔])])}

which is an obvious instance of the Robbins equation.

Line 8 of the EQP Proof

Line 8 of the EQP proof is

ProofLine[8] =(OverBar[z⊕(OverBar[z⊕(OverBar[y⊕z])⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])])])==(OverBar[y⊕z])

The EQP proof says only that line 8 can be obtained via some substitution strategy involving lines 1 and 5.  To see the relevant strategy, let 𝕕=(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])]).  Then, ProofLine[8] becomes

(ProofLine[8])'=ProofLine[8]//.{(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])->𝕕}

From line 5, we know that z=(OverBar[(OverBar[y ⊕z]) ⊕(OverBar[z ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])])=(OverBar[(OverBar[y ⊕z]) ⊕(OverBar[z ⊕𝕕])]).  Substituting (OverBar[(OverBar[y ⊕z]) ⊕(OverBar[z ⊕𝕕])])  for the first instance of z in  (ProofLine[8])' yields

((ProofLine[8])')'=(OverBar[(OverBar[(OverBar[y⊕z])⊕(OverBar[z⊕𝕕])])⊕(OverBar[z⊕𝕕⊕(OverBar[y⊕z])])])==(OverBar[y⊕z])

((ProofLine[8])')' is the following substitution instance of line 1.

((ProofLine[8])')'==(ProofLine[1]/.{y->(OverBar[y⊕z]),x->z⊕𝕕})

Line 9 of the EQP Proof

Line 9 of the EQP proof is

ProofLine[9] = (OverBar[(OverBar[u⊕(OverBar[y⊕z])])⊕(OverBar[u⊕z⊕(OverBar[z⊕(OverBar[y⊕z])⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])])])])==u

The EQP proof says only that line 9 follows somehow from lines 1 and 8.  To see how, let 𝕖=(OverBar[y ⊕z]) ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])]).   Then, ProofLine[9] becomes

(ProofLine[9])'=ProofLine[9]//.{(OverBar[y⊕z])⊕(OverBar[y⊕(OverBar[x])])⊕(OverBar[x⊕y⊕y⊕(OverBar[y⊕(OverBar[x])])])->𝕖}

From line 8, we know that (OverBar[y ⊕z])=(OverBar[z ⊕(OverBar[z ⊕(OverBar[y ⊕z]) ⊕(OverBar[y ⊕(OverBar[x])]) ⊕(OverBar[x ⊕y ⊕y ⊕(OverBar[y ⊕(OverBar[x])])])])])=(OverBar[z ⊕(OverBar[z ⊕𝕖])]).  Substituting (OverBar[z ⊕(OverBar[z ⊕𝕖])])  for  (OverBar[y ⊕z])  in  (ProofLine[9])' yields

((ProofLine[9])')'=(ProofLine[9])'//.{(OverBar[y⊕z])->(OverBar[z⊕(OverBar[z⊕𝕖])])}

((ProofLine[9])')' is the following substitution instance of line 1.

((ProofLine[9])')'==(ProofLine[1]/.{y->u,x->z⊕(OverBar[z⊕𝕖])})

Line 10 of the EQP Proof

Line 10 of the EQP proof is

ProofLine[10] =(OverBar[x⊕(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])])==(OverBar[x⊕(OverBar[x])])

The EQP proof tells us only that line 10 can be deduced from lines 1, 2, and 9.  To see how, let 𝕗=(OverBar[x ⊕(OverBar[x])]).  Then, ProofLine[10] becomes

(ProofLine[10])'=ProofLine[10]/.{(OverBar[x⊕(OverBar[x])])-> 𝕗}

From line 2, we know that (OverBar[x ⊕x ⊕x ⊕𝕗])=(OverBar[x ⊕𝕗⊕(OverBar[x ⊕𝕗⊕(OverBar[x ⊕x]) ⊕(OverBar[x ⊕x ⊕x ⊕𝕗])])]).  To see this, perform the following pair of substitutions on ProofLine[2]

ProofLine[2]/.{x->x⊕x,y->x⊕𝕗}

Substituting (OverBar[x ⊕𝕗⊕(OverBar[x ⊕𝕗⊕(OverBar[x ⊕x]) ⊕(OverBar[x ⊕x ⊕x ⊕𝕗])])])  for  (OverBar[x ⊕x ⊕x ⊕𝕗])  in (ProofLine[10])' yields

((ProofLine[10])')'=(ProofLine[10])'/.{(OverBar[x⊕x⊕x⊕𝕗])->(OverBar[x⊕𝕗⊕(OverBar[x⊕𝕗⊕(OverBar[x⊕x])⊕(OverBar[x⊕x⊕x⊕𝕗])])])}

It may not be terribly obvious to the naked-eye, but ((ProofLine[10])')' is a substitution instance of line 9.  To see this, perform the following quadruple of substitutions on ProofLine[9].

(SuperStar[ProofLine[9]])=ProofLine[9]//.{u->(OverBar[x⊕(OverBar[x])]),x->x,y->x,z->x}

Now, if we replace (OverBar[x ⊕(OverBar[x])]) with 𝕗 (as assumed above) throughout (SuperStar[ProofLine[9]]), we get

(SuperStar[(SuperStar[ProofLine[9]])])=(SuperStar[ProofLine[9]])//.{(OverBar[x⊕(OverBar[x])])-> 𝕗}

Then, from line 1 and the definition of 𝕗, we know that (OverBar[𝕗⊕(OverBar[x ⊕x])])=(OverBar[(OverBar[x ⊕x]) ⊕(OverBar[x ⊕(OverBar[x])])])=x.  Finally, substituting x for (OverBar[𝕗⊕(OverBar[x ⊕x])]) in (SuperStar[(SuperStar[ProofLine[9]])]) yields

(SuperStar[(SuperStar[(SuperStar[ProofLine[9]])])])=(SuperStar[(SuperStar[ProofLine[9]])])//.{(OverBar[𝕗⊕(OverBar[x⊕x])])->x}

To complete the proof of line 10, we verify that ((ProofLine[10])')' =  (SuperStar[(SuperStar[(SuperStar[ProofLine[9]])])]).

((ProofLine[10])')' == (SuperStar[(SuperStar[(SuperStar[ProofLine[9]])])])

Line 11 of the EQP Proof

Line 11 of the EQP proof is

ProofLine[11] =(OverBar[(OverBar[y⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[x⊕y⊕(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])])])==y

The EQP proof says only that line 11 can be derived from lines 1 and 10.  To see how, let 𝕘=(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])]).  Then, ProofLine[11] becomes

(ProofLine[11])'=ProofLine[11]//.{(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])->𝕘}

From line 10, we know that (OverBar[x ⊕(OverBar[x])])=(OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[x ⊕𝕘]).  Substituting (OverBar[x ⊕𝕘]) for (OverBar[x ⊕(OverBar[x])]) in  (ProofLine[11])' yields

((ProofLine[11])')'=(ProofLine[11])'//.{(OverBar[x⊕(OverBar[x])])->(OverBar[x⊕𝕘])}

((ProofLine[11])')' is the following substitution instance of line 1.

((ProofLine[11])')'==(ProofLine[1]/.{y->y,x->x⊕𝕘})

Line 12 of the EQP Proof

Line 12 of the EQP proof is

ProofLine[12] =(OverBar[(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])])==x

The EQP proof says only that line 12 follows from lines 1 and 10.  To see how, let 𝕙=x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]).  Then, ProofLine[12] becomes

(ProofLine[12])'=ProofLine[12]//.{x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->𝕙}

From line 10, we know that (OverBar[x ⊕(OverBar[x])])=(OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[x ⊕(OverBar[𝕙])]).  Substituting (OverBar[x ⊕(OverBar[𝕙])]) for (OverBar[x ⊕(OverBar[x])]) in  (ProofLine[12])' yields

((ProofLine[12])')'=(ProofLine[12])'//.{(OverBar[x⊕(OverBar[x])])->(OverBar[x⊕(OverBar[𝕙])])}

This is an obvious instance of line 1.

Line 13 of the EQP Proof

Line 13 of the EQP proof is

ProofLine[13] =(OverBar[x⊕(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])])==(OverBar[x⊕(OverBar[x])])

The EQP proof says only that line 13 can be deduced from lines 1 and 12.  To see how, let 𝕚=x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]).  Then, ProofLine[13] becomes

(ProofLine[13])'=ProofLine[13]//.{x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->𝕚}

From line 12, we know that x=(OverBar[(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[(OverBar[𝕚]) ⊕(OverBar[x ⊕(OverBar[x])])]).  Substituting (OverBar[(OverBar[𝕚]) ⊕(OverBar[x ⊕(OverBar[x])])]) for the first instance of x in (ProofLine[13])'  yields

((ProofLine[13])')'=(OverBar[(OverBar[(OverBar[𝕚])⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[𝕚⊕(OverBar[x⊕(OverBar[x])])])])==(OverBar[x⊕(OverBar[x])])

((ProofLine[13])')' is the following substitution instance of the Robbins equation.

((ProofLine[13])')'==(ProofLine[1]/.{y->(OverBar[x⊕(OverBar[x])]),x->𝕚})

Line 14 of the EQP Proof

Line 14 of the EQP proof is

ProofLine[14] =(OverBar[(OverBar[y⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[x⊕y⊕(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])])])==y

The EQP proof says only that line 14 can be obtained via lines 1 and 13.  To see how, let 𝕛=(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])⊕(OverBar[x ⊕(OverBar[x])])]).   Then, ProofLine[14] becomes

(ProofLine[14])'=ProofLine[14]//.{(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])->𝕛}

From line 13, we know that (OverBar[x ⊕(OverBar[x])])=(OverBar[x ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[x ⊕𝕛]).  Substituting (OverBar[x ⊕𝕛]) for (OverBar[x ⊕(OverBar[x])]) in  (ProofLine[14])' yields

((ProofLine[14])')'=(ProofLine[14])'//.{(OverBar[x⊕(OverBar[x])])->(OverBar[x⊕𝕛])}

And, ((ProofLine[14])')' is the following substitution instance of line 1.

((ProofLine[14])')'==(ProofLine[1]/.{y->y,x->x⊕𝕛})

Line 15 of the EQP Proof

Line 15 of the EQP proof is

ProofLine[15]=(OverBar[x⊕(OverBar[x⊕(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])])])==(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])

The EQP proof says only that line 15 follows from lines 7 and 11.  To see how, let 𝕜=(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])⊕(OverBar[x ⊕(OverBar[x])])]).  Then, ProofLine[15]  becomes

(ProofLine[15])'=ProofLine[15]//.{(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])->𝕜}

From line 7, we know that x=(OverBar[(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[𝕜⊕(OverBar[x ⊕(OverBar[x])])]).  Substituting (OverBar[𝕜 ⊕(OverBar[x ⊕(OverBar[x])])]) for the first occurrence of x in  (ProofLine[15])' yields

((ProofLine[15])')'=(OverBar[(OverBar[𝕜⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[x⊕𝕜⊕(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])])])==𝕜

((ProofLine[15])')' is the following substitution instance of line 11.

((ProofLine[15])')' == (ProofLine[11]//.{y->𝕜})

Line 16 of the EQP Proof—The last line of the proof (finally!)

Line 16 of the EQP proof is

ProofLine[16] =(OverBar[x⊕x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])⊕(OverBar[x⊕(OverBar[x])])])==(OverBar[x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])])

The EQP proof says only that line 16 can be obtained using some substitution strategy involving lines 4, 14, and 15.  To see the relevant strategy, let 𝕝=x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]).  Then, ProofLine[16] becomes

(ProofLine[16])'=ProofLine[16]//.{x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->𝕝 }

From line 15, we know that (OverBar[x ⊕𝕝 ⊕(OverBar[x ⊕(OverBar[x])])])=(OverBar[x ⊕(OverBar[x ⊕(OverBar[𝕝]) ⊕(OverBar[x ⊕𝕝 ⊕(OverBar[x ⊕(OverBar[x])])])])]).  To see this, perform the following substitution on ProofLine[15]

ProofLine[15]//.{x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->𝕝 }

Substituting  (OverBar[x ⊕(OverBar[x ⊕(OverBar[𝕝]) ⊕(OverBar[x ⊕𝕝 ⊕(OverBar[x ⊕(OverBar[x])])])])])  for  (OverBar[x ⊕𝕝 ⊕(OverBar[x ⊕(OverBar[x])])])  in (ProofLine[16])' yields

((ProofLine[16])')'=(ProofLine[16])'/.{(OverBar[x⊕𝕝⊕(OverBar[x⊕(OverBar[x])])])->(OverBar[x⊕(OverBar[x⊕(OverBar[𝕝])⊕(OverBar[x⊕𝕝⊕(OverBar[x⊕(OverBar[x])])])])])}

From line 4, we know that x=(OverBar[(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])])])=(OverBar[(OverBar[𝕝]) ⊕(OverBar[x ⊕(OverBar[x])])]).  Substituting (OverBar[(OverBar[𝕝]) ⊕(OverBar[x ⊕(OverBar[x])])]) for the first instance of x in  ((ProofLine[16])')' yields

(((ProofLine[16])')')'=(OverBar[(OverBar[(OverBar[𝕝])⊕(OverBar[x⊕(OverBar[x])])])⊕(OverBar[x⊕(OverBar[𝕝])⊕(OverBar[x⊕𝕝⊕(OverBar[x⊕(OverBar[x])])])])])==(OverBar[𝕝])

Finally, (((ProofLine[16])')')' is the following substitution instance of line 14.

(((ProofLine[16])')')' == (ProofLine[14]//.{y->(OverBar[𝕝]) ,x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->𝕝})

What have we just proved?

We have just proved that (OverBar[x ⊕x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]) ⊕(OverBar[x ⊕(OverBar[x])])])=(OverBar[x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])])]).  To see that the Winker Condition follows from this, let C=x ⊕x ⊕x ⊕(OverBar[x ⊕(OverBar[x])]), and D=x ⊕(OverBar[x ⊕(OverBar[x])]).  Then, it is straightforward to verify that line 16 entails (OverBar[C ⊕D])=(OverBar[C]), which implies the Winker Condition.

ProofLine[16]//.{x⊕x⊕x⊕(OverBar[x⊕(OverBar[x])])->C, x⊕(OverBar[x⊕(OverBar[x])])->D}

This concludes our Mathematica–aided deciphering of the EQP proof of the Winker Condition.  In conjunction with the results previously reported in Winker (1992), this proof establishes that all Robbins algebras are Boolean algebras (i.e., that the Robbins conjecture is correct).        □

Concluding Remarks

Although the EQP proof of the Robbins conjecture (which has now been verified both automatically and by hand by several different researchers) firmly establishes the truth of the Robbins conjecture, the EQP proof object does little to help human beings understand how to prove the Robbins conjecture.  In fact, the EQP proof object is quite difficult to follow (or even parse!).  After several frustrating and fruitless weeks of trying to work through the EQP proof object by hand, I started experimenting with Mathematica.  Just a couple of days later, I had a complete Mathematica reconstruction of the proof!  The keys to my success were (1) Mathematica's two-dimensional Boolean notation for the complementation operator \(•\&_\) which allowed me to see many complex syntactical patterns that were all but invisible in EQP's one-dimensional notation, and (2) Mathematica's powerful, interactive symbolic engine, which allowed me to experiment with many complicated substitution strategies in "real time."  I used Mathematica exclusively in both my scratch work, and in generating the polished reconstruction that appears here.

One of the most pressing current problems facing researchers in automated theorem-proving (according to Professor Kenneth Kunen, personal communication) is the translation and reconstruction of complex, unintuitive computer proofs into forms that are more readily understood by human beings.  I think my "Robbins success story" illustrates how Mathematica can be used quite effectively to help people comprehend complicated computer proofs of this kind.

Appendix

All Boolean algebras are Robbins algebras

I mentioned above that, in the context of Boolean algebra, the Robbins equation is logically equivalent to the Huntington equation.  We can prove this rather easily using Mathematica, as follows.  In the context of Boolean algebra (specifically, in Boolean logic), the binary relation ⊕ is just Boolean disjunction ∨, and the unary relation (OverBar[•]) is just Boolean negation ¬.  So, we define the following list of replacement rules to capture the assumption that we are working within Boolean logic.

Boolean={(OverBar[x__])->¬x,x__⊕y__->x∨y};

Then, we use Mathematica's LogicalExpand function to construct the following one-line proof of the logical equivalence of the Huntington equation and the Robbins equation, within the context of Boolean algebra.

((OverBar[y⊕(OverBar[x])])⊕(OverBar[(OverBar[x])⊕(OverBar[y])])\[Implies](OverBar[(OverBar[x⊕y])⊕(OverBar[x⊕(OverBar[y])])]))&&((OverBar[(OverBar[x⊕y])⊕(OverBar[x⊕(OverBar[y])])])\[Implies](OverBar[y⊕(OverBar[x])])⊕(OverBar[(OverBar[x])⊕(OverBar[y])]))//.Boolean
//LogicalExpand

Together with the results in Huntington (1933a,b), this entails that all Boolean algebras are Robbins algebras.     □

Double Negation is sufficient to make any Robbins algebra Boolean

Earlier, I claimed that the double negation condition (OverBar[(OverBar[x])])=x is sufficient to make any Robbins algebra Boolean.  We can demonstrate this using Mathematica, as follows.

The Robbins equation says

Robbins=(RobbinsExpand[x,y]==x)

And,  the Huntington equation says

Huntington=((OverBar[(OverBar[x])⊕y])⊕(OverBar[(OverBar[x])⊕(OverBar[y])])==x)

If we assume double negation, then the Robbins equation is equivalent to

((OverBar[RobbinsExpand[(OverBar[x]),y]])==x)//.{(OverBar[(OverBar[x__])])->x}

which is obviously identical to the Huntington equation.     □

Acknowledgments

I would like to thank Tina Eliassi–Rad and Professor Kenneth Kunen for getting me interested in the Robbins problem, Bill McCune for solving the Robbins problem and for inspiring me to publish my Mathematica reconstruction of his EQP proof object, and an anonymous referee of Mathematica in Education and Research for his detailed comments and suggestions on an earlier version of this paper.

Notes

1 Much of the history of the Robbins problem reported here is taken from McCune (1997) and Wos et al (1992).  See McCune (1997) for the full story on the recent computer proof of the Robbins conjecture.  Also, check-out Bill McCune's home page at http://www.mcs.anl.gov/home/mccune/ar/, and, especially, his "Robbins Algebras are Boolean" page at http://www.mcs.anl.gov/home/mccune/ar/robbins/ for lots of information about the Robbins conjecture and automated reasoning in general.

\(TraditionalForm\`\(\^2\ \)\)See Kneale and Kneale (1962, pages 404–427) for a scholarly trace of the historical development of Boolean algebra and Boolean logic from Boole (1854) to Huntington (1933 a,b).

\(TraditionalForm\`\(\^3\ \)\)The relation ⊗ is then defined in terms of ⊕ and \(TraditionalForm\`•\&_\) as follows: x ⊗ y ≡ (OverBar[\(x\&_\) ⊕(OverBar[y])]).  Showing that Huntington's simpler (1933a,b) axiomatization is equivalent to his more complex (1904) axiomatization is not very difficult to do by hand.  Halmos (1963, page 9) gives this proof as an introductory exercise.

4 See McCune (1997) for all technical details, and see Kolata (1996), and Peterson (1997) for less technical news reports about the computer proof and its significance.

\(TraditionalForm\`\(\^5\ \)\)See Argonne's automated reasoning page at http://www.mcs.anl.gov/home/mccune/ar/ for more about EQP and Otter.  See, also, Wos et al (1992) for a general introduction to the theory and practice of automated reasoning.

	\(TraditionalForm\`\(\^6\ \)\)Apparently, Boole (1854, page 147) was the first to use the overbar notation \(TraditionalForm\`x\&_\) to denote the negation or complementation of x in the context of formal logic and algebra.  This notation was later adopted by C.S. Peirce, but not by E.V. Huntington.  See Cajori (1993, ¶ 685) for the historical development of the overbar notation in formal logic and algebra.

\(TraditionalForm\`\(\^7\ \)\)The actual EQP output of this proof can be obtained from the following URL http://www.mcs.anl.gov/home/mccune/ar/robbins/eqp-theorem.proof.txt.

\(TraditionalForm\`\(\^8\ \)\)We don't tell Mathematica anything about the attributes of the complementation operator \(TraditionalForm\`•\&_\).  This is as it should be.  We are only allowed to assume that \(TraditionalForm\`•\&_\) is a unary function obeying the Robbins equation.

\(TraditionalForm\`\(\^9\ \)\)EQP also handles commutativity and associativity implicitly in this way.  No information is given in the EQP proof object about the roles that commutativity and associativity play in the proof.

References

Boole, G., 1854, The Laws of Thought, Dover, New York.

Cajori, F., 1993, A History of Mathematical Notations, Dover, New York.

Halmos, P., 1963, Lectures on Boolean Algebras, Van Nostrand, New York.

Huntington, E.V., 1904, Sets of independent postulates for the algebra of logic, Transactions of the American Mathematical Society 5, 288–309.

Huntington, E.V., 1933a, New sets of independent postulates for the algebra of logic, Transactions of the American Mathematical Society 35, 274–304.
       
Huntington, E.V., 1933b, Boolean algebra: A correction, Transactions of the American Mathematical Society 35,  557–558. 

Kneale, W., and Kneale, M., 1962, The Development of Logic, Clarendon: Oxford University Press, Oxford.

Kolata, G., 1996, Computer Math Proof Shows Reasoning Power, The New York Times, December 10, 1996.

McCune, W., 1997, Solution of the Robbins Problem, forthcoming in the Journal of Automated Reasoning.  A preprint of this paper is available at ftp://info.mcs.anl.gov/pub/Otter/www-misc/robbins-jar-final.ps.gz.

Peterson, I., 1997, Computers and Proof: Applying automated reasoning to prove mathematical theorems, Science News 151(12), March 22, 1997.

Stoll, R., 1963, Set Theory and Logic, W.H. Freeman and Company, San Francisco.

Tarski, A., Henkin, L., and Monk, D., 1971, Cylindric Algebras: Part I, North-Holland, New York.

Winker, S., 1992, Absorption and idempotency criteria for a problem in near-Boolean algebras, Journal of Algebra 153(2), 414–423.

Wos, L., Overbeek, R., Lusk, E., and Boyle, J., 1992, Automated Reasoning: Introduction and Applications, Second Edition, McGraw Hill, New York.

About the Author

Branden Fitelson is a philosophy graduate student at the University of Wisconsin–Madison.  He earned his BS (Mathematics) from the University of Wisconsin–Madison in 1992, and his MA (Philosophy) from the University of Wisconsin–Madison in 1997.  He is currently working toward his PhD (Philosophy).  His research interests include philosophy of science and logic.  See Branden's home page at http://polyglot.lss.wisc.edu/philosophy/PEOPLE/TA/BF/BF.HTM, for more professional and personal information about the author.