Logic – Double Negation Elimination in Constructive Logic

constructive-mathematicslogic

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

Best Answer

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

Related Question