Constructive proof for: P => ((P => Q) => Q) I'm trying to find a constructive proof for the proposition:
P => ((P => Q) => Q)
given P and Q to nullary proposition symbols but I can't find a proof without using the excluded middle rule. Anyone has an idea on how to build a constructive demonstration for the proposition?
 A: Andrej Bauer explained the proof in a comment.  But a useful technique if you can't think of a constructive proof is to try to construct a program with the same type.  The structure of the program tells you the proof.
In this case we want a function of type $p\to(p\to q)\to q$.  That is, the function takes an argument $x$ of type $p$ and an argument $y$ of type $p\to q$ and somehow produces a result of type $q$.  There's evidently only one way to do this, which is to apply the function $y$ to the argument $x$.  The function we get is $$\lambda x. \lambda y. y x.$$  Function abstraction $\lambda a. E$ where $a$ has type $s$ and $E$ has type $t$ means to assume $s$ and prove $t$.  Function application $(y\ x)$ where $y$ has type $p\to q$ and $x$ has type $p$ mean to use modus ponens and deduce $q$.
So the proof that corresponds to the program above is:

*

*Assume $p$

*Assume $p\to q$

*From 1 and 2, deduce $q$

*From 2 and 3, conclude $(p \to q)\to q $

*From 1 and 4, conclude $p\to((p \to q)\to q)$
[ Addendum 20140823: I gave a talk that explains this in more detail; materials are here. ]
[ Addendum 20220310: A more interesting example of the same idea. ]
