Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the identity:
F=x ⋅ Fx+x' ⋅ Fx'
F
x
x'
x
Fx
Fx'
F
x
1
0
The terms
Fx
Fx'
F
x
\operatorname{restrict}(F,x,0)
\operatorname{restrict}(F,x,1)
It has been called the "fundamental theorem of Boolean algebra". Besides its theoretical importance, it paved the way for binary decision diagrams (BDDs), satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits.In such engineering contexts (especially in BDDs), the expansion is interpreted as a if-then-else, with the variable
x
Fx
x
Fx'
x
A more explicit way of stating the theorem is:
f(X1,X2,...,Xn)=X1 ⋅ f(1,X2,...,Xn)+X1' ⋅ f(0,X2,...,Xn)
f(X1,X2,...,Xn)=X1 ⋅ f(1,X2,...,Xn) ⊕ X1' ⋅ f(0,X2,...,Xn)
f(X1,X2,...,Xn)=(X1+f(0,X2,...,Xn)) ⋅ (X1'+f(1,X2,...,Xn))
Repeated application for each argument leads to the Sum of Products (SoP) canonical form of the Boolean function
f
n=2
\begin{align} f(X1,X2)&=X1 ⋅ f(1,X2)+X1' ⋅ f(0,X2)\\ &=X1X2 ⋅ f(1,1)+X1X2' ⋅ f(1,0)+X1'X2 ⋅ f(0,1)+X1'X2' ⋅ f(0,0) \end{align}
Likewise, application of the dual form leads to the Product of Sums (PoS) canonical form (using the distributivity law of
+
⋅
\begin{align} f(X1,X2)&=(X1+f(0,X2)) ⋅ (X1'+f(1,X2))\\ &=(X1+X2+f(0,0)) ⋅ (X1+X2'+f(0,1)) ⋅ (X1'+X2+f(1,0)) ⋅ (X1'+X2'+f(1,1)) \end{align}
F=H'
Fx=H'x
If
F=G ⋅ H
Fx=Gx ⋅ Hx
If
F=G+H
Fx=Gx+Hx
If
F=G ⊕ H
Fx=Gx ⊕ Hx
F=x ⋅ Fx+Fx'
If F is negative unate then
F=Fx+x' ⋅ Fx'
\partialF | |
\partialx |
=Fx ⊕ Fx'
\forallxF=Fx ⋅ Fx'
\existsxF=Fx+Fx'
George Boole presented this expansion as his Proposition II, "To expand or develop a function involving any number of logical symbols", in his Laws of Thought (1854), and it was "widely applied by Boole and other nineteenth-century logicians".
Claude Shannon mentioned this expansion, among other Boolean identities, in a 1949 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.