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