When asserting that a Turing machine exists, how do you know you can find it?

Question

Let $\langle x_n\rangle$ be a sequence of real numbers. Let $\langle \phi_n\rangle$ be an enumeration of the Turing machines (in ZFC?). Consider the following two "definitions" of a computable sequence:

Correct definition: We call $\langle x_n\rangle$ computable if there exists a Turing machine that given $n$ will give an "index name" for $x_n$. That is, a Turing machine which given $j \in \mathbf N$ will give a rational number $q$ with $|x_n - q| < 2^{-j}$.

Garbled definition: We call $\langle x_n\rangle$ computable if $x_n$ is computable for each $n \in \mathbf N$.

Obviously, there are many sequences that are computable under the second definition but not the first. Consider for example if $x_n$ is the indicator of some non-computable subset of $\mathbf N$. The problem is that while we know that for each $n \in \mathbf N$, a Turing machine can compute $x_n$, we don't know which one does so. By my understanding, this means that for some $n \in \mathbf N$, ZFC cannot prove if any particular Turing machine computes $x_n$. E.g. for this $n$, ZFC can't prove whether $\phi_5$ computes $x_n$. Indeed, the value of $x_n$ may depend on what model of ZFC you are in.

My understanding is that if for each $n \in \mathbf N$, ZFC proved a theorem of the form "$\phi_k$ computes $x_n$" for some $k \in \mathbf N$, then $\langle x_n\rangle$ would be a computable sequence. My thought would be that you could enumerate the theorems of ZFC, search for a theorem of the form "$\phi_k$ computes $x_n$" for some $k \in \mathbf N$, and report the first $k$ that is found. This would give a Turing machine that witnesses the computability of $\langle x_n\rangle$ as in the first definition, I should think.

The reason why I've come to ask this question is because I'm wanting to define a property of an object $X$, which is the assertion that some Turing machine exists. As part of proofs, I want to be able to take this Turing machine, put numbers into it, and play with its output to obtain another Turing machine. Obviously, asserting mere existence is not sufficient, just like with the definition of a computable sequence. Is it proper to assert, say, "object $X$ has property $P$ if for some $e \in \mathbf N$ ZFC can prove that the Turing machine $\phi_e$ gives certain information about $X$"? Then, I could perhaps just search the theorems of ZFC for theorems of the form "$\phi_e$ witnesses that $X$ has property $P$" in order to identify the Turing machine I want. In practice, when you prove $X$ has property $P$, you would likely construct a Turing machine doing the thing you want rather than anything non-constructive, so this is just an issue that arises when working with general $X$ I think.

Are there issues with anything I've said here? I have essentially only just learnt the basics of model theory, and am still learning computability theory. I am somewhat concerned about "internality" and "externality" in statements like "for some $n \in \mathbf N$, ZFC proves [...]", and whether something weird can happen with the enumeration of the Turing machines between different models of ZFC, specifically.

Answer 1

Not sure if this is worth posting an answer about, but I did resolve it to my satisfaction.

As part of proofs, I want to be able to take this Turing machine, put numbers into it, and play with its output to obtain another Turing machine.

You do not need the index of the original Turing machine to do this - you can do computable manipulations to the output (and/or input) of a Turing machine and get another Turing machine, this is just the result that the composition of computable functions is computable. The mere existence of such a machine was sufficient to generate a contradiction (by obtaining a Turing machine that provably does not exist) in my case, I didn't need an index. I think of this as not having to "see inside" the machine to get a contradiction, that is does a certain thing is enough.

As to:

"object $X$ has property $P$ if for some $e \in \mathbf N$ ZFC can prove that the Turing machine $\phi_e$ gives certain information about $X$"

As mihaild and some other people have pointed out, this would be fine to say, but is likely far stronger than just asserting some Turing machine exists with this property. And again, I did not need the index.

My understanding is that if for each $n \in \mathbf N$, ZFC proved a theorem [...] I should think.

I think this is all fine, but again ZFC proving such things would be quite strong and not at all required for computability (as mihaild says). I couldn't eliminate the possibility of ZFC failing to prove such theorems for relatively trivial reasons concerning the enumeration of the Turing machines, as well (rather than anything "intrinsic").