Euclid's Proof that √2 is Irrational | Hacker News Reader

Euclid's Proof that √2 is Irrational

mathsisfun.com

172 pointsthunderbong93 comments

For those who are interested in connections to more advanced mathematics, there is a sense in which √2 is still an integer, even though it is irrational. Specifically there is the notion of “algebraic integers”, which are the set of all complex numbers expressible as the root of a monic polynomial:

  x^n + a_{n-1}x^(n-1) + … + a_1x + a_0.

Here each a_i is a usual integer in ℤ, and monic refers to the leading coefficient being equal to 1.

It turns out the set of such roots is actually closed under multiplication, addition, and subtraction, and there is even an analogue of prime factorization if you squint. Moreover, the intersection of these “algebraic integers” and the rational numbers ℚ are exactly the usual integers ℤ. This is why you sometimes might hear an algebraic number theorist refer to ℤ as the set of “rational integers”.

Maths is always a bit boggling. You say that root two can be considered an integer despite being irrational.

What does "usual integer" mean?

By “usual integer”, I mean what people usually refer to as an integer:

  …, -2, -1, 0, 1, 2, …

As opposed to “algebraic integer”, which is a more general notion.

If I wasn't familiar with that concept already, then I would probably assume that math is no more rigorous than psychology after encountering this thread.

The exact disciplines are doing themselves a terrible disservice by muddying up established terminology like this (and "algebraic integers" are far from the only such case).

The red herring principle[1] is unfortunately popular enough in mathematical terminology to have a name and a page about it.

Roughly, a fooish bar will frequently be something like a bar except fooish, so not actually a bar. (Algebraic integer, multivalued function, manifold with boundary, etc.) On the other hand, a nonfooish baz when baz is normally fooish often means a not necessarily fooish baz, so a particular one might be fooish but we can’t assume that. (Noncommutative ring, nonassociative algebra, the very field of noncommutative geometry, etc.)

[1] https://ncatlab.org/nlab/show/red+herring+principle

Ah yes, good ol' clopen sets.

> The exact disciplines are doing themselves a terrible disservice by muddying up established terminology like this

So, what term do propose they use for this? “Hutyfreklop” or “gensym_167336871904” would probably be unique, but wouldn’t tell anything about the subject itself, “roots of polynomials with integer coefficients and a leading coefficient of one” would get cumbersome soon.

Yeah, you might as well call any countable set "integers" because you can find a 1:1 mapping between them. This is silly.

I don't think that's fair.

Mathematicians pretty reliably say "algebraic integer" or "integer in [some specific class of numbers that has non-rational integers in it]" when they are talking about the broader notion, and if they're doing something where that broader notion is often relevant they will generally say something like "rational integer" when they mean the narrower notion. So in practice there is seldom any confusion.

And algebraic integers really _are_ like ordinary integers in important ways. Inventing a completely new term would not obviously be an improvement.

It's not like this sort of thing is unique to mathematics. Once upon a time a "language" was a thing human beings used to communicate with one another. Then along came "programming languages" which are not languages in that sense. And then things like "hypertext markup language" which isn't a language in the programming sense either.

(Arguably this is partly mathematicians' fault since I think they were the first to use "language" to refer to purely formal constructs. But I think the use of "language" in computing arose mostly by analogy to human languages.)

And it happens plenty outside "the exact disciplines". A republican is someone who favours a mode of government that doesn't have monarchs, but if you call someone a "Republican" in the US you mean something rather more specific and a few "Republicans" would actually quite like a system hard to distinguish from monarchy. A window is a transparent thing placed in a wall to let light in, but a window of opportunity is something quite different. A czar is the absolute ruler of Russia, but when someone says (rightly or wrongly) that Kamala Harris was "border czar" they don't mean that. A star is a gigantic ball of stuff undergoing nuclear fusion and producing unimaginable amounts of energy, but even the most impressive rock stars don't do that, and some people called "rock stars" have never played or sung a note of rock music in their lives.

Terminology is often times used to encapsulate a lot of information in a single word or phrase. It’s sort of a compression of information to facilitate communication. Things like “roots of f” is a shorter way to say that: “the set of all x such that f(x) = 0”. As you get deeper into a subject the more terminology you encounter. This is why research papers are generally unintelligible to those with no training in the areas that the research is about. To not use terminology would make papers insanely long and far too tedious to read.

This seems a bit harsh. Mathematicians tend to be mostly unambiguous when they write. This isn't even on the same planet as the empirical disciplines.

Mathematicians (with books in hand) tend to have the ability to disambiguate when confusion arises. But they rarely do, instead relying on context and the intelligence of the reader to derive meaning.

https://math.stackexchange.com/questions/778004/why-study-in...

There's a good explanation of the motivation for this concept, here.

Perhaps a translation issue?

I've always referred to that set as "algebraic numbers" ( https://en.wikipedia.org/wiki/Algebraic_number ). Since they are equipotent with integers, you _can_ call them that, but it's misleading.

In general, won't some algebraic numbers' minimal polynomials have a leading coefficient greater than 1, when written with integer coefficients?

As already mentioned by another poster, algebraic numbers are more general than algebraic integers, because the leading coefficient of the polynomial does not have to be one, similarly to the difference between rational numbers and integer numbers, where for the former the denominator does not have to be one, like for the latter.

Ahh, that would explain why the intersection of algebraic integers and Q is Z. I wasn’t convinced of that when I had the notion of algebraic numbers in place of algebraic integers.

I like teaching this kind of stuff to my grade 9 and 10 advanced math classes. It’s not that hard to understand and yet it gives students a sense of wonder about how math works. I might try to show the grade 10s algebraic integers now.

You sound like an amazing teacher :)

No, algebraic integers are a different set than algebraic numbers. (A subset.)

Algebraic integers are much cooler, since there is a number theory on them: https://en.wikipedia.org/wiki/Algebraic_integer . (And also because the most basic facts about it, like that it forms a ring, are not trivial to prove, that's a good sign for a concept to be cool and useful.)

These two number sets are more or less in a relationship like regular integers (with a number theory), and rational numbers. In fact A = O/Z where A denotes the set of algebraic numbers, O denotes the set of algebraic integers, and Z denotes the set of integers.

Yes, but did God make the algebraic integers? Because this looks suspiciously like the work of man.

This depends on your philosophy of mathematics. If you believe god gave us the nonnegative integers then in a very natural way one is led to the notion of algebraic integers. Whether this would be god’s creation or man’s creation depends on your view of who gets the credit in such a situation.

I think next time I’d better make the apologies to Kronecker explicit.

Sorry. I missed it. It was too clever for me!

> the set of such roots is actually closed under multiplication, addition, and subtraction, and there is even an analogue of prime factorization if you squint

I did a maths undergrad, but I don’t think I ever studied algebraic integers. That’s something I shall have to remedy now, thanks!

If you took abstract algebra (which presumably you did as a math major), you certainly encountered these at least in the exercises as groups of the form ax + b where x is some irrational number (or imaginary) and a and b are integers are a staple of chapter 1–2 proofs. Gaussian integers (ai + b) are a special case that are loads of fun to play with it. They are not unique factorization domains like the integers (e.g., 5 can be expressed as both 1∙5 and (1 - 2i)² where 1, 5 and 1 - 2i are all irreducible).

You are right, of course. Clearly, I have been away from mathematics too long.

Nit: while it is not generally the case that rings of algebraic integers must be unique factorization domains, it is the case for Gaussian integers! In your example, 5 is uniquely factorizable up to units as (1-2i)(1+2i).

Indeed, the integers have the same limitation -- factorization is unique only up to units. 1 = -1 * -1

In elementary mathematics, people wave away "-1" by saying silly things like "positive integers", before Gaussian integers arrive and force us to figure out precisely what we are trying to say without silly ideas from analysis like "ordering". :-)

These days I much prefer a different proof of this fact, attributed to Conway: https://www.youtube.com/watch?v=wNOtOPjaLZs -- I'm actually about half-way through teaching it to my kids right now!

I hadn't seen this before, it's fantastic! Thanks!

The cool thing is this argument immediately generalizes to zeroes of monic polynomials with integer coefficients, i.e. x^n + a_0 x^{n-1} + ... + a_n.

In commutative algebra one says "the ring Z is integrally closed in its field of fractions Q", or short "Z is normal".[1]

[1] https://en.wikipedia.org/wiki/Integrally_closed_domain#Norma...

We can also assume that the p/q=√2 is already the simplest form of the fraction, since every fraction must have one, as in the first section of the article.

Then if we figure out that both p and q are even, it means that p/q can be simplified (by dividing p and q by 2), which contradicts the assumption about the simplest form - and we don't need to use the infinite descent.

I was going to say this. The proof, unfortunately, sidelines into some very deep mathematics that it didn’t need to. I imagine but don’t know for sure that Euclid stopped where you do.

I’m not sure when infinite descent would be considered to have been formally proven to a modern mathematician but I bet it wasn’t in Euclid’s time!

Isn't the proof just claiming that you can't divide an integet infinitely many times by 2, and still expect it to be an integer?

I think the idea is that any strictly decreasing sequence of positive integers starting at N is a subsequence of (N, N-1, N-2, ..., 1) which has N elements, so any such sequence must have a finite number of elements.

So if you manage to produce an infinite sequence of strictly decreasing positive integers starting at a particular positive integer, then you've reached a contradiction.

Yes, I understand it intuitively, as would I think most non-suspicious people. It sounds very reasonable! As does the axiom of choice. We could even “prove” it using high school induction methods.

In practice though, concepts with infinity are very tricky, and the Greeks definitely did not have a strong accurate theory of infinity, Aleph-zero even, much less (as is the point talking about the sqrt(2)), the reals.

In this case, I think embedded in a high school proof would be the assumption that for any integer you can list there are not an infinite number smaller than them. This is manifestly true about the integers, but it is not true for the rationals, despite the two sets having the same cardinality, and a solid proof would need to be able to distinguish the reasons why. It’s this part that I think would be beyond the Greeks.

That assumes that every fraction has a unique simplest form. The first section of the article makes no such claims about the existence of a simplest form of fraction. The proof uses just algebraic manipulation, the fact that a sequence of strictly decreasing positive integers is finite in length, and the definition of a rational number (there exist integers p, q (q != 0) such that the number can be expressed as p/q).

The article explicitly claims

> Rational numbers or fractions must have a simplest form.

They make no claim about uniqueness, but that is not needed in the argument.

t0mek sais "the simplest form", but the comment is fixable by changing that to "a simplest form". (For example, if hypothetically a/b and c/d where somehow the same number, and yet somehow there is no x such that a/b = xc/xd, the argument about how 2 divides into a and b also applies to c and d.)

It's an interesting exercise to find the right generalization of this proof to sqrt(n) for arbitrary numbers n that are not perfect squares, and for kth roots for m >= 2. I.e. prove that if kth_rt(n) is rational, then n is a perfect kth power (or equivalently, that if n is not a perfect kth power, then kth_rt(n) is irrational).

(I'm talking about adapting the ideas of this divisibility-based proof. abstractbill's post https://news.ycombinator.com/item?id=41314547 about Conway's method, https://www.youtube.com/watch?v=wNOtOPjaLZs, is a completely different (and very cool) way to do this that I hadn't seen before today.)

I remember being extremely struck by how general this proof was. In fact it made me suspicious that it would even apply to perfect squares. Running the proof on the square root of 4 took a little while to sink in.

(Important thing to do while understanding any theorem! Test the boundaries, discover what happens when you relax every hypothesis.)

I thought this was basically the same proof that got someone killed in the Pythagorean cult. https://www.scientificamerican.com/article/how-a-secret-soci... shows it was a different proof in a similar vein, though. Fun times.

Another version of the same story:

https://existentialcomics.com/comic/189

If you know a child in middle school, this is a great way to get them started on "cool mathematical thinking", which I called "Mathematia" when I discussed with my son when he was young (to distinguish from the horrible Math being taught in school):

  1. Introduce ℤ & ℚ - this is easy. Perhaps, fingers and slices of pizza. Now s/he's ready to be as surprised as the members of the Phythagorean cult

  2. Go over the classical proof for √2 given here. We now have a number that's not in ℤ or ℚ!

  3. It's one thing to show a result, a very different thing to *grasp* it. Why is (2) a big deal? It smashes the simple notion Greeks had that *any* two lengths (rational numbers) are commensurable, which is a perfectly simple and obvious (and wrong) thing to believe: "Have one stick for one side of a square and another for the diagonal. You cannot cut both sticks into pieces of the same length, no matter what length you choose." *This is amazing*

  4. We only discovered one such weird number. Are there others? Motivated by the above, how about checking √3. Show that it's weird, too.

  5. √4 is just 2. How about √5? OMG, that's weird, too.

  6. So the square root of an integer is either an integer or one of these weird numbers. It cannot be of the general ℚ form p/q. This is an interesting proof. (While thinking about that with the youngster you can think about another generalization: roots higher than second. Turns out it's true for those, too: https://math.stackexchange.com/questions/4467/how-to-prove-if-a-b-in-mathbb-n-then-a1-b-is-an-integer-or-an-irratio

  7. How do we work these weird numbers? For example, can we add them up, e.g. √2 + √3? How do we do that? Is that another weird number or could it ever be an integer? Some facts about these sums are trivial to prove: https://math.stackexchange.com/questions/157245/is-the-sum-and-difference-of-two-irrationals-always-irrational

  8. Using the wacky notion of adding two numbers as "mating" you can generally outline some higher algebra concepts, e.g. if a lion mates with a lion the result is always a lion. What if it mates with a tiger? (depends, liger or tigon). Can we think of adding a ℚ to one of these weird numbers the same way? Such intuitions may be misleading (remember the Greeks?) but are fun.

Couldn’t you stop the proof at the statement q^2 must equal 2m^2 since it’s obvious there’s no solutions to q^2 = 2m^2.

To explain why it’s obvious, squares always have an even number if factors of two (an even multiple of any prime factor since it’s a square but just focus in on 2 here for now).

A square times two always has an odd number of factors of 2 since it’s the above (an even number of factors of two) plus one more factor.

An odd number of prime factors on one side can’t be equal to an even number of factors on the other side. q^2 can never equal 2m^2 for any integer value of a or m. Therefore it’s irrational.

This ends the proof much earlier right?

Yep, that does work, although it needs a bunch of extra machinery (the fundamental theorem of arithmetic, which guarantees existence and uniqueness of prime factorisation). If you're happy to take that machinery as having already been proved - it's not entirely trivial, and it's definitely not obvious! - then you can indeed stop there.

Why do I claim that it's not obvious? Consider the ring of integers with sqrt(-5): that is, all complex numbers of the form `a + b sqrt(-5)` with a, b integers. This is a ring - it has all the nice additive and multiplicative properties that the integers do - but it doesn't have unique factorisation, because 6 has two distinct factorisations.

That’s reasonable. I’ve been taught unique prime factorization is a thing since primary school but never considered the history behind that knowledge. I feel anyone with that basis could reasonably stop at the third line here. In fact they could quickly create a generalization since a^2 could clearly never equal b(c^2) unless b was also a square for integer a and c but that obviousness is based on a lot of other knowledge.

> To explain why it’s obvious

Have you considered a career in mathematics?

This proof has almost nothing to do with Euclid. The Pythagoreans knew about it more than a century before his birth (Hippasus was apocryphally killed for divulging this proof), and the proof is widely believed to have only been inserted into Elements by others after Euclid's death.

Yeah, this can't be done in the geometrical way Euclid worked

Mostly because you need the Archimedean property for it which can not be derived from Euclid's axioms.

> Likewise if a number is even and is a square of an integer, then its square root must be even.

The proof would be more compelling if this was proven instead of being taken as an obvious fact.

It is really trivial though.

Even x Even results Even

Even x Odd irrelevant if squaring

Odd x Odd results Odd

except sqrt(2) x sqrt(2) is even ( i know we're talking about numbers in Z in this case, and sqrt(2) definitely isn't in Z, but still)

Which made me wonder if the original sentence isn't already assuming something about sqrt(2) and even/odd properties.

(i stopped at the same step as OP wondering if this is as trivial as it seemed)

>Odd x Odd results Odd

This isn't obvious and can't be taken for granted. The explanation posted above (2k+1)^2 by Smaug123 explains this part.

Let n = 2r, and n = xx for some integers r and x, because n is even and n is a square. So xx = 2r.

Because of the fundamental theorem of arithmetic, we know that x must be representable as the product of a unique string of prime numbers.

Because 2 is prime, then since xx = 2r, there must be a 2 in the string of primes for xx.

But since 2 is prime, it must be in x as well, because a prime cannot come out of nowhere. In other words, if there is a given prime P in xx, there must be at least two P in xx, because there was at least one in x, and the number of each one got doubled in xx.

Therefore xx = 2r = 2*2*y = 4y for some integer y.

Therefore n = 4y and sqrt(n) = sqrt(4y) = sqrt(4)sqrt(y) = 2sqrt(y) which is an even number.

Therefore sqrt(n) is even.

FTA is massive overkill. For every number n, either n can be expressed as 2k for some k, or 2k+1 for some k, but not both (proof: by induction); in particular the square root can too. If the square root is (2k+1), then the square is 4k^2 + 4k + 1 = 2(2k^2+2k) + 1, which is by definition odd, not even as we supposed.

True, but the FTA proof is just really intuitive for me and I like it.

Thanks for the proof, it was fun to follow, and I agree that it's quite intuitive.

I think that it would be helpful to mention why sqrt(y) must be an integer.

(I know that it is, but it also feels a bit glossed over, given that all the other steps of the proof were explained so thoroughly.)

The FTA proof is the one that's obvious, though. If it's really easy to do something using a basic tool, why worry that the basic tool is complex to describe?

Where in Euclid's Elements does this proof appear? I can't seem to find it.

Euclid X prop 9. http://aleph0.clarku.edu/~djoyce/java/elements/bookX/propX9....

(300 BCE)

slightly related but mathsisfun is a goated website. one of the all time greats. myself and many other people only got through maths because of this site.

1) it's not a proof by contradiction, it's a proof of a negation :grump:

2) I am not a fan of this phrasing "we can't simplify forever". Why can't we? It's obvious if you phrase it in the usual way as "the denominator is strictly smaller than it was before", but the "simplify" operation is kind of complex! They don't even mention "decreasing" until the very final Note box where they say offhand that actually it's an infinite descent (which is a critical part of the proof they've otherwise handwaved).

> 1) it's not a proof by contradiction, it's a proof of a negation :grump:

I don't get your complaint. It is a proof of a negation, yes, the conclusion is that √2 ∉ ℚ.

But the proof is done by contradiction; "it's not a proof by contradiction" is flat-out false. "Proof by contradiction" describes the method of the proof, and "proof of a negation" describes its conclusion, which is why one of those phrases uses by and the other one uses of.

https://en.wikipedia.org/wiki/Proof_by_contradiction, https://ncatlab.org/nlab/show/proof+by+contradiction, https://web.stanford.edu/class/cs103/guide_to_proofs#proof-b... all agree (the first three things that came up when I googled for "proof by contradiction"): a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true. There is already a perfectly cromulent term for proofs of negations: "refutation by contradiction" (https://ncatlab.org/nlab/show/refutation+by+contradiction), which admittedly nlab says it prefers to its other name "proof of negation".

The two seem isomorphic. Just sub R for \not P. Doesn't seem to change anything interesting about the proof structure.

As I said, according to the three sources above, which are the first sources I clicked on which didn't seem like blogspam, the phrase "proof by contradiction" is a term of art which means "uses the law of excluded middle to conclude the truth of a statement given a proof that its negation is false". It may be unfortunate that the mathematical world has standardised on the phrase "proof by contradiction" for this, but it has standardised on that phrase!

> but it has standardised on that phrase!

To me, the only formal distinction you can make between the two lies in the use of the excluded middle. However, this distinction has not standardised in mathematics, as many mathematicians simply do not care for intuitionistic logic.

Such a mathematician could see the above proof as: I want to show ¬P by contradiction. Therefore I assume ¬(¬P) which is just P to me (the unintuitionistic mathematician has just used the excluded middle, without really caring). I derive a contradiction. Therefore ¬P holds.

While I personally enjoy the kind of subtleties that can be thought of about mathematical reasoning, I also think the rant-train on contradiction vs negation must stop. You are expecting a consensus from the wrong community.

> To me, the only formal distinction you can make between the two lies in the use of the excluded middle.

It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all.

Could you please explain this? Clearly we both understand something completely different by either the term "excluded middle" or "contradiction". Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.

>>>> As I said, according to the three sources above, which are the first sources I clicked on which didn't seem like blogspam, the phrase "proof by contradiction" is a term of art which means "uses the law of excluded middle to conclude the truth of a statement given a proof that its negation is false"

(quote from you; my emphasis)

In that case your "It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all." is simply false: you can use contradiction to refute a proposition without proving that proposition, without using LEM.

excluded middle: the logical axiom that, for any proposition P, (P v ¬P) is a tautology/valid/always holds.

contradiction: a proof of ⊥. The definition of ⊥ does not matter (it just means false), thanks to the ex falso quodlibet principle.

A proof by contradiction: proving P by showing that (¬P -> ⊥).

Notice that I haven't defined the ¬ operator. This is due to the fact that its definition differs between classical logic and intuitionistic logic. Since the intuitionistic definition of ¬, i.e. "¬P" is a short-hand for "P -> ⊥", is classically equivalent to the definition of ¬ in the classical context (¬P is the statement "P does not hold"), it makes sense to adopt this definition. The astute reader will notice that, with this definition of ¬, a proof by contradiction is exactly a proof of ¬¬P, and it happens that ¬¬P -> P is an equivalent formulation of the excluded middle.

Now, back to Euclid's proof. Let P = "√2 is rational". We want to show Q = ¬P. We can do so by contradiction: assume ¬Q, and derive a contradiction. It *happens* that, when using the scheme of proof by contradiction on a property of the form ¬A, you can simply rearrange the negations to get rid of the use of the excluded middle.

So, going back to your statement,

>Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.

Well, whether Euclid's proof is intuitionistically valid is a question of point of view. Historically? I doubt it. I doubt that Euclid gave any kind of thought to whether he used the excluded middle, and probably used it pervasively, as all "classical" mathematicians today. However, I agree that it can be made intuitionistically valid using a purely syntactic rewriting. Said differently, Euclid's proof does not rely on the excluded middle. This does not mean you cannot use it because that's how you think or because you prefer it that way. When you see the blow-up of sizes of certain proofs in the non-classical context, you understand why many mathematicians would rather not give a thought to their use of the excluded middle. The same way many people in this thread used the PTA to show that √2 is irrational: that's overkill, but they prefer it that way !

Sure, I agree with everything you've said; I was sloppy in saying "Euclid's proof" (whose baroque language I haven't actually bothered to wade through) when I meant "the proof in the OP", though I was precise in saying "it can't use LEM" where you've interpreted it as "a mathematician can't use LEM".

(I asked for an explanation because I resented being called "dumb" by someone I'm pretty sure doesn't actually understand the distinction I'm talking about.)

> a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true.

And this proof matches that description exactly, with P = "√2 ∉ ℚ". The only case where these would be different ideas is the case where ¬¬P ≠ P.

And of course, that can never happen.

Your statement is, I think, being wilfully sloppy.

To quote the outline of the proof: "First Euclid assumed √2 was a rational number.". To quote the proof itself: "Euclid's proof starts with the assumption that √2 is equal to a rational number p/q.". In two different places, the proof explicitly states that it is showing that "√2 in ℚ" is false. It is not showing that "√2 ∉ ℚ" is not false; such a proof would begin "Suppose that it were not the case that √2 ∉ ℚ", which is obviously not how the proof starts (and for good reason, because that would be much more confusing).

By all means argue that "nobody cares about excluded middle"! You're probably right, and when I insist that "proof by contradiction" has a meaning that is correctly stated by Wikipedia and the nlab, I'm just like one of the old fogeys complaining about things like "could care less" or "irregardless"! But don't misquote arguments and say that they support your case when they don't.

It's both a proof by contradiction and a refutation by contradiction because it's the same thing in this context. Positing "P = is rational and ¬P = is irrational" is as valid as positing "P = is irrational and ¬P = is rational".

No, "is not irrational" isn't the same as "is rational" without excluded middle; that's the whole point. (Equality of real numbers is not computable, so there is nonconstructive content to the implication "if not irrational, then rational".)

(I will retract a whole bunch of my worldview if you can inhabit the type "not-not-rational -> rational" in something like MLTT.)

You take a set S and partition it into two subsets, A and B, so that each element uniquely belongs to either of them. For each element of S it is true that "not-not-in-A -> in-A". Can this be shown to be true in MLTT? I don't know much about setoids to show it, but if it can't, that's the problem of MLTT, not mine. In the context of this proof, it is true.

This distinction is only made by a small number of mostly constructivists. It is not common usage, and most working mathematicians will have no idea what you're talking about.

> They don't even mention "decreasing" until the very final Note box where they say offhand that actually it's an infinite descent (which is a critical part of the proof they've otherwise handwaved).

That isn't actually a critical part of the proof; you can just assume that your initial two integers are relatively prime and then derive a contradiction directly.

Then why didn't they! Of course the proof can be fixed, we all know sqrt(2) is irrational, but why get so close to proving it and then just not finish the job?

It would be nice if they described Euclid's argument in its original geometric form rather than converting it back to post 1700 algebra notation.

And then in 1737 Euler (another name starting with Eu, definitely a good name) showed that the constant e is irrational.

His proof exploited the fact that the continued fraction representation of any rational number terminates. The CF representation for e does not.

> Eu, definitely a good name

I see what you did there.

The worst non-Euclidean geometries should be called Dysclidean. I think Lovecraft missed an opportunity here.

I really liked the explanation. It’s a proof I could actually follow. Kudos to the author and to thunderbong for posting it!

   that feeling you get when you realize the person who lived ~2300 years before you is smarter than you now...

I wish I was taught math like this when I was younger. So much time lost thinking I didn’t like math.

tldr version: The numerator must be even and the denominator must be odd. The square of this taken modulo 4 must therefore have numerator = 0 mod 4, denominator = 1 mod 4 (1x1 and -1x-1 both become 1 mod 4). 2 times 1 mod 4 cannot be 0 mod 4. Therefore sqrt(2) cannot be rational.

Reply on news.ycombinator.com