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