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

Either:

  • 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.
at

8 comments:

  1. Anonymous3:29 PM

    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...)

    ReplyDelete
  2. Neil Mitchell3:30 PM

    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.

    ReplyDelete
  3. sigfpe6:34 PM

    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...

    ReplyDelete
  4. Unknown3:29 PM

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

    ReplyDelete
  5. Anonymous12:39 AM

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

    ReplyDelete
  6. Daryl Ferreras3:54 PM

    This comment has been removed by the author.

    ReplyDelete
  7. Daryl Ferreras3:56 PM

    This comment has been removed by the author.

    ReplyDelete
  8. Daryl Ferreras4:48 PM

    (sorry my last posts had typos in it)
    Here's my quick and easy proof...
    Givens:
    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)
    QED.

    ReplyDelete