News for hackers. Stuff that matters.
Re:Formalising a new proof that the square root of two is ir... by tromp on Thursday January 19, 2023 @04:00AM (#34438188)
The new proof rephrased:

Let K be the set of positive integers k such that k * sqrt(2) is an integer.

Suppose K is non-empty, denote its minimum as k.

Consider the positive integer k' = k * sqrt(2) - k = k * (sqrt(2) - 1).

Then k' < k and k' is also in K since k' * sqrt(2) = k * 2 - k * sqrt(2).

Re:Formalising a new proof that the square root of two is ir... by gunnihinn on Thursday January 19, 2023 @04:38AM (#34438423)
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 pick the smallest.

Suppose the square root of 2 is rational. Let k be this smallest number for \sqrt 2, and proceed with the rest of the proof to find 0 < k' < k that also works.

Re:Formalising a new proof that the square root of two is ir... by phkahler on Thursday January 19, 2023 @09:20AM (#34440510)
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 ir... by henrydark on Thursday January 19, 2023 @11:48AM (#34442424)
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 ir... by bombcar on Thursday January 19, 2023 @11:48AM (#34442425)
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 ir... by zeroonetwothree on Thursday January 19, 2023 @10:46AM (#34441537)
You don’t have to pick the smallest, just start with q and then find you can keep decreasing it forever.
Re:Formalising a new proof that the square root of two is ir... by martopix on Thursday January 19, 2023 @04:03AM (#34438213)
... which contradicts the hypothesis that k is the minimum. Therefore, K is empty.
Re:Formalising a new proof that the square root of two is ir... by henning on Thursday January 19, 2023 @04:35AM (#34438403)
Good luck getting Internet people to actually explain a proof for mere mortals. The whole point is to omit as much as possible to make yourself look smart. Then you can say that it's "obvious" or it's "left as an exercise" or something dismissive rather than just adding a few extra words to explain.
Re:Formalising a new proof that the square root of two is ir... by jacobn on Thursday January 19, 2023 @10:34AM (#34441392)
For clarity: the proof hinges on (√2 - 1) < 1 (so that k’ < k) and √2 being a square root so that you can multiply k’ by it and indeed get 2 k - k √2.

This is why it also works for √3, but doesn’t work for √5 or 1.5

Re:Formalising a new proof that the square root of two is ir... by perihelions on Thursday January 19, 2023 @11:05AM (#34441783)
Right. It can also generalize for any non-integral square root of an integer √n. Let a be the integer ⌊√n⌋, such that a < √n < a+1 -- strict inequalities, because √n is non-integral. So 0 < √n - a < 1 and the same proof works with

    k' = √n k - a k         (instead of √2 k - 1 k)
       = k(√n - a)          (so 0 < k' < k)

    √n k' = n k - a k √n    (is integral; k' ∈ K)
Re:Formalising a new proof that the square root of two is ir... by n4r9 on Thursday January 19, 2023 @04:12AM (#34438263)
That's a lovely proof. It has the "proof by absurdity" feel of the classic Euclidean proof, but without as much fiddling about with even numbers.
Re:Formalising a new proof that the square root of two is ir... by technion on Thursday January 19, 2023 @04:51AM (#34438492)
What am I missing about why this couldn't also argue sqrt(4) is irrational?
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @04:59AM (#34438549)
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 work for √3, but it seems safe to say that the problem with √3 is correctable and the problem with √4 is not.)

Re:Formalising a new proof that the square root of two is ir... by phkahler on Thursday January 19, 2023 @09:22AM (#34440530)
>> 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 ir... by vlovich123 on Thursday January 19, 2023 @09:33AM (#34440661)
I’m very rusty but I think this proves the positive roots are irrational. If the positive roots are irrational then the negative ones would be too.
Re:Formalising a new proof that the square root of two is ir... by estomagordo on Thursday January 19, 2023 @09:32AM (#34440653)
Which it is, by definition?
Re:Formalising a new proof that the square root of two is ir... by thehappypm on Thursday January 19, 2023 @10:06AM (#34441055)
-1.4ish is another square root of 2
Re:Formalising a new proof that the square root of two is ir... by johnnny on Thursday January 19, 2023 @10:22AM (#34441236)
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, and is continuous between the two) and that solution is unique (using the fact the same function is strictly increasing).

Do you have any other definition of √x?

Re:Formalising a new proof that the square root of two is ir... by thehappypm on Thursday January 19, 2023 @10:55AM (#34441664)
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 vector onto the complex plane. Multiplying two vectors together causes the angles to add and the magnitude to multiply — creating a rotated and extended (or shrunken) new vector as the product.

So what’s the square root of a complex number z? It’s the vector a that, when multiplied by itself, winds up with z.

When z has no imaginary component, it lies flat on the x axis; its magnitude is z and the angle is 0. What’s its square root?

There are two. |a|e^(i 0) and |a|e^(i 180). 180 degrees multiplied together rotates the vector back to 0. And the e^(i 180), in radians, is e^(i pi), or negative one.

So putting it together: there are only two solutions, with the same magnitude, and different signs.

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

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

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

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.

Re:Formalising a new proof that the square root of two is ir... by mannerheim on Thursday January 19, 2023 @11:10AM (#34441863)
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 ir... by thehappypm on Thursday January 19, 2023 @01:32PM (#34443749)
Sure, but doesn’t that weaken the proof? It is an arbitrary restriction on the function that is required
Re:Formalising a new proof that the square root of two is ir... by mannerheim on Thursday January 19, 2023 @01:43PM (#34443885)
Barely? It proves it for the principal root, and you can trivially prove it for the negative root using the principal root's irrationality.
Re:Formalising a new proof that the square root of two is ir... by zeroonetwothree on Thursday January 19, 2023 @10:48AM (#34441569)
I can’t believe you are downvoted. In math sqrt is defined as the positive one. It seems HN readers need a refresher.
Re:Formalising a new proof that the square root of two is ir... by BeetleB on Thursday January 19, 2023 @12:25PM (#34442938)
Most people are taught that there are two values for the square root. It was only in later math courses (e.g. precalculus) that they reserved the square root symbol exclusively for the positive square root.
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @03:08PM (#34444959)
That is not what people are taught. If that were true, the numerator in the quadratic equation would be "-b + √(b² - 4ac)", not "-b ± √(b² - 4ac)".
Re:Formalising a new proof that the square root of two is ir... by BeetleB on Thursday January 19, 2023 @04:34PM (#34445931)
Your statement assumes the educational system values consistency, which is a clearly false assumption.
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @06:41PM (#34447245)
Textbooks aren't that bad. Here's what Pearson's Algebra 1 says when introducing the novel concept of the radical sign:

> The radical symbol √ indicates a nonnegative square root, also called a principal square root.

I quoted that one because it's available on libgen ( http://library.lol/main/BE522034F8D3680B248162CD2C35D455 , page 16), but obviously every basic algebra textbook covers this. The symbol is never discussed -- or used -- in any other terms than that it uniquely refers to a positive square root.

Re:Formalising a new proof that the square root of two is ir... by BeetleB on Thursday January 19, 2023 @07:58PM (#34447826)
Your evidence is consistent with my claims. Or rather: I never claimed there aren't textbooks that define it as the positive square root.
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Friday January 20, 2023 @02:46AM (#34450231)
All textbooks define it that way. There is no other definition available for that symbol.
Re:Formalising a new proof that the square root of two is ir... by mannykannot on Thursday January 19, 2023 @09:58AM (#34440969)
If I am not mistaken, the proof in the article works for √3, and your lemma 1 can be modified by noting that when x > 1, √x > 1 and also 1 < 3 < 4 so 1 < √3 < 2, 0 < √3 - 1 < 1, and k' = k(√3 - 1) < k.
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @04:54AM (#34438510)
There are some assumptions in there that you haven't made explicit. They're correct, but they make the proof feel a little "cheaper".

1. Let K be the set of positive integers {n: n√2 ∈ ℤ}

2. Supposing K is non-empty, denote its minimum as k.

3. Consider k' = k√2 - k = k(√2 - 1)

Lemma 1: k' < k

L1. When x > 1, √x < x. Therefore, √2 < 2, √2 - 1 < 1, and k' = k(√2 - 1) < k.

Lemma 2: k' is a positive integer

L2a: By hypothesis, k√2 ∈ ℤ.

L2b: By hypothesis, k is a positive integer.

L2c: The difference of any two integers is itself an integer, so k' ∈ ℤ.

L2d: When x > 1, √x > 1. Therefore, √2 > 1, k√2 > k, and so k' = k√2 - k > 0.

4. k'√2 = (k√2 - k)√2 = 2k - k√2 ∈ ℤ. Therefore, k' ∈ K.

5. This contradicts the assumption that k is the minimum element of K. Thus K must be empty.

To make this proof work, we needed some general information about the behavior of the square root function over the entire real domain. (Or, some special knowledge about the numerical value of √2, but from an elegance perspective that's even worse.) This is something you can easily get away with, but it's somewhat annoying. The proof based on "assume this rational number is represented in its simplest form, such that gcd(n,d) = 1" seems a little more self-contained.

Re:Formalising a new proof that the square root of two is ir... by rhn_mk1 on Thursday January 19, 2023 @06:42AM (#34439275)
Thanks, this is actually a much better description, especially 4. OP's description can be used to "prove" that 1/2 is irrational.
Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @07:45AM (#34439713)
> 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.

Re:Formalising a new proof that the square root of two is ir... by rhn_mk1 on Thursday January 19, 2023 @08:14AM (#34439915)
Fair enough. Take 3/2 in that case.
Re:Formalising a new proof that the square root of two is ir... by hgsgm on Thursday January 19, 2023 @08:39AM (#34440097)
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' < K so there is no contradiction.

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 ir... by rhn_mk1 on Thursday January 19, 2023 @09:03AM (#34440353)
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 ir... by ummonk on Thursday January 19, 2023 @04:57AM (#34438541)
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...
Re:Formalising a new proof that the square root of two is ir... by mananaysiempre on Thursday January 19, 2023 @11:59AM (#34442590)
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 ir... by xurukefi on Thursday January 19, 2023 @06:39AM (#34439252)
That's an interesting proof, because I can easily follow it mechanically, but I have absolute no intuition for it.
Re:Formalising a new proof that the square root of two is ir... by pfortuny on Thursday January 19, 2023 @08:09AM (#34439890)
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 ir... by scotty79 on Thursday January 19, 2023 @07:58AM (#34439816)
Let K be the set of positive integers k such that k * 3 is an integer.

Suppose K is non-empty, denote its minimum as k.

Consider the positive integer k' = k 3 - k = k (3 - 1).

Then k' < k (?!) and k' is also in K since k' 3 = 2 k - k 3, contradicting non-emptyness of K.

--

I guess my questions are why k' < k and why k'√2 is positive?

Re:Formalising a new proof that the square root of two is ir... by pfortuny on Thursday January 19, 2023 @08:04AM (#34439850)
Notice thay you know sqrt(2)<2 (this is easy), which does not happen in your case.
Re:Formalising a new proof that the square root of two is ir... by phkahler on Thursday January 19, 2023 @09:19AM (#34440498)
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 ir... by scotty79 on Thursday January 19, 2023 @09:37AM (#34440706)
I think we are basing it on what we know about root 2. That it's larger than one and less than 2.
Re:Formalising a new proof that the square root of two is ir... by DNied on Thursday January 19, 2023 @09:48AM (#34440844)
You forget that √x always has 2 solutions: 1 positive and 1 negative.
Re:Formalising a new proof that the square root of two is ir... by johnnny on Thursday January 19, 2023 @10:18AM (#34441195)
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, and is continuous between the two) and that solution is unique (using the fact the same function is strictly increasing).

Do you have any other definition of √x?

Re:Formalising a new proof that the square root of two is ir... by zeroonetwothree on Thursday January 19, 2023 @10:47AM (#34441553)
The sqrt symbol is defined as the positive root
Re:Formalising a new proof that the square root of two is ir... by syzarian on Thursday January 19, 2023 @12:43PM (#34443160)
The equation :

x^2 = a

where a is a positive real number has two solutions. An equation can have multiple solutions (even infinitely many solutions). Sqrt(x) is a function and as such it can have only one output for a given input. Functions don’t have solutions. By definition, sqrt(a) is the nonnegative solution of the equation x^2=a. Here, a can be zero.

Re:Formalising a new proof that the square root of two is ir... by Omin on Thursday January 19, 2023 @10:31AM (#34441349)
It's not an assumption, √x is defined to be the positive square root (the principal square root). The negative one is -√x.