2
$\begingroup$

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 ?

$\endgroup$
2
$\begingroup$

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)

$\endgroup$
  • $\begingroup$ Thanks - about the second part (with $\lnot$), the "critical point" is that the last two rules ($\lnot$-I and $\lnot \lnot$-E) do not really satisfy the inversion principle: in the $\lnot$-I we have the symbol $\lnot$ already in the premisse, and in the $\lnot \lnot$-E the $\lnot$ symbol is "doubled" in the premisse. $\endgroup$ – Mauro ALLEGRANZA Feb 2 '14 at 20:47
1
$\begingroup$

The rules of primitive negation are:

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

and

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.