We have shown in my logic lecture that PA (and even the weaker subsystem Q) are complete with respect to $\Sigma_0^1$-Sätzen. A $\Sigma_0^1$-Satz is a closed formula of the form $\exists v_0\exists v_1 ... \exists v_ n \phi$ where $\phi$ is a $\Delta_0^0$-formula. A $\Delta_0^0$-formula is a formula which is build from atomic formulas and bounded quantifiers.
The completeness result we have shown is : if $\phi$ is a $\Sigma_0^1$-Satz and the interpration of $\phi$ is true in the standard model of the natural numbers (sitting inside ZFC) then there is a formal proof of $\phi$ in the formal system $Q$ (and thus also in PA). The proof proceeds as follows.
If the interpretation of $\phi = \exists v_0... \exists v_k\psi$ is true, then there must be some numbers $n_0,...,n_k$ such that the interpretation of $\psi [\overline{n_0}/v_0,....,\overline{n_k}/v_k]$ is true. We have previously shown (in a constructive manner) how to produce from the truth of a $\Delta_0^0$-Satz a formal proof of it in the system Q. Hence, using this proof and a sequence of existence introductions we find a proof of $\phi$.
So here is my question. The explicit construction on the proof of $\phi$ depends on us knowing explicit numbers $n_0,...,n_k$ evaluated at which $\psi$ is true.
Is it possible to cook up a $\phi= \Sigma_0^1$-sentence $\exists v_0 ...\exists v_k\psi$ such that we can proof classically that the interpretation of the sentence in $\mathbb N$ is true, but we are unable to pin down any concrete numbers $n_0,...,n_k$ such that $\psi$ evaluated at the corresponding numerals is true? Maybe because the proof of the truth of $\phi$ uses the law of excluded middle or reductio ad absurdum or something similar. In such a situation we would know that there is a proof of $\phi$ in Q, but we wouldn't be able to write it down.