I’d like to share a simple proof I’ve discovered recently of a surprising fact: there is a universal algorithm, capable of computing any given function!
Wait, what? What on earth do I mean? Can’t we prove that some functions are not computable? Yes, of course.
What I mean is that there is a universal algorithm, a Turing machine program capable of computing any desired function, if only one should run the program in the right universe. There is a Turing machine program with the property that for any function on the natural numbers, including non-computable functions, there is a model of arithmetic or set theory inside of which the function computed by agrees exactly with on all standard finite input. You have to run the program in a different universe in order that it will compute your desired function .
Theorem There is a Turing machine program , carrying out the specific algorithm described in the proof, such that for any function , there is a model of arithmetic , or indeed a model of set theory or more (if consistent), such that the function computed by program inside agrees exactly with on all standard finite input.

The proof is elementary, relying essentially only on the ideas of the classical proof of the Gödel-Rosser theorem. To briefly review, for any computably axiomatized theory extending , there is a corresponding sentence , called the Rosser sentence, which asserts, “for any proof of in , there is a smaller proof of .” That is, by smaller, I mean that the Gödel-code of the proof is smaller. One constructs the sentence by a simple application of the Gödel fixed-point lemma, just as one constructs the usual Gödel sentence that asserts its own non-provability. The basic classical facts concerning the Rosser sentence include the following:
- If is consistent, then so are both and
- proves .
- The theories , and are equiconsistent.
- If is consistent, then does not prove .
The first statement is the essential assertion of the Gödel-Rosser theorem, and it is easy to prove: if is consistent and , then the proof would be finite in the meta-theory, and so since would have to prove that there is a smaller proof of , that proof would also be finite in the meta-theory and hence an actual proof, contradicting the consistency of . Similarly, if , then the proof would be finite in the meta-theory, and so would be able to verify that is true, and so , again contradicting consistency. By internalizing the previous arguments to PA, we see that will prove that neither nor are provable in , making vacuously true in this case and also establishing and , for the second and third statements. In particular, , which implies that does not prove by the incompleteness theorem applied to the theory , for the fourth statement.
Let’s now proceed to the proof of the theorem. To begin, we construct what I call the Rosser tree over a c.e. theory . Namely, we recursively define theories for each finite binary string , placing the initial theory at the root, and then recursively adding either the Rosser sentence for the theory or its negation at each stage to form the theories at the next level of the tree.
Each theory is therefore a finite extension of by successively adding the appropriate Rosser sentences or their negations in the pattern described by . If the initial theory is consistent, then it follows by induction using the Gödel-Rosser theorem that all the theories in the Rosser tree are consistent. Extending our notation to the branches through the tree, if is an infinite binary sequence, we let be the union of the theories arising along that branch of the Rosser tree. In this way, we have constructed a perfect set of continuum many distinct consistent theories.
I shall now describe a universal algorithm for the case of computing binary functions. Consider the Rosser tree over the theory . This is a consistent theory that happens to prove its own inconsistency. By considering the Gödel-codes in order, the algorithm should begin by searching for a proof of the Rosser sentence or its negation in the initial theory . If such a proof is ever found, then the algorithm outputs or on input , respectively, depending on whether it was the Rosser sentence or its negation that was found first, and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory. Then, it starts searching for a proof of the Rosser sentence of that theory or its negation. At each stage in the algorithm, there is a current theory , depending on which prior proofs have been found, and the algorithm searches for a proof of or . If found, it outputs or accordingly (on input ), and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory.
If is any binary function on the natural numbers, then let be the theory arising from the corresponding path through the Rosser tree, and let be a model of this theory. I claim that the universal algorithm I just described will compute exactly on input inside this model. The thing to notice is that because was part of the initial theory, the model will think that all the theories in the Rosser tree are inconsistent. So the model will have plenty of proofs of every statement and its negation for any theory in the Rosser tree, and so in particular, the function computed by in will be a total function. The question is which proofs will come first at each stage, affecting the values of the function. Let and notice that is true in . Suppose inductively that the function computed by has worked correctly below in , and consider stage of the procedure. By induction, the current theory will be exactly , and the algorithm will be searching for a proof of or its negation in . Notice that just in case is true in , and because of what asserts and the fact that thinks it is provable in , it must be that there is a smaller proof of . So in this case, the algorithm will find the proof of first, and therefore, according to the precise instructions of the algorithm, it will output on input and add (the opposite statement) to the current theory, moving to the theory in the Rosser tree. Similarly, if , then will be true in , and the algorithm will therefore first find a proof of , give output and add to the current theory, moving to . In this way, the algorithm finds the proofs in exactly the right way so as to have as the current theory at stage and thereby compute exactly the function , as desired.
Basically, the theory asserts exactly that the proofs will be found in the right order in such a way that program will exactly compute on all standard finite input. So every binary function is computed by the algorithm in any model of the theory .
Let me now explain how to extend the result to handle all functions , rather than only the binary functions as above. The idea is simply to modify the binary universal algorithm in a simple way. Any function can be coded with a binary function in a canonical way, for example, by having successive blocks of s in , separated by s, with the block of size . Let be the algorithm that runs the binary universal algorithm described above, thereby computing a binary sequence, and then extract from that binary sequence a corresponding function from to (this may fail, if for example, the binary sequence is finite or if it has only finitely many s). Nevertheless, for any function there is a binary function coding it in the way we have described, and in any model , the binary universal algorithm will compute , causing this adapted algorithm to compute exactly on all standard finite input, as desired.
Finally, let me describe how to extend the result to work with models of set theory, rather than models of arithmetic. Suppose that is a consistent c.e. extension of ZFC; perhaps it is ZFC itself, or ZFC plus some large cardinal axioms. Let be a slightly stronger theory, which is also consistent, by the incompleteness theorem. Since interprets arithmetic, the theory of Rosser sentences applies, and so we may build the corresponding Rosser tree over , and also we may undertake the binary universal algorithm using as the initial theory. If is any binary function, then let be the theory arising on the corresponding branch through the Rosser tree, and suppose . This is a model of , which also thinks that is inconsistent. So again, the universal algorithm will find plenty of proofs in this model, and as before, it will find the proofs in just the right order that the binary universal algorithm will compute exactly the function . From this binary universal algorithm, one may again design an algorithm universal for all functions , as desired.
One can also get another kind of universality. Namely, there is a program , such that for any finite , there is a model of (or , etc.) such that inside the model , the program will enumerate the set and nothing more. One can obtain such a program from the program of the theorem: just let run the universal binary program until a double is produced, and then interprets the finite binary string up to that point as the set to output.
Let me now also discuss another form of universality.
Corollary
There is a program , such that for any model and any function that is definable in , there is an end-extension of to a taller model such that in , the function computed by program agrees exactly with on input in .
Proof
We simply apply the main theorem inside . The point is that if thinks , then it can build what it thinks is the tree of Rosser extensions, and it will think that each step maintains consistency. So the theory that it constructs will be consistent in and therefore have a model (the Henkin model) definable in , which will therefore be an end-extension of .
QED
This last application has a clear affinity with a theorem of Woodin’s, recently extended by Rasmus Blanck and Ali Enayat. See Victoria Gitman’s posts about her seminar talk on those theorems: Computable processes can produce arbitrary outputs in nonstandard models, continuation.
Alternative proof. Here is an alternative elegant proof of the theorem based on the comments below of Vadim Kosoy. Let be any consistent computably axiomatizable theory interpreting PA, such as PA itself or ZFC or what have you. For any Turing machine program , let be a program carrying out the following procedure: on input , search systematically for a finite function , with finite and , and for a proof of the statement “program does not agree with on all inputs in ,” using the function simply as a list of values for this assertion. For the first such function and proof that is found, if any, give as output the value .
Since the function is computable, there is by Kleene’s recursion theorem a program for which and compute the same function, and furthermore, proves this. So the program is searching for proofs that itself does not behave in a certain way, and then it is behaving in that way when such a proof is found.
I claim that the theory does not actually prove any of those statements, “program does not agree with on inputs in ,” for any particular finite function . If it did prove such a statement, then for the smallest such function and proof, the output of would indeed be on all inputs in , by design. Thus, there would also be a proof that the program did agree with this particular , and so would prove a contradiction, contrary to our assumption that it was consistent. So actually proves none of those statements. In particular, the program computes the empty function in the standard model of arithmetic. But also, for any particular finite function , we may consistently add the assertion “program agrees with on inputs in ” to , since did not refute this assertion.
For any function , let be the theory together with all assertions of the form “program halts on input with value ”, for the particular value . I claim that this theory is consistent, for if it is not, then by compactness there would be finitely many of the assertions that enable the inconsistency, and so there would be a finite function , with , such that proved the program does not agree with on inputs in . But in the previous paragraph, we proved that this doesn’t happen. And so the theory is consistent.
Finally, note that in any model of , the program computes the function on standard input, because these assertions are exactly made in the theory. QED