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

Re:Formalising a new proof that the square root of two is ir... by simiones on Thursday January 19, 2023 @11:20AM (#34441993)

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.

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by thehappypm on Thursday January 19, 2023 @11:30AM (#34442135)

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.

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by simiones on Thursday January 19, 2023 @11:40AM (#34442269)

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

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

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by mannerheim on Thursday January 19, 2023 @12:01PM (#34442644)

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

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @02:37PM (#34444585)

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

The gap is much wider than that; double-entry bookkeeping speaks of "credit" and "debit" (defined to be exactly the same concept as positive and negative numbers) because negative numbers were still nearly unknown to Europeans in the 15th century.

[ Parent | on HN ]