# 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 ?

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