Is there a proof of LEM implying DNE that doesn't use $\bot\vdash\varphi$?

Question

Is there a proof not using $\bot\vdash\varphi$, proving that Law of The Excluded Middle implies Double Negation Elimination in natural deduction? The ones I've seen would use $\bot\vdash\varphi$ at some point.

Answer 1

Couple of thoughts:

First, any question like 'is there a proof ...' should always be couched relative to some proof system. i.e you should really ask 'Is there a proof system in which there exists a proof ...'

Second, when you ask for a proof that LEM implies DNE ... that's a little weird, since in classical logics DNE holds without making any further assumptions. That is, for all complete systems $S$ for classic propositional logic we have $\vdash_S \neg \neg \phi \rightarrow \phi$

EDIT: From the comments I understand you are looking for a proof that does not use LEM (nor $\bot \rightarrow \phi$ ... I'll refer to that rule as $\bot$ Elim) as one of its steps. OK, below is a proof done in Fitch, where $\neg$ Elim is defined as going from $\neg \neg \phi$ to $\phi$, so that doesn't use LEM or $\bot$ Elim:

Finaly, if you're looking for a system where you do have to derive $\neg \neg \phi \rightarrow \phi$, but that still does not use LEM or $\bot$ Elim, I point you the Hilbert system, which does not have LEM or $\bot$ Elim as its rules, but you can prove $\neg \neg \phi \rightarrow \phi$ in that system nevertheless.

Answer 2

If we look at this from the perspective of something like intuitionistic natural deduction, I don't believe so.

First, recall that we can take negation to be non-primitive, i.e. ($\neg P := P \rightarrow \bot$). Recall also that $\bot$ has no intro rules and a single elimination rule which corresponds to $\bot \vdash \varphi$. Thus, if we remove this rule, we're basically treating $\bot$ like an arbitrary formula. It seems to me then that a proof of LEM implying DNE should hold if we sub out $\bot$ for some arbitrary $Q$. Doing this to LEM yields to scheme $P \vee (P \rightarrow Q)$, and DNE yields $((P \rightarrow Q) \rightarrow Q) \rightarrow P$. Notice that the first is a classical tautology and the second is not even valid classically. Since we then can't prove this implication classically, we certainly won't be able to do it intuitionistically.