Proof theory: example of an existence proof of a proof?

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.

Thanks.

Excellent example, thanks; yes, please, more details

Quote:

Originally Posted by

**emakarov** Every mathematical theorem is a tautology :)

This depends on your definition of theorem. I consider, say, the Continuum Hypothesis as a valid but not tautological theorem, while you might require the full statement "L |= CH" as the theorem.

Quote:

Originally Posted by

**emakarov** The thing hat comes to mind is the Henkin's proof of completeness.

Thanks! Perfect example.

Quote:

Originally Posted by

**emakarov** Note, by the way, that any proof of Prov_T("S") is not

*essentially* nonconstructive because there is an algorithm (

Gödel–Gentzen negative translation) that turns any such proof into a constructive one. Please ask if you need more details about this.

Interesting. I will take you up on your offer of more details, as the Wiki link does not give the proof. I would like to see the proof before I see it as an algorithm. The double-negation method in Glivenko's theorem is an algorithm, but this is only valid for propositions without quantifiers, whereas the provability formula has the existence quantifier. Therefore there must be something more to the proof of Gödel–Gentzen for Peano. Do you have a link for this proof?