2
$\begingroup$

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

$\endgroup$
2
  • 2
    $\begingroup$ 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". $\endgroup$ Mar 1 at 2:50
  • $\begingroup$ @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! :) $\endgroup$
    – Sho
    Mar 1 at 4:57

0

You must log in to answer this question.

Browse other questions tagged .