Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalising a new proof that the square root of two is irrational

lawrencecpaulson.github.io

Post reply on HN
Print view View original

31–40 of 94 posts

Re: Formalising a new proof that the square root of two is irrational

#31

Post by pfortuny »

xurukefi wrote: post #23
tromp wrote: post #9

The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.

That's an interesting proof, because I can easily follow it mechanically, but I have absolute no intuition for it.

The minimum k is the denominator of the supposed irreducible fraction p/q=sqrt(2). He is stating that then there is a different irreducible fraction r/s=sqrt(2). This is because you would have

p^2=2q^2

with p and q mutually prime, which is impossible.

Instead of irreducible fractions with coprime numbers, he is doing the “dual” using the minimum possible value of the denominator.

Re: Formalising a new proof that the square root of two is irrational

#32

Post by rhn_mk1 »

thaumasiotes wrote: post #27
rhn_mk1 wrote: post #24

Earlier quoted context omitted.

Thanks, this is actually a much better description, especially 4. OP's description can be used to "prove" that 1/2 is irrational.

> OP's description can be used to "prove" that 1/2 is irrational. That won't work; in that case, k' will not be a positive number (k/2 - k is negative whenever k is positive), so you'll fail to produce a contradiction.

Fair enough. Take 3/2 in that case.

Re: Formalising a new proof that the square root of two is irrational

#33

Post by [deleted] »

scotty79 wrote: post #29
tromp wrote: post #9

The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.

[deleted]

[deleted]

Re: Formalising a new proof that the square root of two is irrational

#34

Post by hgsgm »

rhn_mk1 wrote: post #32
thaumasiotes wrote: post #27

Earlier quoted context omitted.

> OP's description can be used to "prove" that 1/2 is irrational. That won't work; in that case, k' will not be a positive number (k/2 - k is negative whenever k is positive), so you'll fail to produce a contradiction.

Fair enough. Take 3/2 in that case.

Doesn't work, because in

    k * (3/2 - 1)(3/2) = k'(9/4) - k(3/2)
(3/2)^2 = 9/4 is not an integer, you don't get k' You'd only get an integer if 4 divides k', which doesn't happen, because

    k = 2
and

    k' = k(3/2 -1) = k/2 = 1

Re: Formalising a new proof that the square root of two is irrational

#35

Post by hgsgm »

tromp wrote: post #20
graycat wrote: post #18

Let's have a simple proof so that we don't have to argue about more complicate issues: For integers p, q with q not 0, suppose 2 = (p/q)^2 Then 2 q^2 = p^2 and the left size has an odd number of factors of 2 and the right side has an even number of factors of 2, a contradiction. Therefore such p, q do not exist, and 2 does not have a rational square root. Done.

It is simple if you can assume unique factorization of positive integers [1]. [1] https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithme...

Which is proven in a similar way as OP's proof.

Re: Formalising a new proof that the square root of two is irrational

#36

Post by rhn_mk1 »

hgsgm wrote: post #34
rhn_mk1 wrote: post #32

Earlier quoted context omitted.

Fair enough. Take 3/2 in that case.

Doesn't work, because in k * (3/2 - 1)(3/2) = k'(9/4) - k(3/2) (3/2)^2 = 9/4 is not an integer, you don't get k' You'd only get an integer if 4 divides k', which doesn't happen, because k = 2 and k' = k(3/2 -1) = k/2 = 1

Thanks, you're right. I missed that there was supposed to be a √2*√2 in the expansion of the last line.

Re: Formalising a new proof that the square root of two is irrational

#37

Post by phkahler »

tromp wrote: post #9

The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.

Love a proof by infinite descent! But you do make the assumption that (√2 - 1) is positive and less than 1. Root 2 can be negative.

Re: Formalising a new proof that the square root of two is irrational

#38

Post by phkahler »

gunnihinn wrote: post #13
tromp wrote: post #9

The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.

As the post points out this involves some claims about infinite sets that are maybe not super obvious to laypeople (every infinite set of natural numbers has a least element). But we can rephrase this to avoid mentioning sets: For any rational number p/q (with q > 0) there exists a smallest positive natural number k such that k * p/q is natural: Clearly q works, so we check the finitely many numbers 1, ..., q and pic…

Fermat did several proofs by infinite descent without bringing set theory into it ;-)

Re: Formalising a new proof that the square root of two is irrational

#39

Post by phkahler »

thaumasiotes wrote: post #17
technion wrote: post #14

Earlier quoted context omitted.

What am I missing about why this couldn't also argue sqrt(4) is irrational?

The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1. (This is necessary when we conclude that k(√2 - 1) is less than k.) The same is not true of √4 - 1. If you look at my more explicit proof sidethread, the problem occurs in line L1, where instead of going from "√2 < 2" to "√2 - 1 < 1", you'd go from "√4 < 4" to "√4 - 1 < 3" and then you'd be stuck. (My proof won't even…

>> The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1.

Doesn't it also rely on √2 being positive?

Re: Formalising a new proof that the square root of two is irrational

#40

Post by estomagordo »

phkahler wrote: post #39
thaumasiotes wrote: post #17

Earlier quoted context omitted.

The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1. (This is necessary when we conclude that k(√2 - 1) is less than k.) The same is not true of √4 - 1. If you look at my more explicit proof sidethread, the problem occurs in line L1, where instead of going from "√2 < 2" to "√2 - 1 < 1", you'd go from "√4 < 4" to "√4 - 1 < 3" and then you'd be stuck. (My proof won't even…

>> The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1. Doesn't it also rely on √2 being positive?

Which it is, by definition?
Post reply on HN