A Proof of Proof by Infinite Descent

I like that the article uses the concrete example of proving √2 is not rational to demonstrate the abstract priciples of induction, while also not hand-waving away the formal details of the general case.

I got a little caught up on on the proof of (no) infinite descent by well-founded induction without a base case. I thought, "something is wrong; (∀y∈X.y⊏x⟹¬Φ(y)) only implies ¬Φ(x) if you assume (∀y∈X.y⊏x⟹¬Φ(y)) in the firsts place". But that's actually fine, because the principle of well-founded induction lets you assume it out of thin air, and as long as it implies ¬Φ(x), you're good.

The intuition of this, to me at least, is that well-founded induction has an implicit base case of the empty set. (∀y∈X.y⊏x⟹Ψ(y))⟹Ψ(x) means Ψ(x) is required to be automatically true if ∄y∈X, so (∀y∈X.y⊏x⟹Ψ(y)) may be assumed out of thin air and then used inductively for all the cases where ∃y∈X.

Back to the specific example, ¬Φ(x) is automatically true if ∄y∈X because Φ(x) implies ∃y∈X. However note that this base case doesn't need to be explicitly shown, because it's included in the general case.

> a well-founded relation ⊏ is a well-ordering if and only if it relates every distinct pair of elements, i.e. x1≠x2 implies either x1⊏x2 or x2⊏x1.

The author here explains well-founded relation prior to this. I want to add an example here. Consider the set of positive real numbers. If we use the natural ordering < then we have a total order. But that's not a well-ordering. If x were to be the least element you could always divide it by 2 to get a lesser element. So there's no least element in the set of positive reals using the conventional < ordering. However, the amazing thing is that assuming axiom of choice, such a well ordering exists.

How does infinite descent work using a proof assistant? It's been quite a while, so I may be remembering incorrectly, but this is my understanding:

Coq uses an inductive type like "N = 0 : N | S : N → N", and a first-order theory with integers axiomatized this way admits nonstandard models (whose prefixes are isomorphic to the naturals but have elements not reachable by repeated application of S, defeating infinite descent). But universal quantification in system F (inherited by the calculus of inductive constructions) corresponds to a fragment of second-order logic, where there is only one model (– the theory is categorical).

Is that right?

> I imagine that one could also prove that √−1 is not rational

I feel like this was a marvellous joke but I can’t prove it.

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.

In the step of √2 = a/b you can get away without asking for relatively prime, using GCD or this descent by asking for least a for which this holds. Then when you get a/b = 2c/2d = c/d, but c would be less than a, hence contradiction.

Couldn't you always do this instead of doing this infinite descent? If relation is well-founded then there will be a least element.

What is the best way to write LaTeX in Blogspot sites, like the author has here?

“rife with defaults” does this parse, for a math person?