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?
On
One might argue that $\lnot$I corresponds to the formula (($\phi$$\rightarrow$0)$\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$$\rightarrow$0)$\rightarrow$$\phi$). This doesn't correspond to any definition quite so easily.
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.