Running programs in nonstandard models of PA

Question

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.

Answer 1

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.

Answer 2

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.