"Exists X | P(X)" holds but for no X does P(X) hold

Question

Is there a known case in any classical logic rich enough to obey the Incompleteness Theorem in which:

$$\exists x \space | \space P(x) $$

yet at the same time:

$$\forall x \space \not \exists G \space | \space Proof(G, P(x))$$

where $Proof(G, P)$ is the relation that $G$ is a proof of $P$ ?

Answer 1

Your question is a little unclear, but the following observation shows that the answer is yes according to all interpretations I can come up with (in particular, I think by "logic" you mean "theory"):

There is a consistent recursively axiomatizable theory $T$ containing PA, and a formula $\varphi$ in the language of $T$, such that $T\vdash\exists x\varphi(x)$ but for each term $t$ in the language of $T$ do we have $T\vdash\neg \varphi(t)$.

Proof: Just take $T$ to be PA + "PA is inconsistent," and let $\varphi(x)$ be "$x$ is a PA-proof of $0=1$." $T$ can "analyze proofs," and so for any specific term $t$ can check that $t$ does not correspond to a PA-proof of $0=1$. $\quad\Box$

(Note that the terms here correspond exactly to the standard natural numbers, and a model of PA is nonstandard exactly when it has an element not corresponding to any term.) The above is an example of $\omega$-inconsistency. Note that in order for this to occur, $T$ must have the property that any model of $T$ must have many elements not corresponding to any term.

We can also whip up a slightly less exciting phenomenon in a more natural theory:

There is a formula $\psi$ such that PA proves $\exists x\psi(x)$ but for no term $t$ does PA prove $\psi(t)$.

(Note that assuming that PA is sound, we can't possibly get the stronger phenomenon of PA$\vdash\neg\psi(t)$ for each term $t$.)

Proof: Let $\psi(x)$ be the formula "(PA is inconsistent and $x=1$) or (PA is consistent and $x=0$)." Then PA proves $\psi(0)\vee\psi(1)$, but can't prove either $\psi(0)$ or $\psi(1)$ specifically. $\quad\Box$