Totally order turing machines by halting Does there exist some computable relation "<" on turing machines, such that the set of machines that halt is an initial segment. (If A and B are Turing machines, and A halts and B doesn't then A<B)
One approach, if for all turing machines A and B, either $ZFC\vdash A'\implies B'$ or $ZFC\vdash B'\implies A'$ ($A'$ means A halts)
(This works for any consistent theory that can make statements about Turing machines)
Then we can run a brute force proof search until we find one of the two. (Of course there is no garantee of transitivity.
We can restore transitivity by taking the turing machines in lexical order. Maintain a list with a halting initial segment, adding new Turing machines one at a time. Any time you have a proved a cycle of implication, you add the new Turing machine in an arbitrary but deterministic place.
By godels completeness, anything that is true in all models can be proved. So can there exist turing machines A and B, and nonstandard models of the integers M, and N such that:
A halts in M
B does not halt in M
A does not halt in N
B halts in N

I was trying to prove that, for any two models of the naturals, one is an embedding of the other. (If there is an embedding from M to N, then any TM that halts in M must halt in N)
Ie for any two models of PA, or ZFC, or whichever other consistent theory that can talk about turing machines that is most convenient) there exists an injective function $f:M\to N$ . And for any relation R, $R_M(a,b,c...)\iff R_N(f(a),f(b),f(c)...)$ and for any function G, $f(G_M(a,b...))=G_N(f(a),f(b)...)$ (Which direction this function is in may depend on the models, $f=id$ if $M=N$)
 A: Define the region of a halting Turing machine T by running it until it halts, and then taking the 2^(10*|T|) nearest symbols on the tape as a string. (This function is basically arbitrary, I just need enough space to encode the turing machine.)
Suppose that for any Turing machine T, that in any model, it either doesn't halt,  or halts with a fixed region.
Then by Godels completeness theorem, a for all T there exists r such that a statement of the form "if T halts, then it halts with  region r" is provable .
Then pick k a number.
Create a Turing machine that, for each Turing machine H with |H|<k, searches for proofs of the form "if H halts, then it halts with region r". Once you have found one such proof for each Turing machine, stop searching.
Then look through the list of potential regions. There must be one that is missing, by pigeon-hole, we picked the regions to be big enough.
Output the lexographically first missing region onto your tape, then stop in the middle of it.
But we can pick k to be bigger than the size of the turing machine just described. We have therefore constructed a Turing machine of size <k that outputs a region that is not outputted by any halting Turing machine of size <k. Contradiction
Hence our assumption that for any Turing machine T, that in any models of PA, M and N, that if T halts in M and N, then it halts with the same region, is false.
So pick a Turing machine T that halts with region r in some models, and halts with region s in others. Make A a machine that runs T, and then checks if the region is r, if not, A loops forever.
Let B likewise run T, and loop forever if the region isn't s.
As such, there are models where A halts, and models where B halts, but no model where they both halt.
So if you have any computable ordering, it must put A before B in some models, and B before A in others.
But both of those models have the standard model as an initial segment. If the computation puts B<A in one nonstandard model, and A<B in another, then it can't have outputed its decision within the standard numbers. Ie the program runs forever in the standard model.
