How does the existence property fail in $PA$?

Question

Who or what is a good reference that explains how the (numerical) existence property fails for $PA$? Alternatively, what is a good example? It e.g. is clear that the disjunction property must fail because $PA$ is incomplete, as we for Gödel's sentence $G$ will have $PA\vdash G\vee\lnot G$ but both $PA\nvdash G$ and $PA\nvdash\lnot G$.

May the failure of the existence property for $PA$ affect the use of existential instantiation with a novel constant in any particular derivation supported by $PA$ with its classical underlying logic?

Answer 1

I guess that you are looking for an instance where $\newcommand\PA{\text{PA}}\PA\vdash\exists x\ \varphi(x)$, but $\PA\not\vdash\varphi(n)$ for any particular $n$.

If we are using classical logic in the proof system, then it seems that this follows immediately from the failure of the disjunction property, by the following method. Consider the property $\varphi(x)$ asserting $(G\wedge x=1)\vee (\neg G\wedge x=0)$. It is easy to see that $\PA\vdash \exists x\ \varphi(x)$, but there is no particular value $n$ for which $\PA\vdash\varphi(n)$, since $\PA$ does not settle $G$. One can use any independent assertion in place of $G$ here.