archives

Computational equivalent of incompleteness theorems?

Godel's Incompleteness Theorems are well-known, but I haven't come across any interpretation of incompleteness in terms of computation that aren't typed. neelk's comment is a great example of how it applies to programming language type systems via Curry-Howard, but I'm looking for an untyped correspondence, like at the level of the raw lambda calculus or Turing machines.

For instance, if I squint, the Halting Problem looks very much like an instance of the first incompleteness theorem. No program H can be constructed which can compute the termination value of every other program, ie. there are programs which halt but for which H cannot compute that fact.

Wikipedia isn't much help here, implying there is some established connection, but not describing it in any accessible way or providing useful pointers.

Has such a correspondence been established? Hopefully I'm not spewing nonsense and someone can point me in the right direction!