Natural Deduction rules for $\lnot$ in classical and intuitionstic logic Following the very useful answer by Peter Smith to my prevoius post , I'm still reflecting about the "imperfection" connected with the Intro- ans Elim-rules for $\lnot$ in Natural Deduction (I mean with imperfection, the difficulty to formulate the rules according to the inversion principle).
If we stay with $\lnot$ as primitive, the role of $\bot$ can be played by $A \land \lnot A$.
With this, we can replace the $\bot_I$ rule of Prawitz with the following :

($\lnot$E) $$\frac {A \quad \lnot A } B$$

I think that for classical logic we must add :

($\lnot$I) $$\frac { } { A \lor \lnot A}$$

If I understand correctly the inversion principle, this couple of rules "does not invert"; moreover, in both cases they contain another connective, differently from all other couples of rules.
My question is this : if I avoid the $\bot$ symbol and stay with $\lnot$ as primitive, what are the "most fitting" rules regarding $\lnot$ for Classical and for Intuitionistic logic ?
 A: To be honnest I think that $ \bot$ better fits in Intuitionistic logic.
So I will  put both systems here.
If you use $ \bot $ you have the rules:
$\bot$ Introduction
 i |  A
 : |  : 
 j |  ~A
---------
 k |  _|_   i,j _|_ I

$\bot$ Elimination (Ex falso quidlibet)
i |  _|_
---------
k |  B    i _|_ E

$\lnot$ Introduction (reductio ad absurdum)
i | |____  A       Assumption
: | :      :
j | |      _|_
. | <--------------- end subproof
k |  ~ A     i-j  ~ I

No $\lnot$ Elimination rule
Notice that $\lnot$ I discharges an assumption while \bot $ E does not dischage an assumption.
Without $\bot $ you have the rules:
$\lnot$ Eliminationn (Ex falso quidlibet)
i |  A
: |  : 
j |  ~ A
---------
k |  B     i,j ~ Elimination

$\lnot$ Introduction (reductio ad absurdum) 
i | |____  A       Assumption
: | :      :
j | |      B & ~ B
. | <--------------- end subproof
k |  ~ A     i-j  ~ I

Personally I prefer the version with $\bot$ but you are free to have another preference.
For Classical logic you can just add the rule
$\lnot \lnot $ Elimination (Double negation eliminationt)
i |  ~~ A
---------
k |  A    i  ~~ E

But some logicians like to do it different:
they add a second reductio ad absurdum proof  (start with a negation and end without one)
A: The rules of primitive negation are: 

  
*
  
*$\lnot$-I: If $A$ leads to $B$, if $A$ leads to $\lnot B$, then $\lnot A$
  

and 


  
*$\lnot$-E: from $A$ and $\lnot A, \quad B$ can be concluded. (The first rule is "impure.") 
  

Repeated applications of these produce redundancies that can be simplified, but there is no systematic scheme so these are ad hoc: The cases are $\lnot$-I followed by $\lnot$-I and $\lnot$-I followed by $\lnot$-E. 
If the above rules are rewritten with $\lnot A = A \to \bot$ and implication rules, then the two cases turn out to be non-normalities, and the elimination of the non-normalities gives exactly the ad hoc simplifications. Details are found in my recent book "Elements of Logical Reasoning" pp. 47-49, (and sorry for the advertisement, but it hasn't been done elsewhere to my knowledge).
So, the definition $\lnot A = A \to \bot$ gives a negation that behaves like the rest of the connectives in proofs of normalization. The primitive rules work instead nicely in sequent calculus. 
