Editing Boolean algebra (structure) (section)

== Axiomatics ==

{| align="right" class="wikitable collapsible collapsed" style="text-align:left"
! colspan="2" | '''Proven properties'''
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''UId<sub>1</sub>''' !!   !! colspan="2" | If ''x'' ∨ ''o'' = ''x'' for all ''x'', then ''o'' = 0
|-
| Proof:      ||    || colspan="2" | If ''x'' ∨ ''o'' = ''x'', then
|-
|             ||  || 0
|-
|             || = || 0 ∨ ''o'' || by assumption
|-
|             || = || ''o'' ∨ 0 || by '''Cmm<sub>1</sub>'''
|-
|             || = || ''o'' || by '''Idn<sub>1</sub>'''
|}
| '''UId<sub>2</sub>''' &nbsp; [dual] &nbsp; If ''x'' ∧ ''i'' = ''x'' for all ''x'', then ''i'' = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''Idm<sub>1</sub>''' !!   !! ''x'' ∨ ''x'' = ''x''
|-
| Proof:      ||   || ''x'' ∨ ''x''
|-
|             || = || (''x'' ∨ ''x'') ∧ 1 || by '''Idn<sub>2</sub>'''
|-
|             || = || (''x'' ∨ ''x'') ∧ (''x'' ∨ ¬''x'') || by '''Cpl<sub>1</sub>'''
|-
|             || = || ''x'' ∨ (''x'' ∧ ¬''x'') || by '''Dst<sub>1</sub>'''
|-
|             || = || ''x'' ∨ 0 || by '''Cpl<sub>2</sub>'''
|-
|             || = || ''x'' || by '''Idn<sub>1</sub>'''
|}
| '''Idm<sub>2</sub>''' &nbsp; [dual] &nbsp; ''x'' ∧ ''x'' = ''x''
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''Bnd<sub>1</sub>''' !!   !! ''x'' ∨ 1 = 1
|-
| Proof:      ||   || ''x'' ∨ 1
|-
|             || = || (''x'' ∨ 1) ∧ 1 || by '''Idn<sub>2</sub>'''
|-
|             || = || 1 ∧ (''x'' ∨ 1) || by '''Cmm<sub>2</sub>'''
|-
|             || = || (''x'' ∨ ¬''x'') ∧ (''x'' ∨ 1) || by '''Cpl<sub>1</sub>'''
|-
|             || = || ''x'' ∨ (¬''x'' ∧ 1) || by '''Dst<sub>1</sub>'''
|-
|             || = || ''x'' ∨ ¬''x'' || by '''Idn<sub>2</sub>'''
|-
|             || = || 1 || by '''Cpl<sub>1</sub>'''
|}
| '''Bnd<sub>2</sub>''' &nbsp; [dual] &nbsp; ''x'' ∧ 0 = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''Abs<sub>1</sub>'''  !!   !! ''x'' ∨ (''x'' ∧ ''y'')  = ''x''
|-
| Proof:      ||   || ''x'' ∨ (''x'' ∧ ''y'')
|-
|             || = || (''x'' ∧ 1) ∨ (''x'' ∧ ''y'') || by '''Idn<sub>2</sub>'''
|-
|             || = || ''x'' ∧ (1 ∨ ''y'') || by '''Dst<sub>2</sub>'''
|-
|             || = || ''x'' ∧ (''y'' ∨ 1) || by '''Cmm<sub>1</sub>'''
|-
|             || = || ''x'' ∧ 1 || by '''Bnd<sub>1</sub>'''
|-
|             || = || ''x'' || by '''Idn<sub>2</sub>'''
|}
| '''Abs<sub>2</sub>''' &nbsp; [dual] &nbsp; ''x'' ∧ (''x'' ∨ ''y'') = ''x''
|- valign="top"
| colspan="2" |
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''UNg'''  !!   !! colspan="2" | If ''x'' ∨ ''x''<sub>n</sub> = 1 and ''x'' ∧ ''x''<sub>n</sub> = 0, then ''x''<sub>n</sub> = ¬''x''
|-
| Proof:      ||   || colspan="2" | If ''x'' ∨ ''x''<sub>n</sub> = 1 and ''x'' ∧ ''x''<sub>n</sub> = 0, then
|-
|             ||   ||''x''<sub>n</sub>
|-
|             || = || ''x''<sub>n</sub> ∧ 1 || by '''Idn<sub>2</sub>'''
|-
|             || = || ''x''<sub>n</sub> ∧ (''x'' ∨ ¬''x'') || by '''Cpl<sub>1</sub>'''
|-
|             || = || (''x''<sub>n</sub> ∧ ''x'') ∨ (''x''<sub>n</sub> ∧ ¬''x'') || by '''Dst<sub>2</sub>'''
|-
|             || = || (''x'' ∧ ''x''<sub>n</sub>) ∨ (¬''x'' ∧ ''x''<sub>n</sub>) || by '''Cmm<sub>2</sub>'''
|-
|             || = || 0 ∨ (¬''x'' ∧ ''x''<sub>n</sub>) || by assumption
|-
|             || = || (''x'' ∧ ¬''x'')  ∨ (¬''x'' ∧ ''x''<sub>n</sub>) || by '''Cpl<sub>2</sub>'''
|-
|             || = || (¬''x'' ∧ ''x'')  ∨ (¬''x'' ∧ ''x''<sub>n</sub>) || by '''Cmm<sub>2</sub>'''
|-
|             || = || ¬''x'' ∧ (''x'' ∨ ''x''<sub>n</sub>) || by '''Dst<sub>2</sub>'''
|-
|             || = || ¬''x'' ∧ 1 || by assumption
|-
|             || = || ¬''x'' || by '''Idn<sub>2</sub>'''
|}
|- valign="top"
| colspan="2" |
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''DNg'''  !!   !! ¬¬''x'' = ''x''
|-
| Proof:      ||     || ¬''x'' ∨ ''x'' = ''x'' ∨ ¬''x'' = 1 || by '''Cmm<sub>1</sub>''', '''Cpl<sub>1</sub>'''
|-
|             || and || ¬''x'' ∧ ''x'' = ''x'' ∧ ¬''x'' = 0 || by '''Cmm<sub>2</sub>''', '''Cpl<sub>2</sub>'''
|-
|             || hence || ''x'' = ¬¬''x'' || by '''UNg'''
|}
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''A<sub>1</sub>'''  !!   !! ''x'' ∨ (¬''x'' ∨ ''y'') = 1
|-
| Proof:      ||   || ''x'' ∨ (¬''x'' ∨ ''y'')
|-
|             || = || (''x'' ∨ (¬''x'' ∨ ''y'')) ∧ 1 || by '''Idn<sub>2</sub>'''
|-
|             || = || 1 ∧ (''x'' ∨ (¬''x'' ∨ ''y'')) || by '''Cmm<sub>2</sub>'''
|-
|             || = || (''x'' ∨ ¬''x'') ∧ (''x'' ∨ (¬''x'' ∨ ''y'')) || by '''Cpl<sub>1</sub>'''
|-
|             || = || ''x'' ∨ (¬''x'' ∧ (¬''x'' ∨ ''y'')) || by '''Dst<sub>1</sub>'''
|-
|             || = || ''x'' ∨ ¬''x'' || by '''Abs<sub>2</sub>'''
|-
|             || = || 1 || by '''Cpl<sub>1</sub>'''
|}
| '''A<sub>2</sub>''' &nbsp; [dual] &nbsp; ''x'' ∧ (¬''x'' ∧ ''y'') = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''B<sub>1</sub>'''  !!   !! (''x'' ∨ ''y'') ∨ (¬''x'' ∧ ¬''y'') = 1
|-
| Proof:      ||   || (''x'' ∨ ''y'') ∨ (¬''x'' ∧ ¬''y'')
|-
|             || = || ((''x'' ∨ ''y'') ∨ ¬''x'') ∧ ((''x'' ∨ ''y'') ∨  ¬''y'') || by '''Dst<sub>1</sub>'''
|-
|             || = || (¬''x'' ∨ (''x'' ∨ ''y'')) ∧ (¬''y'' ∨ (''y'' ∨ ''x'')) || by '''Cmm<sub>1</sub>'''
|-
|             || = || (¬''x'' ∨ (¬¬''x'' ∨ ''y'')) ∧ (¬''y'' ∨ (¬¬''y'' ∨ ''x'')) || by '''DNg'''
|-
|             || = || 1 ∧ 1 || by '''A<sub>1</sub>'''
|-
|             || = || 1 || by '''Idn<sub>2</sub>'''
|}
| '''B<sub>2</sub>''' &nbsp; [dual] &nbsp; (''x'' ∧ ''y'') ∧ (¬''x'' ∨ ¬''y'') = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''C<sub>1</sub>'''  !!   !! (''x'' ∨ ''y'') ∧ (¬''x'' ∧ ¬''y'') = 0
|-
| Proof:      ||   || (''x'' ∨ ''y'') ∧ (¬''x'' ∧ ¬''y'')
|-
|             || = || (¬''x'' ∧ ¬''y'') ∧ (''x'' ∨ ''y'') || by '''Cmm<sub>2</sub>'''
|-
|             || = || ((¬''x'' ∧ ¬''y'') ∧ ''x'') ∨ ((¬''x'' ∧ ¬''y'') ∧ ''y'') || by '''Dst<sub>2</sub>'''
|-
|             || = || (''x'' ∧ (¬''x'' ∧ ¬''y'')) ∨ (''y'' ∧ (¬''y'' ∧ ¬''x'')) || by '''Cmm<sub>2</sub>'''
|-
|             || = || 0 ∨ 0 || by '''A<sub>2</sub>'''
|-
|             || = || 0 || by '''Idn<sub>1</sub>'''
|}
| '''C<sub>2</sub>''' &nbsp; [dual] &nbsp; (''x'' ∧ ''y'') ∨ (¬''x'' ∨ ¬''y'') = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''DMg<sub>1</sub>'''  !!   !! ¬(''x'' ∨ ''y'') = ¬''x'' ∧ ¬''y''
|-
| Proof:      ||   || by '''B<sub>1</sub>''', '''C<sub>1</sub>''', and '''UNg'''
|}
| '''DMg<sub>2</sub>''' &nbsp; [dual] &nbsp; ¬(''x'' ∧ ''y'') = ¬''x'' ∨ ¬''y''
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''D<sub>1</sub>'''  !!   !! (''x''∨(''y''∨''z'')) ∨ ¬''x'' = 1
|-
| Proof:      ||   || (''x'' ∨ (''y'' ∨ ''z'')) ∨ ¬''x''
|-
|             || = || ¬''x'' ∨ (''x'' ∨ (''y'' ∨ ''z'')) || by '''Cmm<sub>1</sub>'''
|-
|             || = || ¬''x'' ∨ (¬¬''x'' ∨ (''y'' ∨ ''z'')) || by '''DNg'''
|-
|             || = || 1 || by '''A<sub>1</sub>'''
|}
| '''D<sub>2</sub>''' &nbsp; [dual] &nbsp; (''x''∧(''y''∧''z'')) ∧ ¬''x'' = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''E<sub>1</sub>'''  !!   !! ''y'' ∧ (''x''∨(''y''∨''z'')) = ''y''
|-
| Proof:      ||   || ''y'' ∧ (''x'' ∨ (''y'' ∨ ''z''))
|-
|             || = || (''y'' ∧ ''x'') ∨ (''y'' ∧ (''y'' ∨ ''z'')) || by '''Dst<sub>2</sub>'''
|-
|             || = || (''y'' ∧ ''x'') ∨ ''y'' || by '''Abs<sub>2</sub>'''
|-
|             || = || ''y'' ∨ (''y'' ∧ ''x'') || by '''Cmm<sub>1</sub>'''
|-
|             || = || ''y'' || by '''Abs<sub>1</sub>'''
|}
| '''E<sub>2</sub>''' &nbsp; [dual] &nbsp; ''y'' ∨ (''x''∧(''y''∧''z'')) = ''y''
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''F<sub>1</sub>'''  !!   !! (''x''∨(''y''∨''z'')) ∨ ¬''y'' = 1
|-
| Proof:      ||   || (''x'' ∨ (''y'' ∨ ''z'')) ∨ ¬''y''
|-
|             || = || ¬''y'' ∨ (''x'' ∨ (''y'' ∨ ''z'')) || by '''Cmm<sub>1</sub>'''
|-
|             || = || (¬''y'' ∨ (''x'' ∨ (''y'' ∨ ''z''))) ∧ 1 || by '''Idn<sub>2</sub>'''
|-
|             || = || 1 ∧ (¬''y'' ∨ (''x'' ∨ (''y'' ∨ ''z''))) || by '''Cmm<sub>2</sub>'''
|-
|             || = || (''y'' ∨ ¬''y'') ∧ (¬''y'' ∨ (''x'' ∨ (''y'' ∨ ''z''))) || by '''Cpl<sub>1</sub>'''
|-
|             || = || (¬''y'' ∨ ''y'') ∧ (¬''y'' ∨ (''x'' ∨ (''y'' ∨ ''z''))) || by '''Cmm<sub>1</sub>'''
|-
|             || = || ¬''y'' ∨ (''y'' ∧ (''x'' ∨ (''y'' ∨ ''z''))) || by '''Dst<sub>1</sub>'''
|-
|             || = || ¬''y'' ∨ ''y'' || by '''E<sub>1</sub>'''
|-
|             || = || ''y'' ∨ ¬''y'' || by '''Cmm<sub>1</sub>'''
|-
|             || = || 1 || by '''Cpl<sub>1</sub>'''
|}
| '''F<sub>2</sub>''' &nbsp; [dual] &nbsp; (''x''∧(''y''∧''z'')) ∧ ¬''y'' = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''G<sub>1</sub>'''  !!   !! (''x''∨(''y''∨''z'')) ∨ ¬''z'' = 1
|-
| Proof:      ||   || (''x'' ∨ (''y'' ∨ ''z'')) ∨ ¬''z''
|-
|             || = || (''x'' ∨ (''z'' ∨ ''y'')) ∨ ¬''z'' || by '''Cmm<sub>1</sub>'''
|-
|             || = || 1 || by '''F<sub>1</sub>'''
|}
| '''G<sub>2</sub>''' &nbsp; [dual]  &nbsp;  (''x''∧(''y''∧''z'')) ∧ ¬''z'' = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''H<sub>1</sub>'''  !!   !! ¬((''x''∨''y'')∨''z'') ∧ ''x'' = 0
|-
| Proof:      ||   || ¬((''x'' ∨ ''y'') ∨ ''z'') ∧ ''x''
|-
|             || = || (¬(''x'' ∨ ''y'') ∧ ¬''z'') ∧ ''x'' || by '''DMg<sub>1</sub>'''
|-
|             || = || ((¬''x'' ∧ ¬''y'') ∧ ¬''z'') ∧ ''x'' || by '''DMg<sub>1</sub>'''
|-
|             || = || ''x'' ∧ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'') || by '''Cmm<sub>2</sub>'''
|-
|             || = || (''x'' ∧ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'')) ∨ 0 || by '''Idn<sub>1</sub>'''
|-
|             || = || 0 ∨ (''x'' ∧ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'')) || by '''Cmm<sub>1</sub>'''
|-
|             || = || (''x'' ∧ ¬''x'') ∨ (''x'' ∧ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'')) || by '''Cpl<sub>2</sub>'''
|-
|             || = || ''x'' ∧ (¬''x'' ∨ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'')) || by '''Dst<sub>2</sub>'''
|-
|             || = || ''x'' ∧ (¬''x'' ∨ (¬''z'' ∧ (¬''x'' ∧ ¬''y''))) || by '''Cmm<sub>2</sub>'''
|-
|             || = || ''x'' ∧ ¬''x'' || by '''E<sub>2</sub>'''
|-
|             || = || 0 || by '''Cpl<sub>2</sub>'''
|}
| '''H<sub>2</sub>''' &nbsp; [dual]  &nbsp;  ¬((''x''∧''y'')∧''z'') ∨ ''x'' = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''I<sub>1</sub>'''  !!   !! ¬((''x''∨''y'')∨''z'') ∧ ''y'' = 0
|-
| Proof:      ||   || ¬((''x'' ∨ ''y'') ∨ ''z'') ∧ ''y''
|-
|             || = || ¬((''y'' ∨ ''x'') ∨ ''z'') ∧ ''y'' || by '''Cmm<sub>1</sub>'''
|-
|             || = || 0 || by '''H<sub>1</sub>'''
|}
| '''I<sub>2</sub>''' &nbsp; [dual]  &nbsp;  ¬((''x''∧''y'')∧''z'') ∨ ''y'' = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''J<sub>1</sub>'''  !!   !! ¬((''x''∨''y'')∨''z'') ∧ ''z'' = 0
|-
| Proof:      ||   || ¬((''x'' ∨ ''y'') ∨ ''z'') ∧ ''z''
|-
|             || = || (¬(''x'' ∨ ''y'') ∧ ¬''z'') ∧ ''z'' || by '''DMg<sub>1</sub>'''
|-
|             || = || ''z'' ∧ (¬(''x'' ∨ ''y'') ∧ ¬''z'') || by '''Cmm<sub>2</sub>'''
|-
|             || = || ''z'' ∧ ( ¬''z'' ∧ ¬(''x'' ∨ ''y'')) || by '''Cmm<sub>2</sub>'''
|-
|             || = || 0 || by '''A<sub>2</sub>'''
|}
| '''J<sub>2</sub>''' &nbsp; [dual]  &nbsp;  ¬((''x''∧''y'')∧''z'') ∨ ''z'' = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''K<sub>1</sub>'''  !!   !! (''x'' ∨ (''y'' ∨ ''z'')) ∨ ¬((''x'' ∨ ''y'') ∨ ''z'') = 1
|-
| Proof:      ||   || (''x''∨(''y''∨''z'')) ∨ ¬((''x'' ∨ ''y'') ∨ ''z'')
|-
|             || = || (''x''∨(''y''∨''z'')) ∨ (¬(''x'' ∨ ''y'') ∧ ¬''z'') || by '''DMg<sub>1</sub>'''
|-
|             || = || (''x''∨(''y''∨''z'')) ∨ ((¬''x'' ∧ ¬''y'') ∧ ¬''z'') || by '''DMg<sub>1</sub>'''
|-
|             || = || ((''x''∨(''y''∨''z'')) ∨ (¬''x'' ∧ ¬''y'')) ∧  ((''x''∨(''y''∨''z'')) ∨ ¬''z'')|| by '''Dst<sub>1</sub>'''
|-
|             || = || (((''x''∨(''y''∨''z'')) ∨ ¬''x'') ∧ ((''x''∨(''y''∨''z'')) ∨ ¬''y'')) ∧  ((''x''∨(''y''∨''z'')) ∨ ¬''z'')|| by '''Dst<sub>1</sub>'''
|-
|             || = || (1 ∧ 1) ∧ 1 || by '''D<sub>1</sub>''','''F<sub>1</sub>''','''G<sub>1</sub>'''
|-
|             || = || 1 || by '''Idn<sub>2</sub>'''
|}
| '''K<sub>2</sub>''' &nbsp; [dual]  &nbsp;  (''x'' ∧ (''y'' ∧ ''z'')) ∧ ¬((''x'' ∧ ''y'') ∧ ''z'') = 0
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''L<sub>1</sub>'''  !!   !! (''x'' ∨ (''y'' ∨ ''z'')) ∧ ¬((''x'' ∨ ''y'') ∨ ''z'') = 0
|-
| Proof:      ||   || (''x'' ∨ (''y'' ∨ ''z'')) ∧ ¬((''x'' ∨ ''y'') ∨ ''z'')
|-
|             || = || ¬((''x''∨''y'')∨''z'') ∧ (''x'' ∨ (''y'' ∨ ''z'')) || by '''Cmm<sub>2</sub>'''
|-
|             || = || (¬((''x''∨''y'')∨''z'') ∧ ''x'') ∨ (¬((''x''∨''y'')∨''z'') ∧ (''y'' ∨ ''z'')) || by '''Dst<sub>2</sub>'''
|-
|             || = || (¬((''x''∨''y'')∨''z'') ∧ ''x'') ∨ ((¬((''x''∨''y'')∨''z'') ∧ ''y'') ∨ (¬((''x''∨''y'')∨''z'') ∧ ''z'')) || by '''Dst<sub>2</sub>'''
|-
|             || = || 0 ∨ (0 ∨ 0) || by '''H<sub>1</sub>''','''I<sub>1</sub>''','''J<sub>1</sub>'''
|-
|             || = || 0 || by '''Idn<sub>1</sub>'''
|}
| '''L<sub>2</sub>''' &nbsp; [dual]  &nbsp; (''x'' ∧ (''y'' ∧ ''z'')) ∨ ¬((''x'' ∧ ''y'') ∧ ''z'') = 1
|- valign="top"
|
{| align="left" class="collapsible collapsed" style="text-align:left"
! '''Ass<sub>1</sub>'''  !!   !! ''x'' ∨ (''y'' ∨ ''z'') = (''x'' ∨ ''y'') ∨ ''z''
|-
| Proof:      ||   || by '''K<sub>1</sub>''', '''L<sub>1</sub>''', '''UNg''', '''DNg'''
|}
| '''Ass<sub>2</sub>''' &nbsp; [dual]  &nbsp;  ''x'' ∧ (''y'' ∧ ''z'') = (''x'' ∧ ''y'') ∧ ''z''
|-
| colspan="2" |
{| align="left" class="collapsible" style="text-align:left"
|-
! colspan="2" | Abbreviations
|-
| '''UId''' ||  Unique Identity
|-
| '''Idm''' || [[Idempotence]]
|-
| '''Bnd''' || [[Bounded lattice|Boundaries]]
|-
| '''Abs''' || [[Absorption law]]
|-
| '''UNg''' ||  Unique Negation
|-
| '''DNg''' || [[Double negation]]
|-
| '''DMg''' || [[De Morgan's Law]]
|-
| '''Ass''' || [[Associativity]]
|}
|}
{| align="right" class="wikitable collapsible collapsed" style="text-align:left"
! colspan="4"| '''Huntington 1904 Boolean algebra axioms'''
|- valign="top"
| '''Idn<sub>1</sub>'''  || ''x'' ∨ 0 = ''x''
| '''Idn<sub>2</sub>'''  || ''x'' ∧ 1 = ''x''
|- valign="top"
| '''Cmm<sub>1</sub>''' || ''x'' ∨ ''y'' = ''y'' ∨ ''x''
| '''Cmm<sub>2</sub>''' || ''x'' ∧ ''y'' = ''y'' ∧ ''x''
|- valign="top"
| '''Dst<sub>1</sub>'''  || ''x'' ∨ (''y''∧''z'') = (''x''∨''y'') ∧ (''x''∨''z'')
| '''Dst<sub>2</sub>'''  || ''x'' ∧ (''y''∨''z'') = (''x''∧''y'') ∨ (''x''∧''z'')
|- valign="top"
| '''Cpl<sub>1</sub>'''   || ''x'' ∨ ¬''x'' = 1
| '''Cpl<sub>2</sub>'''   || ''x'' ∧ ¬''x'' = 0
|-
| colspan="4" |
{| align="left" class="collapsible" style="text-align:left"
|-
! colspan="2" | Abbreviations
|-
| '''Idn''' || [[Identity element|Identity]]
|-
| '''Cmm''' || [[Commutativity]]
|-
| '''Dst''' || [[Distributivity]]
|-
| '''Cpl''' || [[Complemented lattice|Complements]]
|}
|}

The first axiomatization of Boolean lattices/algebras in general was given by the English philosopher and mathematician [[Alfred North Whitehead]] in 1898.{{sfn|Padmanabhan|Rudeanu|2008|p=[https://books.google.com/books?id=JlXSlpmlSv4C&pg=PA73 73]}}{{sfn|Whitehead|1898|p=37}}
It included the [[#Definition|above axioms]] and additionally {{math|1=''x'' ∨ 1 = 1}} and {{math|1=''x'' ∧ 0 = 0}}.
In 1904, the American mathematician [[Edward V. Huntington]] (1874–1952) gave probably the most parsimonious axiomatization based on {{math|1=∧}}, {{math|1=∨}}, {{math|1=¬}}, even proving the associativity laws (see box).{{sfn|Huntington|1904|pp=292-293}}
He also proved that these axioms are [[Independence (mathematical logic)|independent]] of each other.{{sfn|Huntington|1904|p=296}}
In 1933, Huntington set out the following elegant axiomatization for Boolean algebra.{{sfn|Huntington|1933a}}  It requires just one binary operation {{math|1=+}} and a [[unary functional symbol]] {{math|1=''n''}}, to be read as 'complement', which satisfy the following laws:
{{olist
|1= ''Commutativity'': {{math|1=''x'' + ''y'' = ''y'' + ''x''}}.
|2= ''Associativity'': {{math|1=(''x'' + ''y'') + ''z'' = ''x'' + (''y'' + ''z'')}}.
|3= ''Huntington equation'': {{math|1=''n''(''n''(''x'') + ''y'') + ''n''(''n''(''x'') + ''n''(''y'')) = ''x''}}.
}}
[[Herbert Robbins]] immediately asked: If the Huntington equation is replaced with its dual, to wit:
{{olist|start=4
|1= ''Robbins Equation'': {{math|1=''n''(''n''(''x'' + ''y'') + ''n''(''x'' + ''n''(''y''))) = ''x''}},
}}
do (1), (2), and (4) form a basis for Boolean algebra? Calling (1), (2), and (4) a ''Robbins algebra'', the question then becomes: Is every Robbins algebra a Boolean algebra? This question (which came to be known as the [[Robbins conjecture]]) remained open for decades, and became a favorite question of [[Alfred Tarski]] and his students. In 1996, [[William McCune]] at [[Argonne National Laboratory]], building on earlier work by Larry Wos, Steve Winker, and Bob Veroff, answered Robbins's question in the affirmative: Every Robbins algebra is a Boolean algebra. Crucial to McCune's proof was the computer program [[Equational prover|EQP]] he designed. For a simplification of McCune's proof, see Dahn (1998).

Further work has been done for reducing the number of axioms; see [[Minimal axioms for Boolean algebra]].

{{clear}}