Do there exist a pair of 'orthogonal' non-halting Turing machines?

Question

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.

Answer 1

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