Theorems which are proven by proving the existence of a formal proof without knowing the formal proof

Question

Let $L$ be a first order language. Let $T$ be a set of sentences in $L$ and $S$ a sentence in $L$. Let's define a meta-proof to be a proof that there exists a formal proof of $S$ from $T$.

Question: Are there sentences in the "known" mathematics whose meta-proof is known but whose formal proof is not known.

Remark: when we add constants/defintions to our language and prove the sentence in the new language, we know it works because there is a theorem that says that under suitable conditions a formal proof in the new language implies the existence of a formal proof in our original language. Therefore such a situation counts as an instance of a meta-proof without knowing the formal proof, but I would consider this trivial.

Thank you

Answer 1

Parikh sentences have a short proof that a proof exists but the actual proof can be very long, for example the number of symbols could be greater than the number of atoms in the universe. For a discussion see page 17 of A Universal Approach To Self-Referenctial Paradoxes, Incompleteness And Fixed Points by Noson Yanofsky. This paper is quite readable.

Paraphrasing this paper uses a diagonal argument to construct a sentence ${\mathcal{C}}_{n}$ which says "I do not have a proof of myself that is shorter than $n$."

There follows a short proof that there exists a proof of this sentence.

Answer 2

I use Polish notation. Consider the formula CCa$_1$Ca$_2$...Ca$_1$$_0$$_9$$_4$$_6$bCa$_1$Ca$_1$$_0$$_9$$_4$$_6$Ca$_2$Ca$_3$...Ca$_1$$_0$$_9$$_4$$_5$b. We can write out a meta-proof via something like the following:

The law of commutation CCpCqrCqCpr along with the deduction metatheorem allows us to interchange any variable a$_o$ in a well-formed formula of the form Ca$_1$Ca$_2$...Ca$_n$b:=A with any other variable a$_p$ and obtain a wff B from which we can derive A and conversely. Consequently, there exists a formal proof that CCa$_1$Ca$_2$...Ca$_1$$_0$$_9$$_4$$_6$bCa$_1$Ca$_1$$_0$$_9$$_4$$_6$Ca$_2$Ca$_3$...Ca$_1$$_0$$_9$$_4$$_5$b is a theorem of classical propositional calculus.

However, actually writing out the formal proof comes as another matter entirely, because it's almost surely too long for anyone to bother to write the proof. And even if someone writes such a proof or a computer writes such a proof, the relevant meta-theory ends up implying even longer wffs of this sort are theorems because there is no upper bound on the number of variables here... longer wffs which are theorems exist than could ever get written with all the resources of our entire galaxy.

So, yes, such sentences exist in known mathematics.