About NOT elimination/introduction and RAA rules on Natural Deduction

Question

Can somebody explain the $\neg$-elimination rule in natural deduction?. Searching on books and the web, I found different definitions for it. For example, in my logic I course, the rule is:

$A, \lnot A$ then $\bot$.

This looks just like a $\land$-introduction that generates $\bot$. Anyway, what is the most common or intuitive definition for it?

More on this, this is the $\lnot$-introduction:

Suppose $A$. Derive $\bot$. Then (discharging the assumption $A$) $\lnot A$.

And this is the RAA (reduction to absurd) rule:

Suppose $\lnot A$. Derive $\bot$. Then (discharging the assumption) $A$.

This is supposed to not to be classified as introduction or elimination rule. But seriously, what is the difference between them? It looks more like a syntactic difference than a semantic difference. I can use both for the same purposes and the result is the same.

Answer 1

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.

Answer 2

In constructive and intuitionistic logic, it is common to take $\bot$ as a primitive proposition, and to abbreviate the formula $A \to \bot$ as $\lnot A$. That is, the negation of $A$ is a taken as an abbreviation for “$A$ implies absurdity.” In this formulation, notice that $\bot$-introduction is simply shorthand for $\to$-elimination (modus ponens), since

$A$, $\lnot A$ / $\bot$

is the same as

$A$, $A \to \bot$ / $\bot$

This also means that $\lnot$-introduction is the same as $\to$-introduction. If, after assuming $B$, you can derive $\bot$, then you can terminate the discharge the assumption $B$ and conclude $B\to\bot$, but by the definition, this is exactly $\lnot B$.

Although it's not common practice, as far as I'm aware, to define $\lnot A$ as $A \to \bot$ in classical logic, it can, in my opinion, make some of the naming conventions a bit clearer.

To get classical logic from intuitionistic logic, we add the axiom schema $\lnot\lnot A \to A$, and then reductio ad absurdum (RAA) is simply a derived inference rule:

Suppose $\lnot A$. Derive $\bot$. Then conclude, by $\to$-introduction, $\lnot A \to \bot$. This is, by definition $\lnot\lnot A$. By the axiom schema, $\lnot\lnot A \to A$. Then, by $\to$-elimination, conclude $A$.

Unfortunately, as you've noticed, there is lots of variation among authors as to what different rules are called, and you'll always have to be aware of what different authors mean when they use a particular terminology. For instance, this recent question links to a handout in which a professor defines some natural deduction inference rules. In it disjunctive syllogism is called $\lor$-elimination, both modus ponens and modus tollens are called $\to$-elimination, reductio is called $\lnot$-introduction, and there are three different things called $\lnot$-elimination!

Answer 3

1) You won't go far wrong if you read $\bot$ as "Absurd!" Then the rule "given $A$, $\neg A$ infer $\bot$" encapsulates the evident and natural thought that if you've got both $A$ and $\neg A$ in play, then you're in trouble, you've hit absurdity.

2) The standard not-introduction rule, as you say, is "Given a proof from $A$ to absurdity, you can infer $\neg A$." Now, as an application of that, you can get "Given a proof from $\neg A$ to absurdity, you can infer $\neg\neg A$." But note -- importantly -- that you can't get from that to the RAA rule "Given a proof from $\neg A$ to absurdity, you can infer $A$" unless you have DN, the Double Negation rule "From $\neg\neg A$ infer $A$.

So the situation is this. For classical logic you either need not-introduction and RAA in the forms you give them (and then DN is a derived rule), or not-introduction and DN (and then your RAA is a derived rule).