Proof Strategy I opened the lecture by asking the following question: Given Goal: (Ax.Px) | S and no special information about the context, write two following lines of the proof with appropriate goals, opening boxes where necessary. I suggested that this is the kind of question I might ask on an exam. Here is my analysis: Since the statement is a disjunction, and lacking information about the context, we should expect to prove it by disjunction introduction. This suggests that the following line should be either ~S or ~(Ax.Px): Goal: (Ax.Px) | S | next line: ~S subpremise for disj. intro. | Goal: (Ax.Px) OR Goal: (Ax.Px) | S | next line: ~(Ax.Px) subpremise for disj. intro. | Goal: S Of these two alternatives, the second gives us no help on how to write the next line (we might prefer it if the context contained additional information, but in our current vacuum of context information it is not appealing). Neither the premise ~(Ax.Px) nor the goal S suggest anything further without information from the context. However, the goal (Ax.Px) in the first alternative suggests that we should open a box for univ. intro: Goal: (Ax.Px) | S | next line: ~S subpremise for disj. intro. | Goal: (Ax.Px) | | another line: a=a arbitrary object intro | | Goal: Pa At this point we are helpless without more information from the context. Exercise: Compare this with what is likely to follow (Ax.Px | S). For the rest of the period, I discussed proof strategy, connective by connective. For each connective, the ``introduction'' rule tells us how to prove a goal with that connective as its top-level operation (in the in-class example, it was important to recognize that the top level operation in (Ax.Px) | S is NOT the universal quantifier but the disjunction, so it is NOT appropriate to open a box with arbitrary object intro). The ``elimination'' rule for a connective tells us how to use a previous line with that connective. Conjunction A conjunctive goal Goal: A & B simply breaks apart into two goals Goal: A Goal: B suggesting the following proof pattern: Goal: A & B Goal: A (proof steps) line m: A Goal: B (proof steps) line n: B line n+1: A & B conjunction introduction, lines m,n The typical method of using a conjunctive premise is very similar: line n: A & B line n+1: A line n+2: B Of course, the form of the context could suggest a quite different strategy: line n-1: (A & B) -> C line n. A & B suggests the quite different continuation line n+1: C modus ponens lines n-1,n Disjunction A disjunctive goal Goal: P | Q can be proved in one of four ways. If you can actually prove P or Q, you can prove P | Q this way: Goal: P | Q Goal: P (proof steps) line n: P line n+1: P | Q disj intro (Grantham) OR Goal: P | Q Goal: Q (proof steps) line n: Q line n+1: P | Q disj intro (Grantham) Notice that no box is introduced in either of these proof patterns. A theorem which is a disjunction is unlikely to be proved in this way, because we won't really be interested in a theorem of the form P | Q if P itself is a theorem (or Q). But this kind of proof of a disjunction is likely to occur inside boxes where one has additional assumptions available. A top level proof of a disjunction is more likely to take one of the forms Goal: P | Q | line m: ~P subpremise for disj. intro. | Goal: Q | | (proof steps) | | line n: Q line n+1: P | Q disj. intro. lines m-n OR Goal: P | Q | line m: ~Q subpremise for disj. intro. | Goal: P | | (proof steps) | | line n: P line n+1: P | Q disj. intro. lines m-n It is useful to notice (I asked this as a question in class) that a box like | line m: ~P subpremise | Goal: Q | | (proof steps) | | line n: Q can be used to prove P | Q by disj. intro, but can also be used to prove (~P) -> Q by imp. intro. It can be checked using truth tables that P | Q is equivalent to (~P) -> Q. I may ask questions in which I present a piece of a proof (like this box) and ask what has been proved. Implication The picture for implication is fairly simple. To prove a goal which is an implication we have usually used the standard implication introduction rule: Goal: P -> Q | line m: P subpremise for implication introduction | Goal: Q | | (proof steps) | | line n: Q line n+1: P->Q implication introduction, lines m-n This corresponds to a pattern in mathematical proofs stated in English: Theorem: P -> Q Assume P. Our goal is now to prove Q...(body of proof)...We have proved Q under the assumption that P, so we have established that P->Q. To use a previous line which is an implication, we have implication elimination, also called modus ponens: P P -> Q ------- Q We have variations on both introduction and elimination based on the equivalence of an implication P->Q with its contrapositive (~Q) -> (~P): the derived rule of modus tollens ~Q P -> Q -------- ~P has been used fairly often, and the following pattern of reasoning does appear in the notes above, though we have not used it (or not often): Goal: P->Q | line m: ~Q subpremise for contrapositive introduction | Goal: ~P | | (Proof steps) | | line n: ~P line n+1: P -> Q contrapositive introduction, lines m-n Finally, there are some ``trivial'' implication introduction rules: ~P ------- P -> Q Q ------- P -> Q These suggest that if one has Goal: P->Q it might sometimes be useful (especially if one is inside boxes with additional hypotheses) to continue with Goal: ~P (for an application of false hypothesis) or Goal: Q (for an application of true conclusion) But these are NOT the rules which are usually used to prove implications. Existential Quantifier It is very important to understand the difference between the strategy to follow when one has an existential _premise_: line n: (Ex.Px) and the strategy to follow when one has an existential _goal_: Goal: (Ex.Px) When one has a goal (Ex.Px) one has to produce an object t, already declared in the current environment, and prove Pt. For example, if one can prove P0, one can prove (Ex.Px) in arithmetic. Proof pattern: Goal: (Ex.Px) Goal: Pt (where t is some specific already defined object) (proof steps) line n: Pt (Ex.Px) existential introduction, line n Notice that no box is introduced in this proof; t is not a ``locally declared'' object, but a specific already definable object. (One has to come up with the right object somehow -- this is not always easy!) If one has an existential hypothesis, one has quite a different pattern: line m: (Ex.Px) Goal: X (the structure of the goal isn't important here) | line n: Pa witness intro line n | Goal: X (the goal does not change) | | (proof steps) | | line p: X line p+1: X exist. elim. lines n-p Here the object a is a ``lucky charm'', a witness to an existential statement. It is locally declared inside the box (and does not occur in the goal X!) Here the logical issue is that one is given an existential premise (Ex.Px) but one is not told how to actually produce t such that Pt; the existential elimination rule (with its witness intro subrule) allows us to temporarily introduce such a t -- but we have to get rid of all mention of it when we leave the box. In English, there are proof patterns corresponding to these. For existential introduction: Our aim is to prove (Ex.Px). We set x=t... (body of proof) ... so we have proved Px for the particular value t of x, establishing our goal (Ex.Px). For existential elimination (with witness introduction): Since we are given the hypothesis (Ex.P(x)), we may introduce an object K such that P(K) ...(body of proof)... having drawn the conclusion X (not mentioning K) from the existence of K such that P(K), we conclude that X follows from the hypothesis (Ex.Px). You might want to look at the proof of the Division Theorem for examples of both of these patterns of reasoning presented in English. If one is proving an existential goal, one will not introduce a ``lucky charm'' related to that goal, but one _might_ want to introduce a lucky charm related to some existential hypothesis. line m: (Ex.Qx) Goal: (Ex.Px) | line n: Qa witness intro line m | | (proof steps) | | line p: Pa | line p+1: (Ex.Px) exist. intro. line p line p+2: (Ex.Px) exist. elim. line p+1 is a possible pattern of proof, in which we are somehow (using assumptions not shown) able to prove that any witness to the hypothesis (Ex.Qx) that we introduce will also turn out to be a witness to (Ex.Px). (these notes aren't finished yet -- more to come on Universal Quantifier and Negation, with final comments on indirect proof (proof by contradiction)). Universal Quantifier The universal quantifier, like conjunction, usually seems to present few difficulties. It is important not to get confused by formulas like (Ax.Px) | S in the class example -- this is not a universal quantified statement at top level, so one should apply disjunction introduction rules first. Proof of a universal goal: Goal: (Ax.Px) | line m: a = a arbitrary object intro | Goal: Pa | | (proof steps) | | line n: Pa line n+1: (Ax.Px) univ. intro. lines m-n This corresponds to the pattern of reasoning in English: Our aim is to prove (Ax.Px). Let x be arbitrary. ...(body of proof)...thus Px. Since x was chosen arbitrarily, we can conclude (Ax.Px). On the other hand, line m: (Ax.Px) (proof steps) line n: Pa illustrates use of a universal premise. In standard mathematical practice, explicit universal quantifiers are often omitted: we usually express the commutative law of addition as x+y = y+x rather than (Axy. x+y = y+x). Negation To prove a negated goal, we reason to a contradiction: Goal: ~P | line n: P subpremise for negation introduction | Goal: contradiction | | (proof steps) | | Q & ~Q Notice that the formula Q can be anything. The use of negated premises is a more difficult matter. The ``negation elimination'' rule (the ``official'' way to use negative premises) looks like this: P ~P ---- Q so we can deduce anything at all from a contradiction. One thing we can do with negation elimination is simplify the contradictions in proofs by negation introduction. Suppose we have a proof Goal: ~P | line m: P subpremise for negation introduction | Goal: contradiction | | (proof steps) | line x: Q | | line y: ~Q | | line n: Q & ~Q c.i. lines x,y ~P neg. intro. lines m-n Notice that we can use neg. elim. instead of c.i. in the last line of the box to replace Q & ~Q with any contradiction Z & ~Z, and the proof will still be valid: Goal: ~P | line m: P subpremise for negation introduction | Goal: contradiction | | (proof steps) | line x: Q | | line y: ~Q | | line n: Z & ~Z neg. elim. lines x,y ~P neg. intro. lines m-n This can be useful if Q is very long. A similar maneuver can be essential in this situation: earlier line: (Ex.Qx) Goal: ~P | line m: P subpremise for neg intro | Goal: contradiction: | | line m+1: Qa witness intro earlier line | | Goal: contradiction | | | | (proof steps) | | | | line x: Ra | | | | (proof steps) | | | | line y: ~Ra | | line y+1: Z & ~Z (Z just a propositional letter) neg. elim. lines x,y | line y+2: Z&~Z exist. elim. line y+1 line y+3: ~P neg intro lines m-(y+2) The problem with putting the obvious contradiction Ra & ~Ra on line y+1 is that you cannot copy it out of the ``witness box'' using exist elim, because it mentions the lucky charm. This is not a feature of mathematical reasoning in English, because we simply say there is a contradiction rather than citing a specific one in English. This is purely a technical issue in the formal system (and could be avoided -- for example, if we had ``false'' or ``contradiction'' as a formula we could use it as the conclusion in neg. intro. boxes). Hints for Using Negative Premises The ``official'' ways to use negative premises are in negation elimination (where along with ~P you also need P) and disjunction elimination (where along with ~P you need P | Q). A derived rule which involves negation is modus tollens. A common situation where a negative premise can be used is in a proof by negation introduction earlier line: ~Q Goal: ~P | n. P premise for neg. intro. | Goal: contradiction | Goal: Q (which will give a contradiction with the earlier line) etc. Indirect Proof When all else fails in the proof of a goal Q, we can resort to indirect proof. The proof strategy is easily summarized: Goal: Q (and we have no help from the structure of Q or earlier premises) Goal: ~~Q (attempt indirect proof of Q) | m. ~Q subpremise for negation introduction | Goal: contradiction | | (proof steps) | | n. R & ~R n+1. ~~Q neg intro lines m-n n+2. Q d.n.e. lines m-n In general, we go for indirect proof where the internal structure of the goal gives us no help. In practice, this tends to mean that the goals we prove indirectly will either be atomic sentences (with no top-level connective to guide use of an introduction rule) or existentially quantified sentences (Ex.Px) where we cannot produce a goal Pt (there might be no objects t we know how to describe in the environment, as in the first problem in Homework 7) In the latter case, the informal approach (or the formal approach if we add a suitable rule) would be to prove (Ex.Px) by introducing (Ax. ~Px) as a hypothesis and reasoning to a contradiction (this uses the ``deMorgan'' equivalence between (Ax. ~Px) and ~(Ex.Px) as well as double negation). Anonymous Objects A final point: it is permissible to introduce free variables into proofs which are not arbitrary objects (``Greek curveballs'') or witnesses (``lucky charms''). We give an example: 1. (Ax.Px) premise 2. Py univ. elim. line 1 3. (Ex.Px) exist. intro. line 2. When we do this, we are appealing to the fact that our logic proves that the universe is inhabited. We had a discussion in class as to whether such anonymous objects are more like ``Greek curveballs'' or ``lucky charms''; they are probably a bit more like lucky charms, but they have universal scope (they do not live in a box). I don't think that any proof requires anonymous objects, but some proofs can be shortened by using them.