I can’t figure out why induction is considered an axiom. It seems like it should follow from other axioms.
You can prove that any individual natural number is part of a set by applying S(x) finitely many times, but getting all of them either requires an infinitely long proof (bad) or an axiom.
I think you could express that in first order logic, but the axiom of induction can’t be expressed in first order logic (according to wikipedia.) And that seems like a huge issue and bothers me.
You run into Lowenheim-Skolem. If you could express the axiom of induction in first-order logic, then you’d have a model of arithmetic with k numbers for every infinite cardinal k. That’s the advantage of second-order logic: the original Peano axioms give only one set of natural numbers (up to isomorphism). I believe there are certain formulations that only use first-order logic, but they give weaker results.
You can prove that any individual natural number is part of a set by applying S(x) finitely many times, but getting all of them either requires an infinitely long proof (bad) or an axiom.
You run into Lowenheim-Skolem. If you could express the axiom of induction in first-order logic, then you’d have a model of arithmetic with k numbers for every infinite cardinal k. That’s the advantage of second-order logic: the original Peano axioms give only one set of natural numbers (up to isomorphism). I believe there are certain formulations that only use first-order logic, but they give weaker results.