Algebra di Robbins: differenze tra le versioni

Versione delle 00:32, 27 gen 2021

Versione delle 00:35, 27 gen 2021

Riga 1:

{{U|pagina=Algebra di Boole|argomento=matematica|verso=a|data=maggio 2020}}

In [[algebra astratta]], un'algebra di '''Robbins''' è un'algebra contenente un'unica [[operazione binaria]], solitamente indicata da <math>\lor</math> e un'unica [[operazione unaria]] solitamente indicata da <math>\neg</math> . Queste operazioni soddisfano i seguenti [[Algebra universale|assiomi]] :

Per ogni elemento ''<math>a''</math>, ''<math>b''</math> e ''<math>c'' </math>:

# [[Associativitàassociatività]] : <math>a \lor \left(b \lor c \right) = \left(a \lor b \right) \lor c;</math>

# [[Commutativitàcommutatività]] : <math>a \lor b = b \lor a;</math>

# ''Equazioneequazione di Robbins'' : <math>\neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a.</math>

Per molti anni fu congetturato, ma non dimostrato, che tutte le algebre di Robbins fossero [[Algebra di Boole|algebre booleane]]. La congettura fu dimostrata nel 1996, quindi il termine "algebra di Robbins" può essere considerato sinonimo di "algebra di Boole".

Riga 13:

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'' : <math>\neg(\neg a \lor b) \lor \neg(\neg a \lor \neg b) = a.</math>

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 [[Algebra di Boole|l'algebra booleana]] . <math>\lor</math> sarebbe da interpretare come l'operazione di somma logica e <math>\neg</math> 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 [[Dimostrazione automatica di teoremi|dimostratore automatico di teoremi]] EQP . Per una prova completa della congettura di Robbins in una notazione coerente e vicina alla dimostrazione automatica di McCune, vedivedere Mann (2003). Dahn (1998) ha semplificato la dimostrazione automatica di McCune.

== Voci correlate ==