We write
The elements of are called natural numbers. We regard addition and multiplication on as binary operations
written in infix form as and . We also regard the successor on as a function
written in infix form as . These data are related by the following recursive identities for all .
- .
- .
- .
- .
We also require that is not a successor and that the successor map is injective; that is,
and
for all .
Loading…
Prerequisites
No prerequisites tracked.
Dependents
No dependents yet.
Dependent proofs
No dependent proofs yet.
No relations recorded yet.