[skybrian]

In first-order logic, it's an infinite axiom schema, which means you can take a finite subset of them, like assuming induction axioms hold for the formulas you're actually using and not in any other case.