Dedekind–Peano Structure

Dedekind–Peano Structure

Dedekind–Peano Structure is the ternary tuple \((e,S,\mathbb{N})\) such that

• \(e\) is an element, \(S\) is the a function, \(\mathbb{N}\) is a set

• \(e \in \mathbb{N}\) (neutral element

• \(\forall a \in \mathbb{N}, S(a)\in \mathbb{N}\) (successor function is \(\mathbb{N} \rightarrow \mathbb{N}\))

• \(\forall a,b\in \mathbb{N}, (S(a)=S(b) \implies a=b)\) (successor function is injection)

• \(\forall a \in \mathbb{N}, S(a)\neq e\) (the range of successor function exclude e, no wrap-up, e is the first)

• \(\forall P,\{P(e) \land \forall k \in \mathbb{N},[P(k)\implies P(S(k))]\} \implies [\forall n \in \mathbb{N}, P(n)]\) (induction)

So, we can define \(0 := e, 1:=S(0),2:=S(1)=S(S(0)), ...\)