A proof of Boole's Elimination Theorem

[Theorem 1.4.7. of LMCS]

This theorem is stated on page 24 of LMCS. Boole's proofs, as explained in the historical remarks, were pretty `wild'. Here is a modern version.

Theorem [Elimination Theorem] The most general equation that follows from is obtained by setting

or, more briefly,

where ranges over sequences of 1's and 0's.

Proof. First we show , for the stated choice of F. By expanding E about (see Problem 4.4 on page 25) we have

where . Then from follows

and thus

Taking the union of these two gives

and thus

Now repeat the above steps, except this time expand about , using the last equation which has the form , to obtain

where . Continuing one arrives at the desired conclusion that , as defined above, is 0.

For the converse suppose follows from . Let be any -constituent of H. Then for any -constituent we have is an -constituent of H. But then, by Theorem 4.5, LK must be an -constituent of E as follows from . Then has K as a -constituent, i.e., . So K is a -constituent of F as F is defined to be the intersection over the L's of the 's.

So every -constituent of H is also a -constituent of F. This means, by Theorem 4.5, that follows from , so is a more general conclusion than .