next up previous
Next: Monday, January 31 (Lab Up: Lecture Notes Previous: Wednesday, January 26

Friday, January 28

Notes for Friday, January 28

Re Homework 3:

the tables

+ | 0 1     * | 0 1
-------     -------
0 | 0 1     0 | 0 0
1 | 1 0     1 | 0 1

given in the assignment admit three interpretations relevant to the

uninterpreted  sets of integers  logic interpretation  dual logic interpretation
0              odd integers      true                  false
1              even integers     false                 true
+              addition          <+> (xor)             <-> (biconditional)
*              multiplication    & (conjunction)       | (disjunction)

Because of the interpretation in the integers, we should be able to
see that + and * are commutative and associative, 0 is the identity
of +, 1 is the identity of *.  The additional rules x+x=0 and xx = x
can be verified by inspection.

We claim that the constant 1 and operators + and * are enough to define
all propositional connectives in the logic interpretation:

translate ~x by 1+x, x&y by xy and x|y by x+y+xy

We claim that the logical rules for this system described above are enough
to verify translations of all the axioms of Boolean algebra, and we ask
you to do the verification as exercise 1.

Here's an example:

Verify ~(x|y) == ~x & ~y

First translate into the notation of this system:

~(x|y) translates to 1+(x+y+xy)

~x & ~y translates to (1+x)(1+y)

then verify the equation 1+(x+y+xy) = (1+x)(1+y) between the translated

(1+x)(1+y) = 1+x+y+xy by standard algebra manipulations (and it's enough
to say that in this case; when the special rules x+x=0 and xx = x come
into play one should be more explicit).

Most of the laws of Boolean algebra listed in the notes should have
short verifications; ones involving disjunction will be the most

Exercise 2 requires you to think about the logical meaning of
formulas like




using this interpretation (actually, use the dual interpretation in
the second case).  In both cases, what you are thinking about is how
to evaluate the sum of a list of 0's and 1's in this little algebra; a
brief description of how to evaluate sums, filtered through the
logical interpretations, gives a brief description (already known to some
of you) of the truth values of propositional formulas of the two kinds

Natural Deduction

Now we will start to develop a style of formal reasoning in propositional
calculus which is more closely related to the way we ``naturally'' reason
(that's why I'll call it ``natural deduction'').

Any formal reasoning involves drawing a conclusion from a set of premises.

Where G is a set of formulas and C is a formula, we write

G |- C 

if the truth of all the elements of the set G (premises) allows
us to conclude that the formula C (the conclusion) is true.  The
meaning of this notation is related to but not identical to the meaning
of the notation A |= B (A entails B).  We call expressions of this
kind ``derivations''.

It is important to note that verification of assertions of the form
G|-C will generally be on syntactical grounds; we consider manipulations
of expressions (formal rules operating on syntax) rather than our
knowledge of what the expressions are supposed to mean (semantics).
Truth tables are an example of a semantically motivated method (though
we have seen in our motivation of Boolean algebra that a syntax-driven
approach can simulate truth table based reasoning).

Some rules about valid derivations:

G |- C when C is an element of G

If G is a subset of H and G |- C then H |- C

If G |- C1 and G u {C1} |- C2 then G |- C2

We can always take a premise as a valid conclusion, and adding more
premises does not affect the validity of our conclusion.  If we can
draw a conclusion from a set of premises, we can add that conclusion
to our set of premises and draw further conclusions (which will follow
from our original set of premises).

Now that we've introduced formal notation for these ideas, we'll
speak a little more informally about rules related to our connectives.

In any proof, we will have a theorem in mind to prove, which we will
call our ``goal'', and some premises which we are allowed to use (which
I may also call ``hypotheses'').

For each propositional connective, we will have two different kinds of rules.
``Introduction rules'' for a connective allow us to prove a goal
with that connective; ``elimination rules'' for a connective allow us
to use premises with that connective.  (The reasons for these names may
not be entirely obvious).

Let's start with the example of conjunction:

To prove a conclusion of the form A & B it seems natural to prove
A and then prove B, and the introduction rule for conjunction takes the



-------------  (conjunction introduction)

A & B

In terms of derivations, we can write this ``{A,B} |- A&B is a valid
derivation for any formulas A,B''

If we have a premise of the form A & B, how can we use it?  It seems
that one can draw the simpler conclusion A or the simpler conclusion B
(this seems to be all that one can do!)

so we have two elimination rules

A & B

-------------  (conjunction elimination 1)



A & B

-------------  (conjunction elimination 2)


In terms of derivations, {A&B}|-A and {A&B}|-B are valid derivations where
A and B are any formulas.

Even with this simple set of rules, we can actually prove things:

1.  A & B  (premise)

2.  A  (conjunction elimination 1 on line 1)

3.  B  (conjunction elimination 2 on line 1)

4.  B & A  (conjunction introduction on lines 3,2)

[a good question was raised at this point as to whether the order
3,2 is important here; I want to see if I can come up with an example
of a rule where it is important to indicate the order of the arguments]

from which we see that we can write {A & B} |- B & A

The format of proof with lines used here can be justified using the
properties of derivations given above.

We leave as an instructive exercise for the reader the restatement of this
proof in the language of derivations.

We briefly introduce an elimination rule



-------  implication elimination 1


doubtless familiar to most of you as Modus Ponens.

Another implication elimination rule is


P -> Q

----------  implication elimination 2


(not covered in lecture).

We briefly introduce the implication introduction rule, which has
new features.

In derivation form, the rule is this:

if G u {P} |- Q, then G |- P->Q

In English, to prove an expression of the form P->Q, introduce P
as a new premise, and prove Q.  The new premise P cannot be used outside
the context of this special proof.

This rule has the curious feature of allowing proofs with no premises
at all (no axioms):

1.  P (premise for subproof ending at line 2)

2.  P (copied from line 1)

3.  P -> P  (implication introduction, lines 1-2)

Of course, there is a premise in this proof in line 1, but it is 
a premise of a subproof, not of the entire proof.

In derivation form, this proof can be presented thus:

{P} |- P  (because P is an element of {P})

emptyset u {P} |- P  (set theory -- emptyset is the identity of union)

emptyset |- P->P  (implication introduction)

in which form it is clearer that P is not a true premise of the proof.

Randall Holmes