Connexions

You are here: Home » Content » Propositional Logic: subproofs
Content Actions
Lenses

What is a lens?

Lenses

A lens is a custom view of Connexions content. You can think of it as a fancy kind of list that will let you see Connexions through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to Connexions materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual Connexions member, a community, or a respected organization.

This content is ...
Affiliated with (?)
This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.

  • This module is included inLens: Rice University OpenCourseWare
    By: OpenCourseWare ConsortiumAs a part of collection:"Intro to Logic"

    Click the "Rice University OCW" link to see all content affiliated with them.

    Rice University OCW
Tags

(?)

These tags come from the endorsement, affiliation, and other lenses that include this content.

Propositional Logic: subproofs

Module by: Ian Barland, John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen

Summary: Using subproofs, to show RAA or to aid in presentation.

Subproofs

The reductio ad absurdum (``RAA'', Latin for ``reduction to absurdity'', seems very strange: If we can prove that false 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 false 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)(payFull→¬boughtAtSMM). You know this slogan is true, and you just made a SuperMegaMart purchase (boughtAtSMMboughtAtSMM), and are suddenly wanting a proof that you got a good deal. Well, suppose we didn't — that is, suppose payFullpayFull. Then (by the truth of the marketing slogan), we infer ¬boughtAtSMM¬boughtAtSMM. But this contradicts boughtAtSMMboughtAtSMM (that is, from ¬boughtAtSMM¬boughtAtSMM and boughtAtSMMboughtAtSMM together we can prove that false is true). The problem must have been our pessimistic assumption payFullpayFull; clearly that couldn't have been true, and we're happy to know that ¬payFull¬payFull.
Example 1 
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 ``¬¬''. 1
Example 2 
We'll prove ⊢ ¬ (χ∧¬χ) ⊢ ¬ (χ∧¬χ) .
1subproof:(χ∧¬χ) ⊢ false(χ∧¬χ) ⊢   
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  false falseIntro, lines 1.b,1.c, where φφ=χχ
2¬ (χ∧¬χ) ¬ (χ∧¬χ)   RAA, line 1, where φφ=(χ∧¬χ)(χ∧¬χ)
Problem 1
Here's another relatively simple example which uses RAA. Show that the modus tollens rule holds: (χ→υ), ¬υ ⊢ ¬χ(χ→υ), ¬υ ⊢ ¬χ
[ Click for Solution 1 ]
Solution 1
1(χ→υ)(χ→υ)  Premise
2¬υ¬υ  Premise
3subproof:χ ⊢ falseχ ⊢   
3.a  χχ Premise for subproof
3.b  υυ →→Elim, lines 1,3.a
3.c  false falseIntro, lines 2,3.b
4¬χ¬χ  RAA, line 3
[ Hide Solution 1 ]
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.
Example 3 
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, ¬(χ∧υ) ⊢ ¬(υ∧χ)¬(χ∧υ) ⊢ ¬(υ∧χ).
warning: 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 — 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, falseIntro, 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 falseElim, we'd have to first prove false, i.e., obtain a contradiction, but our only premise isn't self-contradictory. The only remaining option is RAA.
1¬(χ∧υ)¬(χ∧υ)  Premise
2subproof:(υ∧χ) ⊢ false(υ∧χ) ⊢   
2.a  (υ∧χ)(υ∧χ) Premise for subproof
2.b  (χ∧υ)(χ∧υ) Theorem: ∧ commutes, line 2a
2.c  false falseIntro, 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:
  1. Assume the premise ¬(χ∧υ)¬(χ∧υ).
  2. Again, use commutativity to show that ((υ∧χ)→(χ∧υ))((υ∧χ)→(χ∧υ))
  3. Use modus tollens to obtain the conclusion.
We can organize the proof into corresponding subparts:
1¬(χ∧υ)¬(χ∧υ)  Premise
2subproof:((υ∧χ)→(χ∧υ))((υ∧χ)→(χ∧υ))  
2.a  (υ∧χ) ⊢ (χ∧υ)(υ∧χ) ⊢ (χ∧υ) Theorem statement: ∧ commutates
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.
Example 4 
Let's redo the first example's proof formally and show (H-has-2∧J-safe) ⊢ G-unsafe(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)))(H-has-2→(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe)))  WaterWorld domain axiom, choosing a grouping of the ternary ∨∨, as justified by ∨ commutativity
2(H-has-2∧J-safe)(H-has-2∧J-safe)  Premise
3H-has-2H-has-2  ∧∧Elim (left), line 2
4(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe))(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe))  →→Elim, lines 1,3
5J-safeJ-safe  ∧∧Elim (right), line 2
6(J-safe→¬J-unsafe)(J-safe→¬J-unsafe)  WaterWorld domain axiom
7¬J-unsafe¬J-unsafe  →→Elim, lines 5,6
8subproof:(G-unsafe∧J-unsafe) ⊢ false(G-unsafe∧J-unsafe) ⊢   
8.a  (G-unsafe∧J-unsafe)(G-unsafe∧J-unsafe) Premise for subproof
8.b  J-unsafeJ-unsafe ∧∧Elim (right), line 8.a
8.c  false falseIntro, lines 7,8.b
9¬ (G-unsafe∧J-unsafe) ¬ (G-unsafe∧J-unsafe)   RAA, line 8
10((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))  CaseElim (right), lines 4,9
11subproof:(J-unsafe∧P-unsafe) ⊢ false(J-unsafe∧P-unsafe) ⊢   
11.a  (J-unsafe∧P-unsafe)(J-unsafe∧P-unsafe) Premise for subproof
11.b  J-unsafeJ-unsafe ∧∧Elim (left), line 11.a
11.c  false falseIntro, lines 7,11.b
12¬ (J-unsafe∧P-unsafe) ¬ (J-unsafe∧P-unsafe)   RAA, line 11
13(P-unsafe∧G-unsafe)(P-unsafe∧G-unsafe)  CaseElim (right), lines 10,12
14G-unsafeG-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''.
Example 5 
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)))(H-has-2→(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe)))   WaterWorld domain axiom, choosing a grouping of the ternary ∨∨, as justified by ∨ commutativity
2subproof:⊢ H-has-2⊢ H-has-2   
2.a  (H-has-2∧J-safe)(H-has-2∧J-safe)  Premise
2.b  H-has-2H-has-2  ∧∧Elim (left), line 2.a
3(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe))(((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))∨(G-unsafe∧J-unsafe))   →→Elim, lines 1,3
4subproof:⊢ ¬J-unsafe⊢ ¬J-unsafe   
4.a  (H-has-2∧J-safe)(H-has-2∧J-safe)  Premise
4.b  J-safeJ-safe  ∧∧Elim (right), line 4.a
4.c  (J-safe→¬J-unsafe)(J-safe→¬J-unsafe)  WaterWorld domain axiom
4.d  ¬J-unsafe¬J-unsafe  →→Elim, lines 4.b,4.c
5subproof:⊢ (P-unsafe∧G-unsafe)⊢ (P-unsafe∧G-unsafe)   
5.a  subproof:(G-unsafe∧J-unsafe) ⊢ false(G-unsafe∧J-unsafe) ⊢   
5.a.i   (G-unsafe∧J-unsafe)(G-unsafe∧J-unsafe) Premise for subproof
5.a.ii   J-unsafeJ-unsafe ∧∧Elim (right), line 5.a.1
5.a.iii   false falseIntro, lines 4,5.a.2
5.b  ¬ (G-unsafe∧J-unsafe) ¬ (G-unsafe∧J-unsafe)   RAA, line 5.a
5.c  ((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))((P-unsafe∧G-unsafe)∨(J-unsafe∧P-unsafe))  CaseElim (right), lines 3,5.b
5.d  subproof:(J-unsafe∧P-unsafe) ⊢ false(J-unsafe∧P-unsafe) ⊢   
5.d.i   (J-unsafe∧P-unsafe)(J-unsafe∧P-unsafe) Premise for subproof
5.d.ii   J-unsafeJ-unsafe ∧∧Elim (left), line 5.d.1
5.d.iii   false falseIntro, lines 4,5.d.2
5.e  ¬ (J-unsafe∧P-unsafe) ¬ (J-unsafe∧P-unsafe)   RAA, line 5.d
5.f  (P-unsafe∧G-unsafe)(P-unsafe∧G-unsafe)  CaseElim (right), lines 5.c,5.e
6G-unsafeG-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.
Example 6 
ww-nontrivial.png
Figure 1: Example WaterWorld board
Consider the above figure. We'll show (B-has-1∧(G-has-1∧J-has-1)) ⊢ K-unsafe(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¬A-unsafe, G-has-1 ⊢ H-unsafe
  • Lemma B: ¬A-unsafe, B-has-1 ⊢ C-unsafe¬A-unsafe, B-has-1 ⊢ C-unsafe
  • Lemma C: H-unsafe, C-unsafe, J-has-1 ⊢ falseH-unsafe, C-unsafe, J-has-1 ⊢
  • Lemma D: A-unsafe, B-has-1 ⊢ C-safeA-unsafe, B-has-1 ⊢ C-safe
  • Lemma E: A-unsafe, G-has-1 ⊢ H-safeA-unsafe, G-has-1 ⊢ H-safe
  • Lemma F: C-safe, H-safe, J-has-1 ⊢ K-unsafeC-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.
1(B-has-1∧(G-has-1∧J-has-1))(B-has-1∧(G-has-1∧J-has-1))  Premise
2B-has-1B-has-1  ∧∧Elim (left), line 1
3(G-has-1∧J-has-1)(G-has-1∧J-has-1)  ∧∧Elim (right), line 1
4G-has-1G-has-1  ∧∧Elim (left), line 3
5J-has-1J-has-1  ∧∧Elim (right), line 3
6subproof:¬A-unsafe ⊢ false¬A-unsafe ⊢   
6.a  ¬A-unsafe¬A-unsafe Premise for subproof
6.b  H-unsafeH-unsafe Lemma A, lines 6.a,4
6.c  C-unsafeC-unsafe Lemma B, lines 6.a,2
6.d  false Lemma C, lines 6.b,6.c,5
7A-unsafeA-unsafe  RAA, line 6
8C-safeC-safe  Lemma D, lines 7,2
9H-safeH-safe  Lemma E, lines 7,3
10K-unsafeK-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¬A-unsafe, G-has-1 ⊢ H-unsafe
1¬A-unsafe¬A-unsafe  Premise
2G-has-1G-has-1  Premise
3subproof:(A-unsafe∧H-safe) ⊢ false(A-unsafe∧H-safe) ⊢   
3.a  (A-unsafe∧H-safe)(A-unsafe∧H-safe) Premise for subproof
3.b  A-unsafeA-unsafe ∧∧Elim
3.c  false falseIntro, lines 1,3b
4¬(A-unsafe∧H-safe)¬(A-unsafe∧H-safe)  RAA, line 3
5(G-has-1→((A-safe∧H-unsafe)∨(A-unsafe∧H-safe)))(G-has-1→((A-safe∧H-unsafe)∨(A-unsafe∧H-safe)))  WaterWorld domain axiom
6((A-safe∧H-unsafe)∨(A-unsafe∧H-safe))((A-safe∧H-unsafe)∨(A-unsafe∧H-safe))  →→Elim, lines 5,2
7((A-unsafe∧H-safe)∨(A-safe∧H-unsafe))((A-unsafe∧H-safe)∨(A-safe∧H-unsafe))  ∨∨ commutes, line 6
8(A-safe∧H-unsafe)(A-safe∧H-unsafe)  CaseElim, lines 4,7
9H-unsafeH-unsafe  ∧∧Elim (right), line 8
Lemma B: ¬A-unsafe, B-has-1 ⊢ C-unsafe¬A-unsafe, B-has-1 ⊢ C-unsafe
1¬A-unsafe¬A-unsafe  Premise
2B-has-1B-has-1  Premise
3subproof:(A-unsafe∧C-safe) ⊢ false(A-unsafe∧C-safe) ⊢   
3.a  (A-unsafe∧C-safe)(A-unsafe∧C-safe) Premise for subproof
3.b  A-unsafeA-unsafe ∧∧Elim (left), line 3a
3.c  false falseIntro, lines 1,3b
4¬(A-unsafe∧C-safe)¬(A-unsafe∧C-safe)  RAA, line 3
5(B-has-1→((A-safe∧C-unsafe)∨(A-unsafe∧C-safe)))(B-has-1→((A-safe∧C-unsafe)∨(A-unsafe∧C-safe)))  WaterWorld domain axiom
6((A-safe∧C-unsafe)∨(A-unsafe∧C-safe))((A-safe∧C-unsafe)∨(A-unsafe∧C-safe))  →→Elim, lines 5,2
7((A-unsafe∧C-safe)∨(A-safe∧C-unsafe))((A-unsafe∧C-safe)∨(A-safe∧C-unsafe))  ∨∨ commutes, line 6
8(A-safe∧C-unsafe)(A-safe∧C-unsafe)  CaseElim, lines 4,7
9C-unsafeC-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.
In summary, we must state one of the following four possible reasons for each step in a proof, allowing subproofs.
  • This step's WFF is a premise.
  • This step's WFF is an axiom.
  • This step's WFF follows from a inference rule applied to previous steps' WFFs. The reason includes a statement of which inference rule is used and how.
  • This step's WFF follows from a subproof, where that subproof may temporarily introduces additional premises. The reason includes the entire subproof. When that subproof has been shown elsewhere, such as in class or another exercise, it may simply be cited, for brevity. Of course, subproofs may have additional embedded subproofs, in turn.
Technically, when using subproofs, one must be careful to rename variables, to avoid clashes. Rather than formalize this notion, we'll leave it as ``obvious''.
1. 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?

Comments, questions, feedback, criticisms?

Send feedback