\( \newcommand{\matr}[1] {\mathbf{#1}} \newcommand{\vertbar} {\rule[-1ex]{0.5pt}{2.5ex}} \newcommand{\horzbar} {\rule[.5ex]{2.5ex}{0.5pt}} \newcommand{\E} {\mathrm{E}} \)
deepdream of
          a sidewalk
Show Question
\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \newcommand{\multiBetaReduction}[0] {\twoheadrightarrow_{\beta}} \newcommand{\betaReduction}[0] {\rightarrow_{\beta}} \newcommand{\betaEq}[0] {=_{\beta}} \newcommand{\string}[1] {\texttt{"}\mathtt{#1}\texttt{"}} \newcommand{\symbolq}[1] {\texttt{`}\mathtt{#1}\texttt{'}} \newcommand{\groupMul}[1] { \cdot_{\small{#1}}} \newcommand{\groupAdd}[1] { +_{\small{#1}}} \newcommand{\inv}[1] {#1^{-1} } \newcommand{\bm}[1] { \boldsymbol{#1} } \require{physics} \require{ams} \require{mathtools} \)
Math and science::Analysis::Tao::02. The natual numbers

Addition, the definition for natural numbers

Let m be a natural number. 
To add zero to \( m \), we define: 

\( 0 + m := m \)

Now, suppose inductively that we have defined how to add \( m \) to \( n \), another natural number. Then we can add \( n++ \) to \( m \) by defining:

\((n++) + m := (n + m)++ \)

This is a definition, not an axiom, as it is the creation of new syntax to refer to something that already exists according to the existing axioms for natural numbers.

The definition can be viewed as a 2-input 1-output operation. Incrementing the LHS causes the output to be incremented. If this process is reversed, we can decrement until the LHS is zero, then the output collapses to be the RHS. 

There are only two definitions (and no axioms) for the natural numbers in Tao's book that allow two variables (combined with a symbol) to be equated to a single variable. One is the first part of the definition above, and the second is the complementary statement making up the definition of multiplication. So any statement that involves a reduction in variable count must enact one of these definitions. 


Source

Analysis I, Tao