Successor '

The successor operator adds (1) to a number. The successor of x is written as (S x). The successor is an even more basic operation than addition. In fact, the properties of addition are derived using the successor operations. The properties of the successor are derived directly from the Peano axioms. The number 1 is defined as (= (1) (S (0))) /edit/peano_new/arithmetic/naturals/add_multiply_min.gh/df-1

Important Theorems

Arithmetic Overview

Login to edit