I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
When should I use RAA in natural deduction proofs
formal-proofslogicnatural-deductionproof-theory
Related Solutions
One intuitive explanation for $\bot$ is "I am insane". Thus, the rule:
Given $A$ and $\neg A$, one may infer $\bot$
expresses that:
Accepting something as true and false at the same time is insane.
And when we're insane, nothing is out of the question, so we obtain $\bot$-elimination:
Given $\bot$, one may infer $A$, for any $A$.
The distinction between RAA and $\neg$-I is a bit more subtle. For the purpose of classical logic, we may treat them as the same. We may do this due to the acceptance of the following:
"Something is either true or false": $A \lor \neg A$. Equivalently, $\neg \neg A \leftrightarrow A$ ("if something is not false, then it must be true").
In this sense, the distinction between RAA and $\neg$-I is indeed syntactical, and semantically, there is no difference.
However, in different semantics, such as Intuitionistic Logic, the rule mentioned above does no longer hold. This is because in intuitionism, one only accepts $A \lor B$ as true when one knows which of $A$ and $B$ holds (more accurately, that we either have proven $A$, or have proven $B$). We take the expression $A \to \bot$ a definition of $\neg A$ ("$A$ is demonstrably false").
Now, there is a difference between the two:
- "Given $A \to \bot$, then $\neg A$" ($\neg$-I) is tautologous;
- "Given $\neg A \to \bot$, then $A$" does not hold. Suppose that $A = B \lor C$. Then $\neg A \to \bot$ expresses "$B$ and $C$ cannot both be false". However, a proof of $A$ now requires proving one of $B$ or $C$, but $\neg A \to \bot$ provides us no clue as to which of $B$ and $C$ could be provable.
If you enjoy logic, I encourage you to study intuitionistic logic and its bewildering implications once you've got a firm understanding of classical logic.
Probably your last comment about double negation elimination breaking the symmetry of natural deduction is the 'reason' for the cited quote, though I don't agree with the sentiment.
Basically, natural deduction has introduction and elimination rules for each one of "$\land$" and "$\lor$" and "$\to$", which correspond to their intended meanings. We also have negation introduction in the form "$A \to \bot \vdash \neg A$" and negation elimination in the form "$A , \neg A \vdash \bot$". So double negation elimination (DNE) is an 'odd one out', so to speak, being "$\neg \neg A \vdash A$" or equivalently "$( A \to \bot ) \to \bot \vdash A$". I'm excluding the principle of explosion here because it is redundant in the presence of DNE.
Also, note that you can prove each instance of LEM using DNE plus the other rules, so adding DNE suffices to recover classical logic. If you added LEM instead of DNE, you would also have to add the principle of explosion, namely "$\bot \vdash A$" for any proposition $A$. In that sense DNE can be said to be slightly stronger than LEM. Intuitively it is obviously the case, because we would need at least one rule that reduces the total number of occurrences of "$\neg$" or "$\bot$", and LEM does not do so. Both the principle of explosion and DNE reduce that number, by $1$ and $2$ respectively. But adding just the principle of explosion is not enough to get classical logic, because it only results in intuitionistic logic.
For your other points, your statement that natural deduction is less suitable than sequent calculus for automated proof systems is arguably false. Even though the LK calculus works without the cut rule, it is not useful to take that rule away because it shortens proofs drastically in the same way that allowing on-the-fly definitions makes modern mathematics possible (we can't get far if we're not allowed to define arbitrary new terminology).
And as for the cut rule being implicit in ND via implication introduction and elimination, well is that really implicit? We could modify the other rules appropriately so that none of them use the implication symbol, and then indeed those two rules would become redundant in the same manner as the cut rule. So it looks quite explicit to me. As with LK, it is not useful in practice to take away these rules.
Best Answer
I can think of $4$ explicit situations:
Your goal is the negation of something. If you goal is $\neg \varphi$, assume $\varphi$ and see if you can get a contradiction
Your goal is some atomic statement $P$: Assume $\neg P$, get a contradiction, get $\neg \neg P$ using RAA, and finally derive $P$ from $\neg \neg P$ (classical logics typically have a $\neg \ Elim$ rule for this)
Your goal is a disjunction $\varphi \lor \psi$ ... and you don't have any disjunction that you can work with (if you do have a disjunction, set up a $\lor \ Elim$ on that one.). The nice thing about doing an RAA here is that once you assume $\neg ( \varphi \lor \psi)$, you should be able to derive both $\neg \varphi$ and $\neg \psi$ (using two RAA proofs themselves!), and now you have some useful stuff to work with on your way to a contradiction.
Your goal is an existential $\exists x \ \varphi(x)$ ... and you don't have some other existential to work with (if you do have another existential, set up a $\lor \ Elim$ on that one.). So here the assumption will be $\neg \exists x \ \varphi(x)$ which, with a bit of work (and probably another RAA inside) should allow you to prove $\forall x \ \neg \varphi(x)$ ... and that will be useful to try and get to a contradiction given whatever else you have.