Last year I made a post about the universal program, a Turing machine program $p$ that can in principle compute any desired function, if it is only run inside a suitable model of set theory or arithmetic. Specifically, there is a program $p$, such that for any function $f:\newcommand\N{\mathbb{N}}\N\to\N$, there is a model $M\models\text{PA}$ — or of $\text{ZFC}$, whatever theory you like — inside of which program $p$ on input $n$ gives output $f(n)$.
This theorem is related to a very interesting theorem of W. Hugh Woodin’s, which says that there is a program $e$ such that $\newcommand\PA{\text{PA}}\PA$ proves $e$ accepts only finitely many inputs, but such that for any finite set $A\subset\N$, there is a model of $\PA$ inside of which program $e$ accepts exactly the elements of $A$. Actually, Woodin’s theorem is a bit stronger than this in a way that I shall explain.
Victoria Gitman gave a very nice talk today on both of these theorems at the special session on Computability theory: Pushing the Boundaries at the AMS sectional meeting here in New York, which happens to be meeting right here in my east midtown neighborhood, a few blocks from my home.
What I realized this morning, while walking over to Vika’s talk, is that there is a very simple proof of the version of Woodin’s theorem stated above. The idea is closely related to an idea of Vadim Kosoy mentioned in my post last year. In hindsight, I see now that this idea is also essentially present in Woodin’s proof of his theorem, and indeed, I find it probable that Woodin had actually begun with this idea and then modified it in order to get the stronger version of his result that I shall discuss below.
But in the meantime, let me present the simple argument, since I find it to be very clear and the result still very surprising.
Theorem. There is a Turing machine program $e$, such that
- $\PA$ proves that $e$ accepts only finitely many inputs.
- For any particular finite set $A\subset\N$, there is a model $M\models\PA$ such that inside $M$, the program $e$ accepts all and only the elements of $A$.
- Indeed, for any set $A\subset\N$, including infinite sets, there is a model $M\models\PA$ such that inside $M$, program $e$ accepts $n$ if and only if $n\in A$.
Proof. The program $e$ simply performs the following task: on any input $n$, search for a proof from $\PA$ of a statement of the form “program $e$ does not accept exactly the elements of $\{n_1,n_2,\ldots,n_k\}$.” Accept nothing until such a proof is found. For the first such proof that is found, accept $n$ if and only if $n$ is one of those $n_i$’s.
In short, the program $e$ searches for a proof that $e$ doesn’t accept exactly a certain finite set, and when such a proof is found, it accepts exactly the elements of this set anyway.
Clearly, $\PA$ proves that program $e$ accepts only a finite set, since either no such proof is ever found, in which case $e$ accepts nothing (and the empty set is finite), or else such a proof is found, in which case $e$ accepts only that particular finite set. So $\PA$ proves that $e$ accepts only finitely many inputs.
But meanwhile, assuming $\PA$ is consistent, then you cannot refute the assertion that program $e$ accepts exactly the elements of some particular finite set $A$, since if you could prove that from $\PA$, then program $e$ actually would accept exactly that set (for the shortest such proof), in which case this would also be provable, contradicting the consistency of $\PA$.
Since you cannot refute any particular finite set as the accepting set for $e$, it follows that it is consistent with $\PA$ that $e$ accepts any particular finite set $A$ that you like. So there is a model of $\PA$ in which $e$ accepts exactly the elements of $A$. This establishes statement (2).
Statement (3) now follows by a simple compactness argument. Namely, for any $A\subset\N$, let $T$ be the theory of $\PA$ together with the assertions that program $e$ accepts $n$, for any particular $n\in A$, and the assertions that program $e$ does not accept $n$, for $n\notin A$. Any finite subtheory of this theory is consistent, by statement (2), and so the whole theory is consistent. Any model of this theory realizes statement (3). QED
One uses the Kleene recursion theorem to show the existence of the program $e$, which makes reference to $e$ in the description of what it does. Although this may look circular, it is a standard technique to use the recursion theorem to eliminate the circularity.
This theorem immediately implies the classical result of Mostowski and Kripke that there is an independent family of $\Pi^0_1$ assertions, since the assertions $n\notin W_e$ are exactly such a family.
The theorem also implies a strengthening of the universal program theorem that I proved last year. Indeed, the two theorems can be realized with the same program!
Theorem. There is a Turing machine program $e$ with the following properties:
- $\PA$ proves that $e$ computes a finite function;
- For any particular finite partial function $f$ on $\N$, there is a model $M\models\PA$ inside of which program $e$ computes exactly $f$.
- For any partial function $f:\N\to\N$, finite or infinite, there is a model $M\models\PA$ inside of which program $e$ on input $n$ computes exactly $f(n)$, meaning that $e$ halts on $n$ if and only if $f(n)\downarrow$ and in this case $\varphi_e(n)=f(n)$.
Proof. The proof of statements (1) and (2) is just as in the earlier theorem. It is clear that $e$ computes a finite function, since either it computes the empty function, if no proof is found, or else it computes the finite function mentioned in the proof. And you cannot refute any particular finite function for $e$, since if you could, it would have exactly that behavior anyway, contradicting $\text{Con}(\PA)$. So statement (2) holds. But meanwhile, we can get statement (3) by a simple compactness argument. Namely, fix $f$ and let $T$ be the theory asserting $\PA$ plus all the assertions either that $\varphi_e(n)\uparrow$, if $n$ is not the domain of $f$, and $\varphi_e(n)=k$, if $f(n)=k$. Every finite subtheory of this theory is consistent, by statement (2), and so the whole theory is consistent. But any model of this theory exactly fulfills statement (3). QED
Woodin’s proof is more difficult than the arguments I have presented, but I realize now that this extra difficulty is because he is proving an extremely interesting and stronger form of the theorem, as follows.
Theorem. (Woodin) There is a Turing machine program $e$ such that $\PA$ proves $e$ accepts at most a finite set, and for any finite set $A\subset\N$ there is a model $M\models\PA$ inside of which $e$ accepts exactly $A$. And furthermore, in any such $M$ and any finite $B\supset A$, there is an end-extension $M\subset_{end} N\models\PA$, such that in $N$, the program $e$ accepts exactly the elements of $B$.
This is a much more subtle claim, as well as philosophically interesting for the reasons that he dwells on.
The program I described above definitely does not achieve this stronger property, since my program $e$, once it finds the proof that $e$ does not accept exactly $A$, will accept exactly $A$, and this will continue to be true in all further end-extensions of the model, since that proof will continue to be the first one that is found.
You may possibly know Blanck-Enayat’s paper “Marginalia on a theorem of woodin” which extends Woodin’s theorem (the paper is available at https://www.researchgate.net/profile/Ali_Enayat2/publication/281936409_Marginalia_on_a_theorem_of_Woodin/links/57035ade08aedbac126f4b1e/Marginalia-on-a-theorem-of-Woodin.pdf).
Oh yes, this paper was mentioned last year in connection with my post on the universal algorithm.
Pingback: A program that accepts exactly any desired finite set, in the right universe | ExtendTree
Two notes: (1) the paper of mine with Blanck mentioned by Mohammad and mentioned in Joel’s post from last year on the universal program has now appeared in print in the March issue of the Journal for Symbolic Logic; (2) some weaker forms of Woodin’s theorem (including the ones discussed in Joel’s post) follow from a classic (early 1960s) fixed-point construction of Kripke, as discussed in section 4 of my paper with Blanck (in particular, see Corollary 4.3 there).
Thanks for the update, Ali! Here is a link to the published version: https://doi.org/10.1017/jsl.2016.8.
Can you explain in a bit more detail what you mean by a Turing machine accepting a set “inside a model”?
In particular, say there is a model M of PA in which a Turing machine e accepts {1} , in the terminology of your first theorem. Does e actually run inside M and accept {1}? If so, doesn’t that mean that e has found a proof in PA that e does not accept {1}? How can this be? A proof in PA is still a proof in M, isn’t it, so doesn’t this show M is inconsistent?
PA sometimes misses things, does the above hold as well with ZFC in place of PA?
Sure, let me explain it a little more fully. The main point is that it makes sense to run a program $e$ inside a model of arithmetic, even if that model is not the standard model. The computation of a program $e$ on a certain input corresponds to the existence of a sequence of snapshots of the machine, one after each step of computation, such that the first snapshot is the input configuration and each next snapshot is obtained from the previous in the way specified by the program $p$ and the last snapshot shows the computation halting with a certain output. All of this makes sense even in a nonstandard model of arithmetic, and this is what we mean by saying that we shall run the program inside that model.
But the intriguing thing is that not all models of arithmetic will agree on the behavior of a given program. Consider for example the program $p$ that searches for a proof of a contradiction in PA, and when it finds one, then it begins to print out the digits of $\pi$. In the real world, PA is consistent, and there is no such proof of a contradiction. So in the real world, program $p$ will never get to the writing-out-$\pi$ part, since it will be forever in the searching-for-a-contradiction part of the algorithm. But meanwhile, in light of the incompleteness theorem, there are models of arithmetic that think Con(PA) is false, and in those models, there is a proof of a contradiction. So if you were living inside one of the those models and you ran the program $p$, it would eventually find that proof of a contradiction and then it would write out the digits of $\pi$.
In the post, I explain how one can actually find a universal program $e$, which has any desired behavior in a suitably chosen model of arithmetic.
Thank you for the explanation. I still find this all a bit bizarre because I think of Turing machines and accepting computations as being concrete finite objects. I don’t quite get what it can mean for them to differ in a model.
In your example, suppose the model where Con(PA) is false is M. M believes there is some integer, (or M-integer I guess) n* such that after n* steps, p finds an inconsistency. For simplicity let’s assume p prints the proof of inconsistency on the tape after p finds the proof. So M can find the first symbol, the second symbol, the i’th symbol of this proof for every i. What is the proof then? Does it exist or not? The proof itself is independent of the model isn’t it, it would be a proof in PA itself.
Honestly this is spinning me around. If there is an external paper that explains this a bit more – I am certain that any computer scientist with some logic would find this equally as bizarre as me.
Particularly since M was built using PA, or using something that incorporates it, I don’t know what M is supposed to do when it sees a proof on the tape that the logic M itself uses is inconsistent.
The proof inside $M$ would have a non-standard length, and so it wouldn’t be an actual proof of a contradiction. Inside the model $M$, what is thought to be a finite position on the tape might actually be at a nonstandard position, infinitely far out from the starting position. But the model can’t tell what is standard or nonstandard and so it looks like any other pseudo-finite position.
I suspect that we can modify program $e$ to make satisfy Woodin’s requirement. Namely, if it find a proof for a finite set $A$ s.t. the input $n$ is in $A$, it accepts, but if the input $n$ is not in $A$, it continues the search for sets $B \supset A$. However, I’m not ready to write down a full proof that it works.
I’d love to hear about it, if you can develop this idea. One should note, however, that this is already starting to resemble Woodin’s method.
I think I now have a way to do this. I’m writing something up now, and I’ll post it soon.
Pingback: The universal algorithm: a new simple proof of Woodin’s theorem | Joel David Hamkins
Pingback: The universal definition — it can define any mathematical object you like, in the right set-theoretic universe | Joel David Hamkins