Axioms in Boolean Algebra

              a ∧ T = a                     {∧ identity}
              a ∨ F = a                     {∨ identity}
              a ∧ a = a                     {∧ idempotence}
              a ∨ a = a                     {∨ idempotence}
              a ∧ F = F                     {∧ null} annihilation
              a ∨ T = T                     {∨ null} absorbtion
              a ∧ b = b ∧ a                 {∧ commutative}
              a ∨ a = b ∨ a                 {∨ commutative}
        (a ∧ b) ∧ c = a ∧ (b ∧ c)           {∧ associative}
        (a ∨ b) ∨ c = a ∨ (b ∨ c)           {∨ associative}
        a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)     {∧ distributes over ∨}
        a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)     {∨ distributes over ∧}
           ¬(a ∧ b) = ¬a ∨ ¬b               {DeMorgan's law}
           ¬(a ∨ b) = ¬a ∧ ¬b               {DeMorgan's law}
                 Β¬T = F                     {negate T}
                 Β¬F = T                     {negate F}
              Β¬(Β¬a) = a                     {double negation}
             a ∧ ¬a = F                     {∧ complement} NCL
             a ∨ ¬a = T                     {∨ complement} LEM

                  a β†’ a ∨ b                 {∨ implication} weakening
              a ∧ b β†’ a                     {∧ implication} ∧El
              a ∧ b β†’ b                     {∧ implication} ∧Er

          β†’     ≑     β†’     ≑     ∨
        a β†’  b  ≑  Β¬b β†’ Β¬a  ≑  Β¬a ∨  b      {implication}
       Β¬a β†’  b  ≑  Β¬b β†’  a  ≑   a ∨  b
        a β†’ Β¬b  ≑   b β†’ Β¬a  ≑  Β¬a ∨ Β¬b
       Β¬a β†’ Β¬b  ≑   b β†’  a  ≑   a ∨ Β¬b

              a β†’ b ≑ Β¬a ∨ b                {implication}
              a β†’ b ≑ Β¬b β†’ Β¬a               {contrapositive}

        a ∧ (a β†’ b) β‡’ b                     {Modus Ponens}   a, a β†’ b ⊒ b
  (a β†’ b) ∧ Β¬b      β‡’ Β¬a                    {Modus Tollens}  a β†’ b, Β¬b ⊒ Β¬a
  (a ∨ b) ∧ Β¬a      β‡’ b                     {∨ syllogism}    (a ∨ b), Β¬a ⊒ b
  (a β†’ b) ∧ (b β†’ c) β‡’ a β†’ c                 {β†’ chain} transitivity
  (a β†’ b) ∧ (c β†’ d) β‡’ (a ∧ c) β†’ (b ∧ d)     {β†’ combination}

        (a ∧ b) β†’ c ≑ a β†’ (b β†’ c)           {Currying}
 (a β†’ b) ∧ (a β†’ Β¬b) ≑ Β¬a                    {absurdity}
              a ↔ b ≑ (a β†’ b) ∧ (b β†’ a)     {equivalence}

Last updated