Formal Proofs and Boolean Logic PDF

FORMAL PROOFS AND BOOLEAN LOGIC CHAPTER 6 1 Formal rules for conjunction Some questions: What does a formal proof using conjunction elimination look like? What does a formal proof using the conjunction introduction look like?...

FORMAL PROOFS AND BOOLEAN LOGIC CHAPTER 6 1 Formal rules for conjunction Some questions: What does a formal proof using conjunction elimination look like? What does a formal proof using the conjunction introduction look like? 2 We are going to describe the formal counterparts of the informal reference rules: They make a part of the deductive system F, a natural deduction system. →Design to be a model of natural reasoning, the kind of reasoning we do every day →Thus, the relationship between formal and informal proofs is very direct. 3 When building a proof, you are required not to omit any steps—this is how a formal system departs from being a model of informal reasoning. Example: you cannot just assert one of de Morgan’s Laws in the middle of the proof → No rule in F allows it. → If you want such equivalence, you first have to prove it using the rules that F contains → You can prove anything in system F that a kind of a system we have looked at, that also contained equivalences could prove – we don’t really need de Morgan’s Laws because anything we can do with them, we can do that in our system F. 4 Natural deduction systems contain two inference rules for each connective in the language:  One allows us to prove a formula with that connective as its main connective – reasoning to conjunction, for example – Introduction rules → It allows us to introduce a formula with that connective as its main connective into the proof  The other rule enables us to prove things from sentences with this connective as its main connective – reasoning form conjunction, for example – Elimination rules. → It allows us to start with a sentence containing that connective as its connective and reason to conclude a sentence that may not have that connective. 5 Two inference rules for the identity predicate: 1. Identity Introduction →Allows us to assert t=t into a proof for any term t whenever we want to 2. Identity Elimination →Allows us to use an identity to substitute one name for an object for another name of the same object within another formula 6 Conjunction Elimination and Introduction The informal technique for reasoning about conjunction has simple steps:  If we have derived a conjunction, we can introduce any of its conjuncts into the proof – conjunction elimination.  Conjunction introduction – allows us to form a conjunction of any of the formulas we have already introduced into the proof. 7 Conjunction elimination P1…….Pn..... Pi The symbol for the inference rule we are describing – in this case, the conjunction elimination rule 8 is introduced in this step Conjunction elimination rule: If a conjunction in the proof consists of the conjuncts P1, P2, P3 to Pn, then we are entitled to infer Pi, i.e., any of those conjuncts. 9 Notice this important point: → The conjunction to which you apply ∧ Elim must appear by itself on a line in the proof. → You cannot apply this rule to a conjunction embedded in a larger sentence. For example, this is not a valid use of ∧ Elim: ∧ Elim can only be applied to 1. ¬(Cube(a) ∧ Large(a)) conjunctions, and the line 2. ¬Cube(a) ∧ Elim that X this “proof” purports to apply it to is a negation. 10 Conjunction introduction If in the proof we end up with sentences P1 up thorough Pn, The down no matter where in the proof arrow means they appear before the somewhere in concluding sentence, then we the proof, we P1 can use a conjunction have P1, P2, introduction to gather them etc. They do all together in a single not need to Pn conjunct. So, if we get, for appear in the example. P1, P2, P3, P4, we can order in which. then conclude P1 P2 P3 they appear in. P4….so forth. It can be used the for however many conjuncts conjunction – P1……Pn that we want to put together. we might have There may be sentences P1, P3, P5 – we between P1 and Pn that we are can then order Conclusion of the not using in this conjunction, them however concluding sentence provided the sentences P1 we want: of the rule 11 through Pn appear somewhere P5P1…, and so in the proof. They may be Example: the premise ABC The goal: CB →Discard the conjunct A and flip the order of the two conjuncts 1. ABC This also shows how you would prove 2. B  Elim 1 commutation of conjunction if you 3. C  Elim 1 wanted to. 4. C B  Intro 3,2 Suppose, the premise was just BC, and we want to conclude CB. Basically, the proof is here. It shows we 12 don’t need that equivalence. Using the conjunction rules in Fitch Three premises: Dodec(c)  Large(c) Tet(d)  Medium(d) Likes(c,d) Likes (d,c) Goals: Medium(d)  Large(c) Tet(d)  Dodec(c) ( Likes(c,d) Likes (d,c)) 13 First, let’s try to prove: Medium(d)  Large(c) 1. Dodec(c)  Large(c) 2. Tet(d)  Medium(d) 3. Likes(c,d) Likes (d,c) 4. Medium(d)  Elim 2 5. Large(c)  Elim 1 6. Medium(d)  Large(c)  Intro 4,5 7. Tet(d)  Elim 2 8. Dodec(c)  Elim 1 9. Tet(d)  Dodec(c) (Likes(c,d) Likes (d,c)) Intro 7,8,3 14 One of the things that Fitch lets us do is use -elimination to infer not just a single conjunct of the conjunction but any subset of the conjuncts of our support formula. Example: From sentence A  B C, I could directly infer sentence A  C in one step. 15 One tricky point when using -introduction: → When you use this rule, it's tempting to write the formulae in the support steps with conjunction symbols between them. → But this will sometimes result in not a well-formed sentence of the language. 1. AB 2. C 3. (AB)C Intro 1,2 We have to put parentheses to make the sentence well- formed (in order to avoid ambiguity) 16 The Formal Rules for Disjunction Questions:  Under which circumstances can we apply disjunction introduction?  Is it always the case that information increases when the formula gets longer?  What does disjunction elimination look like as a formal rule?  What is a subproof? 17 Disjunction Introduction  It throws away information.  It starts with a sentence P, and then we conclude PQ  It allows us to move from any formula to any disjunction that includes that formula as a disjunct (that formula could be anywhere in the disjunction). Pi.. You might need to introduce parentheses to ensure the. resulting formula is well- P1…Pi…Pn 18 formed. Disjunction Elimination and Subproofs  This corresponds to the method of proof that we called Proof by Cases  The method of proof involves making temporary assumptions  When we carry out Proof by Cases, we have a premise that is a disjunction, and we have to temporarily assume each of the disjuncts in turn to derive our common conclusion  These temporary assumptions work just like new premises for the proof, except they are only temporary  In the system F, we model the idea of a temporary assumption with what we call a subproof 19 A subproof – a smaller proof which appears as a component of the larger proof →It has premises, just like the larger proof –it has just one premise, the temporary assumption. →Contains steps that are produced by inferences →It is inside the main proof – it begins after the main proof and ends before the main proof. 20 Example: the same proof as an informal proof – goal BD 1.(AB)  (CD) Temporary assumptions don’t have 2.AB any justifications: – they are just assumptions they 3.B  Elim 2 do not follow from anything that’s 4.BD  Intro 3 gone before – we are assuming them 5.CD temporarily to see what happens 6.D  Elim 5 as it were, rather than asserting that they actually follow from 7.BD  Intro 6 anything that’s gone before –  Intro at steps 4 and 7 is 8.BD  Elim 1,2-4,5-7 necessary to make sure that we get the same sentences BD in each of our subproofs 21 This proof shows that BD follows from AB, and BD follows from CD. Consequently, it follows from the disjunction. The schematic form of the disjunction elimination: P1….Pn The subproof may be ended at any. time. When the subproof ends, the. vertical line stops, and the next line either “jumps out” to the original P1 vertical proof line or a new. subproof may be begun. As we’ll. see, ∨ Elim involves using two (or more) subproofs, typically S (although not necessarily) entered  one immediately after the other. Pn You must end the subproof first. before you begin the next. subproof. S 22 S The schematic form of the disjunction elimination rule shows the following things: 1. We need a disjunction P1 through Pn. 2. We need several subproofs, each of which begins with a different one of the disjuncts as its temporary assumption. 3. Here, we have proof P1 with its temporary assumption P1, and the proof leads to some formula S – we need proof like that for each of the disjuncts. 4. The down arrow indicates that we have a collection of subproofs, each leading to the same formula S, from a different temporary assumption, each of which is a disjunct of the original disjunction. 5. If we have a subproof like that for every disjunct of the original disjunction, and they all arrive at the same formula, S, then23we can infer S based on the disjunction alone. Example: Prove that A in either case 1.(AB)  (CA) In general, we need to cite the disjunction from which we are 2.AB eliminating that's providing us 3.A  Elim 2 with the temporary assumptions for each of the 4.CA cases and then each of the subproofs that justify our 5.A  Elim 4 common conclusion from one 6.A  Elim 1, 2-3, 4-5 of those temporary assumptions. We are citing the entire subproof as a part of the justification 24 Reiteration in Proof by Cases  Restating a formula that we have already earlier introduced into the proof  Sometimes, we want to use reiteration in some of the subproofs  It could be useful to give proof some substance, that is, in one of the cases when the temporary assumption gives you exactly the result that you want to reach 25 Example: 1.(AB)  A 2. AB 3. A  Elim 2 4. A 5. A Reit 4 6. A  Elim 1, 2-3, 4-5 26 Implementation in Fitch Example: (Cube(c)  Large(c))  Medium (c) Goal: Medium(c)  Large(c) 1. (Cube(c)  Large(c))  Medium (c) 2. Cube(c)  Large(c) 3. Large(c)  Elim 2 4. Medium (c)  Large(c)  Intro3 5. Medium(c) 6. Medium(c)  Large(c)  Intro 5 7. Medium(c)  Large(c)  Elim 1, 2-4, 5-6 27 The Formal Rules for Negation Some questions:  What is negation elimination?  What is negation introduction?  What is the rule that we must apply (beside  Intro itself), every time we apply  Intro?  Under what circumstances are we allowed to apply  Intro?  What is  Elim? 28 Negation Elimination  A simpler rule  It allows us to infer the conclusion S from P a formula of the form “not not S.”  It is like the principle of double negation.  The rule allows us to apply one-half of. that equivalence between S and “not not. S” to remove the double negation.  You cannot use the rule to add negations; P you only use it to infer a formula with them removed. 29 Negation Introduction  This is a formal analog of proof by contradiction.  We will need to use a subproof to indicate the fact that we are making a temporary assumption (proof by contradiction says if you want to prove something, assume its negation and show that a contradiction follows – then you can infer a thing you have started with) Subproof begins with the temporary P assumption of P.. In that subproof, if you can. derive a contradiction, indicated by the symbol. falsum, then you can conclude  the negation of P P 30 How do we get  into the proof?  We need a new inference rule to bring it into the proof.  The main reason that we need this symbol is that there are many different ways in which a contradiction can be found – we need something that we can use to represent any one of this set of contradictions.  A contradiction introduction or falsum introduction really gets all of the contradictions into a common form. 31 The contradiction introduction rule: If at any point in the proof you have a sentence P, and somewhere else in the proof, there is a sentence that negates P, you can conclude falsum, contradiction – you do that by contradiction introduction or falsum introduction. Ordinarily – we will use the contradiction introduction rule within a subproof, which will show that the assumption of the subproof contradicts the premises. We can use this rule at the top level of a proof, too – then we have shown that the initial premises of the proof are mutually inconsistent. 32 Deriving a Contradiction Goal: to prove  Tet(a) from the assumption Tet(a) 1. Tet(a) 2.  Tet(a) temporary assumption 3.  Intro 1,2 (we already have two formulae, P and P in the proof) If we can derive a contradiction from  Tet(a) we are 4.  Tet(a) permitted to infer  Tet(a) from this subproof The negation of the temporary assumption – negation introduction 2-3, 1 33 A negation introduction requires we cite the subproof, which starts with the assumption that we are trying to refute and ends with the contradiction symbol. The contradiction symbol is just another formula of our language, and it can be used in the same way:  For example, if we are in proof by cases, then this formula, the contradiction symbol, can serve as the common formula that we are deriving in each of the cases, as well as any other formula that can  If all of the subproofs in a proof lead to a contradiction, then this formula can be inferred by disjunction elimination 34 Example: 1. AB 2.  A 3.  B 4. A 5.   Intro 2,4 6. B 7.   Intro 3,6 8.   Elim 1, 4-5, 6-7 We have reached a contradiction within each of the proof 35 cases. The rule of contradiction:  It can introduce an explicit contradiction between a formula and its negation.  There are single sentences that are contradictory, such as (A A)  There are other mutually inconsistent sets of sentences: ⎯ Suppose we have derived every member of such a mutually inconsistent set of sentences in a proof ⎯ How are we going to prove a contradiction? – if we are in this situation where we have derived one or more sentences that are TT contradictory, then we can use the rules for Boolean connectives to derive P and P for some formula - we can then derive the contradiction symbol 36 Whenever we have a set of sentences that are mutually inconsistent, we can get from that set of sentences to an explicit contradiction between a formula P and another formula P: → Before doing such a proof, it is useful to check whether a set of sentences is mutually contradictory → In the Fitch program, use the Taut Con procedure to derive a contradiction 37  Other kinds of contradictions that are not tautological: Cube(b)  Cube(c) b=c These are mutually contradictory, but there is no truth table contradiction (it involves the meaning of the predicate equality): → The truth table method can only capture truth table contradictions. → When we have this kind of contradiction, we will need the rules of identity elimination and introduction in addition to the Boolean rules. → We might use those rules while developing the proof of contradiction. → We will need to use the FO Con rule from the Fitch program to derive the contradiction symbol (not the Taut Con rule) since the FO Con rule considers the identity predicate’s meaning. 38  A contradiction that depends on the meanings of the Blocks World predicates Cube(a) Tet(a) → This contradiction is neither a first-order contradiction nor a tautological contradiction. → We will use the Ana Con rule to infer an explicit contradiction since the Ana Con rule understands the meaning of the Blocks World predicates. Tet(a) You can infer Tet(a) from Cube(a) 39 So, we get a contradiction Tet(a) Tet(a) Other kinds of contradictions The rule of ⊥ intro lets us derive ⊥ whenever we have a pair of explicit contradictory sentences. But there are other contradictory pairs: non-explicit TT- contradictory, such as FO-contradictories that are TT-consistent, logical contradictories that are FO-consistent, and TW- contradictories that are logically consistent. 40 Here are some examples of these other types of contradictory pairs: Tet(a) ∨Tet(b) and Tet(a) ∧ Tet(b) TT-contradictory Cube(b) ∧ a = b and Cube(a) FO-inconsistent, but not TT- inconsistent Cube(b) and Tet(b) Logically inconsistent, but not TT or FO-inconsistent Tet(a) ∧ Cube(a) and Dodec(a) TW-inconsistent →In example (1), we have TT-contradictory sentences but not an explicit contradiction, as defined above. →In (2), we have a pair of sentences that are FO-inconsistent (they cannot both be true in any possible circumstance) but not TT-inconsistent (a truth- table would not detect their inconsistency). →In (3), we have a logically inconsistent pair but not FO-inconsistent (or TT- inconsistent). →In (4), we have a pair of TW-contradictories (there is no Tarski world in which both sentences are simultaneously true). However, they are 41logically consistent—an object can be neither a tetrahedron, cube, or dodecahedron (it may be a sphere). The rule of ⊥ Intro does not apply directly in any of these examples. In each case, it takes a bit of maneuvering before we develop an explicitly contradictory pair of sentences, as the rule requires. Example 1 1. Tet(a) ∨ Tet(b) Here, we used ∧ Elim twice to 2. Tet(a) ∧ Tet(b) get the two conjuncts of (2) separately, and then 3. Tet(a) ∧ Elim: 2 constructed a proof by cases 4. Tet(b) ∧ Elim: 2 to show that whichever disjunct of line (1) we choose, 5. Tet(a) we get to an explicit 6. ⊥ ⊥ Intro: 3, 5 contradiction. 7. Tet(b) 8. ⊥ ⊥ Intro: 4, 7 9. ⊥ ∨ Elim: 1, 5-6, 7-8 42 Example 2 1. Cube(b) ∧ a=b Here, we used ∧ 2. ¬Cube(a) Elim to get Cube(b) 3. Cube(b) ∧ Elim: 1 and a = b to stand alone, and then = 4. a=b ∧ Elim: 1 Elim (substituting 5. ¬Cube(b) = Elim: 2, 4 b for a in line 2) to 6. ⊥ ⊥ Intro: 3, 5 get the explicit contradiction of Cube(b). 43 Example 3 1. Cube(b) 2. Tet(b) 3. ¬Tet(b) Ana Con: 1 4. ⊥ ⊥ Intro: 2, 3 Here, we had to use Ana Con. Of course, as long as we were going to use Ana Con at all, we could have used it instead of ⊥ Intro to get our contradiction, as follows: 1. Cube(b) 2. Tet(b) 3. ⊥ AnaCon:1,2 44 Example 4 1. ¬Tet(a) ∧ ¬Cube(a) 2. ¬Dodec(a) 3. ⊥ AnaCon:1,2 To see these different forms of contradictions in action, do the You try it on p. 159. It’s an excellent illustration of these differences. You’ll find that you often need to use the Con mechanisms to introduce a ⊥ into your proof since ⊥ Intro requires an explicit contradiction in the form of a pair of sentences, P and ¬P. 45 Contradiction Elimination Inference rules in the system F always come in pairs – introduction and elimination rules for each connective. A rule for contradiction elimination:  Any sentence follows from a contradiction.  If you derive, at some point in your proof, the contradiction symbol, then you can introduce any sentence S whatsoever.  When we have a contradiction symbol in the proof, we know we are in the presence of inconsistent information.  One of the main uses of this inference rule is to ensure that a proof by cases will go through, even though some cases 46 are contradictory. Schema: ⊥... S 47 Example using Fitch: using this rule to infer Tet(a) from these premises: Tet(a)Cube(a) Contradiction elimination, which allows us to introduce Cube(a) any sentence, is not odd 1.Tet(a)Cube(a) when used in context. 2.Cube(a) In this particular case, contradiction elimination is 3. Tet(a) used inside the subproof, so 4. Tet(a) Reit 3 within this subproof, because the assumption is 5. Cube(a) contradictory, it contradicts 6.   Intro 2,5 some of our premises, we can infer any sentence we 7. Tet(a)  Elim 6 want – in this case, we needed Tet(a) – in the world 8.Tet(a) Elim 1,3-4,5-7 that that subproof 48 represents, things are so bizarre that anything is true. More on Subproofs Questions:  Can information inside a subproof be cited outside the subproof?  Can information outside a subproof be cited within the subproof?  What does “a proof of logical truth” look like? 49 Citing Formulae Inside Subproofs →We encounter two inference rules, disjunction elimination and negation introduction, whose application involves subproofs. The structure of subproofs is used to mark out where the assumptions are and what depends or may depend on that assumption:  Anything in the subproof may depend on that assumption  Once you have done with the subproof, you no longer have that assumption, and you cannot reach inside and 50 cite a sentence inside the subproof. A more general example: P  A subproof starts by introducing a new assumption.  In this schematic example, the assumption heading. up in the subproof is the formula R..  The reasoning within the subproof may depend on that assumption Q  Here, S may depend on both P, the premise of the R whole proof, and R, the temporary premise  Because S lives inside the subproof, and the. subproof ends, any subsequent reasoning may no longer use the assumption R or anything like S that S depends on it. T  We say that subproof has ended, and the assumption R has been discharged.  When we justify step T in this proof, we know that. we can’t cite the formula R or S 51  We might cite P or Q or even the subproof from R to S as a whole We cannot cite any sentence that appears in subproof from a place in the proof after the subproof has ended. → We are allowed to cite sentences that are outside of the subproof from within it. P.. Q The step R containing S might. cite P, Q, or any formula between, S provided the T formula doesn’t 52. appear in some other subproof. Proofs with no Premises What does this argument mean? (P  P) No premises The formula (PP) follows from no premises whatsoever – thus, the formula is a logical truth. If we were able to complete this proof based on no premises whatsoever, then we would have shown that the formula that we proved 53 is a logical truth There is a proof of validity of this argument:  The formula we are trying to prove is a negation, so it could be proven by a negation introduction, which requires a subproof in support – we get a premise for free, so to speak  No premises above the horizontal Fitch 1. P P bar  Assumption P P 2. P  Elim 1  We derive a contradiction using - 3. P  Elim 1 elimination in the context of a subproof  Once we have a contradiction, we can 4.   Intro 2,3 apply negation introduction, and we get the conclusion that we were trying to 5. (P  P)  Intro 1-4 prove (P  P) by negation introduction If a formula is provable from no premises, and the subproof 1-4 then that formula must be a logical truth 54 A sentence that can be proven without any premises is necessarily true. A proof with no premises can be constructed in a couple of ways: →Use negation introduction – could be used to prove any formula. →Use identity introduction to introduce an identity formula into the proof: Identity introduction doesn’t require citing an earlier step We can prove things about identity using no premises whatsoever (example page 175) 55 Summary: Advice on using subproofs The information inside a subproof cannot be cited outside of the subproof Within a subproof, you may cite information from outside, provided they are not themselves embedded inside a different subproof Information can go into a subproof, but not out 56 Strategy and Tactics for Formal Proofs Some questions: What should we do to show that the conclusion follows from the premises? What should we do to show that the conclusion doesn’t follow from the premises? Under which circumstances do we often apply the strategy of “working backward? 57 The Need for a Strategy Difficulties:  Knowing when to start and end subproofs  Knowing which formulas are available to cite from which point in the proof 58 Here are a few simple rules of thumb that can be used to construct formal proofs successfully: Always remember what sentences in the proof mean, so you don’t try to prove things that are not, in fact, consequences of premises. The first step should always be to convince yourself that the conclusion follows from the given information. Pretend you are trying to convince somebody else by writing an informal proof of why the conclusion follows from the premises. 59 Working Backwards A powerful technique for finding a formal proof It is often a good plan to insert the conclusion formula into the proof first and then think about what you would need to prove that conclusion. Add those other formulas into the proof and justify the inference of the goal formula from those formulas you have introduced using the appropriate inference rule. Then think about how to prove the new goal formulas and so on (hopefully, they are simpler than the formula you started with, or you can see more directly how to 60 prove them. Example using Fitch: →We should prove that a formula (Tet(a)Cube(b)) follows from the premise Tet(a)Cube(b) (an instance of one of de Morgan’s laws) If the premise formula is true, then one of P or Q is false, so the formula P and Q must be false, too. If the premise formula is true, Tet(a) is false, or Cube(b) is false. Thus, the conjunction Tet(a)Cube(b) must be false 61 1.Tet(a)Cube(b) 2. Tet(a)Cube(b) 3. Tet(a) 4. Tet(a) Elim 2 5. Intro 3,4 6. Cube(b) 7. Cube(b) Elim 2 8.  Intro 6,7 9.  Elim 1, 3-5, 6-8 10. (Tet(a)Cube(b)) Intro 2-9 62  The goal formula (Tet(a)Cube(b)) is a negation One way to prove a negation is to use proof by contradiction, negation introduction. Add Step Before Subproof – the assumption of the subproof is going to be Tet(a)Cube(b) If we can, within that subproof, prove a contradiction, then we can cite that subproof and use negation introduction to prove the conclusion that we want How to prove a contradiction – break into cases based on our premise and then prove a contradiction within each of the cases Add Step Before Two subproofs: in each of them, we want to prove a contradiction, and if we achieve that, we would be able to use -elimination rule and cite the premise and those two subproofs 1. assumption Tet(a) 63 2. assumption Cube(b) Since we have proven a contradiction in both subroofs, the contradiction Summary of how to construct proof (page 173): 1.Understand what sentences are saying 2.Decide whether the conclusion follows from the premises 3.If you are not sure, or you think it doesn’t follow, try to find a counterexample 4.If you think it does follow, try to give an informal proof for it (the rules of Fitch, actually, parallel the rules we use for informal proofs) 5.Try to convert your informal proof into a formal proof 64 6. Don’t forget the tactic of working backward 7. When working backward, make sure that the intermediate goals that you introduce to get the goal conclusion actually make sense and that they follow from the premises: → There are going to be many ways you could use to prove a goal → Some of the ways are going to be suggested by the structure of the formula, and some of them might not necessarily be based on the structure of the formula that we are trying to prove 65 8. A subproof is like a trap You always need to know how to get out before you get in If you are starting a subproof, be sure that you know why you are doing it At this point, we have two proof rules that involve subproofs, proof by contradiction, and proof by cases It would be best if you were sure you are doing one of those things before even thinking about setting up a subproof 66  You want to ensure the inference you are planning to do is going through before you work on the body of the subproof: →A proof by contradiction – start the subproof with the premise that the contradiction calls for, put in the line that has the contradiction symbol in it, and then check that this use of negation introduction is going to work before you think about filling in the body of the subproof →A proof by cases – always set up all of the subproofs with the correct assumptions and desired common conclusion, check that the disjunction elimination rule is going to work, and then work on the individual cases. 67