# 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

## 1 Answer

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:

1. Lectures on Philosophical Logic

2. 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.