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 :-)