In algebra astratta, un'algebra di Robbins è un'algebra contenente un'unica operazione binaria, solitamente indicata da 
e un'unica operazione unaria solitamente indicata da 
. Queste operazioni soddisfano i seguenti assiomi:
Per ogni elemento 
, 
e 
:
- associatività:
- commutatività:
- equazione di Robbins:
Per molti anni fu congetturato, ma non dimostrato, che tutte le algebre di Robbins fossero algebre booleane. La congettura fu dimostrata nel 1996, quindi il termine "algebra di Robbins" può essere considerato sinonimo di "algebra di Boole".
Storia
Nel 1933, Edward Huntington propose una nuova serie di assiomi per le algebre booleane, composta dagli assiomi (1) e (2) introdotti precedentemente, più:
- Equazione di Huntington:
Da questi assiomi, Huntington derivò i soliti assiomi dell'algebra booleana.
Poco tempo dopo, Herbert Robbins pose la "congettura di Robbins", vale a dire che l'equazione di Huntington poteva essere sostituita con quella che venne chiamata l'equazione di Robbins, e il risultato sarebbe stato ancora l'algebra booleana. sarebbe da interpretare come l'operazione di somma logica e come complemento booleano. Il prodotto booleano e le costanti 0 e 1 sono facilmente definite dalle primitive dell'algebra di Robbins. In attesa della verifica della congettura, il sistema di Robbins era chiamato "algebra di Robbins".
La verifica della congettura di Robbins richiedeva la dimostrazione dell'equazione di Huntington, o qualche altra assiomatizzazione di un'algebra booleana, come teoremi di un'algebra di Robbins. Huntington, Robbins, Alfred Tarski e altri hanno lavorato al problema, ma non sono riusciti a trovare una prova o un controesempio.
William McCune dimostrò la congettura nel 1996, usando il dimostratore automatico di teoremi EQP. Per una prova completa della congettura di Robbins in una notazione coerente e vicina alla dimostrazione automatica di McCune, vedere Mann (2003). Dahn (1998) ha semplificato la dimostrazione automatica di McCune.
Bibliografia
Voci correlate
Collegamenti esterni
