# Can we say classical logic has DNE axiom as well because it's equivalent to LEM?

Since according to this page, law of the excluded middle is an axiom of classical logic, Does the paragraph starting with "Classical logic can be characterized by a number of equivalent axioms:" on page 2 of this doc mean that, for instance since double negation elimination is equivalent to LEM then it's also an axiom of classical logic?

• It's a tautology, anyway. What exactly the axioms are is a matter of taste. – Qiaochu Yuan Sep 23 '17 at 8:59
• @QiaochuYuan So that's a yes? – Pooria Sep 23 '17 at 9:28
• @Pooria No, it's not a "yes". Usually, one or the other (or a different equivalent statement, e.g. Peirce's law) will be taken as an axiom. Then the other will be a theorem and not an axiom. You could take both as axioms, but we usually try to avoid redundant axioms. – Derek Elkins Sep 23 '17 at 9:44
• @Pooria It's not incorrect. All it is saying, literally, is that: "We might consider making the logic we've seen so far classical by adding one or more rules that correspond to these axioms". If you were to be extremely pedantic, you might use "theorem" instead of "axiom". The point is that in a specific presentation of classical logic some of those statements will be theorems and some axioms (and thus also theorems), but the paragraph isn't referring to any particular presentation of classical logic, and all those statements are commonly chosen as axioms in different presentations. – Derek Elkins Sep 23 '17 at 10:55
• @Pooria That page is not talking about formal logic or presentations of formal logics at all except for the 21 "rules of inference" it presents later which doesn't take the law of the excluded middle as axiomatic. I also have no idea why you think that page should be considered more authoritative than the lecture notes. Why not consider the lecture notes correct and that page in error? (I'm not suggesting this, instead I'm suggesting that they are simply talking about different things: one formal logic, the other some person's personal take on informal logic.) – Derek Elkins Sep 23 '17 at 11:22

The second set of lecture notes is about a form of "Constructive Logic" used in describing proofs computationally. Its earlier chapters are on formal theories like "Martin Lof Type Theory". These theories are both formally presented and do not assume axioms like $$P \vee \lnot P$$ ("Law" of Excluded Middle) and $$P = \lnot \lnot P$$ ("Double Negation Elimination").