There is an important feature of Boolean algebra as a formal system which may be so obvious as to be invisible. We allow ourselves to replace any expression with an equivalent expression in the course of a calculation (and we also allow uniform replacement of any letter in a theorem with the same expression to generate a new theorem). These are the familiar rules of algebraic calculation familiar from high school in a new context. We present these rules in some detail. Let A[B/X] represent the propositional formula which results when we replace the propositional letter (variable) X with the propositional formula B in the propositional formula A. We have the following rules: 1. A == A is a theorem for any formula A. (equivalence is reflexive). 2. if A == B is a theorem then B == A is a theorem. (equivalence is symmetric). 3. if A == B and B == C are theorems, then A == C is a theorem. (equivalence is transitive). 4. if B == C is a theorem, then A[B/X] == A[C/X] is a theorem. (equals can be substituted for equals). 5. if A == B is a theorem, then A[C/X] == B[C/X] is a theorem. (any more specific value can replace a variable everywhere in an equation). These are the basic rules of inference used in algebra, except that we have equivalence instead of equality. There is an important difference between axioms (statements we agree are true when we start developing a logical or mathematical theory) and rules of inference (procedures which we accept for deriving new true statements (theorems) from old). To see how these principles work in algebraic reasoning (and even how they might be formalized in theorem proving or computer algebra software) let's take a look at what happens when an algebraic rule is applied in the example we did on Tuesday. Here's some text from the Tuesday notes: The result is == ((~P | Q) | ((~R | S) & (~S | R))) & ((~Q | P) | ((~R | S) & (~S | R))) We then distribute on the right in the left conjunct to get == (((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R))) & ((~Q | P) | ((~R | S) & (~S | R))) We are given the equation A | (B & C) == (A|B) & (A|C). We can use property 5 to conclude that (~P | Q) | ((~R | S) & (~S | R)) == ((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R)) (actually, we use property 5 three times, once replacing A with (~P | Q), once replacing B with (~R | S), and once replacing C with (~S | R)). We then use property 4 to prove the main result: consider the term X & ((~Q | P) | ((~R | S) & (~S | R))), and replace X by (~P | Q) | ((~R | S) & (~S | R)) to get the left side of the desired equation and by ((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R)) to get the right side of the equation. All of this might seem obvious and tedious when put this way. It's the same as what you might do in showing an algebraic step like this: (a+b)(c+d) - u(v+w) = (a(c+d) + b(c+d)) - u(v+w) The logical analysis of this calculation would look much the same. This calculation is easy and obvious for all of you because it's familiar from high school algebra; I want to make the point that generalizing those algebra skills (and understanding how to generalize them) will allow you to do computations in more general contexts. There's another analysis of this calculation which might be instructive. We'll look at how a computer program like Watson determines that the distributive law we used in the previous example can be applied and carries out the application. We are trying to apply the distributive law A|(B&C) == (A|B)&(A|C) to the term (~P | Q) | ((~R | S) & (~S | R)). The verification that the law applies proceeds by a process of ``matching'' the structure of the parse trees of the term A|(B&C) and the term (~P | Q) | ((~R | S) & (~S | R)). | | : : : -------------------------- ------------- : : : : | & A & ------- ----------------- ----------- : : : : : : ~ Q --------- ------------- B C : : : : : P ~ S ~ R : : R S The story goes as follows: at the top level, both terms match (we see that | is the top-level connective in both cases. So we match the corresponding subterms. On the left, the variable A matches the term ~P|Q, so we record something like A --> ~P|Q. On the right, we see terms which match so far (they are both conjunctions) so we match their corresponding subterms. On the left, we have B matching ~R|S, so we record B --> ~R|S. On the right, we have C matching ~S|R, so we record C --> ~S|R. We use the list of variable matchings we have constructed: A --> ~P|Q B --> ~R|S C --> ~S|R as a directive to make substitutions in the other side (A|C) & (A|B) of the equation we are applying: the result is ((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R)) The rules of the matching process are that at each step we have to see the same ``top connective'' (and match corresponding subterms) or see a propositional letter (in a more general context, a free variable) matching any term. Moreover, the matches assigned to propositional letters must be consistent. For example, if we tried to use the same procedure to apply the theorem P&P == P to the formula A&B we would need to match the term P&P to the term A&B: the first step would succeed (the two terms have the same top connective) but we would get two different matches P --> A P --> B when we tried to match the subterms, which indicates that the theorem cannot be applied (the matching process fails). This is also an outline of the procedure that the theorem prover uses when it tries to apply a theorem. I hope that you see that this is a procedure which lends itself to computer implementation.