Are there existential theorems of ZFC, or PA say, with no witnesses?
Ie does there exist a formula $\phi$ such that ZFC $\vdash\exists x \phi(x)$, but for all numerals $\underline{n}$, ZFC $\nvdash \phi(\underline{n})$?
Can you give an example of such a formula?
The answer is yes, provided these theories are consistent. For example, PA proves that there is a number $n$, such that if there is no proof of a contradiction in PA of size at most $n$, then there is no proof of a contradiction in PA at all. This is trivial if you think about it, since either there is a proof of a contradiction in PA, in which case you can let $n$ be any number larger than that proof, or else there isn't such a proof of a contradiction, in which case any $n$ has the desired property. But PA does not prove that any particular number $n$ has this property, since then PA would prove its own consistency, which violates the incompleteness theorem.
Here is another kind of example: Let $\sigma$ be any statement that is independent of PA, and let $\phi(n)$ assert that $(n=0\wedge\sigma)\vee(n=1\wedge\neg\sigma)$. So PA proves $\phi(0)\vee \phi(1)$, and in particular it proves $\exists x\ \phi(x)$, but PA doesn't prove either case separately, because $\sigma$ is independent.
If you strengthen the conclusion of your question, however, to say that the theory should actually prove $\neg\phi(n)$ for every numeral $n$, then you would be asking whether these theories are $\omega$-inconsistent. Of course, we all think that our theories are $\omega$-consistent, because we want and expect that the natural numbers referred to inside the theory are somehow the same as those in the meta theory. But of course, because of the incompleteness theorem, we cannot prove this within the theory itself. Notice that a theory must be $\omega$-consistent in the case that it has an $\omega$-model, a model in which the natural numbers of the model are the same as the natural numbers of the meta-theory. For this reason, our stronger theories can often prove that our weaker theories are $\omega$-consistent. For example, ZFC proves that PA is $\omega$-consistent, and ZFC+large cardinals proves that ZFC is $\omega$-consistent. My own view is the assertion that a theory is $\omega$-consistent is just one stop along a continuum, from assuming consistency up to iterated consistency up to having a well-founded model up to large cardinals and so on, moving up in consistency strength at each step.
Meanwhile, if these theories are consistent, then it is easy to make examples of $\omega$-inconsistent theories extending them. For example, the theories PA+$\neg$Con(PA) and ZFC+$\neg$Con(ZFC) are consistent by the incompleteness theorem, but not $\omega$-consistent, because each of them asserts that there is a certain proof of a contradiction, which is provably not instantiated by any actual natural number witness.
$\def\epn{\mathrm{EP}_\mathbb N}\def\dp{\mathrm{DP}}$When a theory $T$ (with a distinguished definable set of “natural numbers” satisfying a suitable minimal arithmetic) has the property in the question, viz.
$$\tag{$\epn$}T\vdash\exists x\in\mathbb N\,\phi(x)\text{ implies }T\vdash\phi(\underline n)\text{ for some $n\in\mathbb N$,}$$
$T$ is said to have the numerical existence property. As explained in Joel’s answer, classical theories can have the numerical existence property only if inconsistent or complete, which prevents any interesting examples by virtue of Gödel’s incompleteness theorem.
However, the situation is quite different for theories over intuitionistic logic. Indeed, most natural constructive theories (e.g., Heyting arithmetic) do have $\epn$.
Since $\phi\lor\psi$ is equivalent to $\exists n\,((n=0\land\phi)\lor(n=1\land\psi))$, $\epn$ implies the seemingly weaker disjunction property
$$\tag{$\dp$}T\vdash\phi\lor\psi\implies T\vdash\phi\text{ or }T\vdash\psi.$$
By a result of Harvey Friedman, $\dp$ is in fact equivalent to $\epn$ if $T$ is recursively axiomatizable.
We may stratify the definition by restricting the complexity of the formulas. A consistent recursively axiomatizable classical theory never has $\epn$ for $\Pi^0_1$ formulas, or $\dp$ for $\Pi^0_1$ sentences, or $\dp$ for $\phi\in\Sigma^0_1$ and $\psi\in\Pi^0_1$. This leaves $\Sigma^0_1$ as the only realistic possibility. Friedman’s argument shows that for recursively axiomatized $T$, the following are equivalent:
$T$ has $\epn$ for $\Sigma^0_1$ formulas,
$T$ has $\dp$ for $\Sigma^0_1$ sentences,
$T$ is $\Sigma^0_1$-sound or inconsistent.
Naturally occurring theories are $\Sigma^0_1$-sound (e.g., PA) or assumed to be $\Sigma^0_1$-sound (e.g. ZFC).
See also Visser (§7) for an interesting connection of Friedman’s characterization to (non)interpretability of inconsistency.
