Suppose that we wanted to construct a mathematical universe where all objects were computable in some sense. How would we do it?
Well, we could certainly allow the set into our universe: natural numbers are the most basic computational objects there are. (Notation: I’ll use to refer to when we’re considering it as part of the universe we’ll building, and just when we’re talking about the set of natural numbers in the “real” world.) What should we take as our set of functions from to ? Since we want to admit only computable things, we should let be the set of computable functions from to , which we can represent non-uniquely by their indices (i.e., by the programs which compute them).
(For clarity, I’ll use the following notation for computable functions: denotes the partial function from to computed by the th Turing machine. Given , it is possible that the computation never halts; in that case, I’ll write and say that is undefined. If it does halt, I’ll write and say that is defined. If it halts, then it yields an output . To indicate what it is, I’ll write or .)
So, we’ve decided that should equal . What should equal? At this point, there is a slight subtlety: It’s not simply the set of computable functions from (considered as a subset of ) to (considered as ), because we would like to only admit those functions from to that return the same number when given inputs which represent the same element of .
Therefore, we’ll let be the set of such that, for all , , and whenever are such that for all , , then .
We can similarly define , except that there are now two places where we should take into account that we consider equivalent if for all , : We’ll let be the set of such that, whenever are equivalent in the aforementioned sense, and are defined and equivalent in the aforementioned sense.
In a similar fashion, we can define and so on; these sets are called the sets of hereditarily computable functions.
Can we generalize this construction to a category that incorporates all possible computable representations of real objects? More ambitiously, can we generalize to a category that is a genuine mathematical universe in the sense that questions like “Does the Riemann Hypothesis hold in this category?” are meaningful? The answer, due to Martin Hyland, is yes.