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)

Answer 2

The rules of primitive negation are:

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

and

2. $\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.