next up previous
Next: Friday, March 17, 2000, Up: Lecture Notes Previous: Solutions to the Proofs

Official List of Rules and Theorems

Official List of Rules and Theorems

This may of course have typos in it; please bring anything you have
doubts about to my attention!  Nothing in this handout may be taken
to contradict anything I said in class or in previous notes except
where I say this specifically.

Logical Rules

Rules are listed by connective or quantifier.  Notice that an
``introduction'' rule is a rule for proving a goal with the
appropriate top-level connective or quantifier, while an ``elimination''
rule is a rule for using a premise or previous conclusion with that
the appropriate top-level connective.

Negation

basic rules

P                                    P & ~P

~P                                   ----------  negation elimination

--------  negation elimination       Q

Q

Either form is OK.

G , P |- Q & ~Q

----------------  negation introduction

G |- ~P

If you don't like the |- notation, here's the box format:

G  (all your earlier knowledge)

Goal:  ~P

|  P            subpremise for neg. intro.
|  Goal: contradiction
|  .
|  .
|  .
|  Q & ~Q       (however you prove this)

~P              negation introduction, previous box

Double Negation

These are derived rules, but they are really part of our basic toolbox.

P                                     ~~P

----  double negation introduction    ------ double negation elimination

~~P                                   P

Conjunction

P                                 P & Q     P & Q

Q                                 ------    ------  conjunction elimination

------  conjunction introduction  P         Q       (no need to number them)

P & Q

Disjunction Elimination Rules

basic

P | Q           P | Q

~P              ~Q

-------         -------   disjunction elimination

Q               P


proof by cases:  this is a derived rule but again a basic part of our
toolkit.

P | Q

P -> R

Q -> R

-------  proof by cases (Grantham's disjunction elimination)

R

proof by cases also has a ``box'' form:

P | Q

|   P   subpremise for proof by cases (case 1)
|   .
|   .
|   R

(notice that these two boxes are separate)

|   Q
|   .
|   .
|   R

R          proof by cases -- you should refer to the disjunction and the two
           boxes if you use this form.

If you are uncertain about the box form, notice that it is easily 
expanded to the first form by using the boxes to prove the implications
P -> R and Q -> R.

Disjunction Introduction

basic rules:

G , ~P |- Q      G , ~Q |- P

-----------      ------------    disjunction introduction

G |- P | Q       G |- P | Q

or in box form

first box form:

Goal: P | Q

| ~P          subpremise for disj. intro.
| Goal: Q
| .
| .
| .
| Q

P | Q  disjunction introduction (refer to whole box)

second box form:

Goal: P | Q

| ~Q         subpremise for disj. intro.
| Goal: P
| .
| .
| .
| P

P | Q  disjunction introduction (refer to whole box)

derived rules:

P            Q

-----        -----        disjunction introduction (Grantham)

P | Q        P | Q


I also sometimes call these ``disj. intro. (special)''


______            excluded middle

P | ~P

Notice that this important derived rule has no premises.  It is
often useful with proof by cases.

Implication

basic rules:

P

P -> Q

--------   implication elimination (modus ponens)

Q


G , P |- Q

-----------  implication introduction

G |- P -> Q

or in box form

Goal: P -> Q

| P     subpremise for implication introduction
| Goal: Q
| .
| .
| Q

P -> Q      implication introduction (or m.p.), refer to prev. box.

handy derived rules:

P -> Q                       ~(P -> Q)

~Q                           ----------  negated implication elimination

--------  modus tollens      P & ~Q

~P

Now we start quantifiers.  I will not use explicit substitution
notation in these brief notes, so notice that Px may be any expression
-- and that Pa will be the result of replacing free occurrences of x
with a in Px.

First the easy rules:

(Ax. Px)

---------  universal quantifier elimination

Pa


Pa

----------  existential quantifier introduction

(Ex.Px)

Then the hard rules 

G |- Pa    where a does not occur in G

-------                              universal quantifier introduction

G |- (Ax.Px)

In box form:

| a=a            arbitrary object intro
| .
| .
| .
| Pa
(Ax.Px)          universal quantifier introduction, prev. box.

where a (which we would write as a Greek letter in class) does not
occur outside the box.  (actually, it's OK to re-use Greek letters which
have been used in previous boxes which are now closed, and we have done
this in class -- the point is that a cannot occur in any premises
we are allowed to use).  As I have said in class, the ``a=a'' has
no logical content -- it's just there so we see the locally declared
variable.

G , Pa |- Q     where a does not occur in G or Q

------------                     existential quantifier elimination

G , (Ex.Px) |- Q

In box form:

(Ex.Px)

| Pa          witness intro (refer to the line where Ex.Px occurs)
| .
| .
| .
| Q     

Q             existential quantifier elimination (refer to the prev. box)

The letter a (which would be a ``lucky charm'' in class) may not occur
outside the box.  (re-use of charms actually can occur in boxes which can't
see each other).  Notice that this means that the letter a cannot occur
in the conclusion Q, which is simply copied out of the box at the end.
You have permission to write something like ``ditto'' in place of
the second Q if Q is long.

Grantham does not use boxes with his lucky charms, and so must record
their possible dependencies on Greek letters.  This is an aspect of Grantham's
system you are not allowed to use; all lucky charms must be introduced
in boxes.

derived forms:

Even in the most formal style, I allow multiple uses of univ. elim.
at the same time.  You may use the recently described multiple universal
introduction rule as an ``official'' rule.

Other rules, such as the negation rules on Egbert's handout, may be used
where I do not restrict you to ``official'' rules.  Where I don't
restrict you to ``official'' rules you may introduce any obvious tautology
as a line and substitute logically equivalent formulas for one another.

Equality

Just for the sake of completeness I give the equality rules, though we
have seldom used them explicitly (mercifully!)


--------  equality introduction

t = t



t = u

Pt

--------  equality elimination

Pu

Axioms and Theorems of Arithmetic

Axioms:

1.  (Ax. ~x'=0)

2.  (Ax.(Ay.x = y <-> x' = y'))

I notice that I did present ax. 2 as a biconditional, but it is
nice to know that x=y -> x'=y' is just a consequence of properties of
equality.

3.  (Ax.x+0 = x)

4.  (Ax.(Ay.x+(y') = (x+y)'))

5.  (Ax.(Ay.x*0 = 0))

6.  (Ax.(Ay.x*(y') = (x*y)+x))

plus math induction which we present as a rule:

Goal: (Ax.Px)

Goal (basis step):  P0

(followed by proof of basis step...)

P0

|  Pa         ind hyp  (a is new in this box)
|  Goal: P(a')
|  .
|  .
|  .
|  P(a')

(Ax.Px)       math induction, refer to the line with P0 and the whole
              box with the induction step.


Definitions:

1 = 0'

(x =/= y) <-> (~ (x = y))

x <= y <-> (Ez. x+z = y)

x < y <-> (x <= y & x =/= y)

Even(x) <-> (Ey. y+y = x)

Odd(x) <-> (Ey. y+y' = x)

an equivalent form (which is used in the proof in the take-home)
is

Odd(x) <-> (Ey. (y+y)' =x)

You just need to apply axiom 4 to get from either one to the other.

Theorems proved in class:

T1. (Ax.x+1=x')

T2. (Ax. x=/=0 -> (Ey. y' = x))

T3. (Axy. x'+y = (x+y)')  (lemma in the proof of comm +)  

T4. (Axy. x+y = y+x)      (comm +)

T5. (Axyz. (x+y)+z = x+(y+z))   (assoc +)

T6. (Axyz. x+z = y+z -> x=y)    (cancellation property of addition)

T7. (Axy. x+y = x -> y = 0)     (this is a corollary of the last theorem)

T8. (Ax. x <= x)

T9. (Ax.((x <= y & y <= z) -> x <= z))

T10. (Ax. x*y = y*x)

Theorems we will assume in further work:

T11.  (Axy. (x <= y | y <= x))

T11 was left out of my earlier list by accident.

T12.  (Axy. (x <= y & y <= x) -> x = y)

T11 and T12 together give the standard trichotomy property of order.

I do not explicitly list well-known properties of <.

T13.  (x+y)*z = x*z + y*z

T14.  (x*y)*z = x*(y*z)

There may be well-known basic properties left off this list -- for example,
in class I proved x*1 = 1*x = x.  Ask me about anything obvious you
think I might have omitted -- or prove it if you can :-)



Randall Holmes
2000-05-05