The induction axiom of Peano Arithmetic. If p(0) is true, and p(x) implies p(suc x) for all x, then p(x) is true for all x.
p(0)
p(x)
p(suc x)
x
axiom peano5 {x: nat} (p: wff x): $ [0 / x] p -> A. x (p -> [suc x / x] p) -> A. x p $;