# How to know if true statement for $\mathbb{N}$ is derivable in $\mathsf{PA}$

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)$$)?

• For instance, let $\phi_0(x,y,z)$ say "$\phi_1(x,y,z)$ if there is no proof of $0=1$ in PA with length less than $x,$ otherwise z=0". Mar 1 at 2:50
• @spaceisdarkgreen So assuming consistency of $\mathsf{PA}$, we cannot have that $\mathsf{PA} \vdash \forall xyzw \ [\phi_0(x, y, z) \rightarrow (\phi_0(x, S(y), w) \leftrightarrow w = zx)]$ as $w = zx$ always exists, and the second clause ("otherwise $z = 0$") shan't happen, but this would imply that there exists no proof of $0 = 1$ in $\mathsf{PA}$, i.e., $\mathsf{PA} \vdash \mathrm{Con}(\mathsf{PA})$. Thank you! :)
– Sho
Mar 1 at 4:57