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.