Negation Propositional natural deduction

The negation of a proposition is what is asserted when that proposition is denied. In English there is a range of negative constructions, the simplest being the word 'not' which is usually inserted just before the main verb. The negation of 'Logic is exciting' is 'Logic is not exciting'. As you see, negation turns truths into falsehoods. It also turns falsehoods into truths, of course. Care must be taken over negation in natural language, however. While one equivalent of 'not exciting' is 'unexciting', we cannot use the prefix 'un-' indiscriminately to form negations. 'Bob is unhappy' is not really the negation of 'Bob is happy', for Bob may be neither happy nor unhappy but neutral in respect of happiness. Sometimes the most idiomatic negation involves changes to other words as well as the insertion of 'not'. The negation of 'Logic makes sense to someone', for instance, is not 'Logic does not make sense to someone' but 'Logic does not make sense to anyone'. Moreover, there are many subtleties concerning negation which we do not want to reflect in our basic logical account. For instance, the negative particle is sometimes placed not before the verb but before some other particle, as in this sentence.

In sentential logic we start with the simplest kind of negation which applies to a whole sentence to turn the statement that so-and-so is the case into the statement that so-and-so is not the case. Formally we use the symbol 'NOT' for this purpose. We read  NOTp  as 'It is not the case that p' or more briefly 'Not p' and think of it as having the opposite force from that of p. It is easy to set out a table showing the conditions under which negation results in a true statement or in a false one:

That is, negation simply reverses truth value. Some of the salient features of negation can be read off this table. For one thing, re-negating the negation of p reverses its truth value again, leaving us back where we were:

Hence 'It is not not the case that p' is logically equivalent to p. This is so obvious that in ordinary discourse we do not usually assert the negation of a negation, except to make a special point:

This equivalence is called the Law of Double Negation. It gives rise to a pair of formal rules as specified in DN. The annotation for these is the one source line number and the rule name NOTNOTI or NOTNOTE. In neither direction is there any effect on the stock of assumptions, so the 'X ⊢ ... ' has been omitted for clarity as usual. It is also worth noting that like all the rules these two only allow introduction and elimination of main connectives (or pairs of connectives in this case). The string 'NOTNOT' in minor positions cannot be added or deleted by the double negation rules alone. For example, in order to derive NOTNOTp AND q in our natural deduction calculus from p AND NOTNOTq we must go through the logic of conjunction:

The double negation rules alone are not sufficient to capture the logic of negation. To complete the theory we need to add rules that somehow introduce and eliminate single negation operators. For this purpose, it is convenient to enrich the formal language with a special proposition, BAD, intended to be absurd, or logically contradictory all by itself. We might read it as 'We're in trouble!' or simply 'False'. BAD is a formula—an atomic formula, like p or q—which can never be true no matter how the world may be. It can also be seen as a zero-adic connective, since it yields a sentence without requiring any shorter sentences to be plugged into it.

Now the rules for introducing and eliminating BAD are at the same time the rules for eliminating and introducing negation (NOTrules). Firstly, if in the course of a derivation we arrive at a pair of mutually contradictory statements A and NOTA, then we are in trouble, so in one step we may add BAD. This seems clear enough: A and NOTA together constitute a logical contradiction, so they have as an immediate consequence the special formula which says that things are inconsistent. Secondly, if some assumptions lead validly to BAD then at least one of those assumptions must be false. Therefore, if all the assumptions apart from A are true, it must be A that is false, so NOTA can be inferred. That is, NOTA is an immediate consequence of a [sub]derivation of BAD from A.

A couple of proofs will serve to illustrate the logic of negation. These are written out in the sequential format not because that is in any important way preferable to the tree format, but because it makes text-processing easier.

Here we start by assuming the two premises of the sequent to be proved. Then we look at the desired consequence, NOTp. This is negative, so the natural way to prove it is to assume p and try to derive a contradiction. In fact, one simple inference step gets us q, and we already have NOTq, so the derivation is not hard! At the last step, the assumption of p is discharged.

The argument form just proved valid

If p then q
But it is not the case that q
Therefore it is not the case that p

occurs quite often. Consider for example

The generic form is common to many scientific experiments, and perhaps with suitable elaborations to all of them. Again,

This is very similar, except that when the offending assumption NOTp is denied at line (5) the result is NOTNOTp rather than p, so an extra step is needed to eliminate the double negation. SP {pIMPq ⊢ NOT(pAND NOTq)} PL {1} {1} {p IMP q} {A} PL {2} {2} {p AND NOTq} {A} PL {2} {3} {p} {2 ANDE} PL {1,2} {4} {q} {1,3 IMPE} PL {2} {5} {NOTq} {2 ANDE} PL {1,2} {6} {BAD} {4, 5 NOTE} PL {1} {7} {NOT(p AND NOTq)} {6 [2] NOTI} EP

There is little to observe here. The sequent says that if p implies q then we can't have p without q, which is fairly obvious. Conversely:

Taken together, the above two proofs show that the conditional p IMP q is logically equivalent to the negated conjunction NOT(p AND NOTq).

For the animated walkthrough of these two proofs, click here.

As usual, to do it yourself click here. and here.

Now here's a proof that a contradiction entails absolutely everything:

We shall return to this rather surprising sequent later in the course. For now, note that the proof is fine according to the way orthodox logic is set up. Lines (1) and (2) contradict each other, and we are allowed by the rules to blame the contradiction on an innocent bystander, NOTq. The empty brackets in the annotation of line 4 indicate that no actual assumption was discharged.

You may have noticed that in all of the above proofs the absurd constant BAD is introduced only to be eliminated again at the next step. You may also wonder whether in that case it is worthwhile having BAD in the language at all: if we were to add another rule that simply short-circuits the detour through BAD, could we still prove everything we want in the BAD-free vocabulary?

The answer is yes. The rule RAA (reductio ad absurdum) allows us to pass in one step of immediate consequence from a contradictory pair A and NOTA to the conclusion NOTB, discharging zero or more assumptions of B as we go. That is, it gives precisely the effect of NOTE followed by NOTI without mention of BAD. raa shows the rule as a transformation on sequents. Note that the assumption B need not be actually present in the left-hand sides of both input sequents. Indeed, we allow the case where it is not present at all. As in the other rules which discharge assumptions, we can think of it as being implicitly added by the monotonicity of the consequence relation if we like.

RAA rests intuitively on a very plausible principle. If two sets of assumptions lead logically to opposite conclusions (one to A and the other to NOTA) then they cannot both be correct. Hence, if all of the assumptions other than B are true, it must be B that is false. That is to say, NOTB follows from the rest of the assumptions all taken together.

RAA is the formal rule corresponding to this thought. RAA yields a powerful proof strategy. To derive a negative conclusion NOTA it suffices to assume A and aim to derive a contradiction. Any contradiction will do. Also, in cases where there is no obvious route to a desired conclusion A we can assume its negation NOTA and try for a contradiction. Applying RAA will then give us NOTNOTA which by NOTNOTE turns into A. The RAA strategy is known as indirect proof or proof by contradiction.