Propositional Logic: subproofs

Subproofs The reductio ad absurdum (RAA), Latin for reduction to absurdity, seems very strange: If we can prove that is true, then we can prove the negation of our premise. Huh!?! What on Earth does it mean to prove that false is true? This is known as proof-by-contradiction. We start by making a single unproven assumption. We then try to prove that is true. Clearly, that it nonsense, so we must have done something wrong. Assuming we didn't make any mistakes in the individual inference steps, then the only thing that could be wrong is the assumption. It must not hold. Therefore, we have just proven its negation. This form of reasoning is often expressed via contrapositive. Consider the slogan If you paid list price, you didn't buy it at SuperMegaMart. (This is a contrapositive, because the real statement the advertisers want to make is that if you buy it at SuperMegaMart, then you won't pay list price.), which we'll abbreviate payFull boughtAtSMM . You know this slogan is true, and you just made a SuperMegaMart purchase (boughtAtSMM), and are suddenly wanting a proof that you got a good deal. Well, suppose we didn't. That is, suppose payFull. Then by the truth of the marketing slogan, we infer boughtAtSMM. But this contradicts boughtAtSMM (that is, from boughtAtSMM and boughtAtSMM together we can prove that is true). The problem must have been our pessimistic assumption payFull; clearly that couldn't have been true, and we're happy to know that payFull. Spot the proof-by-contradiction used in The Simpsons: Bart, filing through the school records: Hey, look at this: Skinner makes $25,000 per year! Other kids: Ooooh! Milhouse: And he's 40 years old; that makes him a millionaire! Skinner, indignantly: I wasn't a principal when I was 1! Milhouse: And, he paints houses during the summer … he's a billionaire! Skinner: If I were a billionaire, would I still be living with my mother? [Kids' laughter] Skinner, to himself: The kids just aren't responding to logic anymore! In the particular set of inference rules we have chosen to use, RAA is surprisingly important. It is the only way to prove formulas that begin with a single ¬. This is an example of reasoning about our logic system. It shows us that while we might have some redundant inference rules, RAA isn't one of them. The only other rule which produces formulas starting with an initial ¬ is ¬Intro. Is this also essential, or could we still prove all the same things even without ¬Intro? We'll prove ⊢ α α . 1subproof: α α ⊢ 1.a α α Premise for subproof 1.b α ∧Elim (left), line 1.a, where φ α , and ψ α 1.c α ∧Elim (right), line 1.a, where φ α , and ψ α 1.d Intro, lines 1.b,1.c, where φ α 2 α α RAA, line 1, where φ α α

Here's another relatively simple example which uses RAA. Show that the modus tollens rule holds: α β, β ⊢ α 1α β Premise 2β Premise 3subproof:α ⊢ 3.a α Premise for subproof 3.b β ⇒Elim, lines 1,3.a 3.c Intro, lines 2,3.b 4α RAA, line 3

Another use of subproofs is to organize proofs' presentations. Many proofs naturally break down into larger subparts, each with its own intermediate conclusion. These steps between these subparts are big enough to correspond to our intuition, but too big to correspond to individual inference rules. This gives additional useful structure to a proof, aiding our understanding. Previously, we showed that ∧ (AND) commutes. However, that conclusion is only directly applicable when the ∧ is at the top-level, i.e., not nested inside some other connective. Here, we'll show that ∧ commutes inside ¬, or more formally, α β ⊢ β α . When doing inference-style proofs, we will not use the Boolean algebra laws nor replace subformulas with equivalent formulas. Conversely, when doing algebraic proofs, don't use inference rules! While theoretically it's acceptable to mix the two methods, for homeworks we want to make sure you can do the problems using either method alone, so keep the two approaches separate! We'll do two proofs of this to illustrate that there's always more than one way to prove something! In our first proof, we'll use RAA. Why? Looking at our desired conclusion, what could be the last inference rule used in the proof to reach the conclusion? By the shape of the formula, the last step can't use any of the introduction inference rules (∧Intro, ∨Intro, ⇒Intro, Intro, or ¬Intro). We could potentially use any of the elimination inference rules. But, for ∧Elim, ∨Elim, ⇒Elim, ¬Elim, or CaseElim, we would first have to prove some more complicated formula to obtain our desired conclusion. That seems somewhat unlikely or unnecessary. For Elim, we'd have to first prove , i.e., obtain a contradiction, but our only premise isn't self-contradictory. The only remaining option is RAA. 1 α β Premise 2subproof:β α ⊢ 2.a β α Premise for subproof 2.b α β Theorem: ∧ commutes, line 2a 2.c Intro, lines 1,2.b 3 α β RAA, line 2

The proof above uses a subproof because it is necessary for the use of RAA. In contrast, the proof below uses two subproofs simply for organization. For our second proof, let's not use RAA directly. Our plan is as follows: Assume the premise α β. Again, use commutativity to show that β α α β Use modus tollens to obtain the conclusion. We can organize the proof into corresponding subparts: 1α β Premise 2subproof: β α α β 2.a β α ⊢ α β Theorem statement: ∧ commutes 2.b β α α β ⇒Intro, line 2.a 3subproof:β α 3.a β α α β , α β ⊢ β α Theorem statement: modus tollens 3.b β α α β α β β α ⇒Intro, line 3.a 3.c β α α β α β ∧Intro, lines 2,1 3.d β α ⇒Elim, lines 3.b,3.c

More examples Now let's use these rules in a couple larger proofs, to show some more interesting results. Let's redo the first example's proof formally and show H-has-2 J-safe ⊢ G-unsafe. The inference rules we used informally above don't correspond exactly to those in our definition, so the formal proof is more complicated. 1 H-has-2 P-unsafe G-unsafe J-unsafe P-unsafe G-unsafe J-unsafe WaterWorld axiom, choosing a grouping of the ternary ∨, as justified by ∨ commutativity 2H-has-2 J-safe Premise 3H-has-2 ∧Elim (left), line 2 4 P-unsafe G-unsafe J-unsafe P-unsafe G-unsafe J-unsafe ⇒Elim, lines 1,3 5J-safe ∧Elim (right), line 2 6 J-safe J-unsafe WaterWorld axiom 7J-unsafe ⇒Elim, lines 5,6 8subproof:G-unsafe J-unsafe ⊢ 8.a G-unsafe J-unsafe Premise for subproof 8.b J-unsafe ∧Elim (right), line 8.a 8.c Intro, lines 7,8.b 9 G-unsafe J-unsafe RAA, line 8 10 P-unsafe G-unsafe J-unsafe P-unsafe CaseElim (right), lines 4,9 11subproof:J-unsafe P-unsafe ⊢ 11.a J-unsafe P-unsafe Premise for subproof 11.b J-unsafe ∧Elim (left), line 11.a 11.c Intro, lines 7,11.b 12 J-unsafe P-unsafe RAA, line 11 13P-unsafe G-unsafe CaseElim (right), lines 10,12 14G-unsafe ∧Elim (right), line 13

Wow! This formalization is a lot longer than the original informal proof. That's a result of the particular set of inference rules we are using, that we can only make inferences in small steps. Also, here we were pickier about the distinction between not safe and unsafe. The previous example is a perfect candidate for adding structure to the proof by using additional subproofs. The following is more similar to the original informal proof. Note also that subproofs can have their own subproofs. 1 H-has-2 P-unsafe G-unsafe J-unsafe P-unsafe G-unsafe J-unsafe WaterWorld axiom, choosing a grouping of the ternary ∨, as justified by ∨ commutativity 2subproof:⊢ H-has-2 2.a H-has-2 J-safe Premise 2.b H-has-2 ∧Elim (left), line 2.a 3 P-unsafe G-unsafe J-unsafe P-unsafe G-unsafe J-unsafe ⇒Elim, lines 1,3 4subproof:⊢ J-unsafe 4.a H-has-2 J-safe Premise 4.b J-safe ∧Elim (right), line 4.a 4.c J-safe J-unsafe WaterWorld axiom 4.d J-unsafe ⇒Elim, lines 4.b,4.c 5subproof:⊢ P-unsafe G-unsafe 5.a subproof:G-unsafe J-unsafe ⊢ 5.a.i G-unsafe J-unsafe Premise for subproof 5.a.ii J-unsafe ∧Elim (right), line 5.a.1 5.a.iii Intro, lines 4,5.a.2 5.b G-unsafe J-unsafe RAA, line 5.a 5.c P-unsafe G-unsafe J-unsafe P-unsafe CaseElim (right), lines 3,5.b 5.d subproof: J-unsafe P-unsafe ⊢ 5.d.i J-unsafe P-unsafe Premise for subproof 5.d.ii J-unsafe ∧Elim (left), line 5.d.1 5.d.iii Intro, lines 4,5.d.2 5.e J-unsafe P-unsafe RAA, line 5.d 5.f P-unsafe G-unsafe CaseElim (right), lines 5.c,5.e 6G-unsafe ∧Elim (right), line 5

A standard way of presenting proofs is by using lemmas to show parts of the proofs. Lemmas are simply formulas which we prove not as an end result, but as intermediate steps in a larger proof. So, they are simply another way of presenting subproofs.

Consider the above figure. We'll show B-has-1 G-has-1 J-has-1 ⊢ K-unsafe. We'll do this through the following series of lemmas: Lemma A: A-unsafe, G-has-1 ⊢ H-unsafe Lemma B: A-unsafe, B-has-1 ⊢ C-unsafe Lemma C: H-unsafe, C-unsafe, J-has-1 ⊢ Lemma D: A-unsafe, B-has-1 ⊢ C-safe Lemma E: A-unsafe, G-has-1 ⊢ H-safe Lemma F: C-safe, H-safe, J-has-1 ⊢ K-unsafe First, we'll show the main proof, assuming each of the lemmas. Then, proofs of each of the lemmas will follow. 1B-has-1 G-has-1 J-has-1 Premise 2B-has-1 ∧Elim (left), line 1 3G-has-1 J-has-1 ∧Elim (right), line 1 4G-has-1 ∧Elim (left), line 3 5J-has-1 ∧Elim (right), line 3 6subproof:A-unsafe ⊢ 6.a A-unsafe Premise for subproof 6.b H-unsafe Lemma A, lines 6.a,4 6.c C-unsafe Lemma B, lines 6.a,2 6.d Lemma C, lines 6.b,6.c,5 7A-unsafe RAA, line 6 8C-safe Lemma D, lines 7,2 9H-safe Lemma E, lines 7,3 10K-unsafe Lemma F, lines 8,9,5

And that's the desired proof! Now it just remains to show each of the six lemmas. Lemma A: A-unsafe, G-has-1 ⊢ H-unsafe 1A-unsafe Premise 2G-has-1 Premise 3subproof:A-unsafe H-safe ⊢ 3.a A-unsafe H-safe Premise for subproof 3.b A-unsafe ∧Elim 3.c Intro, lines 1,3b 4A-unsafe H-safe RAA, line 3 5 G-has-1 A-safe H-unsafe A-unsafe H-safe WaterWorld axiom 6 A-safe H-unsafe A-unsafe H-safe ⇒Elim, lines 5,2 7 A-unsafe H-safe A-safe H-unsafe Theorem: ∨ commutes, line 6 8A-safe H-unsafe CaseElim, lines 4,7 9H-unsafe ∧Elim (right), line 8

Lemma B: A-unsafe, B-has-1 ⊢ C-unsafe 1A-unsafe Premise 2B-has-1 Premise 3subproof:A-unsafe C-safe ⊢ 3.a A-unsafe C-safe Premise for subproof 3.b A-unsafe ∧Elim (left), line 3a 3.c Intro, lines 1,3b 4A-unsafe C-safe RAA, line 3 5 B-has-1 A-safe C-unsafe A-unsafe C-safe WaterWorld axiom 6 A-safe C-unsafe A-unsafe C-safe ⇒Elim, lines 5,2 7 A-unsafe C-safe A-safe C-unsafe Theorem: ∨ commutes, line 6 8A-safe C-unsafe CaseElim, lines 4,7 9C-unsafe ∧Elim (right), line 8

Proving the other lemmas is left as an exercise to the reader. Note that we took a little shortcut: we used the lemmas as if they were inference rules. According to our previous definition of proofs, we technically should present the lemma as a subproof and then use an inference rule or two to show how that applies, as we've done in previous examples. This shorter form is common practice and much easier to read.