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

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.