Examples of “Non-Logical Theorems” Proven by Logic

I am still an undergraduate student, and so perhaps I just haven't seen enough of the mathematical world.

Question: What are some examples of mathematical logic solving open problem outside of mathematical logic?

Note that the Ax-Grothendieck Theorem would have been a perfect example of this (namely, If $P$ is a polynomial function from $\mathbb{C}^n$ to $\mathbb{C}^n$ and $P$ is injective then $P$ is bijective). However, even though there is a beautiful logical proof of this result, it was first proven not specifically using mathematical logic. I'm curious as to whether there are any results where "the logicians got there first".

Edit 1:Bonus: I am quite curious if one can post an example from Reverse Mathematics.

Edit 2:This post reminded me that the solution to Whitehead's Problem came from logic (a problem in group theory). According to the wikipedia article, the proof by Shelah was 'completely unexpected'. It utilizes the fact that ZFC+(V=L) implies every Whitehead group is free while ZFC+$\neg$CH+MA implies there exists a Whitehead group which is not free. Since these two separate axiom systems are equiconsistent, hence Whitehead's problem is undecidable.

-
What's "mathematical logic" in this case? –  Asaf Karagila Jul 28 '14 at 23:14
You can find many examples of applications of model theory in this MathOverflow thread. –  Alex Kruckman Jul 28 '14 at 23:42
I believe Ramsey's theorem was motivated by a problem in mathematical logic, but I guess that's not what you're looking for. Well, sticking with Ramsey theory, what about the Halpern-Läuchli partitio theorem? Wasn't that proved using mathematical logic? –  bof Jul 28 '14 at 23:43
I agree with @bof that the Halpern-Läuchli theorem is a good example. The original proof involved a custom-designed deductive system for efficiently handling the complicated nested quantifier combinations that need to be manipulated in the proof. –  Andreas Blass Jul 29 '14 at 7:13

The Tarski–Seidenberg theorem says that the set of semialgebraic sets is closed under projection. It's a pure real-algebraic statement that was originally proved with logic.

Jacobson says this in chapter 5 of his Basic Algebra I:

More generally, Tarski's theorem implies his metamathematical principle that any "elementary" sentence of algebra which is true in one real closed field (e.g., the field of real numbers) is true in every real closed field.

-

I was impressed by Bernstein and Robinson's 1966 proof that if some polynomial of an operator on a Hilbert space is compact then the operator has an invariant subspace. This solved a particular instance of invariant subspace problem, one of pure operator theory without any hint of logic.

Bernstein and Robinson used hyperfinite-dimensional Hilbert space, a nonstandard model, and some very metamathematical things like transfer principle and saturation. Halmos was very unhappy with their proof and eliminated non-standard analysis from it the same year. But the fact remains that the proof was originally found through non-trivial application of the model theory.

Another example is the solution to the Hilbert's tenth problem by Matiyasevich. Hilbert asked for a procedure to determine whether a given polynomial Diophantine equation is solvable. This was a number theoretic problem, and he did not expect that such procedure can not exist. Proving non-existence though required developing a branch of mathematical logic now called computability theory (by Gödel, Church, Turing and others) that formalizes the notion of algorithm. Matiyasevich showed that any recursively enumerable set can be the solution set for a Diophantine equation, and since not all recursively enumerable sets are computable there can be no solvability algorithm.

This example is typical of how logic serves all parts of mathematics by saving effort on doomed searches for impossible constructions, proofs or counterexamples. For instance, an analyst might ask if the plane can be decomposed into a union of two sets, one at most countable along every vertical line, and the other along every horizontal line. It seems unlikely and people could spend a lot of time trying to disprove it. In vain, because Sierpinski proved that existence of such a decomposition is equivalent to the continuum hypothesis, and Gödel showed that disproving it is impossible by an elaborate logical construction now called inner model. As is proving it as Cohen showed by an even more elaborate logical construction called forcing.

-
Do you mean "recursively enumerable"rather than "recursive" at the end of the second paragraph? –  Ned Jul 29 '14 at 22:52
Yes, sorry about that –  Conifold Jul 29 '14 at 23:07
Your first example sounds very convincing, but Hilbert's tenth problem has the concept of algorithm (or procedure, or whatever you call it) in the statement and so must be solved by developing a formalization of this. It's not surprising that this was, in fact, the case, and whether the resulting theory is actually a branch of logic is both an opinion and sort of incidental. –  Ryan Reich Jul 30 '14 at 2:55
@ Ryan Reich Only if you assume it was impossible. Euclid's algorithm existed for centuries without formalization of algorithms, and belongs to number theory as would a Diophantine algorithm if it existed. The ellipse method for linear programming was developed after formalization, and didn't use much of it. Hilbert, a founder of logic, didn't think it was impossible or needed formalization. The arguments Matiyasevich used (recursive deconstruction of expressions) are exactly of the type used in logic, which is why computability theory was developed by many of the same people as logic. –  Conifold Jul 30 '14 at 23:10
And even if you assume it was impossible the non-existence of algorithms for squaring a circle with Euclidean tools, or for solving equations in radicals was proved long before formalization of algorithms, so there is no "must" there, and it was "surprising". I am not sure what "incidental" means, but that the type of computability theory used in the proof "is a field of mathematical logic" even according to Wikipedia, and their "main professional organization" is called Association for Symbolic Logic en.wikipedia.org/wiki/Computability_theory#Name_of_the_subject. –  Conifold Jul 30 '14 at 23:51

Not sure if this qualifies, but Goodstein's theorem which appears quite number theoretic and states that any Goodstein sequence converges, was proved using ordinals.

-
... and it is interesting that you cannot do without ordinals, in some sense. (Details can be found at the wikipedia page.) –  Martin Brandenburg Jul 29 '14 at 18:01

So automated theorem provers consist of an application of mathematical logic. Consequently, the solution of the Robbins conjecture by William McCune using EQP qualifies as solving an open problem outside of mathematical logic by using mathematical logic.

-
Impressive formulas: math.colgate.edu/~amann/MA/robbins_complete.pdf –  Martin Brandenburg Jul 30 '14 at 19:46

The compactness theorem gives many ways to generate theorems of the form "if all finite $X$s have property $P$, then so do all infinite $X$s".

A random example from Bell and Slomson Models and Ultraproducts:

Let $B$ be an infinite set of boys each of whom has at most a finite number of girlfriends. If for each integer $k$, any $k$ of the boys have between them at least $k$ girlfriends, then it is possible for each boy to marry one of his girlfriends without any of them committing bigamy.

This can be deduced (with some work) by using the compactness theorem with this finite version of the lemma:

If $C$ is a set of $m$ boys and for each $k\le m$, any k of the boys have at least k girlfriends between them, then it is possible for each boy to marry one of his girlfriends without any of them committing bigamy.

There are a number of better examples here: Most astonishing applications of compactness theorem outside logic

(Although if you're looking for real world applications of logic, I think type theory for programming languages is a big one.)

-