# Running programs in nonstandard models of PA

I came across the following problem in several places, to paraphrase:

Let $T$ be a recursively axiomatizable, consistent extension of PA. Then there exists some $e$ such that the $e'$th program $\phi_e$ is total, but $T$ does not prove $Tot(e)$.

The solution is usually along the lines of:

Take $e$ such that $\phi_e$ is the program which, for a fixed effective enumeration of the deductive closure of $T$, outputs $0$ on input $n$ if the $n$'th sentence is not $0=1"$, and diverges otherwise. Then $T$ is total by the consistency of $T$, but by Godel's (second) incompleteness theorem $T$ cannot prove $Tot(e)$.

I can't quite accept this solution. Clearly $Tot(e)$ would imply the consistency of $T$, but why should $T$ think that? If $T$ somehow fails to prove $Tot(e)\rightarrow Con(T)$, then we don't yet have a contradiction to Godel's incompleteness theorem.

Naturally then to finish the solution I would like to prove that $T$ DOES prove $Tot(e)\rightarrow Con(T)$. Since I am squeamish to approach syntax and proof grammar, I'd much rather try and use Godel's completeness theorem to establish this step, which means I have to start considering what happens to my program $\phi_e$ when I try to run it in nonstandard models.

Now, I would like to think that explicitely described algorithms are robust enough to work in nonstandard models. That is to say, when you define $\phi_e$ using some condition like

$\forall n$ if $\psi(n)$ then $\phi_e(n)\uparrow$

then $PA$ (or $Q$) should prove the sentence

$\psi(n)\rightarrow \neg (\phi_e(n)\downarrow)$

Perhaps I could phrase this as saying that $PA$ is smart enough to detect intentional divergence, or that there is a way to write a program to intentionally diverge that $PA$ can see.

-
What are your formalized definitions of $Tot(e)$ and $Con(T)$? I would expect that the former is $\neg\exists n: \phi_e(n)\uparrow$, which seems like it makes the equivalency essentially trivial... – Steven Stadnicki Jul 29 '13 at 4:41
Is standard or non-standard relevant? The added sentence(s) may be true. – André Nicolas Jul 29 '13 at 4:45
The nonstandard models stuff isn't the crux of the problem. For one, your "algorithm" isn't possible: you can't just tell your program (in a computable way) "If the input is a standard element, then do X; otherwise do Y." If $\phi_e(x)\downarrow$ for all $x$, then by overspill, in any nonstandard model, there will be nonstandard elements $c$ for which $\phi_e(c)\downarrow$, which means your "algorithm" can't be any of these $\phi_e$s. More importantly... – Alex Kocurek Jul 29 '13 at 6:47
...you're not concerned about nonstandard models; what you're concerned about is what $T$ can prove. Ultimately, then, you're better off taking the syntactic route you wanted to avoid. I haven't worked through the details, but I think you can show that even $\text{PA} \vdash \text{Tot}(e) \rightarrow \text{Con}(T)$. The idea being that $\text{PA}$ is smart enough to know that, if $\text{Tot}(e)$, then if $\neg\text{Con}(T)$, there would be a potential witness that refutes $\text{Tot}(e)$. Again, haven't worked through the details... – Alex Kocurek Jul 29 '13 at 6:50
I'm interested in nonstandard models because I'm interested in all models, and I already know what happens in the standard cases. Because I wish to avoid the syntactic route (obviously it can be done, but I expect it's too ugly to be of interest to me, and moreover regardless of how ugly it is I'm still interested in the semantic argument), what needs to be done is take an arbitrary model of T and ensure that not both $Tot(e)$ and $\neg Con(T)$ hold in the model. Obviously it is both necessary and sufficient to show this the case where T is PA. – Marcel T. Jul 29 '13 at 7:13

You do need to prove this syntactically. One way is to prove the following lemma:

For each $\Sigma^0_1$ formula $A(x_1,\ldots,x_k)$ there is an index $e$ such that PA proves $$(\forall n_1)\cdots(\forall n_k)[ A(n_1,\ldots,n_k) \leftrightarrow \phi_e(n_1,\ldots,n_k)\downarrow]$$

This is proved by induction on the structure of the formula $A$, using the definition of the formalization of "$\phi_e(n_1,\ldots,n_k)\downarrow$" in PA, which is actually Kleene's T predicate.

It is true that if $e,n$ are standard and the standard model thinks that $\phi_e(n)$ converges then so will any nonstandard model. But a nonstandard model could think that $\phi_e(n)$ converges (in a nonstandard number of steps), even when $n$ is standard, even if that computation does not actually converge.

-
Yes, what the semantic proof is missing is some way to model-unambiguously tell a program to go into an infinite loop. A way to build the machine so that it provably diverges--turning the witness that the $c$'th sentence is $0=1$ to a witness that the program $\phi_e$ diverges on $c$. That is: to replace the $\downarrow$ in the statement of your lemma with an $\uparrow$. Intuitively, you'd think something like that would be possible: is it? If not, is there a way to formalize, and prove, that something like that is in some sense impossible? That would be interesting. – Marcel T. Jul 29 '13 at 13:00

My personal opinion is that thinking about "running programs in nonstandard models" gives you the wrong intuition. A nonstandard model merely claims things about programs, and some of these claims are not verifiable. In the situation in which you find yourself, the nonstandard model will claim that the Turing machine runs forever on some input. You ask it "what input?" and it responds "$N$." Well, that wasn't helpful. You ask it "is $N$ greater than $1000$?" and it responds "yes." In general it will behave like an adaptive oracle, always answering your questions in a way that happens to avoid a contradiction, but without ever giving you enough data to pick out $N$ as a standard integer (because of course it isn't a standard integer).

For any fixed standard integer $N$, the claim "this Turing machine outputs this output on input $N$" is provable or disprovable in PA, and so has the same truth value in every model.

-
For the last paragraph, you must have a particular machine in mind. In general, if a program really does halt then PA can prove it, but if the program doesn't halt PA may be unable to prove it. – Carl Mummert Jul 29 '13 at 18:35