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.
[Math] proof of LEM implying DNE that doesn’t use $\bot\vdash\varphi$
natural-deductionproof-writing
Related Solutions
1) $\lnot (A \lor \lnot A)$ --- assumed [a]
2) $A$ --- assumed [b]
3) $A \lor \lnot A$ --- from 1) by $\lor$-intro
4) $\lnot A$ --- from the contradiction : 2) and 3) by $\lnot$-intro, discharging [b]
5) $A \lor \lnot A$ --- $\lor$-intro
6) $\lnot \lnot (A \lor \lnot A)$ --- from the contradiction : 1) and 5) by $\lnot$-intro, discharging [a]
7) $A \lor \lnot A$ --- from 6) by $\lnot \lnot$-elim.
For the different "flavours" of the negation rules in Natural Deduction you can see :
Dag Prawitz, Natural Deduction : A Proof-Theoretical Study (1965), page 35 (for the two $\lnot$-rules replacing the $\bot$-rules in classical logic); or :
Neil Tennant, Natural logic (1978), page 57.
Your idea regarding the proof : $P \to Q \vdash \lnot P \lor Q$ is correct: you can use the "derived" rule :
$$\dfrac { } {\lnot P \lor P}$$
Alternatively :
0) $A \to B$ --- premise
1) $\lnot A$ --- assumed [a]
2) $\lnot A \lor B$ --- by $\lor$-intro
3) $\lnot (\lnot A \lor B)$ --- assumed [b]
4) $\lnot \lnot A$ --- from 1) with contradiction : 2) and 3) by $\lnot$-intro, discharging [a]
5) $A$ --- from 4) by $\lnot \lnot$-elim
6) $B$ --- from 0) and 5) by $\to$-elim
7) $\lnot A \lor B$ --- $\lor$-intro
8) $\lnot \lnot (\lnot A \lor B)$ --- from 3) with contradiction : 7) and 3) by $\lnot$-intro, discharging [b]
9) $\lnot A \lor B$ --- from 8) by $\lnot \lnot$-elim
Thus, from 0) and 9) :
$A \to B \vdash \lnot A \lor B$.
Without a falsum constant, your rule of ex falso quodlibet should look something like $\phi, \neg \phi \vdash \psi$. So from the contradictory assumptions, $\neg\neg a$ and $\neg a$, you may immediately derive $a$.
$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{a \qquad \text{ex falso quodlibet }\neg a, \neg\neg a \vdash a }\\\vdots}$$
PS: If ex falso quodlibet looks like $\phi\wedge\neg\phi\vdash\psi$, simply introduce a conjunction then use it.
PPS
If ex falso quodlibet is not accepted as fundamental, but disjunctive syllogism is, then introduce a disjunction and use that. $$\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{\neg a\vee a\qquad:\text{disjunctive introduction }\neg a\vdash \neg a\vee a\\a \qquad\qquad:\text{disjunctive syllogism }\neg a\vee a, \neg\neg a \vdash a }\\\vdots}$$
P$^3$S
Disjunctive Syllogism and Ex Falso Quodlibet are interprovable - each may be justified only by accepting the other - so which is considered fundamental by a proof system is a matter of preference. (EFQ has a smaller format.) $$\tiny\fitch{((p\lor q)\land\lnot p)\to q:\text{Premise of Disj.Sylogism}}{\fitch{p\land\lnot p}{\lnot p:\text{Conj. Elim.}\\p:\text{Conj.Elim.}\\p\lor q:\text{Disj.Intro}\\(p\lor q)\land\lnot p:\text{Conj.Into.}\\q:\text{Cond.Elim.}}\\(p\land\lnot p)\to q:\text{Cond.Into}}\fitch{(p\land\lnot p)\to q:\text{Premise of Ex Falso Quodlibet}}{\fitch{(p\vee q)\land\lnot p}{\lnot p:\text{Conj.Elim.}\\p\lor q:\text{Conj.Elim.}\\\fitch{p}{p\land\lnot p:\text{Conj.Intro.}\\q:\text{Cond.Elim.}}\\p\to q:\text{Cond.Into.}\\\fitch{q}{}\\q\to q:\text{Cond.Intro.}\\q:\text{Disj.Elim.}}\\((p\vee q)\land\lnot p)\to q:\text{Cond.Into.}}$$
P$^4$S Oh! As Mauro comments, if $\phi\to\psi,\phi\to\neg \psi\vdash \neg \phi$ is considered as the negation introduction rule, then $\phi,\neg\phi\vdash\psi$ (EFQ) could be considered the corresponding negation elimination rule. Thereby cutting out the need for a falsum symbol.
Best Answer
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.