Is there a proof which uses the Peirce's law? Peirce's law $((p\to q)\to p)\to p$, which needs an excluded middle to prove, seems unnatural argument to prove something. I haven't seen it in ordinary mathematics though the excluded middle, proof by contraposition or contradiction is widely used in the mathematics, which is equivalent or more weaker than the Pierce's law in intuitionistic sense.
Is there an example of a proof which uses the Peirce's law? I would appreciate your help.
 A: It's not really a case of whether a particular proof "needs Peirce's law" or not. If you want to prove something that is classically valid but not intuitionistically valid, then your proof has to depend on whichever rule your proof system provides to make it classical rather than intuitionistic. This rule may be Peirce's law, or the law of excluded middle, or some variant of a proof-by-contradiction rule, or the equivalence between $p\to q$ and $\neg p \lor q$, or any of several other ways to get classical logic. Which one you use depends not on what you're proving, but on which tools your proof system happens to provide for it.
(Note that these possibilities are all equivalent in power to each other, and to Peirce's law, in the presence of the usual intuitionistic rules for the various connectives).
What you really mean to ask, I think, is why one would even create a proof system where Peirce's law is the classical primitive rather than one of the more intuitive axioms or rules that would also yield classical logic.
A good answer to that is that Peirce's law seem to be the simplest way to get classical logic that can be formulated using only the $\to$ connective. This makes it a technically attractive choice if you want to develop logic initially in a restricted language without the full set of usual connectives.
Additionally, I think it is inherently interesting that the difference between intuitionistic and classical logic can be phrased using only the connective $\to$. (For example, this shows us that the often-told explanation that intuitionistic logic differs principally in how it allows a disjunction to be proved can't be right).
