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?
 A: Having just seen this unanswered question, I shall make a few comments to clarify. There are two sets of Logic lecture notes being compared here:


*

*Lectures on Philosophical Logic

*Lectures on Constructive Logic
The first set of lectures describe the history of logic, and here "Classical" means (philosophers') understanding of Classical Greek thinking and classical mathematics. This is a two valued theory and the list of supplementary inference rules on that page are all derivable in classical logic. However this page, and indeed this course, is not presenting a formal theory of mathematical logic. It is primarily concerned about "methods of argumentation". So the term "Axiom" is a non-formal phrase here (although the axioms correctly describe such Classical Logic).
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").
The missing link between the two sets of lecture notes, from a modern logic perspective, is the development in the 20th Century of "Intuitionistic Logic"(https://en.wikipedia.org/wiki/Intuitionistic_logic) (under Brouwer) and its eventual linking with the recursion and computation theory of Godel, Turing, etc. This intuitionistic logic has axioms from which neither LEM (nor DNE) can be derived. Hence the need to explicitly add one or the other of these axioms in Chapter 7 of the notes to emulate "Classical Logic" in these systems.
