Robbins algebra

<h2 id="history">History</h2>
<p>In 1933, <a href="/facts/Edward_Huntington/FRagB52P">Edward Huntington</a> proposed a new set of axioms for Boolean algebras, consisting of (1) and (2) above, plus: 
</p>
<ul><li><i>Huntington's equation</i>: 
  
    
      
        ¬
        (
        ¬
        a
        ∨
        b
        )
        ∨
        ¬
        (
        ¬
        a
        ∨
        ¬
        b
        )
        =
        a
        .
      
    
    {\displaystyle \neg (\neg a\lor b)\lor \neg (\neg a\lor \neg b)=a.}
  
</li></ul>
<p>From these axioms, Huntington derived the usual axioms of Boolean algebra.
</p><p>Very soon thereafter, <a href="/facts/Herbert_Robbins/Gk2X6ap9">Herbert Robbins</a> posed the Robbins conjecture, namely that the Huntington equation could be replaced with what came to be called the Robbins equation, and the result would still be <a href="/facts/Boolean_algebra_(structure)/cHbo65jm">Boolean algebra</a>. 
  
    
      
        ∨
      
    
    {\displaystyle \lor }
  
 would interpret Boolean <a href="/facts/Boolean_algebra_(structure)/cHbo65jm">join</a> and 
  
    
      
        ¬
      
    
    {\displaystyle \neg }
  
 Boolean <a href="/facts/Boolean_algebra_(structure)/cHbo65jm">complement</a>. Boolean <a href="/facts/Boolean_algebra_(structure)/cHbo65jm">meet</a> and the constants 0 and 1 are easily defined from the Robbins algebra primitives. Pending verification of the conjecture, the system of Robbins was called "Robbins algebra."
</p><p>Verifying the Robbins conjecture required proving Huntington's equation, or some other axiomatization of a Boolean algebra, as theorems of a Robbins algebra. Huntington, Robbins, <a href="/facts/Alfred_Tarski/7h6NySAj">Alfred Tarski</a>, and others worked on the problem, but failed to find a proof or counterexample.
</p><p><a href="/facts/William_McCune/W8At9gog">William McCune</a> proved the conjecture in 1996, using the <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem prover</a> <a href="/facts/Equational_prover/J6yHzcht">EQP</a>. For a complete proof of the Robbins conjecture in one consistent notation and following McCune closely, see Mann (2003). Dahn (1998) simplified McCune's machine proof.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Algebraic_structure/TkuXca24">Algebraic structure</a></li>
<li><a href="/facts/Minimal_axioms_for_Boolean_algebra/qg0HHCQW">Minimal axioms for Boolean algebra</a></li></ul>

<ul><li>Dahn, B. I. (1998) Abstract to "<a href="https://www.sciencedirect.com/science/article/pii/S0021869398974671">Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem</a>," <i>Journal of Algebra</i> 208(2): 526–32.</li>
<li>Mann, Allen (2003) "<a href="http://math.colgate.edu/~amann/MA/robbins_complete.pdf">A Complete Proof of the Robbins Conjecture.</a>"</li>
<li><a href="/facts/William_McCune/W8At9gog">William McCune</a>, "<a href="http://calculemus.org/MathUniversalis/4/6robbins.html">Robbins Algebras Are Boolean</a>," With links to proofs and other papers.</li></ul>

Robbins algebra open-in-new

Robbins algebra