[someplaceguy]

I think I'm missing something... isn't there an error in the proof when applying the theorem of the principle of infinite descent?

The theorem requires proving the following premise/antecedent (to deduce the consequent):

  ∀x ∈ X. Φ(x) ⟹ ∃y ∈ X.  y ⊏ x  ∧  (...)

... but I don't see how this can be proved when x=0. By substituting `x` for `0` (and using Z as the set X and |<| as the well-founded relation) you get:

  Φ(0) ⟹ ∃y ∈ Z. y |<| 0

Unfolding Φ:

  (∃b ∈ Z. 0^2 = 2 b^2) ⟹ ∃y ∈ Z. y |<| 0

The antecedent of this implication is true (when b = 0), so now you have to prove:

  ∃y ∈ Z. y |<| 0

However, this can't be proved because no `y` satisfies the |<| well-founded relation when applied to zero.

Therefore, this article's sentence doesn't seem to be true:

> Having satisfied the premises of the principle, we use it to deduce that no `a` satisfies the property

... which in fact cannot be true, because `a=0` does satisfy the property `∃b ∈ Z. a^2 = 2 b^2`, does it not? Consider `b=0`.

So what am I missing?

Edit: in fact, if the theorem could be applied in this case, then the conclusion of the theorem would be:

  ∀x ∈ Z. ¬(∃b ∈ Z. x^2 = 2 b^2)

Which is equivalent to:

  ∀x ∀y ∈ Z. ¬(x^2 = 2 y^2)

... which is clearly false when x=0 and y=0. So it seems like the theorem of infinite descent cannot be used to reach this conclusion. Some kind of false assumption would have to exist, but no false assumption was used to instantiate this theorem.

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

[bubblyworld]

Yeah, I think you have to exclude 0 to push that proof through. Your relation is still well-ordered in that case so it's fine I think.