Skip to content Skip to navigation

Connexions

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

Navigation

Recently Viewed

This feature requires Javascript to be enabled.

Propositional Logic: subproofs

Module by: Ian Barland, John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen. E-mail the authors

User rating (How does the rating system work?)
Ratings

Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

How to rate a module

Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

:
(0 ratings)

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

Note: Your browser may not currently support MathML. See our browser support page for additional details. You can always view the correct math in the PDF version.

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 ⊢ ¬α∧¬α⊢ α α .

Table 1
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 φ=α∧¬α φ α α

Exercise 1

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

Solution

Table 2
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

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.

Table 3
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:

  • Assume the premise ¬α∧βα β.
  • Again, use commutativity to show that β∧α⇒α∧β β α α β
  • Use modus tollens to obtain the conclusion.
We can organize the proof into corresponding subparts:

Table 4
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.

Example 4

Let's redo the first example's proof formally and show H-has-2∧J-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.

Table 5
1H-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
2H-has-2∧J-safeH-has-2 J-safe  Premise
3H-has-2H-has-2  ∧Elim (left), line 2
4P-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
6J-safe⇒¬J-unsafe J-safe J-unsafe   WaterWorld axiom
7¬J-unsafeJ-unsafe  ⇒Elim, lines 5,6
8subproof: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
10P-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 ⊢ 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
13P-unsafe∧G-unsafeP-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.

Table 6
1H-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
2subproof:⊢ 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
3P-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-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
5subproof:⊢ 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
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

Figure 1: Example WaterWorld board
a 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-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.

Table 7
1B-has-1∧G-has-1∧J-has-1B-has-1 G-has-1 J-has-1  Premise
2B-has-1B-has-1  ∧Elim (left), line 1
3G-has-1∧J-has-1G-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 ⊢ 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
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-unsafeA-unsafe, G-has-1 ⊢ H-unsafe

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

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

Table 9
1¬A-unsafeA-unsafe  Premise
2B-has-1B-has-1  Premise
3subproof: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-safeA-unsafe C-safe  RAA, line 3
5B-has-1⇒A-safe∧C-unsafe∨A-unsafe∧C-safe B-has-1 A-safe C-unsafe A-unsafe C-safe   WaterWorld axiom
6A-safe∧C-unsafe∨A-unsafe∧C-safe A-safe C-unsafe A-unsafe C-safe   ⇒Elim, lines 5,2
7A-unsafe∧C-safe∨A-safe∧C-unsafe A-unsafe C-safe A-safe C-unsafe   Theorem: ∨ commutes, line 6
8A-safe∧C-unsafeA-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”.

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

Give Feedback:

E-mail the module authors | Rate module ( How does the rating system work?)

Rating system

Ratings

Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

How to rate a module

Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

(0 ratings)

Download:

Module PDF

Add module to:

My Favorites (?)

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

| A lens (?)

Definition of 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.

What are tags? tag icon

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