# Connexions

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

### Lenses

What is a lens?

#### Definition of a lens

##### Lenses

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

##### What is in a lens?

Lens makers point to 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 member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

#### Affiliated with (What does "Affiliated with" mean?)

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.
• Rice Digital Scholarship

This module is included in aLens by: Digital Scholarship at Rice UniversityAs a part of collection: "Intro to Logic"

Click the "Rice Digital Scholarship" link to see all content affiliated with them.

### Recently Viewed

This feature requires Javascript to be enabled.

# Propositional Logic: subproofs

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 ¬boughtAtSMMboughtAtSMM. But this contradicts boughtAtSMMboughtAtSMM (that is, from ¬boughtAtSMMboughtAtSMM 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 ¬payFullpayFull.

### 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 ¬(α¬α) α α .

 1 subproof:α∧¬α ⊢ 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 φ=α∧¬α φ α α

### Exercise 1

Here's another relatively simple example which uses RAA. Show that the modus tollens rule holds: αβ, ¬β ¬αα β, β α

#### Solution

 1 α⇒βα β Premise 2 ¬ββ Premise 3 subproof:α ⊢ 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

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 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, 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 2 subproof:β∧α ⊢ 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:

• 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 2 subproof:β∧α⇒α∧β β α α β 2.a β∧α ⊢ α∧ββ α ⊢ α β Theorem statement: ∧ commutes 2.b β∧α⇒α∧β β α α β ⇒Intro, line 2.a 3 subproof:¬(β∧α)β α 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-2J-safe G-unsafeH-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 axiom, choosing a grouping of the ternary ∨, as justified by ∨ commutativity 2 H-has-2∧J-safeH-has-2 J-safe Premise 3 H-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 5 J-safeJ-safe ∧Elim (right), line 2 6 J-safe⇒¬J-unsafe J-safe J-unsafe WaterWorld axiom 7 ¬J-unsafeJ-unsafe ⇒Elim, lines 5,6 8 subproof:G-unsafe∧J-unsafe ⊢ falseG-unsafe J-unsafe ⊢ 8.a G-unsafe∧J-unsafeG-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 11 subproof:J-unsafe∧P-unsafe ⊢ falseJ-unsafe P-unsafe ⊢ 11.a J-unsafe∧P-unsafeJ-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-unsafeP-unsafe G-unsafe CaseElim (right), lines 10,12 14 G-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 axiom, choosing a grouping of the ternary ∨, as justified by ∨ commutativity 2 subproof:⊢ H-has-2⊢ H-has-2 2.a H-has-2∧J-safeH-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 4 subproof:⊢ ¬J-unsafe⊢ J-unsafe 4.a H-has-2∧J-safeH-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 axiom 4.d ¬J-unsafeJ-unsafe ⇒Elim, lines 4.b,4.c 5 subproof:⊢ P-unsafe∧G-unsafe⊢ P-unsafe G-unsafe 5.a subproof:G-unsafe∧J-unsafe ⊢ falseG-unsafe J-unsafe ⊢ 5.a.i G-unsafe∧J-unsafeG-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 6 G-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

Consider the above figure. We'll show B-has-1G-has-1J-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-unsafeA-unsafe, G-has-1 H-unsafe
• Lemma B: ¬A-unsafe, B-has-1 C-unsafeA-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-1B-has-1 G-has-1 J-has-1 Premise 2 B-has-1B-has-1 ∧Elim (left), line 1 3 G-has-1∧J-has-1G-has-1 J-has-1 ∧Elim (right), line 1 4 G-has-1G-has-1 ∧Elim (left), line 3 5 J-has-1J-has-1 ∧Elim (right), line 3 6 subproof:¬A-unsafe ⊢ falseA-unsafe ⊢ 6.a ¬A-unsafeA-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 7 A-unsafeA-unsafe RAA, line 6 8 C-safeC-safe Lemma D, lines 7,2 9 H-safeH-safe Lemma E, lines 7,3 10 K-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-unsafeA-unsafe, G-has-1 H-unsafe

 1 ¬A-unsafeA-unsafe Premise 2 G-has-1G-has-1 Premise 3 subproof:A-unsafe∧H-safe ⊢ falseA-unsafe H-safe ⊢ 3.a A-unsafe∧H-safeA-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 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 Theorem: ∨ commutes, line 6 8 A-safe∧H-unsafeA-safe H-unsafe CaseElim, lines 4,7 9 H-unsafeH-unsafe ∧Elim (right), line 8

Lemma B: ¬A-unsafe, B-has-1 C-unsafeA-unsafe, B-has-1 C-unsafe

 1 ¬A-unsafeA-unsafe Premise 2 B-has-1B-has-1 Premise 3 subproof:A-unsafe∧C-safe ⊢ falseA-unsafe C-safe ⊢ 3.a A-unsafe∧C-safeA-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 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 Theorem: ∨ commutes, line 6 8 A-safe∧C-unsafeA-safe C-unsafe CaseElim, lines 4,7 9 C-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”.

## Footnotes

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?

## Content actions

PDF | EPUB (?)

### What is an EPUB file?

EPUB is an electronic book format that can be read on a variety of mobile devices.

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

#### Definition of a lens

##### Lenses

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

##### What is in a lens?

Lens makers point to 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 member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks