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

Tuesday, February 1

We discussed problem 1 in Homework 4; I'm not going to reproduce
the discussion here, but we are going to do a fully worked out example
in class on Wednesday, so that it is clear what is wanted.

Reasoning justified in minute detail, as in Homework 4 or in
the natural deduction proofs we are getting into, is not being
presented as a style of proof we should normally do all the time;
the reason for studying this is to see what principles underlie our
usual reasoning.

We discussed Exercise 2 in Homework 3, which I am going to ignore,
since no one seemed to understand what I wanted:

the idea is that a sentence P <+> Q <+> R <+>...
linked by xor translates in the ``mod 2 arithmetic'' system to
the sum P+Q+R...  Such a sum is equal to 1 just in case an odd
number of the summands are equal to 1.  Thus the propositional
formula is true (the interpretation of 1) just in case an odd
number of the formulas linked by xor are true.

Then we look at chained biconditionals: P <-> Q <-> R <->...  will be
interpreted by P+Q+R... in the dual interpretation of the ``mod 2
arithmetic'' system, in which 0 stands for true and 1 for false.  A
sum will equal 0 if an even number of the summands are equal to 1;
using this dual interpretation, we see that the propositional formula
will be true (have value 0) just in case an even number of the
formulas in the chain of biconditionals are false (have value 1).

So the mod 2 arithmetic interpretation can be used to clarify 
the meanings of chains of propositions linked by the associative
operations <-> and <+>.

Homework 3 is an example of the interpretation of one mathematical
system inside another; this phenomenon occurs regularly in math and probably
in CS, and it's useful to have practice reasoning about it.

I put some additional rules on the board, but none were actually
used in example proofs that did not appear in the notes for the first
lecture, so I'll save new rules for the ``official'' list to appear
in a future set of notes (one hopes the notes for tomorrow!)

The example proofs we did in class:

Prove |- (P & Q) -> P (this is a tautology; this proof will
have no top-level premises).  

Proof:

| 1. P&Q premise of subproof
| 2. P by line 1, conjunction elimination 1
3. (P&Q)->P by lines 1-2, implication introduction

Prove {P->Q,Q->R} |- P->R

We first write down the two premises:

1.  P-> Q  premise
2.  Q -> R  premise

Someone suggested using an elimination rule here, but we
don't have one that applies (modus ponens and modus tollens don't
help us).

Suppose that we temporarily assume P

3. P

Then we can add more lines

4. Q by modus ponens, lines 3,1
5. R by modus ponens, lines 4,2

But the structure consisting of lines 1-5 as we have written them is
not a proof.  Here's how it really works:

1.  P-> Q  premise
2.  Q -> R  premise
| 3. P premise of subproof
| 4. Q by modus ponens, lines 3,1
| 5. R by modus ponens, lines 4,2
6. P->R by implication introduction, lines 3-5.

in which it is clear that the assumption in line 3 is doing something
quite different from the assumptions in lines 1 and 2.

The | characters in the margin are used to indent the subproof.  I could
be more fulsome and put them in a box:

1.  P-> Q  premise
2.  Q -> R  premise
----------------------------------
| 3. P premise of subproof       |
| 4. Q by modus ponens, lines 3,1|
| 5. R by modus ponens, lines 4,2|
----------------------------------
6. P->R by implication introduction, lines 3-5.

But I hope that the more economical convention will be clear enough.

Another numbering convention would make it clearer that the block is a unit:

1.  P-> Q  premise
2.  Q -> R  premise
--------------------------------------
| 3.1 P premise of subproof          |     
| 3.2 Q by modus ponens, lines 1, 3.1|
| 3.3 R by modus ponens, lines 2, 3.2|
--------------------------------------
4. P->R by implication introduction, ``line 3''

In any event, one cannot use any line inside a block outside that
block, but note that lines 1 and 2 are available inside the block.
Scoping conventions like this should be familiar from programming
languages.



Randall Holmes
2000-05-05