Do we really need the recursion theorem if we deal only with specific recursively defined functions?

Question

How is it possible to define in a totally rigorous (i.e. from the axioms) was the functions $$h:\mathbb{N}\rightarrow \mathbb{N}, \ n\mapsto 1\cdot\ldots \cdot n$$ or $$ g:\mathbb{N}\rightarrow \mathbb{R}, \ n\mapsto x^n \ $$

without using the recursion theorem , that immediately tells us that these functions exist and are unique ?

Differently said: Do we really need a general statement like the recursion theorem to prove that these two specific functions exist and are unique ? Isn't there an easier proof just for these two functions (I'm thinking of somehow building the sets these functions correspond to directly out of $\mathbb{N}$ and $\mathbb{R}$ via the ZFC axioms, without resorting to the recursion theorem. My naive approach - I never had a course in set theory, so I don't know if this is correct - would be, for example for the second function, to directly build the set $$ \{ (n,r)\in\mathbb{N}\times \mathbb{R} \mid r=x^n \},$$ where $x \in \mathbb{R}$ is some fixed number, via the "axiom schema of separation", which gives me my function $g$, since it is its graph)

Side question: As far as I understood the recursion theorem, the important statement it makes is that these functions are unique (since existence seems to me to already be "given", since one can always define (using the terminology from Wikipedia) a function $F(n):= (f\circ \ldots \circ f)(n)$, where the composition was taken $n$ times, although again I don't really which axioms would let me do that, since this is just my intuition).

Answer 1

You're correct, certainly, that showing the existence of the function is (almost trivially) equivalent to showing the existence of the relation - but how do you propose to define the relation '$r=x^n$' (we can even assume $r$ and $x$ integers here - the problem still isn't easy!) in non-recursive fashion? An excellent exercise (which I first found in Hofstadter's Godel, Escher, Bach) is to characterize the predicate '$n$ is a power of $2$' in explicit fashion - note that 'explicit' here means without the use of recursion or iteration (which is, for these purposes, recursion in disguise)! If you're able to get that one, you might try the predicate '$n$ is a power of $10$' - that should go a long way towards showing just how powerful the recursion theorem is as a tool.

In general, I'd be very wary of using 'intuition' to understand these concepts, because logic and axiomatics are one area where your intuition can lead you strongly astray (for instance, look at the Axiom of Choice) and where formal arguments are a necessity. In fact, it would probably be helpful just to find the appropriate formal way to prove the existence of these functions with the recursion theorem: in its most useful form here the theorem formally states that for any number $a$ and function $f(x):\mathbb{N}\to\mathbb{N}$ there's a function $F(x):\mathbb{N}\to\mathbb{N}$ with $F(0) = a$ and $F(n+1) = f(F(n))$.

To understand what can go wrong, it may be worth understanding how the recursion theorem can fail: imagine an abstract system where our notion of 'number' remains the same, and we're given the basic arithmetic operations of addition and multiplication, but the notion of function is restricted to polynomially bounded functions: for each function $f$ there exist constants $k$ and $C$ such that for all $n$, $|f(n)| \le \left|n\right|^k+C$ . Then we can add and multiply these functions and still get totally legitimate functions, and we can even compose these functions to get legitimate functions: if $f(n)$ and $g(n)$ are polynomially bounded, then the function $h$ defined by $h(n) = f(g(n))$ is polynomially bounded. But the recurion theorem (in the form I gave) fails in this setting - can you see why?