Double negation elimination in constructive logic

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

-
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... –  Ben Millwood Jun 3 '12 at 9:26
Perhaps because it's considered to be a law of thought, as stated in the Wikipedia article. –  Gigili Jun 3 '12 at 9:41
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. –  Ameen Jun 3 '12 at 9:50
Well, what about a model in which it is not fulfilled? –  dtldarek Jun 3 '12 at 9:58
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? –  Carl Mummert Jun 3 '12 at 11:46

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

-
Is this textbook style with suggested exercises appropriate for answering this question? Just asking. –  Doug Spoonwood Jun 3 '12 at 13:00

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.

EDIT:

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.

-
This is a nice example of how the law of excluded middle is devoid of computational content, but it does not answer the question. –  Zhen Lin Jun 3 '12 at 18:11
@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". –  H. Kabayakawa Jun 3 '12 at 20:41
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. –  Carl Mummert Jun 3 '12 at 23:07
@Carl Mummert: thanks for your appreciation. –  H. Kabayakawa Jun 3 '12 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.)

-