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!

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.

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?

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