Meta proof-searching Suppose you have a particular theory (ex: $ZFC$) in which you want to prove a statement $\phi$. One can attempt to find a proof of $\phi$ that can be verified, but another tactic can be to find a proof for the existence of a proof of $\phi$
Are there any examples of such "non constructive proof of proofs" where someone proved that "a proof of $\phi$" exists but did not explicitly find that proof itself? I am curious if for certain problems this would be more tractable/efficient to compute the original proof of the sentence.
 A: It has not turned out to be very helpful to prove that specific theorems are provable indirectly, when no actual proof of the theorem was previously known. 
There are two settings in mathematical logic, however, where we do show indirectly that particular theorems are provable in particular systems or in particular ways. The difference is that, when we work with particular theorems in these settings, we already know (or assume) the theorems are provable in general, and we are just worried with the specific form of a proof.
The first setting is related to cut elimination. Certain kinds of formal proofs are called "cut free"; these are of a particularly simple form. A general theorem shows that, in many systems, if a theorem is provable then it is provable via a cut free proof. This theorem is effective - there is a procedure to create a cut free formal proof from an arbitrary formal proof. But the size of the cut free proof is often much, much larger than the size of the original proof. So we rarely work with cut-free proofs explicitly. They are used primarily as hypothetical objects. 
The second setting is related to showing that particular theorems are provable in weak systems. Sometimes, it can be shown that if a theorem of some particular syntactic form is provable in a stronger system $S$, then it is also provable in a weaker system $W$. These are called "conservation results". 
For example, a $\Pi^0_2$ theorem that is provable in the system $\mathsf{WKL}_0$ of second-order arithmetic is also provable in the system $\mathsf{PRA}$ of first-order primitive recursive arithmetic.  It is much, much easier to work in $\mathsf{WKL}_0$ than $\mathsf{PRA}$. For example, Kikuchi and Tanaka (1994) showed that certain versions of the incompleteness theorem are provable in $\mathsf{PRA}$ by showing that the theorems are provable in $\mathsf{WKL}_0$, where they can use much more general methods. This only gives a theoretical provability result – no actual proof in $\mathsf{PRA}$ is constructed. In principle, the conservation result gives a method to turn a formal proof in $\mathsf{WKL}_0$ into a formal proof in $\mathsf{PRA}$, but the theoretical provability is of primary interest, not the actual formal proof.  
Many conservation results are known. Another example is Shoenfield's absoluteness theorem, which is often used to show that particular results are theoretically provable in ZF set theory, based on the syntactic form of the theorem and the provability of the theorem in ZFC.  This allows us to show that some theorems of particular syntactic forms are provable without the axiom of choice based on their provability in ZFC with the axiom of choice . 
A: Gödel proved that theories like ZFC (or any theory with enough structure to have arithmetic, for that matter) is either complete (all statements are provable, even statements such as "ZFC proves that ZFC proves that ZFC proves that ... $\varphi$) but inconsistent (derive contradictions from tje axioms) or consistent (not-inconsistent) but incomplete (there are statements you can not prove, such as the negation of a given $\varphi$ or the statement "ZFC is consistent"). Therefore, if you ask for the general method to find a proof that a certain proof exists, then you are assuming ZFC et al to be complete. But by Gödel's theorems, that would yield your theory inconsistent and the game is over.
