Specific example of a property $P$ that Peano arithmetic proves holds true for every specific number, but not for all numbers.

Question

Can someone give a specific example, if there is any, of a predicate $P(x)$ expressible in the language of Peano arithmetic, such that the first-order theory of Peano Arithmetic proves $P(0)$, $P(1)$, $P(2)$, etc, but does not prove $(\forall x)P(x)$?

Answer 1

The standard example is $P(x)$ = "$x$ is not a (code for a) proof of a contradiction in $\mathsf{PA}$." Assuming $\mathsf{PA}$ is consistent, we obviously have $\mathsf{PA}\vdash P(n)$ for each individual numeral $n$, but by Godel $\mathsf{PA}\not\vdash\forall x P(x)$. (This is really just the fact that $\mathsf{PA}$ is $\Sigma_1$-complete but not $\Pi_1$-complete.)

Note that this $P$ is $\Delta_0$. With the (proof of the) MRPD theorem, we can get rid of Booleans and bounded quantifiers at the cost of additional variables: there is a specific Diophantine equation $t(\overline{x})=0$ which has no solutions but whose lack-of-solutions is $\mathsf{PA}$-provably equivalent to $\mathsf{Con}(\mathsf{PA})$, so we get $\mathsf{PA}\vdash(\neg t(\overline{n})=0)$ for each tuple of numerals $\overline{n}$ but again by Godel $\mathsf{PA}\not\vdash\forall\overline{x}(\neg t(\overline{x})=0)$. The exact number of variables needed for this is still open; it's easy (via the rational root theorem) to prove that one variable isn't enough, and if memory serves the current upper bound is somewhere in the tens-of-variables, which isn't too bad!

And as usual, nothing here is specific to $\mathsf{PA}$: any sufficiently rich c.e. theory will behave identically.