Boole's expansion theorem


Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the identity:, where is any Boolean function, is a variable, is the complement of, and and are with the argument set equal to and to respectively.
The terms and are sometimes called the positive and negative Shannon cofactors, respectively, of with respect to. These are functions, computed by restrict operator, and .
It has been called the "fundamental theorem of Boolean algebra". Besides its theoretical importance, it paved the way for binary decision diagrams, satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits.

Statement of the theorem

A more explicit way of stating the theorem is:

Variations and implications

; XOR-Form : The statement also holds when the disjunction "+" is replaced by the XOR operator:
; Dual form: There is a dual form of the Shannon expansion :
Repeated application for each argument leads to the Sum of Products canonical form of the Boolean function. For example for that would be
Likewise, application of the dual form leads to the Product of Sums canonical form :

Properties of Cofactors

; Linear Properties of Cofactors:
; Characteristics of Unate Functions:

Operations with Cofactors

; Boolean Difference:
; Universal Quantification:
; Existential Quantification:

History

presented this expansion as his Proposition II, "To expand or develop a function involving any number of logical symbols", in his Laws of Thought, and it was "widely applied by Boole and other nineteenth-century logicians".
Claude Shannon mentioned this expansion, among other Boolean identities, in a 1948 paper, and showed the switching network interpretations of the identity. In the literature of computer design and switching theory, the identity is often incorrectly attributed to Shannon.

Application to switching circuits

  1. Binary decision diagrams follow from systematic use of this theorem
  2. Any Boolean function can be implemented directly in a switching circuit using a hierarchy of basic multiplexer by repeated application of this theorem.