[someplaceguy]

I would argue that technically, the proof has an error because the author says:

> Let X be the integers Z; for integers a,b, let `a ⊏ b` be `a|<|b`; and let the property Φ(a) be “a^2=2 b^2 for some integer b” (formally, `∃b ∈ Z. a^2=2 b^2`).

However, the theorem of infinite descent cannot be applied to this property with the set Z which the author specifically said he would use. Instead, it needs to be applied to the set Z\{0}, which you rightly pointed out (as well as the sibling poster).

Note that this has nothing to do with the rest of the proof about √2.

I do agree that even after this error is corrected, then the proof additionally needs to be fixed by adding a few more simple proof steps to analyze what happens when either `a` or `b` are zero, which was excluded from the set. At this point you'd probably realize that yes, there is an implicit assumption that ¬(b = 0) which should be made explicit, and then you also have to account for the `a = 0` case, which should also be easy.

But still, the error greatly confused me at first because it seemed like the theorem could not be applied in this case. I only realized the theorem could be used correctly in this case when the sibling poster suggested to use a different set.