Theorem BA-1. A first-order proof of Frink’s theorem.

\{ \begin{matrix}x + x = x \\ ((x + y) + z) + u = (y + z) + x → ((x + y) + z) + n(u) = 0 \\ ((x + y) + z) + n(u) = 0 → ((x + y) + z) + u = (y + z) + x \end{matrix} \} ⇒

\{ \begin{matrix}n(x + n(y)) + n(n(x) + n(y)) = y \\ (x + y) + z = x + (y + z) \\ y + x = x + y \end{matrix} \} .

The conclusion is Huntington’s basis for Boolean algebra.

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

1 x = x 2 ((x + y) + z) + u = (y + z) + x → ((x + y) + z) + n(u) = 0 3 ((x + y) + z) + n(u) = 0 → ((x + y) + z) + u = (y + z) + x 4 n(A + n(B)) + n(n(A) + n(B)) = B, B + A = A + B,

(A + B) + C = A + (B + C) → □

6,5 x + x = x

8,7  x + n(x) = 0  [2,5 :6,6,6,6]
9  (x + y) + z = (y + z) + x  [5 → 3 :8 :1]
12  (x + y) + n(z) = 0 → (x + y) + z = (x + y) + x  [5 → 3 :6]
14  (x + y) + z = (z + x) + y  [flip 9]
22  (n(x) + y) + x = 0 + y  [7 → 9, flip]
25,24  (x + y) + x = x + y  [5 → 9, flip]
26  (x + n(y + x)) + y = 0  [7 → 9, flip]
34  (x + y) + n(z) = 0 → (x + y) + z = x + y  [12 :25]
47,46  0 + x = 0  [7 → 24 :8]
49,48  (x + y) + y = y + x  [9 → 24]
51  (n(x) + y) + x = 0  [22 :47]
71  x + y = y + x  [5 → 14 :25,49]

74 n(A + n(B)) + n(n(A) + n(B)) = B,

(C + A) + B = A + (B + C) → □  [14 → 4 :71]
92,91  x + (x + y) = x + y  [24 → 71, flip]
94,93  (x + y) + z = x + (y + z)  [14 → 71]
95  x + (y + z) = y + (z + x)  [9 → 71 :94]
96  n(x) + x = 0  [7 → 71, flip]
98  n(A + n(B)) + n(n(A) + n(B)) = B → □  [74 :94 :95]
99  n(x) + (y + x) = 0  [51 :94]
101  x + (y + n(z)) = 0 → x + (y + z) = x + y  [34 :94,94]
103  x + (n(y + x) + y) = 0  [26 :94]
106,105 x + (y + x) = x + y  [24 :94]
107  x + (y + z) = z + (x + y)  [14 :94,94]
108  n(x) + (x + y) = 0  [71 → 99]
110  x + (y + n(x)) = 0  [71 → 108 :94]
131  x + (y + n(y + x)) = 0  [105 → 103 :94,106]

137  x + (n(x + y) + y) = 0  [71 → 103]
167  n(A + n(B)) + n(n(B) + n(A)) = B → □  [71 → 98]
234  x + n(y) = 0 → x + y = x  [91 → 101 :92,6]
287  n(n(x)) + x = n(n(x))  [234,96]
289  n(x) + y = 0 → y + x = y  [71 → 234]
368,367 x + n(n(x)) = n(n(x))  [71 → 287]
386 x + n(n(n(x))) = 0 [287 → 110]
422,421 n(n(x)) = x  [234,386 :368]
424  x + y = 0 → x + n(y) = x  [421 → 234]
440  x + y = 0 → y + n(x) = y  [421 → 289]
544  x + n(y + n(x)) = x  [424,110]
546  n(x) + n(x + y) = n(x)  [424,108]
587  n(x + n(y)) + y = y  [71 → 544]
663,662 n(x + y) + n(y) = n(y)  [421 → 587]
700,699 n(x + y) + (z + n(x)) = z + n(x)  [546 → 107, flip]
797  n(x + y) + y = y + n(x)  [440,137 :94,700, flip]
801  x + n(x + y) = x + n(y)  [440,131 :94,663, flip]
1090,1089 n(x + y) + n(y + n(x)) = n(y)  [797 → 801 :663]
1099  B = B → □  [167 :1090,422]
1100  □  [1099,1]