I would like an example of a sentence S whereby the statement Prov_T("S") has a non-constructive proof, where Prov_T("S") means "There exists a proof (in the system T) of the codification (e.g. Gödel number) of S."
That is, non-constructive existence proofs (whereby it is proven that an object with given properties exists without exhibiting the object itself) are common, but the ones I know about are not about (codifications of) proofs. I would like to be able to have a proof A that there is a proof B about something non-tautological. Of course, to be rigorous, one would further codify to bring it all onto one level, but an example with A and B being on two different levels is acceptable.