PA├ ∃xP(x) but PA$\nvdash$ P(n) for any n? Problem :
Let P(x) be a wff with one free variable x in the language of PA and $PA\vdash \exists P(x)$. And let PA be $\omega$-consistent.
Then, is there a natural number $n$ s.t. $PA\vdash P(n)$?

Since PA is $\omega$-consistent and the standarad arithmetic model $\mathbb{N} $ is a model of PA,
There should be a natural number $n$ s.t. $\mathbb{N} \models P(n)$. Also, $PA \vDash \exists xP(x)$.
Since PA isn't complete, it may happen that although P(n) is true on $\mathbb{N}, PA \nvdash P(n)$.
Also, the condition that P(n) is a sentence is required since
if P(x) had free variables other than x, then it may fail since
$PA\vdash (\exists x) x=y$, but for any $n\in \mathbb{N}, PA\nvdash n=y$.
One of tries was that finding a property P(x) s.t. there is a sequence of non-standard models $(A_n)_{n\in \mathbb{N}}$ where $\forall n\in \mathbb{N}, A_n\nvDash P(n)$, but $ A_n\vDash \exists xP(x).$  (Well, such P(x) also should be expressible in the language of PA though.)
And for a similar problem but ∀ is used instead of ∃, (i.e. finding G(x) where $PA\nvdash \forall x G(x) $ but $PA\vdash G(n)$ for every $n\in \mathbb{N}$), this is solved since there is Goodstein's Theorem. With a combibation of $\neg$, it may be a key.
Or using Diagonalization lemma may help, but still I couldn't find any examples.
 A: Let $P(x)$ be the formula $$"\!\operatorname{Con}(\mathsf PA)\vee x\textrm { is the Gödel number of a proof of a contradiction from }\mathsf{PA}.\!"$$
Clearly, $\mathsf{PA}\vdash\exists x P(x).$
But suppose, with the aim of reaching a contradiction, that there is a natural number $n$ such that $\mathsf{PA}\vdash P(\pmb{n}).$ Writing out what this means, $\mathsf{PA}$ proves the sentence
$$"\!\operatorname{Con}(\mathsf PA)\vee \pmb{n}\textrm { is the Gödel number of a proof of a contradiction from }\mathsf{PA}.\!"$$
We've assumed that $\mathsf{PA}$ is consistent, so $n$ is not actually the Gödel number of a proof of a contradiction from $\mathsf{PA}.$
Being the Gödel number of the proof of a contradiction from $\mathsf{PA}$ is a finitistic property, so we can examine the specific number $n$ and conclude that the sentence $$"\!\pmb{n}\textrm{ is not the Gödel number of a proof of a contradiction from }\mathsf{PA}\!"$$ is provable in $\mathsf{PA}.$
It follows that $\mathsf{PA}\vdash \mathrm{Con}(\mathsf{PA}),$ contradicting Gödel's incompleteness theorem.
