# What is a constructive proof of $\lnot\lnot(P\vee\lnot P)$?

Glivenko's theorem says that $\lnot\lnot P$ is a theorem of intuitionistic logic whenever $P$ is a theorem of classical logic. Is it closely related to the so-called Gödel–Gentzen negative translation which embeds classical logic into intuitionistic logic.

Since $P\vee\lnot P$ is a well-known theorem of classical logic, I expect that by Glivenko's theorem, $\lnot\lnot(P\vee\lnot P)$ is provable in intuitionistic logic. But I cannot find a proof! I must be overlooking something obvious.

If $\lnot\lnot(P\vee\lnot P)$ is indeed provable in IL, I would like to see a natural deduction or sequent calculus proof of it, or especially a construction of a typed $\lambda$-calculus term with the type $((P\vee(P\to \bot))\to\bot)\to\bot$.

If it is not provable in IL, what have I misunderstood?

Addendum: I cross-checked the proposition with the usual model, letting $P$ be a subset of $\mathbb R$, and interpreting $\vee$ as set union and $\lnot x$ as the interior of the complement of $x$, and the proposition $\lnot\lnot(P\vee\lnot P)$ did seem to come out as all of $\mathbb R$ for any choice of $P$, so if I have made a mistake here too I would like to know what subset of $\mathbb R$ is the counterexample.

-
The Wikipedia article on Intuitionistic logic says that tautologies of classical logic can no longer be proven within intuitionistic logic. Examples include not only the law of excluded middle p ∨ ¬p, but also Peirce's law ((p → q) → p) → p, and even double negation elimination. In classical logic, both p → ¬¬p and also ¬¬p → p are theorems. In intuitionistic logic, only the former is a theorem: double negation can be introduced, but it cannot be eliminated. –  Kaz May 3 '12 at 4:26
A must-read in this context is the short article Constructive Law of Excluded Middle by Oleg Kiselyov. This is related to an interpretation of the law of excluded middle with continuations: If you are asked whether $P$ or $\neg P$ holds, first capture the current continuation and then answer $\neg P$. If you are lucky and $\neg P$ is actually true, you are done at this point. Otherwise, ... –  Ingo Blechschmidt Feb 21 at 14:33
... your opponent might show you proof of $P$, expecting you to prove a contradiction. In this case, take the continuation (i.e., go back in time) and answer differently: Claim that $P$ holds and nastily present the proof your opponent just gave to you. There is also a fairy tale writeup by Edward Z. Yang. –  Ingo Blechschmidt Feb 21 at 14:34
Thanks. This is essentially the construction Wadler gives (originally due to Selinger) in Call-by-Value is Dual to Call-by-Name, in his story about the Devil offering a man either a billion dollars, or the chance to exchange a billion dollars for an unlimited wish. –  MJD Feb 21 at 16:08

Per the BHK interpetation, a proof of $(P \lor (P \to \bot)) \to \bot$ is pair of procedures, one for each disjunct in the hypothesis.

• The first, $s_1$, is a procedure which takes a proof of $P$ as input and produces a proof of $\bot$. In other words, the first is a proof of $P \to \bot$.

• The second, $s_2$, takes any proof of $P \to \bot$ as input and produces a proof of $\bot$. In other words, it is a proof of $(P \to \bot) \to \bot$.

By composing these to form $s_2(s_1)$, we obtain a procedure which takes no input and produces a proof of $\bot$.

The procedure just described (composition) takes any proof of $(P \lor (P \to \bot)) \to \bot$ and produces a proof of $\bot$. This means that $((P \lor (P \to \bot))\to \bot) \to \bot$ is provable.

This description shows how to write a $\lambda$ expression of the appropriate type. All that it does is to break the input into its two components and run the second one with the first as input. In particular, if we view $(P \lor \lnot P) \to \bot$ as a type $p(n,s)$ such that $\lambda s.p(1,s)$ is of type $P \to \bot$ and $\lambda\,s.p(2,s)$ is of type $\lnot P \to \bot$ then $$\lambda\, p(n,s) . p(2,\lambda\, s.p(1,s))$$ is of type $((P \lor \lnot P) \to \bot) \to \bot$

-
Thanks very much; this is exactly what I was looking for. I now understand several things better than I did before. –  MJD May 3 '12 at 13:39

Here's a natural deduction proof:

1. $\lnot (P \lor \lnot P)$ [Assumption]
2. $\lnot P \land \lnot \lnot P$ [De Morgan]
3. $\lnot P$ [$\land$ elimination]
4. $\lnot \lnot P$ [$\land$ elimination]
5. $\bot$ [$\bot$ introduction from 3., 4.]
6. $\lnot \lnot (P \lor \lnot P)$ [$\lnot$ introduction]
-
Here's the derivation of $\lnot P$ ($\lnot \lnot P$ is a virtual replay): 1. $\lnot (P \lor \lnot P)$ [line 1] 2. $P$ [Assumption] 3. $P \lor \lnot P$ [$\lor$-introduction] 4. $\bot$ [1., 3.] 5. $\lnot P$ [$\lnot$ introduction] Then combine using $\land$ introduction. –  student May 3 '12 at 3:38
Thanks, I should have seen that. –  Carl Mummert May 3 '12 at 3:43
sure, no problem :-) –  student May 3 '12 at 3:44
Yes, that portion of De Morgan's law is valid, but I appreciate the extra explanantion. Thanks. If you don't object, I would like to edit it into your answer. –  MJD May 3 '12 at 3:46

Although I've already accepted Carl Mummert's answer, which was just what I wanted, I'm going to append the following variations for future reference.

First, a proof:

1: Assume $((a\vee(a\to\bot))\to\bot$
2a: Assume $a$
2b: $a\vee(a\to\bot)$ [2a, right $\vee$]
2c: $\bot$ [1, 2b, mp]
3: $a\to\bot$ [2a–2c]
4: $a\vee(a\to\bot)$ [3, left $\vee$]
5: $\bot$ [1, 4, mp]
6: $(((a\vee(a\to\bot))\to\bot)\to\bot$ [1–5]

And a program with the requisite type:

λf.
let g = λa. f (Left a)
let h = λn. f (Right n)
in
h g


a has type $a$,
n and g have type $a\to\bot$,
f has type $(((a\vee(a\to\bot))\to\bot)$, and
h has type $((a\to\bot)\to\bot)$.

\f -> let
g = \a -> f (Left a)
h = \n -> f (Right n)
in h g


is accepted by GHC and has type (Either a (a -> t) -> t) -> t.
We can β-reduce this term to

\f -> f (Right ( \a -> f (Left a) ))


which has the same type.

-