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

61–70 of 94 posts

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

#61

Post by mannerheim »

thehappypm wrote: post #56
johnnny wrote: post #48

Earlier quoted context omitted.

I'll repeat myself: it's very obvious in context that they meant the positive solution of xˆ2 = 2. My definition of the square root is as follows: the square root of a positive real number x is the positive number, noted √x, such that (√x) ^ 2 = x. To make this a useable definition, we need to prove that equation has a solution (using the fact the function t -> t^2 is zero for t=0, diverges to +inf when t -> +inf, an…

The most satisfying answer I have for the nature of the square root is to consider complex numbers. For an arbitrary complex number, a + bi, we can plot this as a vector on a two axis scale (x axis real and y axis imaginary). We can also convert any complex number to the form z = r e^(i θ). In other words, draw the complex number vector as an angle and a magnitude, in polar form. So any number can be drawn as a vecto…

The radical symbol always refers to a single-valued function by convention.

x^(1/n) is used for multi-valued functions in complex analysis, not the 'n-radical' symbol, which would usually refer to the principal root.

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

#62

Post by simiones »

thehappypm wrote: post #56
johnnny wrote: post #48

Earlier quoted context omitted.

I'll repeat myself: it's very obvious in context that they meant the positive solution of xˆ2 = 2. My definition of the square root is as follows: the square root of a positive real number x is the positive number, noted √x, such that (√x) ^ 2 = x. To make this a useable definition, we need to prove that equation has a solution (using the fact the function t -> t^2 is zero for t=0, diverges to +inf when t -> +inf, an…

The most satisfying answer I have for the nature of the square root is to consider complex numbers. For an arbitrary complex number, a + bi, we can plot this as a vector on a two axis scale (x axis real and y axis imaginary). We can also convert any complex number to the form z = r e^(i θ). In other words, draw the complex number vector as an angle and a magnitude, in polar form. So any number can be drawn as a vecto…

The initial definition of a square root of a number X (from where the name actually comes from) is "the length of the sides of a square whose area is X". There are some straightedge and compass constructions for this even in Euclid's Elements. That's why the square root is always a positive number; bringing in complex numbers only serves to confuse the issue, and is anachronistic.

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

#64

Post by thehappypm »

simiones wrote: post #62
thehappypm wrote: post #56

Earlier quoted context omitted.

The most satisfying answer I have for the nature of the square root is to consider complex numbers. For an arbitrary complex number, a + bi, we can plot this as a vector on a two axis scale (x axis real and y axis imaginary). We can also convert any complex number to the form z = r e^(i θ). In other words, draw the complex number vector as an angle and a magnitude, in polar form. So any number can be drawn as a vecto…

The initial definition of a square root of a number X (from where the name actually comes from) is "the length of the sides of a square whose area is X". There are some straightedge and compass constructions for this even in Euclid's Elements. That's why the square root is always a positive number; bringing in complex numbers only serves to confuse the issue, and is anachronistic.

Um, I don’t really think that’s right.

using the square root to convert area to perimeter, for example, is an application of square roots, one where the negative root is kinda useless. That’s not the definition of the operation. The definition of the operation is the solution to y = xx. And sure for many applications the negative root is useless, but you can’t argue against that both -2 -2 and 2*2 = 4.

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

#65

Post by simiones »

thehappypm wrote: post #64
simiones wrote: post #62

Earlier quoted context omitted.

The initial definition of a square root of a number X (from where the name actually comes from) is "the length of the sides of a square whose area is X". There are some straightedge and compass constructions for this even in Euclid's Elements. That's why the square root is always a positive number; bringing in complex numbers only serves to confuse the issue, and is anachronistic.

Um, I don’t really think that’s right. using the square root to convert area to perimeter, for example, is an application of square roots, one where the negative root is kinda useless. That’s not the definition of the operation. The definition of the operation is the solution to y = x x. And sure for many applications the negative root is useless, but you can’t argue against that both -2 -2 and 2*2 = 4.

You may not think I'm right, but that is the actual history. This operation was invented at a time where geometry was the main way mathematics was done. The square root is a much older concept than negative numbers (edit: at least in the Hellenistic world; Chinese and Indian mathematics may have had different histories).

So, by definition, the square root of 4 is +2. x * x = 4 has two solutions, which we dub +sqrt(2) and -sqrt(2).

Edit: to discuss just how much older, the concept of a square root appears in Euclid's Elements, c. 300 BC; on the other hand, Diophantus, in Arithmetica, c. 280 AD, was claiming that the equation 4x + 20 = 4 doesn't have any solutions/is absurd. So, the square root is more than 600 years older than negative numbers in the Hellenistic tradition.

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

#66

Post by henrydark »

phkahler wrote: post #38
gunnihinn wrote: post #13

Earlier quoted context omitted.

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

Actually he did use set theory, but there wasn't enough space in the margins

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

#67

Post by bombcar »

phkahler wrote: post #38
gunnihinn wrote: post #13

Earlier quoted context omitted.

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

There's a large body of math that can be proved simply, or proved complexly using set theory ;)

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

#68

Post by mananaysiempre »

ummonk wrote: post #16
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.

This is similar to the proof of the fundamental theorem of arithmetic (from which the irrationality of the square root of 2 trivially follows): https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithme...

This sort of contradiction by infinite descent is not uncommon: e.g. the textbook proofs of Fermat’s last theorem for n = 3 and 4, or the proof that a periodic crystal lattice can only have symmetry axes of order {1,2,3,4,6}.

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

#69

Post by mannerheim »

simiones wrote: post #65
thehappypm wrote: post #64

Earlier quoted context omitted.

Um, I don’t really think that’s right. using the square root to convert area to perimeter, for example, is an application of square roots, one where the negative root is kinda useless. That’s not the definition of the operation. The definition of the operation is the solution to y = x x. And sure for many applications the negative root is useless, but you can’t argue against that both -2 -2 and 2*2 = 4.

You may not think I'm right, but that is the actual history. This operation was invented at a time where geometry was the main way mathematics was done. The square root is a much older concept than negative numbers (edit: at least in the Hellenistic world; Chinese and Indian mathematics may have had different histories). So, by definition, the square root of 4 is +2. x * x = 4 has two solutions, which we dub +sqrt(2)…

The negative root is also a square root, but it isn't the root denoted by the radical symbol.

But anyway, when talking about THE nth root, we're almost always talking about the principal root.

https://news.ycombinator.com/item?id=34441863

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

#70

Post by jameshart »

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.

I don’t think you can make assumptions about how factors combine on multiplication (ie that multiplying by two adds one factor of two) in a context where integers can have rational noninteger roots.

If we can have x=(a/b)^2 and y=(b/c)^2, then xy=(a/c)^2 so any factors of b^2 have somehow dropped out, rather than being added in to the factors of the product.

Obviously in the end this all ends up contradicting the fundamental theorem of arithmetic, but it’s not clear this doesn’t wind up being circular.

Post reply on HN