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?


closed as unclear what you're asking by Rob Arthan, Theoretical Economist, Jyrki Lahtonen, Paul Frost, HK Lee Sep 2 '18 at 10:41

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ "Classical" and "propositional" are adjectives. There is classical propositional logic, intuitionistic propositional logic, classical predicate logic, intuitionististic predicate logic, and a large (ultimately infinite) variety of other logics. There are also many different presentations of the same logic. Some presentations of classical propositional logic may take the Law of Excluded Middle as an axiom, while others take double negation elimination or something else as an axiom. $\endgroup$ – Derek Elkins Sep 1 '18 at 20:08
  • $\begingroup$ I'm not sure what resources you are looking at. The Wikipedia page on propositional logic gives several presentations. "Reflexivity, symmetry, and transitivity" sounds like you're thinking about laws for equality which is orthogonal to propositional logic. Based on your recent questions, you may get something out of my post about the pedagogy of logic. Unfortunately, it is more designed to shake assumptions and provide perspective rather than to teach content. $\endgroup$ – Derek Elkins Sep 1 '18 at 20:14
  • $\begingroup$ Is there a list containing the propositional axioms? Are most things based in classical or intuitionistic? $\endgroup$ – user525966 Sep 1 '18 at 20:26
  • $\begingroup$ If you write "When I see ...", you are referring to references that you have not given us. I vote to close as you have not given enough context. $\endgroup$ – Rob Arthan Sep 1 '18 at 23:52
  • $\begingroup$ @RobArthan I think I had confused it with the wiki article on axioms of equality, but even on the wiki for prepositional calculus I'm not clear on axioms and how it relates to DNE/LEM. I edited my post to remove that paragraph. $\endgroup$ – user525966 Sep 2 '18 at 0:01

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.

  • 1
    $\begingroup$ Actually, classical propositional logic differs from intuitionistic already at $\to$: Peirce's law $((P\to Q)\to P)\to P$ is classically but not intuitionistically valid. $\endgroup$ – Henning Makholm Sep 1 '18 at 23:20
  • $\begingroup$ @HenningMakholm Good point... edited that out. I was just referring to the fact that all the rules were the same up to there cause I was originally going to do different negation elimination rules, but then ended up doing it the way with $\bot$ instead and extending with axioms instead $\endgroup$ – spaceisdarkgreen Sep 1 '18 at 23:21
  • $\begingroup$ @HenningMakholm Actually if I'd seen your answer and comments appear as I wrote this, I'd have probably aborted (for some reason the website isn't always pushing updates as well as it used to for me). It's always odd to me when people prove two classically valid things are equivalent in classical logic and act as if that means something without a much longer discussion. $\endgroup$ – spaceisdarkgreen Sep 1 '18 at 23:32
  • 1
    $\begingroup$ Well, it sounds like the OP will be interested in your more detailed sketch of intuitionistic logic, so it's not like it's wasted effort. $\endgroup$ – Henning Makholm Sep 1 '18 at 23:39
  • $\begingroup$ I'm trying to read my way through this but it's taking me some time to absorb... how are we defining "valid"? How are we defining how these connectives work without being circular? $\endgroup$ – user525966 Sep 2 '18 at 0:52

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.

  • $\begingroup$ How do you derive DNE and EM from "implies"? (and as far as I know, contraposition can be proved from "implies" itself. p -> q, means not p or q, means q or not p, means not q -> not p). Also isn't it $(\neg Q\to \neg P)\iff(P\to Q)$? $\endgroup$ – user525966 Sep 1 '18 at 22:39
  • $\begingroup$ @user525966: Surprisingly it turns out that the single direction $(\neg Q\to \neg P)\to(P\to Q)$ is enough to derive everything, if you just have Modus Ponens and the Deduction Theorem. It will give you DNE and EM and its own converse as well as introduction and elimination rules for $\neg$ all in one breath. But I don't remember how that works well enough to even sketch it. $\endgroup$ – Henning Makholm Sep 1 '18 at 22:54
  • $\begingroup$ Is $\leftrightarrow$ itself considered an axiomatic relation? For example when you say $(P\to Q)\leftrightarrow(\neg P\lor Q)$ is an axiom it's still using $\leftrightarrow$ which in itself is an operator with its own truth table, etc. $\endgroup$ – user525966 Sep 1 '18 at 23:02
  • 1
    $\begingroup$ @user525966: It could be either, though in a natural deduction system one would typically choose a rule that has an implication so it can be framed as a deduction rule rather than an axiom. $\endgroup$ – Henning Makholm Sep 2 '18 at 14:24
  • 1
    $\begingroup$ @user525966: And there are both intuitionistic and classical variants of all of Hilbert systems, natural deduction or sequent calculus. $\endgroup$ – Henning Makholm Sep 2 '18 at 14:25

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.

  • $\begingroup$ So then implication, $A\to B \iff \neg A\vee B$, how is this proven outside of a truth table? Or is this considered an axiom too? $\endgroup$ – user525966 Sep 1 '18 at 22:59
  • $\begingroup$ @user525966 Truth tables aren't about proof. They are about validity (and even then, only for classical propositional logic, not for classical predicate logic or non-classical logics). The soundness and completeness theorems for classical propositional logic connects validity and provability, but this is a meta-theorem and requires an (a priori) unrelated notion of formal proof. $\endgroup$ – Derek Elkins Sep 1 '18 at 23:40
  • $\begingroup$ I don't understand what that means. People use truth tables all the time to show / prove that something works. $\endgroup$ – user525966 Sep 2 '18 at 0:28
  • $\begingroup$ @user525966 yes. This is also an axiom. Truth tables give us "semantic" truths (provided you start with a few tautologies), and proofs give us "syntactic" truths (provided you start with axioms). You confusion exists because you are using "proof" in the common usage (whereas people here have a lot more experience in logic and for them "proof" is burned in them to mean "there exists a deduction from axioms for this proposition". In first order logic syntax and semantics are equivalent ... but only because of the axioms we chose. $\endgroup$ – Squirtle Sep 2 '18 at 0:56
  • $\begingroup$ Some definitions: A tautology is any proposition that is true on a truth table no matter what truth value you give to each of its parts (for example $\neg P\vee P$). When we build an axiomatic system, we include all tautologies as part of our list of axioms (there are other axioms but this is getting off topic). This is why in my answer above I asserted a few axioms. It seems you are stumbling on something important: We cannot prove anything without at least a few basic assumptions and rules to connect things. Related is the following:en.wikipedia.org/wiki/Münchhausen_trilemma $\endgroup$ – Squirtle Sep 2 '18 at 1:02

Two basic equivalences in classical logic are:

Double Negation

$$P \Leftrightarrow \neg \neg P$$


$$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?

  • $\begingroup$ This seems circular. You're actually assuming both and then showing that they are logically equivalent. $\endgroup$ – Squirtle Sep 1 '18 at 21:38
  • $\begingroup$ Not sure I follow what this is trying to show? Seems like it's starting out with something and proving a weaker form of itself? And which aspect is the axiom? $\endgroup$ – user525966 Sep 1 '18 at 21:38
  • $\begingroup$ It's trying to show the final line: Law of excluded middle if and only if P implies itself if and only if Double Negation is a law. The far left and the far right of the final equation are what we use (in a deduction) to replace Truth with ~P or P and ~~P with P. $\endgroup$ – Squirtle Sep 1 '18 at 21:40
  • $\begingroup$ Law of excluded middle though is "p and not p = false" I thought? Or I guess same as "not p or p = true" if we apply demorgans laws but then that's invoking another thing to prove. I'm still not sure I'm following the explanation though. It's showing how you get from one to the other if we assume they work, if I understand correctly. $\endgroup$ – user525966 Sep 1 '18 at 21:55
  • $\begingroup$ you are confusing it with law of noncontradiction. $\endgroup$ – Squirtle Sep 1 '18 at 22:04

Not the answer you're looking for? Browse other questions tagged or ask your own question.