3.5 Propositional logic: subproofs  (Page 2/3)

Another use of subproofs is to organize proofs' presentations. Many proofs naturally break down into larger subparts, each withits own intermediate conclusion. These steps between these subparts are big enough to correspond to our intuition, but too bigto correspond to individual inference rules. This gives additional useful structure to a proof, aidingour understanding.

Previously, we showed that ∧ (AND) commutes . However, that conclusion is only directly applicablewhen the ∧ is at the

top-level

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 toreach the conclusion? By the shape of the formula, the last step can't use any of the

introduction

elimination

The proof above uses a subproof because it is necessary for the use of RAA. In contrast, the proof below uses two subproofssimply for organization.

For our second proof, let's not use RAA directly. Our plan is as follows:

• Assume the premise $\neg (\alpha \land \beta )$ .
• Again, use commutativity to show that $(\beta \land \alpha )\implies (\alpha \land \beta )$
• Use modus tollens to obtain the conclusion.

More examples

Now let's use these rules in a couple larger proofs, to show some more interesting results.