As title states, I'm a bit confused as to how to be certain a statement that is intuitively true for $\mathbb{N}$ is provable in $\mathsf{PA}$.
Specifically, I'm looking to prove the equivalence between two formulae $\phi_0$ and $\phi_1$. The first formula, $\phi_0$, is a functional formula in $\mathscr{L}_\mathsf{PA}$ (i.e., $\mathsf{PA} \vdash \forall xy \ \exists! z \ \phi_0(x, y, z)$), with $\mathrm{FV}(\phi_0) = \{x, y, z\}$, verifying that $a^b = c \implies \phi_0(\overline{a}, \overline{b}, \overline{c})$ for every $a, b, c \in \mathbb{N}$. The second formula, $\phi_1$, is also in $\mathscr{L}_\mathsf{PA}$ and verifies that $\mathsf{PA} \vdash \phi_1(x, 0, z) \leftrightarrow z = 1$ and $\mathsf{PA} \vdash \phi_1(x, y, z) \rightarrow (\phi_1(x, S(y), w) \leftrightarrow w = zx)$.
Now, I seek to prove that the formulae $\phi_0$ and $\phi_1$ are equivalent, i.e., that a formula like $\phi_0$ satisfies $\phi_1$'s properties and vice versa. That $\phi_1$ is functional and verifies $\phi_0$'s main property is simple to prove via induction on $b \in \mathbb{N}$, but I'm having some trouble showing (if showable) $\phi_0$ satisfies $\phi_1$'s second clause. (The issue is, of course, that $\phi_0$ is "focused" on how the formula works for naturals, i.e., elements of the standard model, but $\phi_1$ claims something of all $x$ —and there nonstandard shenanigans start to come in...)
Is there some way to prove that $\phi_0$'s proper functioning over the naturals implies its proper functioning for all models (i.e., $\mathsf{PA} \vdash \phi_0(x, y, z) \rightarrow (\phi_0(x, S(y), w) \leftrightarrow w = zx)$)?