2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ The issue is with the italicized statement (to which you've hinted towards with the italics). How would one go about making a precise mathematical formulation of this particular statement? $\endgroup$ – user52534 Apr 22 '15 at 23:28
1
$\begingroup$

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$.

$\endgroup$
4
  • $\begingroup$ Thank you for taking the time to read my question and writing up an answer. So do I understand it correctly, the significant problem I have with the intuition of not accepting the argument I wrote in italics is similar to the question "What does a proof of $\neg Con(PA)$ look like, in the (non-standard) model of PA + $\neg Con(PA)$". (1/2) $\endgroup$ – Bert Zangle Apr 28 '15 at 17:46
  • $\begingroup$ Similarly, I could ask "What is the sequence in $PA$ that constitutes a proof that the TM/Input pair $(i, j)$ is in the halting set?". And similarly to the question about $\neg Con(PA)$, the answer that would be "intuitively satisfying" (i.e. something that resembles an effective proof of the statement) is not computable, so the real problem for my intuition is to consider what a non-standard model of computation looks like. Is the above roughly correct, i.e. is this related to the similarity between Second Incompleteness and the undecidability of the Halting problem? (2/2) $\endgroup$ – Bert Zangle Apr 28 '15 at 17:53
  • $\begingroup$ Hi zanglebert, I was using $¬\text{Con}(PA)$ as a particular example of how it is possible to have a model for $PA+A$ where 1) $A$ is false in the standard model and 2) there are constants $i,j$ such that asking if $A$ holds is equivalent to asking if $H(i,j)$ holds (provable in some sufficiently strong system $\Gamma$ for which $PA\supseteq\Gamma$). In my answer above, I didn't explicitly mention why 2) holds for $¬\text{Con}(PA)$, but it turns out that it does. $\endgroup$ – user52534 May 1 '15 at 3:50
  • $\begingroup$ But you're right. What you really want them to be describing (ie an assertion about a particular Turing machine with a particular input halting or an assertion about the inconsistency of $PA$) is how the standard model of arithmetic describes it, but those other nonstandard models might be describing something rather nonintuitive. Lastly, a question to think about: What constitutes a "model of computation"? $\endgroup$ – user52534 May 1 '15 at 3:51
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.