Axiom peano5 | index | src |

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.

axiom peano5 {x: nat} (p: wff x):
  $ [0 / x] p -> A. x (p -> [suc x / x] p) -> A. x p $;