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