$\newcommand{\N}{\mathbb{N}}$ $\newcommand{\pp}{\texttt{++}}$ $\newcommand{\set}[1]{\{#1\}}$ $\newcommand{\tand}{\text{ and }}$ $\newcommand{\tor}{\text{ or }}$ In Terrence Tao's analysis, he describes the Peano axioms and then then axioms of ZF set theory, and then gives the reader the following definition of a function:
Let $X,Y$ be sets, and let $P(x,y)$ be a property pertaining to an object $x \in X$ and an object $y \in Y$ , such that for every $x \in X$, there is exactly one $y \in Y$ for which $P(x,y)$ is true (this is sometimes known as the vertical line test). Then we define the function $f : X \to Y$ defined by $P$ on the domain $X$ and range $Y$ to be the object which, given any input $x \in X$, assigns an output $f(x) \in Y$, defined to be the unique object $f(x)$ for which $P(x,f(x))$ is true. Thus, for any $x \in X$ and $y\in Y$,
$$y=f(x) \iff P(x,y)\text{ is true}.$$
Later, after defining the Cartesian product, he gives the following exercise
Let $f : \N \times \N \to \N$ be a function, and let $c$ be a natural number. Show that there exists a function $a : \N \to \N$ such that
$$a(0) = c$$
and
$$a(n\pp) = f(n, a(n))\text{ for all }n \in \N$$
and furthermore that this function is unique.
I believe I was able to prove this in the way that he had in mind, by showing that, for all $N \in \N$, there exists a function $a_N(n)$ that has the desired properties for $n < N$
However, I also came up with another proof that uses the definition Tao gave more directly.
Let $$P(x, y) := (x = 0 \tand y = c) \tor (x = n\pp \tand \exists u, y = f(n, u) \tand P(n, u) )$$. We will show that, by induction on $x$, for every $x \in \N$ there is exactly one $y \in \N$ such that $P( x, y)$ is true.
First the base case. Let $x = 0$, and let $y = c$, then $P(x, y)$ is trivially true. Now suppose that $x = 0$ and $y \neq c$, then $(x = 0 \tand y = c)$ is false, and $x = n\pp \tand y = f(n, a(n))$ is false since there exists no $n$ such that $0 = n\pp$ by Axiom 2.3 in the book (0 is not the successor of any natural number). Therefore $P(x, y)$ is false if $x = 0$ and $y \neq c$, so $y$ is unique for $x = 0$.
Now suppose that, for some $x$, there is exactly one $y$ such that $P(x, y)$. Then let $y' = f(x, y)$ (this exists since $f$ exists by assumption) and $x' = x\pp$. Then $P(x', y')$ is true, since $(x' = x\pp \tand y' = f(x, y) \tand P(x, y))$ is true, and by the induction hypothesis, $y$ is the only $y$ such that $P(x, y)$ is true for that $x$.
To show that $y'$ is unique, assume that $y' \neq f(x, y)$; and assume for contradiction that $P(x', y')$ is true. Since $x' \neq 0$ by Axiom 2.3, we have $(x' = n\pp \tand \exists u, y' = f(n, u) \tand P(n, u)$. We have $x' = x\pp$, so $y' = f(x, y)$. But this is a contradiction, since we have assumed $y' \neq f(x, y)$. Therefore $P(x', y')$ is false if $y' \neq f(x, y)$, and so $y'$ is unique for $x' = x\pp$.
Since we have just shown that, for every $x \in \N$, there is exactly one $y \in \N$ such that $P(x, y)$ is true, we have by definition that there exists a function $a : \N \to \N$ such that $a(x) = y$ if and only if $P(x, y)$.
Let $a$ be the function given by $P(x, y)$ as defined above. Then $a(0) = c$, since we have shown that $P(0, y) \implies y = c$.
Furthermore, $a(n\pp) = f(n, a(n))$. This is because $n\pp \neq 0$, and so $x = n\pp \tand \exists u, y = f(n, u) \tand P(n, u)$ must be true. This implies $P(n, u)$, and so $a(n) = u$. Since also $y = f(n, u)$, we have $y = f(n, a(n))$.
So $a$ exists.
To prove uniqueness, assume that there exists an $a$ and $a'$ such that the definition is met. We will show by induction that $a(n) = a'(n)$ for all $n$.
If $n = 0$, then $a'(0) = c = a(0)$. Now assume $a'(n) = a(n)$ for some $n$, then $a'(n\pp) = f(n, a'(n))$ and by the induction hypothesis $a'(n\pp) = f(n, a(n))$. By definition, $a(n\pp) = f(n, a(n))$, so $a'(n\pp) = a(n\pp)$. So $a'(n) = a(n)$ for all $n$.
This second proof all depends on the predicate $P(x, y)$ being both well formed, and non circular. I am thinking that $P(x, y)$ is well formed, but that the proof is circular, however, I am not sure of either. Terrence Tao's book does not cover predicate logic in enough detail to decide (which feels kind of bad considering that functions are defined by them).
I am pretty sure that in type theory, the proof would be circular, but that the predicate would be well defined, because the predicate would itself be a function, and recursive functions do exist in type theory (I am not 100% positive about this though).
However, based on Tao's definition, a predicate is somehow separate from a function, so I am thinking that it's possible that the proof is non circular and that the predicate is well defined. However, I am not sure.
It is arguably a bit questionable to present a definition of $P$ in this manner, but there is a straightforward way to understand it that causes no issues. There are some minor issues with the proof and it's unnecessarily complicated, but the approach is fine.
Specifically, we assume $P$ is some binary predicate (i.e. add a binary predicate symbol to our theory called $P$) and the only thing we know about it is that the "definition" holds as an axiom (i.e. also add the "defining" equivalence as an axiom of our theory). This would be no different than how we handle any other predicate symbol, e.g. $\in$. However, what we don't get is any guarantee that this completely specifies the behavior of the predicate $P$. In particular, $P$ could fail to be eliminable, meaning that there is no set theoretic formula (not involving $P$) that is provably equivalent to $P$. This would be undesirable for many reasons but is not a problem in itself. (One undesirable property is without eliminability there is the possibility that the new axiom adds a contradiction.)
This turns out not to be an issue. First, the proof would go through even if we were just talking about some predicate that satisfied the given axiom. Second, the proof (more or less) shows that $P$ is eliminable. The proof shows that for all $x\in\mathbb N$, $P(x,y)\iff y = a(x)$ for a function $a$ which ultimately can be defined without reference to $P$. For $x\notin\mathbb N$, it's easy to see that $P(x,y)$ is false for any $y$, and this is implicit in the proof as well. Therefore, $P$ is, in fact, eliminable.
As you allude to, in many type theories, we would be able to directly define predicates (i.e. $\mathsf{Prop}$- or $\mathcal U$-valued functions) via recursion. This isn't possible (and doesn't really make sense) for first-order logic. What you can do, in the context of typical set theories, is define $P(x,y)\equiv (x,y)\in X$ and then define $X$ inductively, internally to the set theory. Indeed, this is what your proof is ultimately doing that implies the eliminability of $P$. It is showing that $P(x,y)\iff (x,y)\in a$ where $a$ is defined inductively.
It doesn't really make sense to talk about the proof being "circular" in type theory. The theorem and the proof are in a totally different language than type theory. It may still require work to show that a type-theoretic predicate $\mathbb N \to \mathbb N \to \mathsf{Prop}$ satisfying the analogues of being a total, functional relation gives rise to a function $\mathbb N\to\mathbb N$. It's possible that this isn't even true depending on exactly how it's stated and the exact details of the type theory.