4 ms·
> 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 e
by 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.