3.5 Propositional logic: subproofs  (Page 3/3)

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

unsafe

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 $\mathrm{B-has-1}\land \mathrm{G-has-1}\land \mathrm{J-has-1}⊢\mathrm{K-unsafe}$ . We'll do this through the following series of lemmas:

• Lemma A: $\neg \mathrm{A-unsafe}\text{,}\mathrm{G-has-1}⊢\mathrm{H-unsafe}$
• Lemma B: $\neg \mathrm{A-unsafe}\text{,}\mathrm{B-has-1}⊢\mathrm{C-unsafe}$
• Lemma C: $\mathrm{H-unsafe}\text{,}\mathrm{C-unsafe}\text{,}\mathrm{J-has-1}⊢\mbox{false}$
• Lemma D: $\mathrm{A-unsafe}\text{,}\mathrm{B-has-1}⊢\mathrm{C-safe}$
• Lemma E: $\mathrm{A-unsafe}\text{,}\mathrm{G-has-1}⊢\mathrm{H-safe}$
• Lemma F: $\mathrm{C-safe}\text{,}\mathrm{H-safe}\text{,}\mathrm{J-has-1}⊢\mathrm{K-unsafe}$

First, we'll show the main proof, assuming each of the lemmas. Then, proofs of each of the lemmas will follow.

And that's the desired proof! Now it just remains to show each of the six lemmas.

Lemma A: $\neg \mathrm{A-unsafe}\text{,}\mathrm{G-has-1}⊢\mathrm{H-unsafe}$

Lemma B: $\neg \mathrm{A-unsafe}\text{,}\mathrm{B-has-1}⊢\mathrm{C-unsafe}$

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 twoto 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 inclass 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