ordering:
1. (∀m)(¬(m<m))
2. (∀a)(∀b)(∀c)(a<b⟹b<c⟹a<c)
3. (∀a)(∀b)(a<b⟹¬(b<a))
4. (∀a)(∀b)(a<b∨b<a)
constants:
1. (∀m)(¬(m<0))
2. 0<ω
3. (∀m)(∃n)(m<ω⟹m=0∨m=S(n))
successor:
1. (∀a)(¬(S(a)=0))
2. (∀a)(¬(S(a)=ω))
3. (∀m)(∀n)(S(m)=S(n)⟹m=n)
4. (∀a)(a<S(a))
addition:
1. (∀m)(m+0=m)
2. (∀m)(∀n)(m+S(n)=S(m+n))
3. (∀m)(∀n)(∀y)((∀x)(x<n⟹(m+x)<y)⟹m+n<y)
4. (∀m)(∀n)(∀x)(m<n⟹x+m<x+n)
multiplication:
1. (∀m)(m⋅0=0)
2. (∀m)(∀n)(m⋅S(n)=(m⋅n)+m)
3. (∀m)(∀n)(∀y)((∀x)(x<n⟹(m⋅x)<y)⟹m⋅n<y)
transfinite induction:
1. (∀m)((∀n)(n<m⟹φ(n))⟹φ(m))⟹(∀m)φ(m)