4 ms·
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 a
by GrantMoyer 2y ago
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.
- pdonis 2y ago> well-founded induction has an implicit base case of the empty set Yes, but that still means the reasoning that proves the induction has to be valid for the empty set--i.e., "if P is true for all y less than x, then P is true for x" has to be validly proven for the case that there are no y less than x--which of course is the case for the natural number 0 in ordinary mathematical induction.
- gizmo686 2y agoIf there are no y less than x, then any statement about all y less than x is vacuously true.
- pdonis 2y ago> If there are no y less than x, then any statement about all y less than x is vacuously true. I suppose this is technically correct, but it doesn't seem like a good basis for doing induction.
- DevelopingElk 2y agoI think it's fine. It's analogous to starting induction from 0 over the natural numbers. It does feel a bit tricky though because there are two nested foralls instead of just one in standard induction. I think to derive it from standard induction you need to perform induction over sets of statements, which takes more power than first order logic. This additional power is generally accepted in math courses. It isn't necessary though, you can prove the irrationality of sqrt 2 using standard induction. The article discussed how additional techniques can be made rigorous in the opening paragraph. I agree that the author didn't fully justify the assumptions in the proof system used, instead bringing this well ordered induction as an axiom. This is an article, I think a full aximization would have taken too long.
- immibis 2y agoBut the second half, "P is true for x", still has to be proven and is not vacuous.