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

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

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.