Introduction and formalization of Boolean algebra

Recently I’ve been teaching my friend boolean algebra for their exams at university. Some exercises included simplifying boolean expressions. While teaching them, I noticed that we mostly relied on the transformation rules and almost mechanically simplified expressions (M of MIU, remember? :))

In this post, we will formalize this algebra and prove some properties about it.

Introduction

What is boolean algebra? It’s simply a formal system that proved to be useful, for example, in the design of digital circuits. We are given a digital circuit and if we represent it as a boolean expression, we can simplify this expression (according to some rules) and thus minimize the usage of logic gates.

The algebra consists of variables (x, y, z), operators + (“or”) and * (“and”), and symbols 0 and 1. The rules of inference (laws) are given in the table below.

Name	Operator and	Operator or
Idempotent Law	$x * x = x$	$x + x = x$
Associative Law	$(x * y) * z = x * (y * z)$	$(x + y) + z = x + (y + z)$
Commutative Law	$x * y = y * x$	$x + y = y + x$
Distributive Law	$x * (y + z) = x * y + x * z$	$x + (y * z) = (x + y) * (x + z)$
Identity Law: 0	$x * 0 = 0$	$x + 0 = x$
Identity Law: 1	$x * 1 = x$	$x + 1 = 1$
Complement Law	$x * \neg x = 0$	$x + \neg x = 1$
DeMorgan’s Law	$\neg (x * y) = \neg x + \neg y$	$\neg (x + y) = \neg x * \neg y$

Together with the Involution law: $\neg (\neg x) = x$

Using these simple rules we can simplify boolean expressions.

Example

For example, consider the expression $x * (\neg x + y)$ . This expression uses three logic gates: one “not” gate (for $\neg x$ ), one “and” gate (for $x$ and $\neg x + y$ ) and one “or” gate for $\neg x$ and $y$ .

We can transform it as follows:

Expression	Rule
$x * ~x + x * y$	Distributive law
$0 + x * y$	Complement law
$x * y$	Identity law

Now, the expression $x * y$ is the same as $x * (\neg x + y)$ but is less complex and uses less logic gates.

If this simplification looks magical to you, it is likely that you are seeing it for the first time. If you do it yourself a couple of times, you will get used to it and it becomes almost mechanical.

Formalization

What comes first to mind when talking about mechanical tasks? Computers!

Let’s formalize this in Metamath and make the computer verify our proofs.

We start by declaring the symbols:

$c = * + ~ ( ) wff |- 0 1 $.

Followed by declaring the variables:

$v x y z $.

As well as all the possible well-formed formulas:

wx $f wff x $.
wy $f wff y $.
wz $f wff z $.
 
wa $a wff ( x * y ) $.
wo $a wff ( x + y ) $.
wn $a wff ( ~ x ) $.
 
wZ $a wff 0 $.
wO $a wff 1 $.

We will use this substitution rule – namely $\frac{\vdash x, x = y}{\vdash y}$ :

${
    eq1 $e |- x $.
    eq2 $e |- x = y $.
    eq  $a |- y $.
$}

That’s the base of our system. Next, we’ll implement all the rules in a single go:

${ ia $a   |- ( x * x = x ) $. $}
${ io $a   |- ( x + x = x ) $. $}
${ aa $a   |- ( ( x * y ) * z ) = ( x * ( y * z ) ) $. $}
${ ao $a   |- ( ( x + y ) + z ) = ( x + ( y + z ) ) $. $}
${ ca $a   |- ( x * y ) = ( y * x ) $. $}
${ co $a   |- ( x + y ) = ( y + x ) $. $}
${ da $a   |- ( x * ( y + z ) ) = ( ( x * y ) + ( x * z ) ) $. $}
${ do $a   |- ( x + ( y * z ) ) = ( ( x + y ) * ( x + z ) ) $. $}
${ idaZ $a |- ( x * 0 ) = 0 $. $}
${ idaO $a |- ( x * 1 ) = x $. $}
${ idoZ $a |- ( x + 0 ) = x $. $}
${ idoO $a |- ( x + 1 ) = 1 $. $}
${ coa $a  |- ( x * ( ~ x ) ) = 0 $. $}
${ coo $a  |- ( x + ( ~ x ) ) = 1 $. $}
${ inv $a  |- ( ~ ( ~ x ) ) = x $. $}
${ dma $a  |- ( ~ ( x * y ) ) = ( ~ x ) + ( ~ y ) $. $}
${ dmo $a  |- ( ~ ( x + y ) ) = ( ~ x ) * ( ~ y ) $. $}

Woot.

We will now prove that from $x * 0$ it follows $0 * x$ , and $0$ subsequently. You can try proving the previous example, that from $x * (\neg x + y)$ ) it follows $x * y$ , but that will be slightly more complicated.

${
    $( We assume that we're given 0 * x $)
    Zax $e |- ( 0 * x ) $.
  
    $( Prove that we can deduce x * 0 $)
    xaZ $p |- ( x * 0 ) $=
        wZ wx wa $( wff 0 * x $)
        wx wZ wa $( wff x * 0 $)
        Zax      $( |- ( 0 * x ) $)
        wZ wx ca $( |- ( 0 * x ) = ( x * 0 ) $)
        eq
    $.
 
    $( Prove that we can deduce 0 from x * 0 $)
    Z $p |- 0 $=
        wx wZ wa   $( wff x * 0. This is `x` in `eq` $)
        wZ         $( wff 0. This is `y` in `eq` $)
        wx Zax xaZ $( |- x * 0 $)
        wx idaZ    $( |- x * 0 = 0 $)
        eq
    $.
$}

Metamath happily reported that all proofs are valid. 🙂