Which mistake(s) in my argument re: representability, definability and the halting problem?

Question

I'd like to ask for your help in showing me the (quite likely: several) flaws in my argument below, relating weak and strong representability in a formal system and the halting problem.

At least part of the problem is most likely that I am too informal in my definitions, leading to wrong conclusions. That said, I still can't point out exactly where my argument goes wrong. Hopefully, someone is patient enough to overlook the lack of rigor in those steps where the argument is correct in principle, and helps me understand the major mistakes of it.

(1) The halting set $HALT$, containing all pairs of numbers $(i, j)$ s.t. the Turing program (enumerated by) $i$ halts (i.e. produces an output) after finite steps on input $j$, is computably enumerable, while its complement set (of program/input pairs that do not halt) is not computably enumerable.

(2) Assuming a first-order formal system $F$ as expressive as Peano arithmetic (PA) is strong enough to reason about computable relations, we can (can we?) define a formula $H$ in $F$ that weakly represents the set $HALT$, i.e. $(i,j) \in HALT \iff \vdash H(i, j)$.

For a (sloppy) definition of $H$: $\forall x,y \: \exists z.H(x, y) \iff CompStateSequence(z, x, y)$, where $CompStateSequence(z, x, y)$ holds if $z$ encodes a finite sequence of program states for a program/input pair $(x, y)$ s.t. each state in the sequence correctly follows from the previous state according to the rules of the program, the first state is the beginning state of $(i,j)$, and and the final state is the output state of a program.

$(\rightarrow)$ If $(i,j) \in HALT$, there must be a finite sequence of computation steps computing $(i,j)$, so there must be a finite sequence of states representing a successful computation of $(i, j)$. Then we can find a proof for $H(x, y)$ in $F$, $\vdash H(i, j)$, by mechanically testing all numbers up to $z$ whether they are the desired sequence of program states.

$(\leftarrow)$ Assume $(i,j) \notin HALT$. Then there is no (finite) sequence of program states s.t. the sequence computes $(i,j)$. Assume $\vdash H(i,j)$. Then by definition of $H$, there must be a number $z$ representing a finite sequence of program states representing a computation of $(i,j)$. Contradiction, so we know $H$ (weakly) represents the set $HALT$ in $F$.

(3) Further, we can use $H$ to define (in the weaker sense of truth, not provability) set $HALT$ in $F$, i.e. $(i, j) \in HALT \iff$ $H(i, j)$ is true in the intended model of F, by a similar argument as in (2) above, with 'truth' in the place of 'provability'.

(4) (Now, for the part where I probably really just confuse myself...) Assume $(i,j) \notin HALT$. By definition of $H$ (and the argument in (3) above) we know that $H(i,j)$ is false in the intended model of $F$.

But if $H(i,j)$ is false in one model of $F$, it must be false in every model of $F$, since $(i,j)$ will not halt in any (correct) model of a theory representing Turing computability.

Then $\neg H(i,j)$ is true in every model of $F$, so $\neg H(i,j)$ is valid, so by (semantic) completeness of $F$, there is a proof of $\neg H(i,j)$ in $F$. But then $\not H$ is weakly representable as well, so together with weak representability of $H$, $HALT$ is strongly representable in $F$, which (by equivalence of strong representability and decidability) contradicts the result that the halting problem is undecidable.

Answer 1

Regardless of any reasonable mathematical formulation for the italicized assertion, let's see what happens when $F=PA$.

Arguing inside of $ZFC$:

"Since there is a model for $PA$ (the standard model of first-order arithmetic), then we have $\text{Con}(PA)$ by the completeness theorem. Therefore $PA\nvdash\text{Con}(PA)$ by the second incompleteness theorem. Hence we have $\text{Con}(PA+\neg$ $\text{Con}(PA))$, and therefore there is a model for $PA+\neg\text{Con}(PA)$ by applying the completeness theorem again."

And notice then that $\neg\text{Con}(PA)$ is a $\Sigma_1$ sentence which is false in the standard model of $PA$ and true in some other model of $PA$.

Answer 2

I believe a mistake is here:

But if $H(i,j)$ is false in one model of $F$, it must be false in every model of $F, ...$

Note that a statement "The program $i$ halts on the input $j$" is actually an existentially quantified arithmetic statement of the form "There is a number $n$ such that the program $i$ halts on the input $j$ after $n$ steps".

But there are non-standard models of arithmetic that have non-standard integers (a model can even have an arbitrary large uncountable set of them). A non-standard model can think that a particular program halts on a particular input after $n$ steps, where $n$ is a non-standard integer, while the standard model will think that this program does not halt (because there is no such $n$ in the standard model), so they actually can disagree on that.

Suppose, you somehow convinced yourself that a particular non-standard model is wrong in this case, and the program does not actually halt. You may add an additional axiom to $F$ specifically stating that this program does not halt, and this will rule out that particular non-standard model. But no matter what recursively enumerable set of new axioms you are adding, there will always be many (a proper class of) other non-standard models remaining. This is the famous incompleteness phenomenon.

In regard to your following argument:

... since $(i,j)$ will not halt in any (correct) model of a theory representing Turing computability.

it looks that it does not prove anything, because you are explicitly saying only about a correct (I assume, standard) model.