s-Peano-axioms

Formalize Peano postulates in epista AST

let 0: N { for all x { 0 != S(x) } }

let 0: N, S: N => N, for all x, φ { 0 != S(x) & S(x) = S(y) -> x = y & (φ(0) & φ(x) -> φ(S(x))) -> for all x φ(x)) }

equality

|- x = x

|- x = y & y = x

|- x = y & y = z -> x = z

definitions

let 0: N

let S: N => N

properties of successor and zero

|- S(x) = S(y) -> x = y

|- 0 != S(x)

let φ any predicate, φ(0); φ(x) -> φ(S(x)) |- φ(x)

note: 帰納法をこういう風に表せないか?

for all x { exists S^n { S^n(0) = x } }