I have never understood this proof either. What in my mind makes it very odd is that a very similar argument can sometimes be used to prove in some sense the exact opposite---that certain equations have solutions with denominators as big as you like. For example the proof in Cassels' "elliptic curves" book that x^3+y^3=9 has infinitely many rational solutions goes like this: "find one point (e.g. (2,1)). Now draw the tangent line through that point, compute the denominators of the new point and observe that they are bigger than those of the old curve. Hence doing this procedure infinitely often produces infinitely many points". You're doing the "new points from old" trick but this time the denominators are getting provably worse rather than provably better.

I have never understood this proof either. What in my mind makes it very odd is that a very similar argument can sometimes be used to prove in some sense the exact opposite---that certain equations have solutions with denominators as big as you like. For example the proof in Cassels' "elliptic curves" book that x^3+y^3=9 has infinitely many rational solutions goes like this: "find one point (e.g. (2,1)). Now draw the line tangent to the curve through that point, giving a new point (the 3rd point of intersection of the line and the curve), compute the denominators of the new point and observe that they are bigger than those of the old curve. Hence doing this procedure infinitely often produces infinitely many points". You're doing the "new points from old" trick but this time the denominators are getting provably worse rather than provably better.