induction axiom

An induction axiom specifies that a theory includes induction, possibly restricted to specific formulas. IND is the general axiom of induction:

$$\varphi (0)\wedge \forall x(\varphi (x)\to \varphi (x+1))\to \forall x\varphi (x)\text{ for any formula }\varphi$$

If $\varphi$ is restricted to some family of formulas $F$ then the axiom is called F-IND, or F induction. For example the axiom ${\mathrm{\Sigma }}_1^0$-IND is:

$$\varphi (0)\wedge \forall x(\varphi (x)\to \varphi (x+1))\to \forall x\varphi (x)\text{ where }\varphi \text{ is }{\mathrm{\Sigma }}_1^0$$