[Math] About NOT elimination/introduction and RAA rules on Natural Deduction

intuitionlogicpropositional-calculus

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.

Best Answer

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.

Related Question