I am reading Kleene’s “Mathematical Logic” $ 2002$ pp 242-246.
Let $ T(i,a,x)$ stand for: $ i$ is the index of a Turing machine (under particular enumeration) which when applied to $ a$ as an argument will at moment $ x$ (but not earlier) have completed the computation of a value (call that value $ \phi_i(a)$ ).
Then Kleene tells the theorem: (A) The predicate $ T(i, a,x)$ is decidable. (B) $ \phi_i(a)$ as a partial function of $ i$ and $ a$ is computable.
I am not sure I understand the definition of a partial function. In the book, Kleene says that “As a function of $ i$ and $ a$ both, $ \phi_i (a)$ as we remarked is defined exactly when there exists $ x$ such that $ T(i,a,x)$ is true. So it is a partially defined number-theoretic function of two variables $ i$ and $ a$ , or briefly a partial function.”
My problem with this definition is that how do we know that there exists $ x$ such that $ T(i,a,x)$ is true? Intuitively, I feel that this condition is not decidable, i.e. there does not exist an algorithm to check this. Because if it is false then I would check each $ x$ but never reach the end. Why do we allow this kind of undecidable property to be in our definition? I feel concerned about this because Turing machines are used in metamathematics, i.e. our reasoning about formal systems, and we want this reasoning to be finitary (whatever that means).
Long story short – if there is a partial function defined by undecidable property, how do I know whether for each specific value as an argument the function is defined or not. And can this create any problems?