This is the third in a series of posts I’ve made recently concerning what I call the universal algorithm, which is a program that can in principle compute any function, if only you should run it in the right universe. Earlier, I had presented a few elementary proofs of this surprising theorem: see Every function can be computable! and A program that accepts exactly any desired finite set, in the right universe.

$$Those arguments established the universal algorithm, but they fell short of proving Woodin’s interesting strengthening of the theorem, which explains how the universal algorithm can be extended from any arithmetic universe to a larger one, in such a way so as to extend the given enumerated sequence in any desired manner. Woodin emphasized how his theorem raises various philosophical issues about the absoluteness or rather the non-absoluteness of finiteness, which I find extremely interesting.

Woodin’s proof, however, is a little more involved than the simple arguments I provided for the universal algorithm alone. Please see the paper Blanck, R., and Enayat, A. Marginalia on a theorem of Woodin, The Journal of Symbolic Logic, 82(1), 359-374, 2017. doi:10.1017/jsl.2016.8 for a further discussion of Woodin’s argument and related results.

What I’ve recently discovered, however, is that in fact one can prove Woodin’s stronger version of the theorem using only the method of the elementary argument. This variation also allows one to drop the countability requirement on the models, as was done by Blanck and Enayat. My thinking on this argument was greatly influenced by a comment of Vadim Kosoy on my original post.

It will be convenient to adopt an enumeration model of Turing computability, by which we view a Turing machine program as providing a means to computably enumerate a list of numbers. We start the program running, and it generates a list of numbers, possibly finite, possibly infinite, possibly empty, possibly with repetition. This way of using Turing machines is fully Turing equivalent to the usual way, if one simply imagines enumerating input/output pairs so as to code any given computable partial function.

Theorem.(Woodin) There is a Turing machine program $e$ with the following properties.

1. $\text{PA}$ proves that $e$ enumerates a finite sequence of numbers.
2. For any finite sequence $s$, there is a model $M$ of $\text{PA}$ in which program $e$ enumerates exactly $s$.
3. For any model $M$ in which $e$ enumerates a (possibly nonstandard) sequence $s$ and any $t\in M$ extending $s$, there is an end-extension $N$ of $M$ in which $e$ enumerates exactly $t$.

It is statement (3) that makes this theorem stronger than merely the universal algorithm that I mentioned in my earlier posts and which I find particularly to invite philosophical speculation on the provisional nature of finiteness. After all, if in one universe the program $e$ enumerates a finite sequence $s$, then for any $t$ extending $s$ — we might imagine having painted some new pattern $t$ on top of $s$ — there is a taller universe in which $e$ enumerates exactly $t$. So we need only wait long enough (into the next universe), and then our program $e$ will enumerate exactly the sequence $t$ we had desired.

Proof. This is the new elementary proof.  Let’s begin by recalling the earlier proof of the universal algorithm, for statements (1) and (2) only. Namely, let $e$ be the program that undertakes a systematic exhaustive search through all proofs from $\text{PA}$ for a proof of a statement of the form, “program $e$ does not enumerate exactly the sequence $s$,” where $s$ is an explicitly listed finite sequence of numbers. Upon finding such a proof (the first such proof found), it proceeds to enumerate exactly the numbers appearing in $s$.  Thus, at bottom, the program $e$ is a petulant child: it searches for a proof that it shouldn’t behave in a certain way, and then proceeds at once to behave in exactly the forbidden manner.

(The reader may notice an apparent circularity in the definition of program $e$, since we referred to $e$ when defining $e$. But this is no problem at all, and it is a standard technique in computability theory to use the Kleene recursion theorem to show that this kind of definition is completely fine. Namely, we really define a program $f(e)$ that performs that task, asking about $e$, and then by the recursion theorem, there is a program $e$ such that $e$ and $f(e)$ compute the same function, provably so. And so for this fixed-point program $e$, it is searching for proofs about itself.)

It is clear that the program $e$ will enumerate a finite list of numbers only, since either it never finds the sought-after proof, in which case it enumerates nothing, and the empty sequence is finite, or else it does find a proof, in which case it enumerates exactly the finitely many numbers explicitly appearing in the statement that was proved. So $\text{PA}$ proves that in any case $e$ enumerates a finite list. Further, if $\text{PA}$ is consistent, then you will not be able to refute any particular finite sequence being enumerated by $e$, because if you could, then (for the smallest such instance) the program $e$ would in fact enumerate exactly those numbers, and this would be provable, contradicting $\text{Con}(\text{PA})$. Precisely because you cannot refute that statement, it follows that the theory $\text{PA}$ plus the assertion that $e$ enumerates exactly $s$ is consistent, for any particular $s$. So there is a model $M$ of $\text{PA}$ in which program $e$ enumerates exactly $s$. This establishes statements (1) and (2) for this program.

Let me now modify the program in order to achieve the key third property. Note that the program described above definitely does not have property (3), since once a nonempty sequence $s$ is enumerated, then the program is essentially finished, and so running it in a taller universe $N$ will not affect the sequence it enumerates. To achieve (3), therefore, we modify the program by allowing it to add more to the sequence.

Specfically, for the new modified version of the program $e$, we start as before by searching for a proof in $\text{PA}$ that the list enumerated by $e$ is not exactly some explicitly listed finite sequence $s$. When this proof is found, then $e$ immediately enumerates the numbers appearing in $s$. Next, it inspects the proof that it had found. Since the proof used only finitely many $\text{PA}$ axioms, it is therefore a proof from a certain fragment ${\text{PA}}_n$, the ${\mathrm{\Sigma }}_n$ fragment of $\text{PA}$. Now, the algorithm $e$ continues by searching for a proof in a strictly smaller fragment that program $e$ does not enumerate exactly some explicitly listed sequence $t$ properly extending the sequence of numbers already enumerated. When such a proof is found, it then immediately enumerates (the rest of) those numbers. And now simply iterate this, looking for new proofs in still-smaller fragments of $\text{PA}$ that a still-longer extension is not the sequence enumerated by $e$.

Succinctly: the program $e$ searches for a proof, in a strictly smaller fragment of $\text{PA}$ each time, that $e$ does not enumerate exactly a certain explicitly listed sequence $s$ extending whatever has been already enumerated so far, and when found, it enumerates those new elements, and repeats.

We can still prove in $\text{PA}$ that $e$ enumerates a finite sequence, since the fragment of $\text{PA}$ that is used each time is going down, and $\text{PA}$ proves that this can happen only finitely often. So statement (1) holds.

Again, you cannot refute that any particular finite sequence $s$ is the sequence enumerated by $e$, since if you could do this, then in the standard model, the program would eventually find such a proof, and then perhaps another and another, until ultimately, it would find some last proof that $e$ does not enumerate exactly some finite sequence $t$, at which time the program will have enumerated exactly $t$ and never afterward add to it. So that proof would have proved a false statement. This is a contradiction, since that proof is standard.

So again, precisely because you cannot refute these statements, it follows that it is consistent with $\text{PA}$ that program $e$ enumerates exactly $s$, for any particular finite $s$. So statement (2) holds.

Finally, for statement (3), suppose that $M$ is a model of $\text{PA}$ in which $e$ enumerates exactly some finite sequence $s$. If $s$ is the empty sequence, then $M$ thinks that there is no proof in $\text{PA}$ that $e$ does not enumerate exactly $t$, for any particular $t$. And so it thinks the theory $\text{PA}+$ “$e$ enumerates exactly $t$” is consistent. So in $M$ we may build the Henkin model $N$ of this theory, which is an end-extension of $M$ in which $e$ enumerates exactly $t$, as desired.

If alternatively $s$ was nonempty, then it was enumerated by $e$ in $M$ because in $M$ there was ultimately a proof in some fragment ${\text{PA}}_n$ that it should not do so, but it never found a corresponding proof about an extension of $s$ in any strictly smaller fragment of $\text{PA}$.  So $M$ has a proof from ${\text{PA}}_n$ that $e$ does not enumerate exactly $s$, even though it did.

Notice that $n$ must be nonstandard, because $M$ has a definable ${\mathrm{\Sigma }}_k$-truth predicate for every standard $k$, and using this predicate, $M$ can see that every ${\text{PA}}_k$-provable statement must be true.

Precisely because the model $M$ lacked the proofs from the strictly smaller fragment ${\text{PA}}_{n-1}$, it follows that for any particular finite $t$ extending $s$ in $M$, the model thinks that the theory $T={\text{PA}}_{n-1}+$ “$e$ enumerates exactly $t$” is consistent. Since $n$ is nonstandard, this theory includes all the actual $\text{PA}$ axioms. In $M$ we can build the Henkin model $N$ of this theory, which will be an end-extension of $M$ in which $\text{PA}$ holds and program $e$ enumerates exactly $t$, as desired for statement (3). QED

Corollary. Let $e$ be the universal algorithm program $e$ of the theorem. Then

1. For any infinite sequence $S:\mathbb{N}\to \mathbb{N}$, there is a model $M$ of $\text{PA}$ in which program $e$ enumerates a (nonstandard finite) sequence starting with $S$.
2. If $M$ is any model of $\text{PA}$ in which program $e$ enumerates some (possibly nonstandard) finite sequence $s$, and $S$ is any $M$-definable infinite sequence extending $s$, then there is an end-extension of $M$ in which $e$ enumerates a sequence starting with $S$.

Proof. (1) Fix $S:\mathbb{N}\to \mathbb{N}$. By a simple compactness argument, there is a model $M$ of true arithmetic in which the sequence $S$ is the standard part of some coded nonstandard finite sequence $t$. By the main theorem, there is some end-extension $M^{+}$ of $M$ in which $e$ enumerates $t$, which extends $S$, as desired.

(2) If $e$ enumerates $s$ in $M$, a model of $\text{PA}$, and $S$ is an $M$-infinite sequence definable in $M$, then by a compactness argument inside $M$, we can build a model $M^{\prime }$ inside $M$ in which $S$ is coded by an element, and then apply the main theorem to find a further end-extension $M^{+}$ in which $e$ enumerates that element, and hence which enumerates an extension of $S$. QED