Choice and the principle of transfinite induction

Question

Does the Axiom of Choice suffice to show Transfinite Induction in ZF?

Also, if possible, could you please give some general remarks/insight on (i) worthwhile noting equivalencies or dependencies between Axiom of Choice (stronger/weaker related forms) and Transfinite Induction or, in particular, (ii) if PA consistency proofs (like Gentzen's, in PRA+'Quantifier Free Transfinite Induction up to ε0') require any form of Axiom of Choice.

Answer 1

Gentzen's proof can be formalized in PRA plus "transfinite induction on $\epsilon_0$", provided the latter is phrased in the right way. It does not require set theory of any sort, much less the axiom of choice. As mentioned by spaceisdarkgreen in the comments, this is one reason (among many) that Gentzen's proof is of interest.

However, as a separate point, "PA is consistent" is a $\Pi^0_1$ sentence, and a sentence of that form provable in ZFC is always provable in ZF as well, so even if we look at ZFC there is no way that proving the consistency of PA could require the axiom of choice. Even if choice were used to simplify a ZFC proof that PA is consistent, the use of choice could be eliminated.

Answer 2

The validity of transfinite induction is established with basically the same proof as for ordinary induction: if there is a counterexample, there must be a least counterexample, but the proof form demonstrates such a thing cannot exist.

The role of the axiom of choice is to allow a specific type of step that one often uses in inductive proofs. For example, one proof that every vector space mimics the usual algorithm for "constructing" a basis that one often sees in finite dimensional linear algebra:

1. Start with the empty set.
2. If your set spans the whole vector space, it's a basis and you can stop.
3. Choose a vector that isn't in the span of your set.
4. Add that vector to the set you're constructing and go back to step 2.

The role of the axiom of choice is to prove that step 3 is actually something that you can use in a transfinite "algorithm" such as this.