In classical logic ~~p -> p? Intuitionistic?

Question

Is the following rule applicable in classical propositional logic?

$\sim (\sim p)\rightarrow p$

In my textbook, it shows that $p \rightarrow\sim(\sim p)$ holds for intuitionistic logic but I was wondering if the converse of that implication was also true? Or would it be:

$\sim p \rightarrow\ \sim(\sim(\sim p))$ ?

Nothing to wonder here...........$p\implies q =\bar{p}+q$ now apply this formula to each one of them. You would get your answer — Mayank Deora, Apr 28 '16 at 06:58
oh nice! thats a great way to think about it, sorry I didn't think of that. Sorry, so both are true then? Since ~(~~p)+p and ~(~p)+(~~~p) are congruent? @MayankDeora — ylun, Apr 28 '16 at 07:01
also, if this is the case, then why is Glivenko's theorem so substantial? Since one can easily derive the fact through this simple definition? @MayankDeora — ylun, Apr 28 '16 at 07:06
$\sim(\sim p)\to p$ is classically valid but not intuitionistically valid. $p\to \sim(\sim p)$ is both classically and intuitionistically valid.. — MJD, Apr 28 '16 at 07:09
@MJD thank you for that clarification! it makes much more sense now — ylun, Apr 28 '16 at 07:14
@MJD is there any way to further reduce ∼(∼p) in intuitionistic logic then? — ylun, Apr 28 '16 at 07:16
@MauroALLEGRANZA Sorry! no that was a person who incorrectly edited my post — ylun, Apr 28 '16 at 09:36

score 0 · Answer 1 · 2016-11-13T18:49:56.447

The answer is partly negative and partly affirmative. Here
is a proof of p -> ~~p in LJ repectively LM, the later since
we dont need ex falso:

------ (Id)   ------ (Id)
p |- p        f |- f 
-------------------- (L->)
    p, ~p |- f
    ---------- (R->)
    p |- ~~p
   ---------- (R->)
   |- p-> ~~p

Now contraposition (as a meta rule) is also valid
(admissible) in LJ respectively LM, again the later
since we don't need ex falso:

   ...
----------   ------ (Id)
G | A -> B   A |- A
------------------- (Cut)  ------ (Id)
  G, A |- B                f |- f
  ------------------------------- (L->)
         G, ~B, A |- f
        -------------- (R->)
          G, ~B |- ~A
         ------------- (R->)
         G |- ~B -> ~A

So we can apply contraposition on p -> ~~p, and
we get ~~~p -> ~p as a generally valid theorem in LJ.

But ~~p -> p is not provable in LJ, this is DNE,
i.e double negation elimination, and if it were
generally valid, we would have LJ=LK.

A LJ counter model can be found that shows that DNE isn't
generally valid in LJ. I guess a LM counter model can
also be found, an edit of this post will follow.

Interestingly although ~~p -> p is not provable,
nevertheless the contraposition ~p -> ~~~p is
provable, in LJ and in LM as well, the later again
since ex falso is not needed:

-------- (Id)  ------ (Id)
~p |- ~p       f |- f
--------------------- (L->)
   ~p, ~~p |- f
   ------------ (R->)
    ~p |- ~~~p
  -------------- (R->)
  |- ~p -> ~~~p

The proof for ~p --> ~~~p is the same as the
proof for p --> ~~p, just replace p by ~p.

Bye

Legend:
LK: Gentzen Sequent Calculus for Classical Logic
LJ: Gentzen Sequent Calculus for Intuitionistic Logic
LM: Gentzen Sequent Calculus for Minimal Logic

In classical logic ~~p -> p? Intuitionistic?

1 Answers1