Here is a classical example of a non-constructive proof.
Thm 1. There exist irrational numbers \(x,y\) such that \(x^y\) is rational.
Proof. If \(\sqrt{2}^{\sqrt{2}}\) is rational, then we may take \(x=y=\sqrt{2}\). Otherwise, we may take \(x=\sqrt{2}^{\sqrt{2}}, y=\sqrt{2}\); then \(x^y=2\), which is certainly rational. \(\blacksquare\)
This proof is non-constructive in that it doesn't actually give a (proven) example of a pair \(x,y\) with the desired property; it gives two possibilities (namely \((\sqrt{2}, \sqrt{2})\) or \((\sqrt{2}^{\sqrt{2}}, \sqrt{2})\)). Of course one can give more constructive proofs; for example, one can take $$x=\sqrt{2}, y=2\log_2(3),$$ and it's relatively easy to check that \(x,y\) are irrational.
What if we ask that \(x,y\) are transcendental, instead of irrational?
Thm 2. There exist transcendental numbers \(x,y\) such that \(x^y\) is rational.
Proof 1. Take \(x=e, y=\ln 2. \blacksquare\)
Of course it is well-known that \(e, \ln 2\) are transcendental, but the proofs (especially in the latter case), are pretty non-trivial. I recently ran across the following non-constructive proof of Thm 2, which is much easier. Before I give the proof, I need a definition:
Definition. A real number is incomputable if there is no computer program (Turing machine) which prints out its decimal expansion.
There are of course lots of incomputable numbers, since there are only countably many computer programs. Of course, any incomputable number is transcendental, since computer programs can approximate roots of polynomials with rational coefficients arbitrarily well.
Proof 2. Let \(x\) be any (positive) incomputable number. Let \(y=\log_x(2)\). Then \(y\) is incomputable, as otherwise \(x\) would be computable; hence \(x,y\) are transcendental, and by definition \(x^y=2\). \(\blacksquare\).
Proof 2 is even worse than our original proof of Theorem 1 -- not only is it non-constructive, the examples it produces cannot in principle be constructed!
The purpose of this post is to observe that with some mild modification, we can make a constructive version of Proof 2. Instead of using the fact that algebraic numbers are computable, we can use the fact that they are efficiently computable. In particular, if a number is algebraic, then the \(n\)-th digit of its decimal expansion may be computed in polynomial time in the number of digits of \(n\).
Proof 3. By the (proof of) the Time Hierarchy Theorem, there exists an(explicit) number \(x\) so that the \(n\)-th digit of \(x\) is not computable in polynomial time, but so that \(x\) is computable. (In particular, \(x\) is computable but transcendental.) Set \(y=\log_x(2)\). Then \(x^y=2\), but \(y\) is not computable in polynomial time, as otherwise \(x\) would be as well, (as one may solve the equation \(x^y=2\) efficiently, since logarithms and exponents may be computed efficiently).\(\blacksquare\)
This is the cheapest constructive proof of Theorem 2 that I know, though of course the \(x, y\) which are produced can only be written down slowly.