Addition in Minimally Inductive Set is Unique

From ProofWiki
Jump to navigation Jump to search

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 beast
To 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

Retrieved from "https://proofwiki.org/w/index.php?title=Addition_in_Minimally_Inductive_Set_is_Unique&oldid=574671"