[lupire]

It's not wrong, but it skips some detail. (It's ironic that an article about "insight via precision" uses such imprecise language.)

This is demonstrated in a Lean tutorial for induction, where first it has you "prove" that √2 is "rational", before adding the requirement that the denominator is not 0, which then of course requires a totally different (semantically valid) proof.

0 does satisfy the theorem on integers, but it doesn't say anything about √2, because rational numbers do not allow a 0 denominator.

The √2 theorem assumes b >= 1, and infinite descent / well-foundedness is based on this subset of Z (and to the author's pedantic point about ordering, also works with Z\{0} and the magnitude ordering on |z|.)

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