Robbins-algebra

Een Robbins-algebra is een algebra bestaande uit de verzameling { 0, 1 } en de logische operatoren $\lor$ (disjunctie, "of") en $\neg$ (negatie, "niet") en de volgende axioma's.

Associativiteit: $a\lor (b\lor c)=(a\lor b)\lor c$

Commutativiteit: $a\lor b=b\lor a$

Axioma van Robbins: $\neg (\neg (a\lor b)\lor \neg (a\lor \neg b))=a$

Elke booleaanse algebra is een Robbins-algebra maar of elke Robbins-algebra een booleaanse algebra is, was enige tijd onbekend. Het vermoeden van Robbins is dat deze axioma's equivalent zijn aan die van de booleaanse algebra. Het werd voor het eerst geformuleerd door Herbert Robbins.

Het vermoeden werd in 1996 bewezen door William McCune met behulp van een automatische stellingbewijzer.

Geschiedenis

In 1933 stelde Edward Huntington een alternatieve verzameling axioma's voor voor de booleaanse algebra's met de axioma's voor associativiteit, commutativiteit en het axioma van Huntington:

$\neg (\neg a\lor b)\lor \neg (\neg a\lor \neg b)=a$

De geldigheid van dit axioma kan gecontroleerd worden met behulp van een waarheidstabel. Huntington toonde ook aan dat uit deze drie axioma's de axioma's van de booleaanse algebra volgen. Later stelde Robbins dat uit zijn axioma het axioma van Huntington volgt (waardoor een Robbins-algebra ook een booleaanse algebra zou zijn). Hijzelf, Huntington en Alfred Tarski (en zijn leerlingen) hebben aan dit probleem gewerkt maar konden het niet bewijzen of een tegenvoorbeeld construeren. Het probleem werd uiteindelijk bewezen door William McCune in 1996 met behulp van zijn stellingbewijzer EQP.

Bronnen, noten en/of referenties