Natural Deduction rules for $\lnot$ in classical and intuitionstic logic

Question

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 ?

Answer 1

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)