Has a conjecture ever originally been decided by constructing the proof with mathematical logic?

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.

For example:

• 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.

I do not know about a conjecture, but I would like to mention the Ax–Grothendieck_theorem.

A very nice way of proof is to show that the (first-order) theory $ACF_0$ of algebraically closed fields with characteristic zero is complete (through quantifier elimination iirc).

Thus, if the statement is false, there is a “somewhat” equivalent (because of the number of variables and degree of polynomials) first-order statement the negation of which can be proved in $ACF_0$.

Since the proof has finite length, there exists some prime $p$ such that the assumption “$p \neq 0$” is not used in the proof. So that first-order statement never holds in any algebraically closed field with characteristic $p$.

It remains to prove that the Ax-Grothendieck theorem holds in the algebraic closure of $\mathbb{F}_p$ for each prime $p$.

In a nutshell, we actually disprove the existence of a general disproof in $ACF_0$ ; since $ACF_0$ is complete, this entails the existence of a proof.

The original proof of the Halpern-Läuchli theorem seems to be the sort of thing you asked for. In their paper, Halpern and Läuchli first set up a formal deductive system and show that a certain formula is deducible in this system. Then they provide a semantics, i.e., meanings for the formulas of their system. They show that the system is sound, i.e., the meanings of deducible formulas are true. And finally, they note that the particular formula whose deducibility they established earlier has, as its meaning, the conclusion that they want to prove.

The MathSciNet citation for the paper is

MR0200172 (34 #71)

Halpern, J. D.; Läuchli, H.

A partition theorem.

Trans. Amer. Math. Soc. 124 1966 360–367.