[SL13] Derivation rules 2

§1. Rules for "v"

As for '&' and '→', there is both an elimination rule and an introduction rule for '∨':

The introduction rule says that you can take any formula you have written down so far and make it longer, by changing it into a disjunction. And you write down the same dependencies. So if the original formula is φ, then the new formula would be (φ∨ψ) or (ψ∨φ). Note that ψ can be any formula at all, from simple, like "A" or "B" to more complicated, like "(A & B)" or "((A→B)&(B→A))". For example

The elimination rule for '∨' lets you break apart a disjunction and write down only one half. Like &I, ∨E starts from two formulas and permits you to write down a third. ∨E permits you to write down φ if you have (φ∨ψ) and ~ψ in your derivation. ∨E also permits you to write down ψ, if you have (φ∨ψ) and ~φ in your derivation. The dependencies of the new formula are the same as the dependencies of the two formulas you had already. A more traditional name for this sort of rule is Disjunctive Syllogism; we will just call it ∨ Elimination, or ∨E for short.

For example:

At this point you can show the interesting fact that anything is derivable from an explicit contradiction: for any φ and ψ, (φ&~φ) ⊢ ψ.

For example, (B & ~B) ⊢ A. Can you see how to show that?

1 1. (B&~B) 	A
1 2. B		1 &E
1 3. ~B		1 &E
1 4. (B∨A) 	2 ∨I
1 5. A		3, 4 ∨E

There is one more rule involving '∨', Proof by Cases, or PC:

It may look complicated, but it is actually almost as simple as &I or ∨E. You need three formulas in order to apply the rule. Sometimes it may be difficult to see how to get these three formulas. But if you do have them written in your derivation, then you can write down a certain disjunction. The new formula depends on everything the three formulas you started with depend on.

Yes, for example:

	1 	1.	(A∨A)	A
	2 	2.	(A→B)	A
	1,2	3.	(B∨B) 	1,2,2 PC

1 	1. ((P&P)∨(Q&Q))		A
2 	2. (P&P)			A
2 	3. P				2 &E
	4. ((P&P)→P)			2,3 →I
5 	5. (Q&Q) 			A
5 	6. Q				5 &E
	7. ((Q&Q)→Q) 			5,6 →I
1 	8. (P∨Q)			1,4,7 PC

1 	1. (P∨P)		A
2 	2. (P→Q)		A
3 	3. P			A
	4. (P→P) 		3, 3 →I
1, 2 	5. (P∨Q)		1, 2, 4 PC

§2. Rules for "~"

There are just two more rules left, the rules for the introduction and elimination of the negation symbol '~'.

Rules ~I and ~E are similar to →I in certain ways. Each of these three rules permits you to take away dependencies. In addition, with each of these three rules, you first assume something, and then you derive something, and then you apply the rule to write down a new formula.

Here is Rule ~I:

Rule ~I provides one way to derive a negation like "~A" or "~(A&B)". Suppose, for example, you want to derive "~(A&B)". In using ~I you would first assume "(A&B)" and then derive an explicit contradiction. (An explicit contradiction is a formula of the form (φ&~φ) such as "(A&~A)" or "((B∨C)&~(B∨C))".) Then you can write down "~(A&B)".

Here is an example using ~I to show (B→A) ⊢ ~(B & ~A).

In this derivation line 2 is the assumption made for the purposes of using ~I. Since we hope to show "~(B & ~A)" using ~I, we assume "(B & ~A)" and try to derive an explicit contradiction. After reaching the explicit contradiction on line 6, we can then write down on line 7 the negation of the assumption on line 2. The result on line 7 depends on everything line 6 depends on except the relevant assumption on line 2.

Notice that just a few changes turns that derivation into one that shows that (B & ~A) ⊢ ~(B→A).

	1	1. (~A∨~B)		A
	2	2. (A&B)		A
	2	3. A			2 &E
	4   	4. ~A  			A
	2, 4	5. (A&~A)	 	3, 4 &I
	2	6. ~~A			4, 5 ~I
	1, 2	7. ~B			1, 6 ∨E
	2	8. B			2 &E
	1, 2	9. (B&~B) 		7, 8 &I
	1	10. ~(A&B)		2, 9 ~I

The elimination rule for '~' is almost the same as the introduction rule. The only difference is that instead of assuming ψ and writing down ~ψ at the end, you assume ~ψ and write down ψ at the end.

Here is an example of ~E:

~~A ⊢ A

	1	1. ~~A			A
	2 	2. ~A			A
	1, 2 	3. (~A&~~A)		1, 2 &I
	1	4. A			2, 3 ~E
		

You have seen all the rules of our natural deduction system! Now try making some derivations on your own.

	1	1. ~~A			A
	2 	2. ~A 			A
	1, 2 	3. (~A&~~A)		1, 2 &I
	1	4. A			2, 3 ~E
		5. (~~A→A)		1, 4 →I

	1 	1. ~(P∨Q)		A
	2 	2. P			A
	2 	3. (P∨Q)		2 ∨I
	1, 2 	4. ((P∨Q)&~(P∨Q))	1, 3 &I
	1	5. ~P			2, 4 ~I
	6	6. Q			A
	6 	7. (P∨Q)		6 ∨I
	1, 6 	8. ((P∨Q)&~(P∨Q)) 	1, 7 &I
	1	9. ~Q			6, 8 ~I
	1	10. (~P&~Q)		5, 9 &I