Can the negation introduction rule of inference be used instead of the usual rule? 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?
 A: Concerning the premises of your second rule of inference: 


*

*$a\qquad\qquad\qquad$ Premise 

*$b \to \lnot a\qquad$ Premise 

*$\lnot\lnot a\qquad\qquad$ (double negation)

*$\therefore \lnot b\qquad\qquad$ by Modus Tollens using 2. and 3.
As you can see, this is merely an application of Modus Tollens. Given an implication, say "A", the negation of the consequent of "A" implies the negation of the antecedent of "A".
Note: we can also take 1. and 2. to be assumptions, and 4. the conclusion derived from those assumptions, from which we can establish the implication (rule of inference):
$$[a \land (b \to \lnot a)] \implies \lnot b.$$
Perhaps your preference for this rule of inference is due to your familiarity with Modus Tollens?
But note that in this rule of inference, for your "premises", you have the conjunction of an implication ($b \to \lnot a$) with the assertion that $a$, where $a$ is not tied up in an implication.  It "stands alone."  
On the other hand, the second rule of inference involves the conjunction of two implications for premises; you do not have assertion a to use as a premise, nor b, in a "stand alone" form.  Formally, we can establish this rule of inference as follows:
$[(b \rightarrow a) \land (b \rightarrow \lnot a)] \implies \lnot b$         


*

*$ \qquad | \underline{[(b \rightarrow a) \land (b \rightarrow \lnot a)]}\qquad $  Assumption/Premise

*$\qquad | b \rightarrow a\qquad $ 1. Conjunction Elimination

*$\qquad | b \rightarrow \land \lnot a \qquad $ 1. Conjunction Elimination

*$\qquad \qquad |\underline{b\qquad} $ Assumption

*$\qquad \qquad |\ a \qquad$  2, 4, Modus Ponens

*$\qquad \qquad | \lnot a\qquad$  3, 4, Modus Ponens

*$\qquad\qquad |\underline{ a \land \lnot a} \qquad$ 5, 6, Conjunction Introduction

*$\qquad \|\underline{\therefore \lnot b \qquad}$  4 - 7, Negation Introduction (contradiction) 

*$ [(b \rightarrow a) \land (b \rightarrow \lnot a)] \implies \lnot b \qquad$, 1 - 8 Conditional Introduction


"Negation Introduction": (8) Based on the fact that our assumption "$b$" led to a contradiction (specifically, $(a \land \lnot a))$, it follows that our assumption "$b$" must thereby be false. So $\lnot b$ must be true, and we are justifying in asserting ("introducing") the negation of "$b$": $\lnot b$.
You have likely gone through such proofs before; I thought by working with each of the rules of inference, perhaps you'd notice differences, as well as similarities.
The two argument forms (rules of inference) you present each have their uses, and it is good to understand the logic behind each of them. I can understand that you see similarities, but there are keen (though subtle) differences in the ways in which each can be used, or when the use of one over the other is most fitting.  This often depends on the information (premises) you have available to use in a proof, and how "cumbersome" the use of one way be when compared to the other. By being familiar with all the "tools" available (i.e., understanding equivalences, all the rules of inferences), you're in a much better position to recognize when one is most applicable.
ADD IN
I claimed, in my comment to the answer provided by the OP, that one can adapt the user's preferred rule of inference to the "usual" rule (usual as judged by user). I demonstrate this below.


*

*$|\;a\qquad$ Premise

*$|\;\underline{b \Rightarrow \lnot a}\qquad$ Premise

*$\quad | \underline{b\qquad\qquad}$ Assumption

*$\quad |  a\qquad\qquad$ 1. Replication

*$\quad | \lnot a \qquad$ 2, 3 Modus Ponens

*$\quad |\underline{a \land \lnot a}\qquad $4,5 Conjunction Introduction

*$|\; \lnot b \qquad\qquad$ 3-6 Negation Introduction (contradiction inference)

A: In presenting a formal logic for foundations of mathematics, the tendency is to use a minimum number of inference rules (typically just modus ponens).  So having a proliferation of rules of inference as often is presented in logic as a philosophy topic is not "logically" necessary.  A mathematical version of propositional logic often replaces the multiplicity of rules of inference with axiom schemes, from which all the valid inferences can be made using only modus ponens.
Both of the inference rules you bring up can be considered forms of "proof by contradiction" or reductio ad absurdum.  This seems particularly clear in the form you dislike, which infers from b implying both a and ¬a, that ¬b must hold.  In other words, assuming b leads to a contradiction (a and ¬a), so b must not be true.
The form of inference you favor goes from premises a and (b implies ¬a) to the conclusion ¬b.  As you point out, it makes sense "that if b implies something which is not true, then b is itself not true."  However the same rationale could be applied to your other form of inference, where b implies both a and ¬a, and clearly "a and ¬a" is "something which is not true".
But the insight that you have is always more powerful (more convincing) than one your teacher merely tells you about, so it's understandable you would find one rule more compelling than the other.
A: OK, I think I have a pretty rigorous argument which validates said replacement.
Let's say that we need to introduce a negation on P. So using the usual inference rule, we prove:


*

*P => Q

*P => ¬Q

*and thereby prove ¬P.


Let's say that there is no way to derive both Q and ¬Q if P is not assumed. But then from P we can derive Q $\land$ ¬Q which will allow us to derive anything, including the negation of a tautology.
So we can prove ¬P using the proposed rule by doing something like this:

1.  |P                 Assumed
... |...
10. |Q
... |...
20. |¬Q
21. |Q /\ ¬Q           /\ introduction on line 10 and 20
22. |¬(A => A)         Derived from line 21 using contradiction lemma
23. P => ¬(A => A)     => introduction on lines 1-22
24. A => A             Anything implies itself (a tautology)
25. ¬P                 ¬ introduction on line 23 and 24

So using tautologies we can always use the proposed rule of inference.
In other words, if you can use the usual rule of inference to introduce a negation, you can use the proposed rule of inference too.
