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.

  • 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$ Commented Mar 1, 2015 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
    Commented Mar 1, 2015 at 3:44
  • $\begingroup$ Can you explain what you mean what you mean by there is a "proof" P ...? $\endgroup$
    – hot_queen
    Commented Mar 8, 2015 at 19:40

1 Answer 1



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

  • $\begingroup$ Thank you this answers my question completely. I really like this construction. $\endgroup$
    – Bill Trok
    Commented Oct 14, 2015 at 19:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .