How to prove that a function defined recursively really exist?

I have an example of an inductively defined set and a function on that set. But I am wondering if one should do more work to really show that the function exist? The set is:

The smallest set that contains $3$ and $4$, and is such that if $x$ is an element of the set and $x$ is an odd number, then $2x-1$ is an element of the set, and also if $x$ is an element of the set and $x$ is an even number then $x+4$ is an element of that set.

I define the function $f$ like this $f(3)=1,f(4)=2$. If $x$ is odd than $f(2x-1)=2f(x)$, if $x$ is even than $f(x+4)=f(x)+2$.

Is there a way to show that the set we are working with and the function we define really are well-defined? Intuitively they will be well-defined since we define it by elements we have already defined, and we only define it on elements that are in our set, but this doesn't seem enough?

So we have the following property on a set $A$:

• $\{3, 4\} \subseteq A$, and
• for all $x \in A,x$ is odd $\implies 2x - 1 \in A$, and
• for all $x \in A,x$ is even $\implies x + 4 \in A$

Note that there is at least one set with this property, $\Bbb N$. Also note that if $\mathscr A$ is a collection of sets all satisfying the property, then the intersection $$\bigcap_{A \in \mathscr A}A := \{x \mid \forall A \in \mathscr A, x \in A\}$$ is also a set satisfying the property.

But we can define such an $\mathscr A$ by $$\mathscr A := \{A \subseteq \Bbb N\mid A \text{ satisfies the property}\}$$ $\mathscr A$ at least has $\Bbb N$ as a member, so the intersection of $\mathscr A$ is not empty.

If $B$ is any set having the property, then $B \cap \bigcap_{A \in \mathscr A}A \subseteq \Bbb N$ and also has the property. Thus $B \cap \bigcap_{A \in \mathscr A}A \in \mathscr A$, which means $$\bigcap_{A \in \mathscr A}A\subseteq B \cap \bigcap_{A \in \mathscr A}A$$ which can only be if $\bigcap_{A \in \mathscr A}A \subseteq B$.

Therefore $\bigcap_{A \in \mathscr A}A$ is a subset of every set with the property, which makes it the smallest such set.

This proof works more generally. If you have some property on sets that is preserved under intersection (even intersections of any collection of sets with the property), and there is at least one set with the property, this proof shows that there must be a smallest set with the property. This is not induction. It just follows from the basic behavior of sets. But it can be used to show that any well-formed inductive definition of a set does indeed fully define the set.

And since functions can be expressed as subsets of the product of the domain and codomain, it also can be used to prove inductive definition of a function is valid.

[Added] One way to apply this to functions is to consider subsets $S$ of $\Bbb N \times \Bbb N$ with the property (for your example)

• $\{(3,1), (4, 2)\} \subseteq S$, and
• if $(x, y) \in S$ and $x$ is odd, then $(2x-1, 2y) \in S$, and
• if $(x,y) \in S$ and $x$ is even, then $(x + 4, x+2) \in S$.

Call this property $P(S)$. Obviously $P(\Bbb N \times \Bbb N)$ holds, and for any collection $\mathscr A$ of sets, if for all $A \in \mathscr A, P(A)$ holds, then $P(\bigcap \mathscr A)$ also holds. Thus as above, there is a smallest subset $f$ of $\Bbb N \times \Bbb N$ for which it holds.

Note that $P$ was applied to general subsets of $\Bbb N \times \Bbb N$, not just to functions. If we had tried to limit $P$ to functions from the start, then no, we do not have a handy top function that satisfies the condition, so we could not claim that $\{A \in \Bbb N^2\mid P(A)\}$ is not empty. In fact, $f$ would be the maximum set in that collection, not the the minimum. To avoid these issues, I allow non-functional sets.

But now you have to show from the properties that $\text{Dom}(f) := \{x \mid \exists y, (x,y) \in f\}$ is the inductively defined set above, and that $f$ is a function. I.e., if $(x,y), (x,z) \in f$ then $y = z$. (For this, you can assume $y \ne z$, then use that to show that either $y$ or $z$ could be discarded without violating $P$, meaning if $f$ contained both it would not be the smallest, contrary to its definition.)