More examples

您在這裡

Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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

Example 2.20

Let's redo the first example (Example 2.11)'s proof formally and show $H - has - 2 \wedge J - safe\vdash G - unsafe$
The inference rules we used informally above don't correspond exactly to those in our defnition, so the formal proof is more complicated.

1	H − has − 2 ⇒ P − unsafe ∧ G − unsafe ∨ J − unsafe ∧ P − unsafe ∨ G − unsafe ∧ J − unsafe		WaterWorld axiom, choosing a grouping of the ternary ∨, as justifed by ∨ commutativity (Example 2.14)
2	H − has − 2 ∧ J − safe		Premise
3	H − has − 2		∧Elim (left), line 2
4	P − unsafe ∧ G − unsafe ∨ J − unsafe ∧ P − unsafe ∨ G − unsafe ∧ J − unsafe		⇒Elim, lines 1,3
5	J − safe		∧Elim (right), line 2
6	J − safe ⇒ ¬J − unsafe		WaterWorld axiom
7	¬J − unsafe		⇒Elim, lines 5,6
8	$subproof:G- unsafe \wedge J - unsafe \vdash false$
8.a		G − unsafe ∧ J − unsafe	Premise for subproof
8.b		J − unsafe	∧Elim (right), line 8.a
8.c		false	falseIntro, lines 7,8.b
9	¬ (G − unsafe ∧ J − unsafe)		RAA, line 8
10	P − unsafe ∧ G − unsafe ∨ J − unsafe ∧ P − unsafe		CaseElim (right), lines 4,9
11	subproof:J − unsafe ∧ P − unsafe f false
11.a		J − unsafe ∧ P − unsafe	Premise for subproof
11.b		J − unsafe	∧Elim (left), line 11.a
11.c		false	falseIntro, lines 7,11.b
12	¬ (J − unsafe ∧ P − unsafe)		RAA, line 11
13	P − unsafe ∧ G − unsafe		CaseElim (right), lines 10,12
14	G − 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 2.21

The previous example (Example 2.20) is a perfect candidate for adding structure to the proof by using additional subproofs. The following is more similar to the original informal proof (Example 2.11).

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			WaterWorld axiom, choosing a grouping of the ternary ∨, as justied by ∨ commutativity (Example 2.14)
2	$subproof: \vdash H-has-2$
2.a		H − has − 2 ∧ J − safe		Premise
2.b		H − has − 2		∧Elim (left), line 2.a
3	P − unsafe ∧ G − unsafe ∨ J − unsafe ∧ P − unsafe ∨ G − unsafe ∧ J − unsafe			⇒Elim, lines 1,3
4	$subproof:\vdash\ \dashv J -unsafe$
4.a		H − has − 2 ∧ J − safe		Premise
4.b		J − safe		∧Elim (right), line 4.a
4.c		J − safe ⇒ ¬J − unsafe		WaterWorld axiom
4.d		¬J − unsafe		⇒Elim, lines 4.b,4.c
5	$subproof: \vdash P-unsafe\wedge G-unsafe$
5.a		$subproof:G - unsafe \wedge J - unsafe \vdash false$
5.a.i			G − unsafe ∧ J − unsafe	Premise for subproof
5.a.ii			J − unsafe	∧Elim (right), line 5.a.1
5.a.iii			false	falseIntro, lines 4,5.a.2
5.b		¬ (G − unsafe ∧ J − unsafe)		RAA, line 5.a
5.c		P − unsafe ∧ G − unsafe ∨ J − unsafe ∧ P − unsafe		CaseElim (right), lines 3,5.b
5.d		$subproof:J - unsafe \wedge P - unsafe \vdash false$
5.d.i			J − unsafe ∧ P − unsafe	Premise for subproof
5.d.ii			J − unsafe	∧Elim (left), line 5.a.1
5.d.iii			false	falseIntro, lines 4,5.d.2
5.e		¬ (J − unsafe ∧ P − unsafe)		RAA, line 5.d
5.f		P − unsafe ∧ G − unsafe		CaseElim (right), lines 5.c,5.e
6	G − 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 2.22

Figure 2.6 Example WaterWorld board

Consider the above figure (Figure 2.6). We'll show B − has − 1 ∧ G − has − 1 ∧ J − has − 1 f K − unsafe. We'll do this through the following series of lemmas:

Lemma A: $\dashv A - unsafe, G - has - 1 \vdash H - unsafe$
Lemma B: $\dashv A - unsafe, B - has - 1 \vdash C - unsafe$
Lemma C: $H - unsafe, C - unsafe,J- has - 1 \vdash false$
Lemma D: $A - unsafe, B - has - 1 \vdash C - safe$
Lemma E: $A - unsafe, G - has - 1 \vdash H - safe$
Lemma F: $C - safe, H - safe,J- has - 1 \vdash 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		Premise
2	B − has − 1		∧Elim (left), line 1
3	G − has − 1 ∧ J −has − 1		∧Elim (right), line 1
4	G − has − 1		∧Elim (left), line 3
5	J − has − 1		∧Elim (right), line 3
6	$subproof:\dashv A-unsafe\vdash false$
6.a		¬A − unsafe	Premise for subproof
6.b		H − unsafe	Lemma A, lines 6.a,4
6.c		C − unsafe	Lemma B, lines 6.a,2
6.d		false	Lemma C, lines 6.b,6.c,5
7	A − unsafe		RAA, line 6
8	C − safe		Lemma D, lines 7,2
9	H − safe		Lemma E, lines 7,3
10	K − 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: $\dashv A-unsafe,G-has-1\vdash H-unsafe$

1	¬A − unsafe		Premise
2	G − has − 1		Premise
3	$subproof:A - unsafe \wedge H - safe \vdash false$
3.a		A − unsafe ∧ H − safe	Premise for subproof
3.b		A − unsafe	∧Elim
3.c		false	falseIntro, lines 1,3b
4	¬ (A − unsafe ∧ H − safe)		RAA, line 3
5	G − has − 1 ⇒ A − safe ∧ H − unsafe ∨ A − unsafe ∧ H − safe		WaterWorld axiom
6	A − safe ∧ H − unsafe ∨ A − unsafe ∧ H − safe		⇒Elim, lines 5,2
7	A − unsafe ∧ H − safe ∨ A − safe ∧ H − unsafe		Theorem: ∨ commutes, line 6
8	A − safe ∧ H − unsafe		CaseElim, lines 4,7
9	H − unsafe		∧Elim (right), line 8

Lemma B: $\dashv A-unsafe,B-has-1\vdash C-unsafe$

1	¬A − unsafe		Premise
2	B − has − 1		Premise
3	$subproof:A-unsafe\wedge C-safe\vdash false$
3.a		A − unsafe ∧ C − safe	Premise for subproof
3.b		A − unsafe	∧Elim (left), line 3a
3.c		false	falseIntro, lines 1,3b
4	¬ (A − unsafe ∧ C − safe)		RAA, line 3
5	B − has − 1 ⇒ A − safe ∧ C − unsafe ∨ A − unsafe ∧ C − safe		WaterWorld axiom
6	A − safe ∧ C − unsafe ∨ A − unsafe ∧ C − safe		⇒Elim, lines 5,2
7	A − unsafe ∧ C − safe ∨ A − safe ∧ C − unsafe		Theorem: ∨ commutes, line 6
8	A − safe ∧ C − unsafe		CaseElim, lines 4,7
9	C − 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".

瀏覽次數：2329