It's well-know that in intuitionistic logic, middle excluded law and double negation elimination are equivalent.

For example, in Johnstone - Topo theory, I read that, in a Heyting algebra, $p\vee\neg p=\top$ holds if and only if $\neg\neg p=p$ for all elements $p$.

In particular, it's easy to prove $(p\vee\neg p)\leq(\neg\neg p\Rightarrow p)$: for we have $p\Rightarrow(\neg\neg p\Rightarrow p)=(p\wedge\neg\neg p)\Rightarrow p=\top$ and $\neg p\Rightarrow (\neg\neg p\Rightarrow p)=(\neg p\wedge\neg\neg p)\Rightarrow\perp\Rightarrow p=\top$, consequently, $(p\vee\neg p)\Rightarrow(\neg\neg p\Rightarrow p)=\top$.

On the other hand, I can't prove inverse inclusion $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$.

Thus my question is:

In a Heyting algebra, does $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$ holds?

The proof that I founded here don't satisfy me because it proves only the inference rule $(\neg\neg p\Rightarrow p)\vdash (p\vee\neg p)$.

  • $\begingroup$ I don't see the problem with the answer in your link. Can you be a bit more specific on why you think it's not possible to adapt it to the present case? $\endgroup$
    – Nagase
    Aug 27, 2014 at 6:45
  • 1
    $\begingroup$ The answer in my link proves that if $\top\Rightarrow(\neg\neg p\Rightarrow p)$ for each $p$, then $\top\Rightarrow (p\vee\neg p)$, while I'm looking for a proof of $(\neg\neg p\Rightarrow p)\Rightarrow (p\vee\neg p)$. $\endgroup$ Aug 27, 2014 at 8:18
  • $\begingroup$ sorry it is just not provable (that is what i read somewhere but forgot where) $\endgroup$
    – Willemien
    Aug 27, 2014 at 9:25
  • $\begingroup$ In many logics a ⊢ b implies ⊢ a ⇒ b. So you can use it in your proof but by using it will result in meta-logic proof instead of proof inside logic. $\endgroup$ Aug 27, 2014 at 10:56
  • $\begingroup$ @Trismegistos: I'm looking for a proof valid, for example, in a Heyting algebra as in the link above. $\endgroup$ Aug 27, 2014 at 12:27

2 Answers 2


As you apparently already know, if $((\neg\neg p)\implies p)=\top$ for all $p$ in some Heyting algebra, then also $(p\lor\neg p)=\top$ for all $p$ in that Heyting algebra. Nevertheless, if $((\neg\neg p)\implies p)=\top$ for a particular $p$ in a Heyting algebra, it does not follow that $(p\lor\neg p)=\top$ for that same $p$.

For example, $((\neg\neg p)\implies p)=\top$ is true whenever $p$ is of the form $\neg q$, because $(\neg\neg\neg q)\implies(\neg q)$ is intuitionistically valid. But it is not intuitionistically valid that $(\neg q)\lor(\neg\neg q)$.

A simple explicit counterexample is the Heyting algebra of open subsets of the real line. Let $p$ be the open half-line $(0,\infty)$. The negation $\neg p$, i.e., the largest open set disjoint from $p$, is the open half-line $(-\infty,0)$, and $\neg\neg p$ equals $p$. So $((\neg\neg p)\implies p)=\top$, but $(p\lor\neg p)=\mathbb R-\{0\}\neq\top$.


We cannot prove in intuitionsitc logic :

$\vdash (\lnot \lnot p \Rightarrow p) \Leftrightarrow (p \lor \lnot p)$.

As you said, we can prove :

$(p \lor \lnot p) \Rightarrow (\lnot \lnot p \Rightarrow p)$.

For the other "direction", we can prove only a "negative version" of the theorem.

References are to Intuitionistic logic and to Heyting algebra.

1) $(\lnot \lnot p \Rightarrow p) \le (\lnot p \Rightarrow \lnot \lnot \lnot p)$ --- the law : $a \Rightarrow b \le \lnot b \Rightarrow \lnot a$ is intuitionistically valid

2) $(\lnot p \Rightarrow \lnot \lnot \lnot p) \le (\lnot p \Rightarrow \lnot p)$ --- the law : $\lnot \lnot \lnot a = \lnot a$ is intuitionistically valid

3) $= \lnot (\lnot p \land p)$ --- the law : $(a \Rightarrow \lnot b) = \lnot (a \land b)$ is intuitionistically valid

4) $= \lnot \lnot (\lnot \lnot p \lor \lnot p)$ --- weak De Morgan's law : $\lnot (x \land y) = \lnot \lnot (\lnot x \lor \lnot y)$ holds in HA

Conclusion :

$(\lnot \lnot p \Rightarrow p) \le \lnot \lnot (\lnot \lnot p \lor \lnot p)$


$\vdash (\lnot \lnot p \Rightarrow p) \Rightarrow \lnot \lnot (\lnot \lnot p \lor \lnot p)$.


Here we have a proof with sequent calculus LK of :

$\vdash (\lnot \lnot P \supset P) \supset (P \lor \lnot P)$.

i) left thread :

$${P \Rightarrow P \over P \Rightarrow P \lor \lnot P } \, \lor\text{-right} \,$$

ii) right thread :

$${P \Rightarrow P \over P, \lnot P \Rightarrow } \, \lnot\text{-left}$$

$${\over \lnot P \Rightarrow \lnot P } \, \lnot\text{-right}$$

$${\over \lnot P \Rightarrow P \lor \lnot P } \, \lor\text{-right}$$

$${\over \Rightarrow P \lor \lnot P, \lnot \lnot P} \, \lnot\text{-right}$$

Note. The last step is not intuitionistically valid because violates the restriction that :

a sequent in LJ is of the form $\Gamma \Rightarrow \Delta$, where $\Delta$ consists of at most one formula.

iii) conclusion

Now we "join" the two threads :

$${P \Rightarrow P \lor \lnot P \quad \quad \Rightarrow P \lor \lnot P, \lnot \lnot P \over \lnot \lnot P \supset P \Rightarrow P \lor \lnot P }\, \supset\text{-left}$$

$${\over \Rightarrow (\lnot \lnot P \supset P) \supset (P \lor \lnot P) }\, \supset\text{-right}$$

Regarding the impossibility of finding a proof of it in LJ, see Jan von Plato, Elements of Logical Reasoning (2013), page 82 :

Given $A \lor \lnot A$, if $\lnot \lnot A$ is assumed, $A$ follows and therefore the implication $\lnot \lnot A \supset A$ follows from $A \lor \lnot A$. An easy proof search in intuitionistic sequent calculus gives a formal derivation for :

$A \lor \lnot A \supset (\lnot \lnot A \supset A)$.

A similar proof search for the converse fails, for there is no derivation of :

$(\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.


The overall situation is that if $\vdash \lnot \lnot A \supset A$, then $\vdash A \lor \lnot A$, but not $\vdash (\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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