Theorem DUAL-BA-4. Independence of a Pixley 2-basis for BA. The following set is not a basis for Boolean algebra.

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

The clauses

x · (y + z) = (x · y) + (x · z) x + x′ = 1 (x · y′) + ((x · x) + (y′ · x)) = x (x · x′) + ((x · z) + (x′ · z)) = z (x · y′) + ((x · y) + (y′ · y)) = x A + A ≠ A

have the following model (found by MACE 1.2.0 on gyro at 0.03 seconds).

. | 0 1        + | 0 1        '   0 1        A: 1
--+----        --+----        -------
0 | 0 0        0 | 0 1            1 0
1 | 0 1        1 | 1 0