# Addition in Minimally Inductive Set is Unique

## Theorem

Let $\omega$ be the minimally inductive set.

Let $A: \omega \times \omega \to \omega$ be the mapping defined as the addition operation:

$\forall \tuple {x, y} \in \omega \times \omega: \map A {x, y} = \begin {cases} x & : y = 0 \\ \paren {\map A {x, r} }^+ & : y = r^+ \end {cases}$

where $r^+$ is the successor set of $r$.

Then $A$ exists and is unique.

## Proof

Let $\omega$ denote the natural numbers as defined by the von Neumann construction.

Let $A$ be a class.

Let $c \in A$.

Let $g: \omega \times A \to A$ be a mapping.

Then there exists exactly one mapping $f: \omega \to A$ such that:

$\forall x \in \omega: \map f x = \begin{cases} c & : x = \O \\ \map g {n, \map f n} & : x = n^+ \end{cases}$

From the von Neumann construction, this $\omega$ is exactly the minimally inductive set as defined in the problem statement.

Let $g: \omega \times \omega \to \omega$ be the mapping defined as:

$\forall \tuple {x, y} \in \omega \times \omega: \map g {x, y} := y^+$

Hence from the Principle of Recursive Definition (Strong Version), there exists a unique mapping $f: \omega \to \omega$ such that:

$\forall x \in \omega: \map f x = \begin{cases} c & : x = \O \\ x^+ & : x = n^+ \end{cases}$

which we get by identifying $\map g {x, y}$ with $y^+$.

Let us fix some arbitrary $x_0 \in \omega$.