Negation Introduction

When I was in university, one of my favorite units was Mathematics of Discrete Structures lectured by Dr Gordon Pace. In propositional logic, we learned about the negation introduction rule of inference which was this:

P => Q, P => ~Q
---------------
     ~P

and which was used like this:

1.  | P   Assumed
... | ...
10. | Q

11. | P   Assumed
... | ...
20. | ~Q
21. ~P   Negation introduction from lines 1-10 and 11-20

In other words, if P implies that Q is true and also P implies that Q is not true, then P must itself not be true.

I never actually understood the logic behind it however. We were told that this how a proof by contradiction works. An example of a proof by contradiction, in words, is this:

If it were raining, the streets would be wet. But the streets are not wet. Therefore it is not raining.

The fact that if a particular proposition is true, it would lead to another proposition which we know is false, implies that the first proposition must itself be false.

The problem with the rule of inference we used for negation introduction is that the way I interpret it linguistically is not at all how a proof by contradiction is usually told. If we had to turn the rule of inference into words, it would be this:

If P implies that something is both true and false, then P is itself false.

A rule of inference which is closer to a proof by contradiction would be this:

Q, P => ~Q
----------
    ~P

which would be used like this:

...
10. Q
11. | P    Assumed
... | ...
20. | ~Q
21. ~P     Negation introduction from lines 10 and 11-20

This is closer to a proof by contradiction.

If P implies something which is not true, then P itself is not true.

The question is, can we use this new rule of inference instead of the usual one?

When can the usual rule of inference be more powerful than the proposed one? Only when both Q and ~Q can ONLY be derived using P. Hence P must be assumed in both cases which cannot be done with the proposed rule of inference.

But this can easily be solved by using the lemma Q /\ ~Q => X and tautologies. If P can derive both Q and ~Q, then we can also derive Q /\ ~Q from which further derive anything we want, including something false. Worst case, if we don't know what to derive which is false, we can derive the negation of a tautology, such as ~(A => A). A => A is a tautology and we can always just insert it in a proof.

So using this trick, we'd do the following:

1.  | P          Assumed
... | ...
10. | Q
... | ...
20. | ~Q
21. | Q /\ ~Q    Conjunction introduction from lines 10 and 20
22. | ~(A => A)  Q /\ ~Q => X lemma from line 21
23. A => A       A => A lemma
24. ~P           Negation introduction from lines 1-22 and 23

And therefore, where ever we can use the usual rule of inference, we can also use the proposed rule of inference.

QED :)