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

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.

• At this point you should know the answer: It all depends on what proof system you are using. – Bram28 Sep 25 '17 at 15:48
• @Bram28 Glad to see you here :D, would you plz answer these questions math.stackexchange.com/questions/2444337/… and math.stackexchange.com/questions/2444424/… ? – Pooria Sep 25 '17 at 15:59
• For some systems, $\bot \rightarrow \phi$ is one of its defined rules. For others, you can derive it from its rules. And for some, you can't, either because $\bot$ isn't part of its alphabet, or because the system is incomplete, or it is not a system for classical logic. – Bram28 Sep 25 '17 at 16:01

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.

• Also I asked for that proof since there's this proof proofwiki.org/wiki/Double_Negation/Double_Negation_Elimination/… that uses LEM – Pooria Sep 25 '17 at 16:12
• @Pooria OK, so you're asking for a proof of $\neg \neg \phi \rightarrow \phi$ that does not use LEM and/or $\bot \rightarrow \phi$ as one of its rules? Well, in the Hilbert system you use neither rule, and in some systems going from $\neg \neg \phi$ to $\phi$ is a rule, so you'd do it in 1 step there. I'll attach a pic of a proof done in Fitch, which is a proof system I use. – Bram28 Sep 25 '17 at 16:19
• @Pooria Hmm, I'm not versed in constructionist or intuitionist logics ... it's pure classical logic for me! :) – Bram28 Sep 25 '17 at 16:38
• @Pooria The author seems to be showing that using LEM as a rule you can derive DNE, and vice versa.... which of course does not mean that you have to use the one to prove the other, as my Answer shows. – Bram28 Sep 25 '17 at 16:49
• @Pooria :) Sure! But that still doesn't mean you have to use LEM.. it's just that you can use it (assuming you have it, of course ... e.g. both Fitch and the Hilbert system do not have LEM as a rule ... though of course both can derive LEM from the rules they do have) .. did I mention that it's all relative to whatever rules you have and do not have? :) – Bram28 Sep 25 '17 at 17:38

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.