FALSE: transfinite induction and recursion need the Axiom of Choice

FALSE. Transfinite induction (Transfinite induction) and transfinite recursion (Transfinite recursion) require the Axiom of Choice (The Axiom of Choice): arguments that run along a well-order past the finite stages are not available in ZF alone.

The claim is plausible because the constructions one meets first do cost the Axiom of Choice. Well ordering an arbitrary set, extending a linearly independent family to a basis, building a maximal object stage by stage: each of these is usually presented as a transfinite recursion, and each really does need choice. The confusion is about which half of the argument is expensive. It is never the recursion.

A useful test. Ask what the value at stage $a$ is. If the answer is a definite description, "the least ordinal such that", "the order type of", "the union of the earlier values", and every object the description mentions is one ZF supplies, then the construction is choice-free. If the answer is "some element with the following property", and there is generally more than one, then a choice function is being used and must be paid for. The parameter clause is not decoration: "the element $c$ picks from the set of points not yet used" is a perfectly definite description, and it is Zermelo's construction, whose whole cost is obtaining $c$.

Three choice-free constructions on this page. The collapsing map of Every well-order has a unique order type, the family of order types in Hartogs: an ordinal that does not inject into a given set, and the comparison map of Comparability of well-orders are all defined by formulas, which is why each is a ZF theorem. Their proofs say so explicitly, and the reason is always the same: rigidity of well-orders makes the relevant witnesses unique (Rigidity of well-orders).

Dependent choice is the usual hidden cost. A construction along $\mathbb{N}$ that picks an object at each step, using the previous one, needs the principle of dependent choice (DC). It is not transfinite recursion that costs this; it is the picking. Where DC sits is a separate question and a strictly metamathematical one: if ZF is consistent, then DC is not a theorem of ZF and DC does not imply the Axiom of Choice, so DC is then strictly between the two. Both separations are external results, established by forcing and permutation models, quoted from the references and proved nowhere in this library; the consistency hypothesis cannot be dropped and cannot be proved inside ZF. The refutation above needs none of this, because transfinite induction and transfinite recursion are outright theorems of ZF and the claim is refuted by exhibiting their proofs. The ledger of principles is The choice ledger: what costs the Axiom of Choice and what does not.

Ordinary induction is the same story. Nobody suspects induction on $\mathbb{N}$ (The principle of mathematical induction) of using choice, and transfinite induction is the same theorem with $\mathbb{N}$ replaced by an arbitrary well-order. The proofs are the same length and use the same single ingredient.