Theorem DUAL-BA-1. An independent self-dual 6-basis for Boolean algebra.

\{ \begin{matrix}(x + y) · y = y & (x · y) + y = y \\ x · (y + z) = (y · x) + (z · x) & x + (y · z) = (y + x) · (z + x) \\ x + x′ = 1 & x · x′ = 0 \end{matrix} \} .

Independence is easily proved with three MACE runs showing that each equation of the left column is independent of the remaining five equations; a model of size three is quickly found in each case. In order to show that the set is a basis for Boolean algebra, it is sufficient to derive commutativity and associativity of either of the operations.

Proof (found by Otter 3.0.4 on gyro at 28.95 seconds).

1 x = x 2 B · A = A · B, (A · B) · C = A · (B · C) → □ 4,3 (x + y) · y = y 5 x · (y + z) = (y · x) + (z · x)

6 (x · y) + (z · y) = y · (x + z) [flip 5]

9,8 x + x′ = 1 11,10 (x · y) + y = y 12 x + (y · z) = (y + x) · (z + x) 13 x · x′ = 0

15  (x + y) · (z + y) = y + (x · z)  [flip 12]
18  0 + x′ = x′  [13 → 10]
21,20  x + x = x  [3 → 10]
23,22  x · x = x  [10 → 3]
29  x · (y + (z + x)) = x  [3 → 6 :11, flip]
31  x · y = y · x  [20 → 6 :21]
36,35  x · (y + x) = x  [22 → 6 :11, flip]
38,37  x + (y · x) = x · (x + y)  [22 → 6]
56  x + y = y + x  [22 → 12 :23]
72  0′ = 1  [8 → 18, flip]
76  0 · 1 = 0  [72 → 13]
94,93  x · (x + y) = x  [20 → 15 :4,38, flip]
98  x + (y · (z · x)) = x  [10 → 15 :4, flip]
115  x + (y · x) = x  [37 :94]
130  x + 0 = (0 + x) · (1 + x)  [76 → 12]
135  (0 + x) · (1 + x) = x + 0  [flip 130]
141  x′ · x = 0  [13 → 31, flip]
150  x + 0 = (y′ + x) · (y + x)  [141 → 12]
153,152 0 + x = x  [141 → 10]
155,154 x · (x′ + y) = y · x  [141 → 6 :153, flip]
156 (x′ + y) · (x + y) = y + 0 [flip 150]
161,160 x + 0 = x  [135 :153,36, flip]
164 (x′ + y) · (x + y) = y [flip 156 :161, flip]
235,234 (x · y) + z = (x + z) · (y + z)  [12 → 56, flip]

236  x′ + x = 1  [8 → 56, flip]^{276,275 x · 1 = x  [236 → 29]}^{366  (x + y) + x = x + y  [93 → 115]}^{1269  x + (x + y) = x + y  [56 → 366]}^{1623  (x′ + y) · x = y · x  [1269 → 154 :155, flip]}^{1922  (x + y′) · (y + x) = x  [56 → 164]}^{4171,4170 ((x + y′) · (z + y′)) · y = (x · z) · y  [12 → 1623]}^{5275,5274 (x · y) · z = x · (y · z)  [98 → 1922 :235,235,9,276,4171]}^{6098  □  [2 :5275 :31,1]}

2