Is there any direct application of Gödel's Theorems outside of logic?

Question

Gödel's incompleteness theorems was a major achievement with ramifications outside the field of mathematics itself. Are there any direct applications of the theorem(s), or any of the methods pioneered in the proof(s) outside the field of logic itself but within mathematics itself. For example, say in Category Theory.

Answer 1

To apply Gödel's incompleteness theorems one needs to be working with formal theories. Whether or not there are mathematical applications outside logic depends on how one draws the boundary of logic, as a subfield of mathematics.

For example, consider the Paris–Harrington theorem which shows that a certain statement of Ramsey theory, formulable in the language of arithmetic, implies the consistency of Peano arithmetic (PA). The Paris–Harrington sentence is a natural combinatorial statement which, by Gödel's second incompleteness theorem, is not provable in our usual system of first-order arithmetic.

There are a number of morals which one could draw from this theorem, but the one I want to call attention to here is this: there are number-theoretic propositions which go beyond our usual axioms for arithmetic, and which we must account for. If we hold the Paris–Harrington statement to be true then we're committed to stronger mathematical axioms than PA; for instance, we might want to assert that we can perform induction up to $\varepsilon_0$ and not just $\omega$ (since this is the usual way the consistency of PA is proved).

In fact a common use of the second incompleteness theorem is to draw boundaries to provability within certain formal systems. For example, we know that we can't prove a version of the Montague–Levy reflection theorem for infinite, rather than finite sets of sentences, because if we could then one of the infinite sets of sentences we could reflect would be the axioms of ZFC itself. Thus we'd have shown in ZFC that ZFC has a model, proving Con(ZFC) and contradicting the second incompleteness theorem. This also gives us the following corollary: ZFC is not finitely axiomatisable.

Assume for a contradiction that there is some finite set of sentences $\Phi$ such that for every formula $\varphi$ in $\mathcal{L}_\in$, $\Phi \vdash \varphi \Leftrightarrow \mathrm{ZFC} \vdash \varphi$. Of course this means that every axiom $\psi \in \Phi$ is a theorem of ZFC. So by the reflection theorem, there is some $V_\alpha$ such that $V_\alpha \models \Phi$. But by our assumption such a model will also be a model of ZFC, so Con(ZFC), contradicting the second incompleteness theorem.

Again, is this an application within logic? If set theory is part of logic, yes. But direct applications of Gödel's results will only ever show up when we deal with formal systems, so if we say that anytime we do that we're working within logic, then by definition they won't be applicable outside of it. Nonetheless incompleteness is, I would argue, a deep phenomenon; the only reason it doesn't appear more often—or more obviously—in mathematics is just that many results are proved in areas which employ in the background systems like ZFC which are far stronger than they need, and that mathematicians are often not careful about stipulating precisely what resources (that is to say, axioms) they do assume.