Why is removing the negation worse than adding it?

Natural Deduction Rule (¬I): Natural Deduction Rule (RAA): My book [Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007)]presents these two rules and then adds:

The use of (RAA) can lead to some very unintuitive proofs. Generally, it is the rule of last resort, if you cannot find anything else that works.

The first rule adds a negation sign, the other rule removes it. For some reason removing is worse then adding. Can you explain why?

• It may depend on your opinion on whether $\neg\neg\phi$ is equivalent to $\phi$. And I find the judgement strange - either the rule is valid even when not used as last resort, or it is invalid especially when no other rules work. Jun 22 '14 at 21:41
• @HagenvonEitzen I agree. I guess it's to pacify intuitionstists, like some people try to avoid the axiom of choice when possible, to pacify those who don't like it. Jun 22 '14 at 21:44
• What do you mean "pacify intuitionists"? Avoiding RAA if possible is not done to pacify the intuitionists. It is done to appease the constructivists! Avoiding RAA is not an ideological position or a matter of taste and style: it is a practical choice with significant consequences when one studies the foundations of mathematics (as distinct from mathematical logic, or more precisely, the mathematical analysis of logic, which necessarily presupposes some foundation). Jun 22 '14 at 23:21

Well, Chiswell and Hodges in the exercises immediately following the quoted remarks in their book explicitly give some examples of sequents whose proofs in their system depend essentially on RAA, including

$$\vdash \neg(\phi \to \psi) \to \phi$$

$$\vdash \phi \to (\neg\phi \to \psi)$$

So: If a conditional is false, its antecedent has to be true(?). A contradictory pair of wffs implies anything(??). I guess these are the kinds of prima-facie counter-intuitive results they had in mind, then.

And I guess you can find these results unintuitive at first blush without being a paid-up intuitionist! [Recall, C&H are aiming to model ordinary mathematically reasoning with the connectives, at this stage: the truth-tables come much later.] Though yes, I doubt whether these are in fact much more unintuitive that some intuitionistically acceptable sequents you can prove without RAA.

• What is C&H? Not everyone is a practicing logician familiar with the textbooks in the area (which I presume C&H is...) Jun 22 '14 at 23:05
• Sorry, the OP has just been posting a series of questions about the textbook by Chiswell and Hodges. And yes, I see he doesn't mention the book again by name in this question, so I've edited my answer. Jun 22 '14 at 23:07

One might argue that $\lnot$I corresponds to the formula (($\phi$$\rightarrow0)\rightarrow$$\lnot$$\phi). This can get thought of as one-half of the definition of \lnot. On the other hand, RAA similarly corresponds to the formula ((\lnot$$\phi$$\rightarrow0)\rightarrow$$\phi$). This doesn't correspond to any definition quite so easily.

• Indeed, C&H write "in derivations, we treat $\neg\phi$ exactly as if it was written $\phi \to \bot$". Jun 22 '14 at 22:55