Meaning of "existence" for an uncomputable function related to the Halting Problem Take the set of all Turing Machines $TM$, we can divide this set in two: $P$, the set of all Turing Machines that will halt if starting from an empty tape, and $Q$, its complement: the set of all Turing Machines that will not halt if starting from an empty tape.
We know every TM fits either one of those sets, and $P \cup Q = TM$. But we also know that we can't always decide, given a particular TM, if it is in $P$ or in $Q$: that is the undecidable Halting Problem.
Now have this set $H = \{\text{Haltable}, \text{Unhaltable}\}$, does the following function "exists"?
$$
F: TM \rightarrow H\\
F(x) =
\begin{cases}
    \text{Haltable} & \quad \text{if } x \in P\\
    \text{Unhaltable}  & \quad \text{if } x \in Q\\
  \end{cases}
$$
$F$ clearly doesn't exists in the sense of recursive function or lambda function, because those are of equivalent computing power of a Turing machine. But it does exists in a sense that every $x \in TM$ is either in $P$ or $Q$.
This question is important when some definition is given concerning the "existence" of some function.
For instance, take the definition of countable set: for a set S to be countable, there must exist a bijective function $C: S \rightarrow \mathbb{N}$.
If we consider the set of computable real numbers, such function $C$ doesn't exists in the constructive sense (it can be shown by diagonalization), but exists in a sense that every computable real number has a TM that computes it, and TMs are countable.
Is there a universally accepted meaning for "existence" in such cases?
 A: There is a universal meaning for "exists". It means that within a given context, there exists an object satisfying such and such. What is the given context? (Which also means that in another way, there is no universal meaning for "exists", since these contexts can change drastically.)

*

*If your given context is just computable functions, or some constructive approach to mathematics, then the answer is possibly no. This function is certainly not computable, and if your definition of constructive sufficiently-coincides with computable, then there is no such function. I don't know if in this context you can even talk about the set of Turing machines, or the set of Turing machines which do not halt for some given input.
Note that in the absence of the law of excluded middle, $\lnot\lnot\exists$
need not be the same as $\exists$.


*If your given context is a set theoretical foundations with classical logic, then the set of Turing machines exists, and each Turing machine either halts or not within a given mathematical universe, so the function is well-defined.
What will not be "entirely clear" is whether a specific Turing machine is halting or not. So it might be the case that different universes of set theory will disagree on whether something halts or not.
