The article plays a little fast and loose with language

> For example, Gödel himself helped establish that the continuum hypothesis, which concerns the sizes of infinity, is undecidable, as is the halting problem

The continuum hypothesis is definitely not "undecidable" in the same way that the halting problem is undecidable. Though there are deep connections behind the two, the two notions of "undecidability" (logical independence in the former and Turing machine computability in the latter) are very different.

Also,

> He also showed that no candidate set of axioms can ever prove its own consistency.

This is powerful as a limiting result, but it has little direct impact for philosophy, because you wouldn't trust the consistency result of a system you suspect might be inconsistent to begin with because inconsistent systems can prove anything. So saying "my axioms prove themselves consistent" shouldn't have increased your trust in those axioms to begin with in the absence of the incompleteness theorems.

I'm not really a fan of "true-but-unprovable" as short-hand the incompleteness theorems, because that hinges a lot on what kind of logic system you're in and how that logic system defines "truth" (taken at face value, how do we know that Godel's incompleteness theorem is "true?").

I prefer rather to pose two questions to reflect on that I think illuminate Godel's incompleteness theorems some more. Most modern logical systems (e.g. first-order logic and its various extensions and variants) equate unproveability with logical independence. So with that in mind, here's two questions.

First, Conway's Game of Life:

Conway's Game of Life seem like they should be subject to Godel's incompleteness theorems. It is after all powerful enough to be Turing-complete.

Yet its rules seem clearly complete (they unambiguously specify how to implement the Game of Life enough that different implementation of the Game of Life agree with each other).

So what part of Game of Life is incomplete? What new rule (i.e. axiom) can you add to Conway's Game of Life that is independent of its current rules? Given that, what does it mean when I say that "its rules seem clearly complete?" Is there a way of capturing that notion? And if there isn't, why haven't different implementations of the game diverged? If you don't think that the Game of Life should be subject to Godel's Incompleteness Theorems why? Given that it's Turing complete it seems obviously as powerful as any other system.

Second, again, in most logical systems, another way of stating that consistency is unproveable is that consistency of a system S is independent of the axioms of that system. However, that means that the addition of a new axiom asserting that S is either consistent or inconsistent are both consistent with S. In particular, the new system S' that consists of the axioms of S with the new axiom "S is inconsistent" is consistent if S is consistent.

What gives? Do we have some weird "superposition" of consistency and inconsistency?

Hints (don't read them until you've given these questions some thought!):

1. Consider questions of the form "eventually" or "never." Can those be turned into axioms? If you decide instead to tackle the question of applicability of the incompleteness theorems, what is the domain of discourse when I say "clearly complete?" What exactly is under consideration?

2. Consider carefully what Godel's arithmetization of proofs gives you. What does Godel's scheme actually give you when it says it's "found" a contradiction? Does this comport with what you would normally agree with? An equivalent way of phrasing this hint, is what is the actual statement in Godel's arithmetization scheme created when we informally say "S is inconsistent?"

At the end of the day, the philosophical implications of Godel's incompleteness theorems hinge on whether you believe that it is possible to unambiguously specify what the entirety of the natural numbers are and whether they exist as a separate entity (i.e. does "infinity" exist in a real sense? Is there a truly absolute standard model of the natural numbers?).