Computation and model theory

Back when we first described computability in the computer science series, we commented that the idea of computability was that there were certain functions that couldn’t be written down or imagined.

While this should be obvious even without a specific example (some randomly chosen function needs an infinite amount of data to store, and cannot be expected to have an algorithm to calculate it), we do have a particular simple example in the form of the halting problem that we will discuss in the next article – the function that maps programs to whether or not they halt is uncomputable; you can’t write down an algorithm to calculate it.

So what exactly does “writing something down” mean? Is “the function that maps programs to whether they halt” a description of a function that writes it down? Is it sufficient to “understand” what a function “is”, or is it only providing an algorithm that counts as “writing it down precisely”?

(Here’s an intuitive description of why “understanding what the function is” is not the same as “providing an algorithm” – asking “will this program ever halt” is, without an algorithm to compute the answer, a question that requires storing an infinite amount of time stamps to answer; similar to how storing an arbitrary function requires an infinite amount of data.)

We want to formalize the notion of “writing something down” (hereby language) in an axiomatic system (hereby theory).

Consider a formal system whose sentences include whether or not each program halts.