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.

## 8 comments:

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

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.

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

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

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

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

Post a Comment