Double negation vs. law of excluded middle? I think I am operating under classic logic here, or propositional logic? Not sure if these are the same thing or what all the options are here.
When I see how to prove double negation elimination, it uses law of excluded middle. When I see how to prove law of excluded middle, it uses double negation elimination.
Are these two things considered equivalent and axiomatic or is there some other proof that handles both? If it is an axiom, what other axioms exist?

Assume that $\neg P\vee P$ is an axiom as well as implication ($A\to B \iff \neg A\vee B)$ and assume that our system allows modus ponens (If $A$ and $A\to B$ hold then $B$).  Lastly $C\iff D$ is short for $(C\to D)\wedge (D\to C$). We also need simplification of conjugation (to the left): This says if $C\wedge D$ then $C$.

(1) $\neg P\vee P$ : Axiom (Law of Excluded Middle)
(2) $ \ \neg P\vee P \iff (\neg\neg P\to P)$ : Axiom (Implication)
(2*) $ \neg P\vee P \to (\neg\neg P\to P) \wedge (\neg\neg P\to P) \to (\neg P\vee P)$ this is line (2) written out in full.
(3) $ \neg P\vee P \to (\neg\neg P\to P)$
(4) $\therefore \neg\neg P \to P : by$  MP applied to lines (1) and (3)

I'm not sure how you can do this in any more of a minimalistic manner.... or why you would want to; but I guess you're just curious.
Hope that helps... if you have any questions, I'll try to answer.
