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?
On
Two basic equivalences in classical logic are:
Double Negation
$$P \Leftrightarrow \neg \neg P$$
Implication
$$P \rightarrow Q \Leftrightarrow \neg P \lor Q$$
Thus, we have:
$$\neg P \lor P \Leftrightarrow P \rightarrow P \Leftrightarrow \neg \neg P \rightarrow P$$
Does that help?
On
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.
On
Double-negation elimination and the law of excluded middle are both things that happen to be true in the semantics we want for classical propositional logic -- defined, for example, by truth tables and how to evaluate a proposition under a given truth assignment.
When we construct a proof system for the logic we want that proof system to be able to prove both double-negation elimination and the law of excluded middle (because they are semantically valid and we want the proof system to prove everything that is semantically valid).
Often this is ensured by considering either double-negation elimination or excluded middle as a primitive proof step.
The proofs you have seen of "DNE implies LEM" and "LEM implies DNE" are not supposed to convince you that the principles are valid -- truth tables are much better for that. The worth of those proof is merely that they show if one of these principles is allowed as a primitive proof step, then the other doesn't need to be.
(It is also not uncommon that neither of these principles are primitive proof step, but something else an equivalent is used instead. For example, this could be a primitive rule for proof-by-contradiction, or $(P\to Q)\to(\neg P\lor Q)$ or the "reverse contraposition" rule $(\neg Q\to \neg P)\to(P\to Q)$ can be declared to be a logical axiom. Then both DNE and LEM can be derived from that).
I ask because when I look up logic axioms I only see basic stuff like reflexivity, symmetry, transitivity, etc, but nothing like double negation or law of excluded middle.
There are many equivalent ways to construct a proof system for classical propositional logic. They have different sets of logical axioms, but they can all prove exactly the same conclusions.
So it does not make sense to ask whether this-or-that formula is a logical axiom in general. You can only ask whether it is a logical axiom in such-and-such proof system.
If you try to google a list of logical axioms, you will find several lists. Some of them will, as is the nature of google results, be misunderstood or nonsense. But each of the ones that aren't will belong to a particular proof system. And it may not always be clear in the context you find that this is the case.
In a propositional logic, the sentences are built out of primative abstract sentences $A_1,A_2,\ldots $ by combining them with connectives. The usual set of connectives are $\{\lnot,\land,\lor,\to, \leftrightarrow\},$ though sometimes a smaller set is used (or a smaller set is taken as primative and the others are defined off of them). Sometimes also there are other connectives too (e.g. in modal propositional logic), but since we're only really focusing on classical and intuitionistic here, which only use the ones I mentioned.
So things like $A_1\to A_2$ and $A_1\lor \lnot A_3$ would be sentences. Here we would write the law of excluded middle as $$ \mathcal A \lor \lnot\mathcal A$$ where it's understood that we can substitute any given sentence for $\mathcal A.$ Such a substitution is called an instance of LEM, so, for instance $ (A_1\land A_2)\lor \lnot(A_1\land A_2)$ is an instance of LEM.
The thing that makes the system "propositional" as opposed to, say, a predicate logic is that the basic building blocks are these primative abstract sentences $A_i.$ In predicate logic, the atomic sentences themselves have structure, and we have variables and constants representing individuals, and relation symbols representing relations between individuals (like equality), and quantifiers. For instance, you've probably seen things like $$\forall x_1 \forall x_2((x_1<x_2)\land (x_2<x_1)).$$ This is a sentence in predicate logic (that is also false in its usual interpretation as a sentence about numbers).
Predicate logic is related to propositional logic cause we can still write things like LEM $$ \mathcal A \lor \lnot\mathcal A,$$ where now we will substitute sentences of predicate calculus in for $\mathcal A$ to generate instances. So we can talk about the LEM in either context. From now on, I'll stick to propositional logic.
Now, we've talked about the grammar, but we still haven't said what these sentences are for. Of course we know that we intend $A_1\to A_2 $ to mean what "if $A_1$, then $A_2$" informally means and $A_1\land A_2$ to mean "$A_1$ and $A_2$", etc. We want is to be able to prove certain sentences valid, for instance, clearly we would like to be able to show somehow $A_1\to A_1$... this is clearly something that "should" be valid.
So we need a deductive system, which consists of rules for taking valid sentences and producing new valid sentences, as well as axioms, sentences we assume are valid. There are tons of different ways to do this: the main systems fall into three categories: Hilbert-style systems, natural deduction, and sequent calculus. No time to explain what these are, of course, other than to say a natural deduction system will be most convenient for our purposes here, so that's the category you're seeing here, though it will usually be presented much more formally (and carefully).
In this, we will take as a primative axiom scheme that $\mathcal A\to \mathcal A$ is valid where anything is substituted for $\mathcal A.$ This will be the only axiom, and everything else will be rules. (EDIT: I actually don't think this axiom scheme is even necessary since every instance of it follows from the $\to$ introduction rule described below.)
For instance, we have an introduction rule for $\lor$ that if a sentence $\phi$ is valid then $\phi\lor \psi$ and $\psi \lor \phi$ are valid for any sentence $\psi.$ Then we have an elimination rule, that if from the assumption of validity of a sentence $\phi$, we can derive that $\psi$ is valid, and separately, if from the assumption of the validity of a sentence $\phi',$ we can derive that same $\psi$ is valid, and $\phi\lor \phi'$ is valid, then $\psi$ is valid.
We can define similar introduction and elimination rules for $\land$... I won't mention what they are for lack of space: they're easier than the ones for $\lor$ and you can probably figure out what they are. Then there is an introduction rule for $\to$: if starting with a hypothetical assumption of $\phi,$ we can derive that $\psi$ is valid, then $\phi\to \psi $ is valid. And then the elimination rule is that if both $\phi$ and $\phi\to \psi$ are valid, then $\psi$ is valid.
Finally, we come to negation. First off, it is most convenient to not take negation as primative, but rather to take special primative sentence $\bot$ which intuitively represents a false statement or a contradiction. Then we define negation as $\lnot \mathcal \phi = \mathcal \phi\to \bot.$ Then we have an elimination rule for $\bot$ that from $\bot$ we can infer any sentence, which formalizes the notion that from an absurdity, we can derive anything. There is no introduction rule for $\bot.$
Notice this gels with our intuitive idea of contradiction, because if we have $\phi$ and $\lnot \phi,$ which recall is just an abbreviation for $\phi\to \bot,$ then by $\to$ elimination, we infer that $\bot$ is valid.
These rules give a version of the deductive system for intuitionistic propositional logic. Any statement whose validity can be proven by these rules is called intuitionistically valid. As I mentioned before, there are many different types of deductive systems that all produce the same valid sentences... I have only given one example.
Now, here's where we finally get down to answering your question. We can convince ourselves that we can neither prove $A_1 \lor \lnot A_1$ nor $\lnot\lnot A_1 \to A_1$ from the above rules. (It's a bit more complicated than this if we want to be careful, but the basic idea for LEM is that in order to get $A_1\lor\lnot A_1,$ we'd need to use the introduction rule for $\lor,$ which requires that we have either $A_1$ or $\lnot A_1$ valid. And it's clear, since $A_1$ is just some abstract sentence, there's no way of proving either of these things.)
So the schemes $\mathcal A \lor \lnot \mathcal A$ and $\lnot\lnot \mathcal A \to \mathcal A$ are not generally valid under intuitionistic logic. However, we can show that by taking either one of these schemes as an axiom, we can derive every instance of the other. So LEM and double negation elimination are equivalent over intuitionistic propositional logic. Adding either of these as an axiom results in classical propositional logic.