Peano axioms

Axioms of natural numbers

code:s

var N

var 0: e N

fn S: N -> N

for all n { S(n) != 0 }

for all n, m { S(n) = S(m) -> n = m }

for all K {

K(0) & for all n { K(n) -> K(S(n)) } -> for all n { K(n) }

}