Friday, April 06, 2007

A beautiful proof

I got told a rather beautiful proof the other day, and wanted to write it down.

Question: Given any two irrational numbers x and y, does x^y ever evaluate to a rational number?

Answer: Yes.

Proof: Given the definitions:

r = 2^0.5 (square root of 2, known to be irrational)
z = r^r


  • z is rational. Set x=r, y=r and you have a proof.
  • z is irrational. Set x=z, y=r. x^y = z^r = (r^r)^r = r^(r*r) = r^2 = 2, which is rational.

This proof does not provide a particular value of x and y, but merely shows there must be one.


Anonymous said...

It's non-constructive, though - can you come up with a curry-howard encoding of its proof as a functional program which uses continuations? :)

(I would be genuinely interested to see this, as I don't feel I quite 'get' how curry-howard extends in this way...)

Neil Mitchell said...

Yes, part of the thing I like about it is that its non-constructive :) After working with Haskell for ages every other proof feels like an algorithm, this has a more beautiful feeling.

sigfpe said...

Anonymous said:

> I don't feel I quite 'get' how curry-howard extends in this way...

It took me a long time to make sense of this. When I figured it out I wrote something about the program corresponding to the non-constructively provable a \/ ~a here.

In principle there *is* a program corresponding to Neil's nice example. You can use the theory developed by Krivine here. But that looks like a pretty hard paper to me...

Malcolm said...

If you're curious which of the options is the correct one, check out the Wikipedia article Nonconstructive proof.

Anonymous said...

True, but that's a trivial proof. The hard one is proving it given x≠y...

DFER said...
This comment has been removed by the author.
DFER said...
This comment has been removed by the author.
DFER said...

(sorry my last posts had typos in it)
Here's my quick and easy proof...
1. sqrt(2) is irrational
2. x and y are non-zero irrational numbers
Prove that the product of x and y can evaluate to a rational number. If we can prove it true for one case, then we have proved it for all. Therefore...
A. x = sqrt(2) (From givens 1 & 2)
B. Proof by one case:
Bi.Assume n where sqrt(n) is rational (ex. a perfect square n=25,36, etc.)
Bii. y=sqrt(2)*sqrt(n) (from a fact that rational #* irrational # = irrational number and also given 2.)
Biii. x*y is sqrt(4)*sqrt(n) (multiplication and some simplification)
Biv. x*y=2*sqrt(n) (more simplification)
Bv. 2*sqrt(n) is rational (rational * rational = rational)
Bvi. x*y is rational (equality - QED Case)
C. Irrational * irrational can = rational (one case/instance proved)