5
$\begingroup$

I'll explain what I mean by orthogonal, which is probably a poor choice of words on my part.

Given two Turing machines $\lambda $ and $\tau$,and two inputs $i$ and $j$. lets say $\tau(i) \preceq \lambda(j)$, if there is a proof $P$, that states that $\tau(i)$ halts if $\lambda(j)$ halts. As an example of where we might have $\tau(i) \preceq \lambda(i)$. For instance, $\lambda$ may simply perform the computation $1+1$, and then run $\tau(i)$.

What I mean by orthogonal is noncomparable under this order. That is does there exist a pair of turing machines $\lambda$ and $\tau$ and inputs $i$ and $j$, where neither $\lambda(j) \preceq \tau(i)$ nor $\tau(i) \preceq \lambda(j)$

I believe I can show that for a fixed non-halting $\tau(i)$, we cannot have $\tau(i) \preceq \lambda(j)$ for all $\lambda(i)$. Since we could then use this to create a machine to solve the halting problem, by enumerating proofs until we find a proof that $\tau(i) \preceq \lambda(j)$. The existence of a proof then gives us that $\lambda(j)$ does not halt as $\tau(i)$ does not.

However, this result is far weaker than my goal.

$\endgroup$
  • 1
    $\begingroup$ I'm not sure I understand the meaning of "orthogonal here". Consider the Turing machine $\tau_n$ that enters an infinite loop if the input is $n$ and otherwise halts immediately (as soon as it's parsed the input). Then are the $\tau_n$ all orthogonal under your definition? (And what does the proof $P$ have to do with it - doesn't your definition work just fine without any proofs?) $\endgroup$ – Greg Martin Mar 1 '15 at 3:25
  • $\begingroup$ @GregMartin I apologize, I forgot inputs on all of those machines. I edited the post hope it makes it clearer. To further illustrate though with your example. For all instance of $t_j(n)$ and $t_i(k)$ would be trivially non-orthogonal since from your definition we can prove whether or not these turing machines halt or not. The definition is only really interesting if we have machine input pair $\lambda(i)$ where $\lambda(i)$ does not halt, but also there exists no proof that it does not halt. $\endgroup$ – Bill Trok Mar 1 '15 at 3:44
  • $\begingroup$ Can you explain what you mean what you mean by there is a "proof" P ...? $\endgroup$ – hot_queen Mar 8 '15 at 19:40
3
$\begingroup$

Yes.

First, of course, you must decide on a theory in which your proof $P$ is to be conducted. Let's call this $T$, and assume that $T$ is true and well-behaved enough that the set of consequences of $T$ is recursively enumerable. For example $T$ could be PA or ZFC.

Now let $P$ be the following program (in some suitable formalism):

  1. Read input $K$.
  2. Search all consequences of $T$.
  3. The first time a consequence of the form $$ T\vdash K\text{ run with input }K\text{ does }not\text{ output }n $$ for some number $n$ is found, halt and output $n$.

Now, if we run $P$ with itself as input, it won't ever terminate, because it can only terminate if it has proved (in the true theory $T$) that it doesn't do what it is in fact about to do.

On the other hand, for every $n$ is it consistent with $T$ that $P(P)$ outputs $n$ -- because otherwise $T$ would prove (by contradiction) that $P(P)\ne n$ for that $n$, which would mean that $P(P)$ cannot diverge, which contradicts the argument just above.

Now let $\tau$ be a machine that (ignores its input and) simulates running $P$ on itself, and terminates iff $P(P)$ outputs 1.

Let $\lambda$ be the machine that simulates running $P$ on itself, and terminates iff $P(P)$ outputs 2.

Now, since it is consistent with $T$ that $P(P)=1$, $T$ will not be able to prove "$\tau\text{ halts}\Rightarrow \lambda\text{ halts}$". Conversely, since it is consistent with $T$ that $P(P)=2$, $T$ cannot prove "$\lambda\text{ halts}\Rightarrow\tau\text{ halts}$".

(This construction is slightly simplified from the discussion at the end of section 4.2 of Pudlák, Logical Foundations of Mathematics and Computational Complexity, which attributes the original idea to Mostowski).

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thank you this answers my question completely. I really like this construction. $\endgroup$ – Bill Trok Oct 14 '15 at 19:30

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.