So, one of the things that mathematical logic does is study theorems as abstract objects. There also many theorems about mathematical logic, and these theorems can have connections to other fields.
Additionally, mathematical logic also proven that certain conjectures are not formally decidable within certain formal systems. This means that mathematicians need stronger formal systems to prove them.
However, has a mathematical theorem ever been proven by constructing the proof with mathematical logic? Or proving that a proof exists?
By this, I mean for statement $C$ which is a mathematical conjecture, instead of writing out a proof of $C$, they write either a constructive or nonconstructive proof that proof exists.
- Use proof theory to prove there are a sequence of inferences to lead to $C$ (this is implied by the previous two bullets, of course)
- Use model theory to prove that all models of some theory $T$, where $T$ is a theory that mathematicians typically use for proofs, satisfy $C$
- Use computer science to construct a program $P$, such that the Curry–Howard correspondence applied to $P$ results in a proof of $C$
What I am not looking for is examples where someone writes a proof of $C$, citing theorems from mathematical logic. In this case, they have actually written down a proof, not simply proved it exists. Like, that is still super cool, and has huge implications for the rest of mathematics, but I am asking about something different.
EDIT: If the conjecture uses a lemma $L$ that satisfies the above, that's fine. However, it must directly use the statement the lemma is stating, not the fact that is has abstractly been proven. That is, the proof of $C$ involves showing that $L$ implies $C$, not that the existence of a proof of $L$ implies $C$.
This is one technical caveat. T can not prove "$\forall C. Provable(C) \implies C$". Moreover, if it does for some $C$, it is vacuously true even within $T$, since one can technically just write a direct proof of $C$ in $T$. However, if $T$ is sound, then Provable(C) does in fact imply C. Since mathematicians usually implicitly assume that the theories they work in are sound (unless they are working in the theory for its meta-mathematical significance instead of its soundness), this should be acceptable. Moreover, proving a proof exists might be more tractable than writing the proof is some instances.