2
$\begingroup$

Can the negation introduction rule of inference, $$\begin{array}{c} a\\ b\longrightarrow \neg a\\ \hline \neg b \end{array}\qquad\qquad\qquad (1)$$ be used instead of the usual $$\begin{array}{c} b\longrightarrow a\\ b\longrightarrow \neg a\\ \hline \neg b\end{array}\qquad\qquad\qquad (2)$$

I find the negation introduction rule which I learned at university a bit confusing to reason out, and think that the rule (1) makes more sense as it means that if $b$ implies something which is not true, then $b$ is itself not true. I can't seem to find an example of where the usual rule is more useful than the one I would like to use. Is there a reason why rule (2) is used as a rule of inference?

  • 0
    Since from b you can derive a /\ ¬a then you can use the contradiction to derive the negation of a tautology and hence still be able to use the proposed rule. I'll post a detailed answer later since I cannot answer my own post before 8 hours.2011-06-01
  • 0
    Assuming you have defined $\lnot b$ as $b \rightarrow \bot$, then the first one is a straightforward deduction using modus ponens (twice). However, it seems to me that isn't how you have defined negation...2011-06-01

3 Answers 3