How can I prove that the double negation elimination is not provable in constructive logic?
To clarify, double negation elimination is the following statement:

$$\neg\neg q \rightarrow q$$

  • $\begingroup$ It's straightforward to prove that double negation elimination is equivalent to the law of excluded middle, but I don't know if that helps... $\endgroup$ Jun 3, 2012 at 9:26
  • $\begingroup$ Perhaps because it's considered to be a law of thought, as stated in the Wikipedia article. $\endgroup$
    – Gigili
    Jun 3, 2012 at 9:41
  • $\begingroup$ I read the article and understand it, however i have this question given in a homework. It was said that is proving it is hard, then argue for it logically. $\endgroup$
    – Ameen
    Jun 3, 2012 at 9:50
  • 1
    $\begingroup$ So are you wanting to prove this or just argue logically? $\endgroup$ Jun 3, 2012 at 10:10
  • 4
    $\begingroup$ What methods have you learned in class for showing that a statement is not provable in constructive logic? What sorts of models for constructive logic are you familiar with? $\endgroup$ Jun 3, 2012 at 11:46

3 Answers 3


There are two ways to go about this:

  1. Proof theory. We analyse the formal proofs in the inference system given, and show that there can be no formal proof of double negation elimination. This is difficult and depends a lot on the details of the inference system.

  2. Model theory. We construct a model of intuitionistic propositional logic in which double negation elimination is visibly false. This is much easier and less sensitive to details, but is conceptually more challenging.

First of all, what is a model of intuitionistic propositional logic? It is an algebraic structure $\mathfrak{A}$ equipped with constants $\top$ and $\bot$ as well as binary operations $\land$, $\lor$, $\to$, plus a partial order $\le$, such that the following soundness rule is valid: given formulae $\phi$ and $\psi$ in the language of intuitionistic propositional logic with propositional variables $x, y, z, \ldots$, if the sequent $\phi \vdash \psi$ is provable, then $\phi \le \psi$ in $\mathfrak{A}$ for all choices of $x, y, z, \ldots$ in $\mathfrak{A}$.

For example, $\mathfrak{A}$ could be a Heyting algebra, which is a algebraic structure satisfying some axioms. First of all $\mathfrak{A}$ is a (bounded) lattice:

  • Unit laws: \begin{align} \top \land x & = x & \bot \lor x & = x \\ x \land \top & = x & x \lor \bot & = x \end{align}
  • Associativity, commutativity, and idempotence: \begin{align} (x \land y) \land z & = x \land (y \land z) & (x \lor y) \lor z & = x \lor (y \lor z) \\ x \land y & = y \land x & x \lor y & = y \lor x \\ x \land x & = x & x \lor x & = x \\ \end{align}
  • Absorption law: \begin{align} x \land (x \lor y) & = x & x \lor (x \land y) & = x \end{align}

One can then verify that $x \le y$ defined by $x \land y = x$ is a partial order on $\mathfrak{A}$ and that $\top$, $\bot$, $\land$, $\lor$ have their usual order-theoretic meanings. We then add some axioms for $\to$:

  • Distributive law: $$x \to (y \land z) = (x \to y) \land (x \to z)$$
  • Internal tautology: $$x \to \top = \top$$
  • Internal weakening: $$y \to (x \land y) = y$$
  • Internal modus ponens: $$x \land (x \to y) = x \land y$$

Exercise. Show that $y \le z$ implies $(x \to y) \le (x \to z)$, and $x \le ((x \land y) \to y)$ and $((x \to y) \land y) \le x$, and hence or otherwise that $x \land y \le z$ if and only if $x \le (y \to z)$.

Exercise. Verify the soundness rule for interpreting intuitionistic propositional logic in a Heyting algebra.

Proposition. Double negation elimination is not valid in intuitionistic propositional logic.

Proof. We construct a three-element Heyting algebra to falsify double negation elimination. Let $\mathfrak{A} = \{ \bot, \omega, \top \}$ and define the binary operations as below: \begin{align} \begin{array}{|r|ccc|} \hline \land & \bot & \omega & \top \\ \hline \bot & \bot & \bot & \bot \\ \omega & \bot & \omega & \omega \\ \top & \bot & \omega & \top \\ \hline \end{array} && \begin{array}{|r|ccc|} \hline \lor & \bot & \omega & \top \\ \hline \bot & \bot & \omega & \top \\ \omega & \omega & \omega & \top \\ \top & \top & \top & \top \\ \hline \end{array} && \begin{array}{|r|ccc|} \hline \to & \bot & \omega & \top \\ \hline \bot & \top & \top & \top \\ \omega & \bot & \top & \top \\ \top & \bot & \omega & \top \\ \hline \end{array} \end{align} Then, observe that $((\omega \to \bot) \to \bot) = \top$, but $\top \nleq \omega$. Therefore $(x \to \bot) \to \bot$ cannot be an axiom of intuitionistic propositional logic.

Remark. De Morgan's laws remain valid in this Heyting algebra. Find one which falsifies part of De Morgan's laws. (See this question.)

  • 1
    $\begingroup$ Is this textbook style with suggested exercises appropriate for answering this question? Just asking. $\endgroup$ Jun 3, 2012 at 13:00
  • $\begingroup$ I believe in the last part you mean "Therefore $((x \to \bot) \to \bot) \to x$ cannot be an axiom of intuitionistic propositional logic." $\endgroup$ Jul 24, 2019 at 23:11

There is an intuitionistic idea which becomes more valuable with the arrival of computational-mathematics. Roughly speaking in constructive logic or math, when you say "object A" exists you are saying "we know some way to build up A". This position implies the 'tertio excluso' rule $\neg(\neg q))\rightarrow q$ fails.

The classic example belongs to Brouwer (1925). We write the decimal expansion of $\pi$, and down to it the number $\rho=0.333\ldots$that we cut when the sequence $012346789$ appear in $\pi$ the first time. With the classical logic we say that $\rho$ is rational. If the sequence $012346789$ doesn't appear $\rho$ will be defined by $ \frac{1}{3}$. With the constructive approach you can't prove $\rho$ is rational before you find the first sequence $0123456789$ in $\pi$ or you have a proof that this sequence never appears in the decimal expansion of $\pi$.

But in constructive math you can prove that it is contradictory that $\rho$ is not rational. If we suposse $\rho$ isn't rational (equivalently, that we have a construction to tell apart $\rho$ of any rational number) then $\rho=0.3333\ldots 3$ must be impossible, and the sequence $0123456789$ doesn't appear in $\pi$. Therefore $\rho=\frac{1}{3}$ which is impossible too. Then it is contradictory that $\rho$ is not rational, but we don't have a proof that $\rho$ is rational.


My answer is complementary to other more formal answers. It goes to the main point to give up the $\neg(\neg q))\rightarrow q$. Essentially my answer is intuitionistic, no a formalism.

  • $\begingroup$ This is a nice example of how the law of excluded middle is devoid of computational content, but it does not answer the question. $\endgroup$
    – Zhen Lin
    Jun 3, 2012 at 18:11
  • $\begingroup$ @Zhen Lin: I think really it is an answer. It contains implicitly a model of the axiom that you have shown in your answer, where $\neg(\neg q))\rightarrow q$ is not true. As you said "There are two ways to go about this". $\endgroup$ Jun 3, 2012 at 20:41
  • $\begingroup$ I think this is a fine answer, and voted it up. The answer can easily be modified to show that there is a constructive proof of the limited principle of omniscience LPO ( ncatlab.org/nlab/show/principle+of+omniscience ) from the scheme $\lnot\lnot P \to P$. Because LPO is not constructively provable in the usual constructive systems, it follows that the double negation elimination scheme is also not provable, and this is completely rigorous. $\endgroup$ Jun 3, 2012 at 23:07
  • $\begingroup$ @Carl Mummert: thanks for your appreciation. $\endgroup$ Jun 3, 2012 at 23:16

A very simple and efficient tree proof method (i.e. a tableau method without signed formulae) for intuitionistic logic has been published by Bell, DeVidi and Solomon in "Logical Options: An Introduction to Classical and Alternative Logics" http://books.google.fr/books/about/Logical_Options.html?id=zUVYx-bTLgMC&redir_esc=y

Here is the tree counter-model for the formula $\neg \neg p \to p$, à la Bell $et{}~ al.$:

$$\underline{?(\neg \neg p \to p)}^{\surd}$$ $$ ? p $$ $$ \neg \neg p$$ $$ \underline{? \neg p }^{\surd}$$ $$ p $$ The tree show a Kripke counter-model where, in a locality expressed by a space between two horizontal lines, $p$ is not known to be true (i.e. is false in the locality), while $\neg \neg p$ is proved, i.e. is known to be true. The symbol $?$ says that the formula is not known to be true, and it sticks the formula in the locality. The symbol $\surd$ says that the formula is deactivated. Every formula without $\surd$ or without $?$ can pass through any horizontal line (truth is persistent). For more details, see Bell et al.'s book.

This is very simple proof method to echo to the very nice explanation given by Zhen Lin. (I wish to thank Zhen Lin warmly for his post.)

Reading this page again, I must add that, contrarily to what Ben Millwood claimed, double negation elimination is not equivalent to the law of excluded middle, because if it is true that $(\neg A \lor A)$ implies $(\neg \neg A \to A)$ in intuitionistic logic, the converse is not intuitionistically provable. The fact that $(\neg \neg A \to A) \to (\neg A \lor A)$ is not an intuitionistic theorem contradicts the claim that double negation elimination is equivalent to the law of excluded middle.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .