Derivation of some lemmas in Boolean algebra
It is shown here, step by step, how one can derive a set of lemmas
from the axioms
| There exist elements 0 and 1, which are not equal. | | [A1]
|
| AB = BA | A+B = B + A | [A2]
|
| A(B+C) = (AB)+(AC) | A+(BC) = (A+B)(A+C) | [A3]
|
| 1A = A | 0+A = A | [A4]
|
| A¬A = 0 | A+¬A = 1 | [A5]
|
The derivation of each lemma is presented only for one of the dual
formulas. The derivation of the missing formulas can be obtained by
exchanging sum and product, 0 and 1, and a and b in the numbers of
axioms.
L1: ¬¬A = A
| ¬¬A = | | | [A4a]
|
| 1¬¬A = | | [A2a]
|
| ¬¬A1 = | | [A5b]
|
| ¬¬A(A+¬A) = | | [A3a]
|
| ¬¬AA + ¬¬A¬A = | | [A2a]
|
| A¬¬A + ¬A¬¬A = | | [A5a]
|
| A¬¬A + 0 = | | [A5a]
|
| A¬¬A + A¬A = | | [A3a]
|
| A(¬¬A+¬A) = | | [A2b]
|
| A(¬A+¬¬A) = | | [A5b]
|
| A1 = | | [A2a]
|
| 1A = | | [A4a]
|
| | A
|
L2: AA = A (and A+A = A)
| AA = | | | [A4b]
|
| 0 + AA = | | [A5a]
|
| A¬A + AA = | | [A3a]
|
| A(¬A + A) = | | [A2b]
|
| A(A + ¬A) = | | [A5b]
|
| A1 = | | [A2a]
|
| 1A = | | [A4a]
|
| | A
|
L3: ¬0 = 1 (and ¬1 = 0)
| ¬0 = | | | [A4b]
|
| 0 + ¬0 = | | [A5b]
|
| | 1
|
L4: AB = 0 & A+B = 1 => B = ¬A
| B = | | | [A4a]
|
| 1B = | | [A2a]
|
| B1 = | | [A5b]
|
| B(A+¬A) = | | [A3a]
|
| BA + B¬A = | | [A2a]
|
| AB + ¬AB = | | [AB = 0]
|
| 0 + ¬AB = | | [A5a]
|
| A¬A + ¬AB = | | [A2a]
|
| ¬AA + ¬AB = | | [A3a]
|
| ¬A(A+B) = | | [A+B = 1]
|
| ¬A1 = | | [A2a]
|
| 1¬A = | | [A4a]
|
| | ¬A
|
L5: 0A = 0 (and 1+A = 1)
| 0A = | | | [A4b]
|
| 0 + 0A = | | [A5a]
|
| A¬A + 0A = | | [A2a]
|
| A¬A + A0 = | | [A3a]
|
| A(¬A+0) = | | [A2b]
|
| A(0+¬A) = | | [A4b]
|
| A¬A = | | [A5a]
|
| | 0
|
L6: A(A + B) = A (and A + AB = A)
| A(A+B) = | | | [A3a]
|
| AA + AB = | | [L2a]
|
| A + AB = | | [A4a]
|
| 1A + AB = | | [A2a]
|
| A1 + AB = | | [A3a]
|
| A(1+B) = | | [L5b]
|
| A1 = | | [A2a]
|
| 1A = | | [A4a]
|
| | A
|
L7: A(BC) = (AB)C (and A+(B+C) = (A+B)+C)
| A(BC) = | | | [A4b]
|
| 0 + A(BC) = | | [A5a]
|
| A¬A + A(BC) = | | [A3a]
|
| A(¬A+BC) = | | [L6a]
|
| [A(A+C)](¬A+BC) = | | [L6b]
|
| [(A+AB)(A+C)](¬A+BC) = | | [A3b]
|
| [A+(AB)C][(¬A+B)(¬A+C)] = | | [A4a]
|
| [A+(AB)C]{[1(¬A+B)](¬A+C)} = | | [A5b]
|
| [A+(AB)C]{[(A+¬A)(¬A+B)](¬A+C)} = | | [A2b]
|
| [A+(AB)C]{[(¬A+A)(¬A+B)](¬A+C)} = | | [A3b]
|
| [A+(AB)C][(¬A+AB)(¬A+C)] = | | [A3b]
|
| [A+(AB)C][¬A+(AB)C] = | | [A2b]
|
| [(AB)C+A][(AB)C+¬A] = | | [A3b]
|
| (AB)C + A¬A = | | [A5a]
|
| (AB)C + 0 = | | [A2b]
|
| 0 + (AB)C = | | [A4b]
|
| | (AB)C
|
L8: ¬A(AB) = 0 (and ¬A+(A+B) = 1)
| ¬A(AB) = | | | [L7a]
|
| (¬AA)B = | | [A2a]
|
| (A¬A)B = | | [A5a]
|
| 0B = | | [L5a]
|
| | 0
|
L9: ¬(AB) = ¬A+¬B (and ¬(A+B) = ¬A¬B)
| (AB)(¬A+¬B) = | | | [A3a]
|
| (AB)¬A + (AB)¬B = | | [A2a]
|
| ¬A(AB) + ¬B(BA) = | | [L8a]
|
| 0 + 0 = | | [A4b]
|
| | 0
|
| AB+(¬A+¬B) = | | | [A2b]
|
| (¬A+¬B) + AB = | | [A3b]
|
| [(¬A+¬B)+A][(¬A+¬B)+B] = | | [A2b]
|
| [A+(¬A+¬B)][B+(¬B+¬A)] = | | [L1]
|
| [¬¬A+(¬A+¬B)][¬¬B+(¬B+¬A)] = | | [L8b]
|
| 11 = | | [A4a]
|
| | 1
|
| (AB)(¬A+¬B) = 0 & AB+(¬A+¬B) = 1 => | | [L4]
|
| ¬(AB) = ¬A+¬B
|
L10: AB = 1 => A = 1 (and A+B = 0 => A = 0)
| A = | | | [A4a]
|
| 1A = | | [A2a]
|
| A1 = | | [A5b]
|
| A(B+¬B) = | | [A3a]
|
| AB + A¬B = | | [AB = 1]
|
| 1 + A¬B = | | [L5b]
|
| | 1
|
Last updated 15.10.1998
Harri Lappalainen
<Harri.Lappalainen@hut.fi>
