# 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

Recall the Principle of Recursive Definition (Strong Version):

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$.

This needs considerable tedious hard slog to complete it.In particular: I will defeat this beastTo discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Finish}}` from the code.If you would welcome a second opinion as to whether your work is correct, add a call to `{{Proofread}}` the page. |

## Sources

- 2010: Raymond M. Smullyan and Melvin Fitting:
*Set Theory and the Continuum Problem*(revised ed.) ... (previous) ... (next): Chapter $3$: The Natural Numbers: $\S 8$ Definition by finite recursion: Exercise $8.4 \ \text {(a)}$