### Proof-Procedures for Propositional Logic

#### Inventing Proofs

Taken together, the nine rules of inference and ten rules of replacement are a complete set in the sense that using just these nineteen rules is sufficient to demonstrate the validity of every valid argument of the propositional calculus. (In fact, there is a good deal of redundancy built into the system: if we happened to forget about M.P. entirely, for example, we could always work around it by using Impl., D.N., D.S., and Impl. again.) What's more, showing the validity of an argument in this way is often more convenient than building the huge truth-table required to cover every possible combination of truth-values.

But constructing proofs isn't always easy, as you've discovered in your last couple of exercise sets. Even if you know the rules inside-out, upside-down, and backwards-and-forwards (as you must) and even if you are skilled at recognizing the intermediate arguments that are their substitution instances in the context of a proof (as you should be), inventing a proof on your own may seem a daunting task. But don't be discouraged. No matter how long and complex a proof becomes, each of its steps is always just the application of one of our nineteen rules; we just have to figure out which ones lead us from premises to conclusion. There's nothing magical about the process. No one simply "sees" the whole proof at the outset, although some people may move a little faster than others. With practice, anyone can learn to perform the necessary steps.

Let's look at one more instance together:

#### A Detailed Example

Consider the following argument:

```		A • (B • C)

(B • A) ⊃ [D ∨ (~E ≡ F)]

~D • ~(G ∨ E)
___________________________

~(G ∨ ~F)
```
The first step, as always is to number and label the premises of the argument as the starting-point for our proof:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]	  	premise
3. ~D • ~(G ∨ E)			premise
```
Now, begin working from the top down. Notice that the first premise is a conjunction whose right conjunct is itself another conjunction. We have several possibilities here, since this statement could be a substitution instance of statement forms that occur in several of our rules: Simp. and Comm. can be applied to any conjunction, and Assoc. will work on one of this form, too.

Which one should we use? Well, let's think ahead a bit. Premise 2 is a conditional statement, and we know that if its antecedent were on a line by itself, then that line together with premise 2 would be a substitution-instance of the premises required for an application of M.P. That is (leaving lots of room for the work we may have to do in between) we would like to be able to build the proof like this:

```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise

B • A				? ? ?
D ∨ (~E ≡ F)			2, ? M.P.
```
But in order to make this work, we have to derive B • A. Looking back at the first premise now, we notice that an application of Assoc. would change the grouping in such a way as to get A and B together, from which we could then simplify to have them on a line of their own:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.

B • A				? ? ?
D ∨ (~E ≡ F)			2, ? M.P.
```
But now it's pretty obvious that all we have to do is commute line 5 to get the missing premise for our M.P.:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
```
This new line is a disjunction, so it would serve as one of the premises of a disjunctive syllogism if we only had ~D. But we can get that easily enough by simplifying our third premise:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.
```
Suppose that at this point, we've run out of ideas about what to do working from the top down. So let's work from the bottom up instead—remember the conclusion we're trying to establish here:
```		~(G ∨ ~F)
```
Since this conclusion is the negation of a disjunction, we naturally think of De Morgan's Theorems, which state its equivalence to a conjunction of negations. And of course, we can form a conjunction by deriving both conjuncts on their own and then using Conj. So we're now guessing that the end of our argument will look something like this:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.

~G					? ? ?

~~F					? ? ?
~G • ~~F				?, ? Conj.
~(G ∨ ~F)				? DeM.
```
All we need to do now is to close the gap between the top part of the proof and the ending that would provide our desired conclusion. So, in effect, we're starting all over: we now have lines 1-9 available as premises, and we need to invent two little proofs, one with the conclusion ~G and the other with the conclusion ~~F.

For the first of these, we need to go back up to line 3, since that's the only place where G occurs. If we commute that line and then simplify, we'll have:

```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.
10. ~(G ∨ E) • ~D			3 Comm.
11. ~(G ∨ E)				10 Simp.

~G					? ? ?

~~F					? ? ?
~G • ~~F				?, ? Conj.
~(G ∨ ~F)				? DeM.
```
Now applying De Morgan's Theorems and simplifying will complete the first of our little arguments:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.
10. ~(G ∨ E) • ~D			3 Comm.
11. ~(G ∨ E)				10 Simp.
12. ~G • ~E				11 DeM.
13. ~G					12 Simp.

~~F					? ? ?
~G • ~~F				?, ? Conj.
~(G ∨ ~F)				? DeM.
```
Now our only goal is to derive ~~F, and that is likely to come from line 9, which is the simplest line in which F occurs. So let's use Equiv. to unpack line 9 and simplify the result:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.
10. ~(G ∨ E) • ~D			3 Comm.
11. ~(G ∨ E)				10 Simp.
12. ~G • ~E				11 DeM.
13. ~G					12 Simp.
14. (~E ⊃ F) • (F ⊃ ~E)			9 Equiv.
15. ~E ⊃ F				14 Simp.

~~F					? ? ?
~G • ~~F				?, ? Conj.
~(G ∨ ~F)				? DeM.
```
But now we're almost done: a little fiddling with line 12 will get us ~E, the other premise we need for an M.P. on line 15, and D.N. will fill the gap completely, so we need only supply the missing line numbers in order to complete the entire proof:
```		 1. A • (B • C)				premise
2. (B • A) ⊃ [D ∨ (~E ≡ F)]		premise
3. ~D • ~(G ∨ E)			premise
4. (A • B) • C				1 Assoc.
5. A • B				4 Simp.
6. B • A				5 Comm.
7. D ∨ (~E ≡ F)			2, 6 M.P.
8. ~D					3 Simp.
9. ~E ≡ F				7, 8 D.S.
10. ~(G ∨ E) • ~D			3 Comm.
11. ~(G ∨ E)				10 Simp.
12. ~G • ~E				11 DeM.
13. ~G					12 Simp.
14. (~E ⊃ F) • (F ⊃ ~E)			9 Equiv.
15. ~E ⊃ F				14 Simp.
16. ~E • ~G				12 Comm.
17. ~E					16 Simp.
18. F					15, 17 M.P.
19. ~~F					18 D.N.
20. ~G • ~~F				13, 19 Conj.
21. ~(G ∨ ~F)				20 DeM.
```
Although this turned out to be a very long proof, it wasn't really difficult, since each of the shorter segments in which we invented it involved only a few simple steps. We simply worked from the top down and from the bottom up until we closed the gap step by step in order to demonstrate the validity of the original argument. 